internlm/Lean-Github huggingface dataset:
Theorem: Sieve.Nat.squarefree_dvd_pow
Proof state before:
case pos
a b N : ℕ
ha : Squarefree a
hab : a = 1
hN : N = 0
⊢ a ∣ b
Tactic:
rw [hab]
Proof state after:
case pos
a b N : ℕ
ha : Squarefree a
hab : a = 1
hN : N = 0
⊢ 1 ∣ b
Theorem: Sieve.Nat.squarefree_dvd_pow
Proof state before:
case pos
a b N : ℕ
ha : Squarefree a
hab : a = 1
hN : N = 0
⊢ 1 ∣ b
Tactic:
simp
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
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, s.nu m
Tactic:
unfold SelbergSieve.selbergBoundingSum
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
⊢ (∑ l ∈ s.prodPrimes.divisors, if ↑l ^ 2 ≤ s.level then s.selbergTerms l else 0) ≥
    ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, s.nu m
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
⊢ ∑ l ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors,
      ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m ≥
    ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, s.nu m
Tactic:
rw [←Finset.sum_biUnion]
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
⊢ ∑
      x ∈
        (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
          Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors,
      s.nu x ≥
    ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, s.nu m

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
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
⊢ ∑
      x ∈
        (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
          Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors,
      s.nu x ≥
    ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, s.nu m

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:
apply Finset.sum_le_sum_of_subset_of_nonneg
Proof state after:
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
⊢ Finset.Icc 1 ⌊√s.level⌋₊ ⊆
    (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
      Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors

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

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
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_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
⊢ (∑ l ∈ s.prodPrimes.divisors, if ↑l ^ 2 ≤ s.level then s.selbergTerms l else 0) ≥
    ∑ l ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors,
      ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m
Tactic:
rw [←Finset.sum_filter]
Proof state after:
case calc_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
⊢ ∑ a ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors, s.selbergTerms a ≥
    ∑ l ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors,
      ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_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
⊢ ∑ a ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors, s.selbergTerms a ≥
    ∑ l ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors,
      ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m
Tactic:
apply Finset.sum_le_sum
Proof state after:
case calc_1.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
⊢ ∀ i ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors,
    ∑ m ∈ Finset.filter (fun x => i ∣ x) (i ^ ⌊s.level⌋₊).divisors, s.nu m ≤ s.selbergTerms i
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_1.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
⊢ ∀ i ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors,
    ∑ m ∈ Finset.filter (fun x => i ∣ x) (i ^ ⌊s.level⌋₊).divisors, s.nu m ≤ s.selbergTerms i
Tactic:
intro l hl
Proof state after:
case calc_1.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
l : ℕ
hl : l ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors
⊢ ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m ≤ s.selbergTerms l
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_1.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
l : ℕ
hl : l ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors
⊢ ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m ≤ s.selbergTerms l
Tactic:
rw [Finset.mem_filter, Nat.mem_divisors] at hl
Proof state after:
case calc_1.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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
⊢ ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m ≤ s.selbergTerms l
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_1.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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
⊢ ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m ≤ s.selbergTerms l
Tactic:
have hlsq : Squarefree l := Squarefree.squarefree_of_dvd hl.1.1 s.prodPrimes_squarefree
Proof state after:
case calc_1.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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m ≤ s.selbergTerms l
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case calc_1.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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m ≤ s.selbergTerms l
Tactic:
trans (∏ p in l.primeFactors, ∑ n in Finset.Icc 1 (Nat.floor s.level), s.nu (p^n))
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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m ≤
    ∏ p ∈ l.primeFactors, ∑ n ∈ Finset.Icc 1 ⌊s.level⌋₊, s.nu (p ^ n)

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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∏ p ∈ l.primeFactors, ∑ n ∈ Finset.Icc 1 ⌊s.level⌋₊, s.nu (p ^ n) ≤ s.selbergTerms l
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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∑ m ∈ Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors, s.nu m ≤
    ∏ p ∈ l.primeFactors, ∑ n ∈ Finset.Icc 1 ⌊s.level⌋₊, s.nu (p ^ n)

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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∏ p ∈ l.primeFactors, ∑ n ∈ Finset.Icc 1 ⌊s.level⌋₊, s.nu (p ^ n) ≤ s.selbergTerms l
Tactic:
rw [prod_factors_sum_pow_compMult (Nat.floor s.level) _ s.nu]
Proof state after:
case 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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ CompletelyMultiplicative s.nu

case hd
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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ Squarefree l

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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ⌊s.level⌋₊ ≠ 0

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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∏ p ∈ l.primeFactors, ∑ n ∈ Finset.Icc 1 ⌊s.level⌋₊, s.nu (p ^ n) ≤ s.selbergTerms l
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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∏ p ∈ l.primeFactors, ∑ n ∈ Finset.Icc 1 ⌊s.level⌋₊, s.nu (p ^ n) ≤ s.selbergTerms l
Tactic:
rw [s.selbergTerms_apply l]
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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∏ p ∈ l.primeFactors, ∑ n ∈ Finset.Icc 1 ⌊s.level⌋₊, s.nu (p ^ n) ≤ s.nu l * ∏ p ∈ l.primeFactors, 1 / (1 - s.nu 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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∏ p ∈ l.primeFactors, ∑ n ∈ Finset.Icc 1 ⌊s.level⌋₊, s.nu (p ^ n) ≤ s.nu l * ∏ p ∈ l.primeFactors, 1 / (1 - s.nu p)
Tactic:
apply prod_factors_one_div_compMult_ge _ _ hnu _ _ hlsq
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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∀ (n : ℕ), n.Prime → n ∣ l → s.nu n < 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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∀ (n : ℕ), 0 ≤ s.nu n
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case 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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ CompletelyMultiplicative s.nu
Tactic:
exact hnu
Proof state after:
no goals
Theorem: Sieve.selbergBoundingSum_ge_sum_div
Proof state before:
case hd
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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ Squarefree l
Tactic:
exact hlsq
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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ⌊s.level⌋₊ ≠ 0
Tactic:
rw [ne_eq, Nat.floor_eq_zero, not_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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ 1 ≤ 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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ 1 ≤ s.level
Tactic:
exact 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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∀ (n : ℕ), n.Prime → n ∣ l → s.nu n < 1
Tactic:
intro p hpp hpl
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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
p : ℕ
hpp : p.Prime
hpl : p ∣ l
⊢ s.nu p < 1
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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
p : ℕ
hpp : p.Prime
hpl : p ∣ l
⊢ s.nu p < 1
Tactic:
apply hnu_lt p hpp (Trans.trans hpl hl.1.1)
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
l : ℕ
hl : (l ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑l ^ 2 ≤ s.level
hlsq : Squarefree l
⊢ ∀ (n : ℕ), 0 ≤ s.nu n
Tactic:
exact hnu_nonneg
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
⊢ Finset.Icc 1 ⌊√s.level⌋₊ ⊆
    (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
      Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors
Tactic:
intro m hm
Proof state after:
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 : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
⊢ m ∈
    (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
      Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors
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 : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
⊢ m ∈
    (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
      Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors
Tactic:
have hprod_pos : 0 < (∏ p in m.primeFactors, p) := by
  apply Finset.prod_pos;
  intro p hp; exact Nat.pos_of_mem_factors $ List.mem_toFinset.mp hp
Proof state after:
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 : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
⊢ m ∈
    (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
      Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors
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 : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
⊢ m ∈
    (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
      Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors
Tactic:
have hprod_ne_zero :  (∏ p in m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0 := by
  apply pow_ne_zero; apply ne_of_gt; apply hprod_pos
Proof state after:
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 : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
⊢ m ∈
    (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
      Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors
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 : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
⊢ m ∈
    (Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors).biUnion fun l =>
      Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors
Tactic:
rw [Finset.mem_biUnion]
Proof state after:
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 : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
⊢ ∃ a ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors,
    m ∈ Finset.filter (fun x => a ∣ x) (a ^ ⌊s.level⌋₊).divisors
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 : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
⊢ ∃ a ∈ Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors,
    m ∈ Finset.filter (fun x => a ∣ x) (a ^ ⌊s.level⌋₊).divisors
Tactic:
simp_rw [Finset.mem_filter, Nat.mem_divisors]
Proof state after:
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 : m ∈ Finset.Icc 1 ⌊√s.level⌋₊
hprod_pos : 0 < ∏ p ∈ m.primeFactors, p
hprod_ne_zero : (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0
⊢ ∃ a, ((a ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑a ^ 2 ≤ s.level) ∧ (m ∣ a ^ ⌊s.level⌋₊ ∧ a ^ ⌊s.level⌋₊ ≠ 0) ∧ a ∣ m