internlm/Lean-Github huggingface dataset:
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case ha.h
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
⊢ ↑0 ≤ s.level

case hb
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
⊢ 0 ≤ (∏ p ∈ m.primeFactors, p).factorization p
Tactic:
norm_cast
Proof state after:
case ha.h
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
⊢ 0 ≤ s.level

case hb
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
⊢ 0 ≤ (∏ p ∈ m.primeFactors, p).factorization p
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case ha.h
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
⊢ 0 ≤ s.level

case hb
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
⊢ 0 ≤ (∏ p ∈ m.primeFactors, p).factorization p
Tactic:
linarith only [s.one_le_level]
Proof state after:
case hb
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
⊢ 0 ≤ (∏ p ∈ m.primeFactors, p).factorization p
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case hb
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
⊢ 0 ≤ (∏ p ∈ m.primeFactors, p).factorization p
Tactic:
norm_num
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
⊢ m.factorization p ≤ m.factorization p * 1
Tactic:
rw [mul_one]
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
⊢ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p ≤ (⌊s.level⌋₊ • (∏ p ∈ m.primeFactors, p).factorization) p
Tactic:
apply le_rfl
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case neg
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
hpp : ¬p.Prime
⊢ m.factorization p * 1 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
Tactic:
rw [Nat.factorization_eq_zero_of_non_prime _ hpp, zero_mul]
Proof state after:
case neg
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
hpp : ¬p.Prime
⊢ 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case neg
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
hpp : ¬p.Prime
⊢ 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
Tactic:
exact hy_mul_prod_nonneg
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case neg
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
hpp : p.Prime
hpdvd : ¬p ∣ m
⊢ m.factorization p * 1 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
Tactic:
rw [Nat.factorization_eq_zero_of_not_dvd hpdvd, zero_mul]
Proof state after:
case neg
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
hpp : p.Prime
hpdvd : ¬p ∣ m
⊢ 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case neg
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
hpp : p.Prime
hpdvd : ¬p ∣ m
⊢ 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
Tactic:
exact hy_mul_prod_nonneg
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
hpp : p.Prime
hpdvd : p ∣ m
⊢ m.factorization p ≤ m
Tactic:
apply le_of_lt $ Nat.factorization_lt _ _
Proof state after:
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
hpp : p.Prime
hpdvd : p ∣ m
⊢ m ≠ 0
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
hpp : p.Prime
hpdvd : p ∣ m
⊢ m ≠ 0
Tactic:
apply hm_ne_zero
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case pos.h₂.ha
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
p : ℕ
hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (∏ p ∈ m.primeFactors, p).factorization p
hpp : p.Prime
hpdvd : p ∣ m
⊢ p.Prime ∧ p ∣ m ∧ m ≠ 0
Tactic:
exact ⟨hpp, hpdvd, hm_ne_zero⟩
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case h.right.left.right
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
⊢ (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
Tactic:
exact hprod_ne_zero
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case h.right.right
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ ↑m ≤ √s.level
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
hm_ne_zero : m ≠ 0
⊢ ∏ p ∈ m.primeFactors, p ∣ m
Tactic:
exact Nat.prod_primeFactors_dvd m
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2.h
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ ⌊√s.level⌋₊
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
⊢ 0 ≤ √s.level
Tactic:
apply Real.sqrt_nonneg
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2.hf
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
⊢ ∀
    i ∈
      (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
        Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors,
    i ∉ Finset.Icc 1 ⌊√s.level⌋₊ → 0 ≤ s.nu i
Tactic:
intro i _ _
Proof state after:
case calc_2.hf
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
a✝¹ :
  i ∈
    (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
      Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors
a✝ : i ∉ Finset.Icc 1 ⌊√s.level⌋₊
⊢ 0 ≤ s.nu i
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2.hf
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
a✝¹ :
  i ∈
    (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
      Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors
a✝ : i ∉ Finset.Icc 1 ⌊√s.level⌋₊
⊢ 0 ≤ s.nu i
Tactic:
apply (hnu_nonneg _)
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
⊢ (↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)).PairwiseDisjoint fun l =>
    Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors
Tactic:
intro i hi j hj hij
Proof state after:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
⊢ (Disjoint on fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i j
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
⊢ (Disjoint on fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i j
Tactic:
intro t hti htj
Proof state after:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
t : Finset ℕ
hti : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
htj : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
⊢ t ≤ ⊥
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
t : Finset ℕ
hti : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
htj : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
⊢ t ≤ ⊥
Tactic:
intro x hx
Proof state after:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
t : Finset ℕ
hti : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
htj : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
x : ℕ
hx : x ∈ t
⊢ x ∈ ⊥
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
t : Finset ℕ
hti : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
htj : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
x : ℕ
hx : x ∈ t
⊢ x ∈ ⊥
Tactic:
simp only [Finset.bot_eq_empty, Finset.not_mem_empty]
Proof state after:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
t : Finset ℕ
hti : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
htj : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
x : ℕ
hx : x ∈ t
⊢ False
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
t : Finset ℕ
hti : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
htj : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
x : ℕ
hx : x ∈ t
⊢ False
Tactic:
specialize hti hx
Proof state after:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
t : Finset ℕ
htj : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
x : ℕ
hx : x ∈ t
hti : x ∈ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
⊢ False
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
t : Finset ℕ
htj : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
x : ℕ
hx : x ∈ t
hti : x ∈ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
⊢ False
Tactic:
specialize htj hx
Proof state after:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : x ∈ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
htj : x ∈ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
⊢ False
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : x ∈ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
htj : x ∈ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
⊢ False
Tactic:
simp_rw [Finset.mem_coe, Finset.mem_filter, Nat.mem_divisors] at *
Proof state after:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i j : ℕ
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i ^ ⌊s.level⌋₊ ∧ i ^ ⌊s.level⌋₊ ≠ 0) ∧ i ∣ x
htj : (x ∣ j ^ ⌊s.level⌋₊ ∧ j ^ ⌊s.level⌋₊ ≠ 0) ∧ j ∣ x
hi : (i ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i ^ 2 ≤ s.level
hj : (j ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j ^ 2 ≤ s.level
⊢ False
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i j : ℕ
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i ^ ⌊s.level⌋₊ ∧ i ^ ⌊s.level⌋₊ ≠ 0) ∧ i ∣ x
htj : (x ∣ j ^ ⌊s.level⌋₊ ∧ j ^ ⌊s.level⌋₊ ≠ 0) ∧ j ∣ x
hi : (i ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i ^ 2 ≤ s.level
hj : (j ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j ^ 2 ≤ s.level
⊢ False
Tactic:
have h : ∀ i j {n}, i ∣ s.prodPrimes → i ∣ x → x ∣ j ^ n → i ∣ j := by
  intro i j n hiP hix hij
  apply Nat.squarefree_dvd_pow i j n (s.squarefree_of_dvd_prodPrimes hiP)
  exact Trans.trans hix hij
Proof state after:
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i j : ℕ
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i ^ ⌊s.level⌋₊ ∧ i ^ ⌊s.level⌋₊ ≠ 0) ∧ i ∣ x
htj : (x ∣ j ^ ⌊s.level⌋₊ ∧ j ^ ⌊s.level⌋₊ ≠ 0) ∧ j ∣ x
hi : (i ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i ^ 2 ≤ s.level
hj : (j ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j ^ 2 ≤ s.level
h : ∀ (i j : ℕ) {n : ℕ}, i ∣ s.prodPrimes → i ∣ x → x ∣ j ^ n → i ∣ j
⊢ False