internlm/Lean-Github huggingface dataset:
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case h.left.left.left.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 : ℕ
hp : p ∈ m.primeFactors
⊢ ↑p ≤ s.level
Tactic:
trans (m:ℝ)
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 : ℕ
hp : p ∈ m.primeFactors
⊢ ↑p ≤ ↑m

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 : ℕ
hp : p ∈ m.primeFactors
⊢ ↑m ≤ s.level
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 : ℕ
hp : p ∈ m.primeFactors
⊢ ↑m ≤ s.level
Tactic:
trans (Real.sqrt s.level)
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 : ℕ
hp : p ∈ m.primeFactors
⊢ ↑m ≤ √s.level

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 : ℕ
hp : p ∈ m.primeFactors
⊢ √s.level ≤ s.level
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 : ℕ
hp : p ∈ m.primeFactors
⊢ √s.level ≤ s.level
Tactic:
apply sqrt_le_self s.level s.one_le_level
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 : ℕ
hp : p ∈ m.primeFactors
⊢ ↑p ≤ ↑m
Tactic:
norm_cast
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 : ℕ
hp : p ∈ m.primeFactors
⊢ p ≤ m
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 : ℕ
hp : p ∈ m.primeFactors
⊢ p ≤ m
Tactic:
exact Nat.le_of_mem_primeFactors hp
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 : ℕ
hp : p ∈ m.primeFactors
⊢ ↑m ≤ √s.level
Tactic:
exact hm.2
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case h.left.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
⊢ s.prodPrimes ≠ 0
Tactic:
exact s.prodPrimes_ne_zero
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case h.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) ^ 2 ≤ s.level
Tactic:
rw [←Real.sqrt_le_sqrt_iff (by linarith only [s.one_le_level]), Real.sqrt_sq]
Proof state after:
case h.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

case h.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
⊢ 0 ≤ ↑(∏ p ∈ m.primeFactors, p)
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case h.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

case h.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
⊢ 0 ≤ ↑(∏ p ∈ m.primeFactors, p)
Tactic:
trans (m:ℝ)
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 ∈ m.primeFactors, p) ≤ ↑m

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
⊢ ↑m ≤ √s.level

case h.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
⊢ 0 ≤ ↑(∏ p ∈ m.primeFactors, p)
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
⊢ ↑m ≤ √s.level

case h.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
⊢ 0 ≤ ↑(∏ p ∈ m.primeFactors, p)
Tactic:
exact hm.2
Proof state after:
case h.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
⊢ 0 ≤ ↑(∏ p ∈ m.primeFactors, p)
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case h.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
⊢ 0 ≤ ↑(∏ p ∈ m.primeFactors, p)
Tactic:
apply le_of_lt
Proof state after:
case h.left.right.a
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
⊢ 0 < ↑(∏ p ∈ m.primeFactors, p)
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case h.left.right.a
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
⊢ 0 < ↑(∏ p ∈ m.primeFactors, p)
Tactic:
norm_cast
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
⊢ 0 ≤ s.level
Tactic:
linarith only [s.one_le_level]
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 ∈ m.primeFactors, p) ≤ ↑m
Tactic:
norm_cast
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 ∈ m.primeFactors, p ≤ m
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 ∈ m.primeFactors, p ≤ m
Tactic:
apply Nat.le_of_dvd (Nat.succ_le.mp hm.1)
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 ∈ m.primeFactors, p ∣ m
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 ∈ 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 h.right.left.left
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
⊢ m ∣ (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊
Tactic:
rw [←Nat.factorization_le_iff_dvd _ hprod_ne_zero, Nat.factorization_pow]
Proof state after:
case h.right.left.left
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
⊢ m.factorization ≤ ⌊s.level⌋₊ • (∏ p ∈ m.primeFactors, p).factorization

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
⊢ m ≠ 0
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case h.right.left.left
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
⊢ m.factorization ≤ ⌊s.level⌋₊ • (∏ p ∈ m.primeFactors, p).factorization

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
⊢ m ≠ 0
Tactic:
intro p
Proof state after:
case h.right.left.left
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.factorization p ≤ (⌊s.level⌋₊ • (∏ p ∈ m.primeFactors, p).factorization) p

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
⊢ m ≠ 0
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case h.right.left.left
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.factorization p ≤ (⌊s.level⌋₊ • (∏ p ∈ m.primeFactors, p).factorization) p

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
⊢ m ≠ 0
Tactic:
have hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (Nat.factorization (∏ p in m.primeFactors, p)) p := by
  apply mul_nonneg; apply Nat.le_floor; norm_cast; linarith only [s.one_le_level]; norm_num
Proof state after:
case h.right.left.left
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 ≤ (⌊s.level⌋₊ • (∏ p ∈ m.primeFactors, p).factorization) p

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
⊢ m ≠ 0
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case h.right.left.left
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 ≤ (⌊s.level⌋₊ • (∏ p ∈ m.primeFactors, p).factorization) p

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
⊢ m ≠ 0
Tactic:
trans (Nat.factorization m) p * 1
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
⊢ m.factorization p ≤ m.factorization p * 1

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 * 1 ≤ (⌊s.level⌋₊ • (∏ p ∈ m.primeFactors, p).factorization) p

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
⊢ m ≠ 0