internlm/Lean-Github huggingface dataset:
Theorem: Sieve.nu_ne_zero_of_mem_divisors_prodPrimes
Proof state before:
s : Sieve
d : ℕ
hd : d ∈ P.divisors
⊢ ν d ≠ 0
Tactic:
apply _root_.ne_of_gt
Proof state after:
case h
s : Sieve
d : ℕ
hd : d ∈ P.divisors
⊢ 0 < ν d
Theorem: Sieve.nu_ne_zero_of_mem_divisors_prodPrimes
Proof state before:
case h
s : Sieve
d : ℕ
hd : d ∈ P.divisors
⊢ 0 < ν d
Tactic:
rw [mem_divisors] at hd
Proof state after:
case h
s : Sieve
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ 0 < ν d
Theorem: Sieve.nu_ne_zero_of_mem_divisors_prodPrimes
Proof state before:
case h
s : Sieve
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ 0 < ν d
Tactic:
apply s.nu_pos_of_dvd_prodPrimes hd.left
Proof state after:
no goals
Theorem: Sieve.multSum_eq_main_err
Proof state before:
s : Sieve
d : ℕ
⊢ s.multSum d = ν d * X + s.rem d
Tactic:
dsimp [rem]
Proof state after:
s : Sieve
d : ℕ
⊢ (∑ n ∈ A, if d ∣ n then s.weights n else 0) = ν d * X + ((∑ n ∈ A, if d ∣ n then s.weights n else 0) - ν d * X)
Theorem: Sieve.multSum_eq_main_err
Proof state before:
s : Sieve
d : ℕ
⊢ (∑ n ∈ A, if d ∣ n then s.weights n else 0) = ν d * X + ((∑ n ∈ A, if d ∣ n then s.weights n else 0) - ν d * X)
Tactic:
ring
Proof state after:
no goals
Theorem: Sieve.siftedSum_as_delta
Proof state before:
s : Sieve
⊢ s.siftedSum = ∑ d ∈ A, s.weights d * δ (P.gcd d)
Tactic:
dsimp only [siftedSum]
Proof state after:
s : Sieve
⊢ (∑ d ∈ A, if P.Coprime d then s.weights d else 0) = ∑ d ∈ A, s.weights d * δ (P.gcd d)
Theorem: Sieve.siftedSum_as_delta
Proof state before:
s : Sieve
⊢ (∑ d ∈ A, if P.Coprime d then s.weights d else 0) = ∑ d ∈ A, s.weights d * δ (P.gcd d)
Tactic:
apply sum_congr rfl
Proof state after:
s : Sieve
⊢ ∀ x ∈ A, (if P.Coprime x then s.weights x else 0) = s.weights x * δ (P.gcd x)
Theorem: Sieve.siftedSum_as_delta
Proof state before:
s : Sieve
⊢ ∀ x ∈ A, (if P.Coprime x then s.weights x else 0) = s.weights x * δ (P.gcd x)
Tactic:
intro d _
Proof state after:
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.Coprime d then s.weights d else 0) = s.weights d * δ (P.gcd d)
Theorem: Sieve.siftedSum_as_delta
Proof state before:
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.Coprime d then s.weights d else 0) = s.weights d * δ (P.gcd d)
Tactic:
dsimp only [Nat.Coprime, delta] at *
Proof state after:
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.gcd d = 1 then s.weights d else 0) = s.weights d * if P.gcd d = 1 then 1 else 0
Theorem: Sieve.siftedSum_as_delta
Proof state before:
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.gcd d = 1 then s.weights d else 0) = s.weights d * if P.gcd d = 1 then 1 else 0
Tactic:
rw [mul_ite_zero]
Proof state after:
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.gcd d = 1 then s.weights d else 0) = if P.gcd d = 1 then s.weights d * 1 else 0
Theorem: Sieve.siftedSum_as_delta
Proof state before:
s : Sieve
d : ℕ
a✝ : d ∈ A
⊢ (if P.gcd d = 1 then s.weights d else 0) = if P.gcd d = 1 then s.weights d * 1 else 0
Tactic:
exact if_congr Iff.rfl (symm $ mul_one _) rfl
Proof state after:
no goals
Theorem: Sieve.nu_lt_self_of_dvd_prodPrimes
Proof state before:
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
⊢ ν d < 1
Tactic:
have hd_sq : Squarefree d := Squarefree.squarefree_of_dvd hdP s.prodPrimes_squarefree
Proof state after:
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ν d < 1
Theorem: Sieve.nu_lt_self_of_dvd_prodPrimes
Proof state before:
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∏ p ∈ d.primeFactors, ν p < ∏ p ∈ d.primeFactors, 1
Tactic:
apply prod_lt_prod_of_nonempty
Proof state after:
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∀ i ∈ d.primeFactors, 0 < ν i

case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∀ i ∈ d.primeFactors, ν i < 1

case h_ne
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ d.primeFactors.Nonempty
Theorem: Sieve.nu_lt_self_of_dvd_prodPrimes
Proof state before:
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∀ i ∈ d.primeFactors, 0 < ν i
Tactic:
intro p hp
Proof state after:
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hp : p ∈ d.primeFactors
⊢ 0 < ν p
Theorem: Sieve.nu_lt_self_of_dvd_prodPrimes
Proof state before:
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hp : p ∈ d.primeFactors
⊢ 0 < ν p
Tactic:
simp only [mem_primeFactors] at hp
Proof state after:
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hp : p.Prime ∧ p ∣ d ∧ d ≠ 0
⊢ 0 < ν p
Theorem: Sieve.nu_lt_self_of_dvd_prodPrimes
Proof state before:
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hp : p.Prime ∧ p ∣ d ∧ d ≠ 0
⊢ 0 < ν p
Tactic:
apply s.nu_pos_of_prime p (by aesop) (hp.2.1.trans hdP)
Proof state after:
no goals
Theorem: Sieve.nu_lt_self_of_dvd_prodPrimes
Proof state before:
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hp : p.Prime ∧ p ∣ d ∧ d ≠ 0
⊢ p.Prime
Tactic:
aesop
Proof state after:
no goals
Theorem: Sieve.nu_lt_self_of_dvd_prodPrimes
Proof state before:
case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∀ i ∈ d.primeFactors, ν i < 1
Tactic:
intro p hpd
Proof state after:
case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hpd : p ∈ d.primeFactors
⊢ ν p < 1
Theorem: Sieve.nu_lt_self_of_dvd_prodPrimes
Proof state before:
case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hpd : p ∈ d.primeFactors
⊢ ν p < 1
Tactic:
rw [mem_primeFactors_of_ne_zero hd_sq.ne_zero] at hpd
Proof state after:
case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hpd : p.Prime ∧ p ∣ d
⊢ ν p < 1
Theorem: Sieve.nu_lt_self_of_dvd_prodPrimes
Proof state before:
case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hpd : p.Prime ∧ p ∣ d
⊢ ν p < 1
Tactic:
apply s.nu_lt_one_of_prime p hpd.left (hpd.2.trans hdP)
Proof state after:
no goals
Theorem: Sieve.nu_lt_self_of_dvd_prodPrimes
Proof state before:
case h_ne
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ d.primeFactors.Nonempty
Tactic:
apply primeDivisors_nonempty _ <| (two_le_iff d).mpr ⟨hd_sq.ne_zero, hd_ne_one⟩
Proof state after:
no goals
Theorem: Sieve.nu_lt_self_of_dvd_prodPrimes
Proof state before:
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∏ p ∈ d.primeFactors, 1 = 1
Tactic:
simp
Proof state after:
no goals
Theorem: Sieve.selbergTerms_pos
Proof state before:
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < g l
Tactic:
rw [selbergTerms_apply]
Proof state after:
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ν l * ∏ p ∈ l.primeFactors, 1 / (1 - ν p)
Theorem: Sieve.selbergTerms_pos
Proof state before:
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ν l * ∏ p ∈ l.primeFactors, 1 / (1 - ν p)
Tactic:
apply mul_pos
Proof state after:
case ha
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ν l

case hb
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ∏ p ∈ l.primeFactors, 1 / (1 - ν p)
Theorem: Sieve.selbergTerms_pos
Proof state before:
case ha
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ν l

case hb
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ∏ p ∈ l.primeFactors, 1 / (1 - ν p)
Tactic:
exact s.nu_pos_of_dvd_prodPrimes hl
Proof state after:
case hb
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ∏ p ∈ l.primeFactors, 1 / (1 - ν p)
Theorem: Sieve.selbergTerms_pos
Proof state before:
case hb
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ∏ p ∈ l.primeFactors, 1 / (1 - ν p)
Tactic:
apply prod_pos
Proof state after:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
⊢ ∀ i ∈ l.primeFactors, 0 < 1 / (1 - ν i)
Theorem: Sieve.selbergTerms_pos
Proof state before:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
⊢ ∀ i ∈ l.primeFactors, 0 < 1 / (1 - ν i)
Tactic:
intro p hp
Proof state after:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
⊢ 0 < 1 / (1 - ν p)
Theorem: Sieve.selbergTerms_pos
Proof state before:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
⊢ 0 < 1 / (1 - ν p)
Tactic:
rw [one_div_pos]
Proof state after:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
⊢ 0 < 1 - ν p
Theorem: Sieve.selbergTerms_pos
Proof state before:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
⊢ 0 < 1 - ν p
Tactic:
have hp_prime : p.Prime := prime_of_mem_primeFactors hp
Proof state after:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : p.Prime
⊢ 0 < 1 - ν p
Theorem: Sieve.selbergTerms_pos
Proof state before:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : p.Prime
⊢ 0 < 1 - ν p
Tactic:
have hp_dvd : p ∣ P := (Nat.dvd_of_mem_primeFactors hp).trans hl
Proof state after:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : p.Prime
hp_dvd : p ∣ P
⊢ 0 < 1 - ν p
Theorem: Sieve.selbergTerms_pos
Proof state before:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : p.Prime
hp_dvd : p ∣ P
⊢ 0 < 1 - ν p
Tactic:
linarith only [s.nu_lt_one_of_prime p hp_prime hp_dvd]
Proof state after:
no goals
Theorem: Sieve.selbergTerms_mult
Proof state before:
s : Sieve
⊢ g.IsMultiplicative
Tactic:
unfold selbergTerms
Proof state after:
s : Sieve
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))).IsMultiplicative
Theorem: Sieve.selbergTerms_mult
Proof state before:
s : Sieve
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))).IsMultiplicative
Tactic:
arith_mult
Proof state after:
no goals
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ 1 / g l = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Tactic:
rw [selbergTerms_apply]
Proof state after:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ 1 / (ν l * ∏ p ∈ l.primeFactors, 1 / (1 - ν p)) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ 1 / (ν l * ∏ p ∈ l.primeFactors, 1 / (1 - ν p)) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Tactic:
simp only [one_div, mul_inv, inv_div, inv_inv, Finset.prod_congr, Finset.prod_inv_distrib]
Proof state after:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ (ν l)⁻¹ * ∏ x ∈ l.primeFactors, (1 - ν x) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ (ν l)⁻¹ * ∏ x ∈ l.primeFactors, (1 - ν x) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Tactic:
rw [(s.nu_mult).prodPrimeFactors_one_sub_of_squarefree _ hl]
Proof state after:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ (ν l)⁻¹ * ∑ d ∈ l.divisors, ↑(μ d) * ν d = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ (ν l)⁻¹ * ∑ d ∈ l.divisors, ↑(μ d) * ν d = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Tactic:
rw [mul_sum]
Proof state after:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
Tactic:
apply symm
Proof state after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹ = ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i)
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹ = ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i)
Tactic:
rw [← Nat.sum_divisorsAntidiagonal' fun d e : ℕ => ↑(μ d) * (ν e)⁻¹]
Proof state after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisorsAntidiagonal, ↑(μ i.1) * (ν i.2)⁻¹ = ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i)
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisorsAntidiagonal, ↑(μ i.1) * (ν i.2)⁻¹ = ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i)
Tactic:
rw [Nat.sum_divisorsAntidiagonal fun d e : ℕ => ↑(μ d) * (ν e)⁻¹]
Proof state after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisors, ↑(μ i) * (ν (l / i))⁻¹ = ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i)
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisors, ↑(μ i) * (ν (l / i))⁻¹ = ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i)
Tactic:
apply sum_congr rfl
Proof state after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∀ x ∈ l.divisors, ↑(μ x) * (ν (l / x))⁻¹ = (ν l)⁻¹ * (↑(μ x) * ν x)
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∀ x ∈ l.divisors, ↑(μ x) * (ν (l / x))⁻¹ = (ν l)⁻¹ * (↑(μ x) * ν x)
Tactic:
intro d hd
Proof state after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
⊢ ↑(μ d) * (ν (l / d))⁻¹ = (ν l)⁻¹ * (↑(μ d) * ν d)
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
⊢ ↑(μ d) * (ν (l / d))⁻¹ = (ν l)⁻¹ * (↑(μ d) * ν d)
Tactic:
have hd_dvd : d ∣ l := dvd_of_mem_divisors hd
Proof state after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ↑(μ d) * (ν (l / d))⁻¹ = (ν l)⁻¹ * (↑(μ d) * ν d)
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ↑(μ d) * (ν (l / d))⁻¹ = (ν l)⁻¹ * (↑(μ d) * ν d)
Tactic:
rw [←div_mult_of_dvd_squarefree ν s.nu_mult l d (dvd_of_mem_divisors hd) hl, inv_div]
Proof state after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ↑(μ d) * (ν d / ν l) = (ν l)⁻¹ * (↑(μ d) * ν d)

case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d ≠ 0
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ↑(μ d) * (ν d / ν l) = (ν l)⁻¹ * (↑(μ d) * ν d)

case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d ≠ 0
Tactic:
ring
Proof state after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d ≠ 0
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d ≠ 0
Tactic:
revert hnu_nonzero
Proof state after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν l ≠ 0 → ν d ≠ 0
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν l ≠ 0 → ν d ≠ 0
Tactic:
contrapose!
Proof state after:
case a
s : Sieve
l : ℕ
hl : Squarefree l
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d = 0 → ν l = 0
Theorem: Sieve.one_div_selbergTerms_eq_conv_moebius_nu
Proof state before:
case a
s : Sieve
l : ℕ
hl : Squarefree l
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d = 0 → ν l = 0
Tactic:
exact multiplicative_zero_of_zero_dvd ν s.nu_mult hl hd_dvd
Proof state after:
no goals
Theorem: Sieve.nu_eq_conv_one_div_selbergTerms
Proof state before:
s : Sieve
d : ℕ
hdP : d ∣ P
⊢ (ν d)⁻¹ = ∑ l ∈ P.divisors, if l ∣ d then 1 / g l else 0
Tactic:
apply symm
Proof state after:
case a
s : Sieve
d : ℕ
hdP : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then 1 / g l else 0) = (ν d)⁻¹
Theorem: Sieve.nu_eq_conv_one_div_selbergTerms
Proof state before:
case a
s : Sieve
d : ℕ
hdP : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then 1 / g l else 0) = (ν d)⁻¹
Tactic:
rw [←sum_filter, Nat.divisors_filter_dvd_of_dvd s.prodPrimes_ne_zero hdP]
Proof state after:
case a
s : Sieve
d : ℕ
hdP : d ∣ P
⊢ ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
Theorem: Sieve.nu_eq_conv_one_div_selbergTerms
Proof state before:
case a
s : Sieve
d : ℕ
hdP : d ∣ P
⊢ ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
Tactic:
have hd_pos : 0 < d := Nat.pos_of_ne_zero $ ne_zero_of_dvd_ne_zero s.prodPrimes_ne_zero hdP
Proof state after:
case a
s : Sieve
d : ℕ
hdP : d ∣ P
hd_pos : 0 < d
⊢ ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
Theorem: Sieve.nu_eq_conv_one_div_selbergTerms
Proof state before:
case a
s : Sieve
d : ℕ
hdP : d ∣ P
hd_pos : 0 < d
⊢ ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
Tactic:
revert hdP
Proof state after:
case a
s : Sieve
d : ℕ
hd_pos : 0 < d
⊢ d ∣ P → ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
Theorem: Sieve.nu_eq_conv_one_div_selbergTerms
Proof state before:
case a
s : Sieve
d : ℕ
hd_pos : 0 < d
⊢ d ∣ P → ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
Tactic:
revert d
Proof state after:
case a
s : Sieve
⊢ ∀ (d : ℕ), 0 < d → d ∣ P → ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
Theorem: Sieve.nu_eq_conv_one_div_selbergTerms
Proof state before:
case a
s : Sieve
⊢ ∀ (d : ℕ), 0 < d → d ∣ P → ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
Tactic:
apply (ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on _ (fun _ _ => Nat.dvd_trans)).mpr
Proof state after:
case a
s : Sieve
⊢ ∀ n > 0, (n ∈ fun x => ∃ c, P = x * c) → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * (ν x.2)⁻¹ = 1 / g n
Theorem: Sieve.nu_eq_conv_one_div_selbergTerms
Proof state before:
case a
s : Sieve
⊢ ∀ n > 0, (n ∈ fun x => ∃ c, P = x * c) → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * (ν x.2)⁻¹ = 1 / g n
Tactic:
intro l _ hlP
Proof state after:
case a
s : Sieve
l : ℕ
a✝ : l > 0
hlP : l ∈ fun x => ∃ c, P = x * c
⊢ ∑ x ∈ l.divisorsAntidiagonal, ↑(μ x.1) * (ν x.2)⁻¹ = 1 / g l
Theorem: Sieve.nu_eq_conv_one_div_selbergTerms
Proof state before:
case a
s : Sieve
l : ℕ
a✝ : l > 0
hlP : l ∈ fun x => ∃ c, P = x * c
⊢ ∑ x ∈ l.divisorsAntidiagonal, ↑(μ x.1) * (ν x.2)⁻¹ = 1 / g l
Tactic:
rw [sum_divisorsAntidiagonal' (f:=fun x y => (μ <| x) * (ν y)⁻¹) (n:=l)]
Proof state after:
case a
s : Sieve
l : ℕ
a✝ : l > 0
hlP : l ∈ fun x => ∃ c, P = x * c
⊢ ∑ i ∈ l.divisors, ↑(μ (l / i)) * (ν i)⁻¹ = 1 / g l
Theorem: Sieve.nu_eq_conv_one_div_selbergTerms
Proof state before:
case a
s : Sieve
l : ℕ
a✝ : l > 0
hlP : l ∈ fun x => ∃ c, P = x * c
⊢ ∑ i ∈ l.divisors, ↑(μ (l / i)) * (ν i)⁻¹ = 1 / g l
Tactic:
apply symm
Proof state after:
case a.a
s : Sieve
l : ℕ
a✝ : l > 0
hlP : l ∈ fun x => ∃ c, P = x * c
⊢ 1 / g l = ∑ i ∈ l.divisors, ↑(μ (l / i)) * (ν i)⁻¹
Theorem: Sieve.nu_eq_conv_one_div_selbergTerms
Proof state before:
case a.a
s : Sieve
l : ℕ
a✝ : l > 0
hlP : l ∈ fun x => ∃ c, P = x * c
⊢ 1 / g l = ∑ i ∈ l.divisors, ↑(μ (l / i)) * (ν i)⁻¹
Tactic:
exact s.one_div_selbergTerms_eq_conv_moebius_nu l
  (Squarefree.squarefree_of_dvd hlP s.prodPrimes_squarefree)
  (_root_.ne_of_gt $ s.nu_pos_of_dvd_prodPrimes hlP)
Proof state after:
no goals
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g l else 0) = g d * (ν d)⁻¹
Tactic:
calc
  (∑ l in divisors P, if l ∣ d then g l else 0) =
      ∑ l in divisors P, if l ∣ d then g (d / l) else 0 := by
    rw [← sum_over_dvd_ite s.prodPrimes_ne_zero hd,
      ← Nat.sum_divisorsAntidiagonal fun x _ => g x, Nat.sum_divisorsAntidiagonal' fun x _ => g x,
      sum_over_dvd_ite s.prodPrimes_ne_zero hd]
  _ = g d * ∑ l in divisors P, if l ∣ d then 1 / g l else 0 := by
    rw [mul_sum]; apply sum_congr rfl; intro l hl
    rw [mul_ite_zero]; apply if_ctx_congr Iff.rfl _ (fun _ => rfl); intro h
    rw [← div_mult_of_dvd_squarefree g s.selbergTerms_mult d l]; ring
    exact h; apply Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree
    apply _root_.ne_of_gt; rw [mem_divisors] at hl ; apply selbergTerms_pos; exact hl.left
  _ = g d * (ν d)⁻¹ := by rw [← s.nu_eq_conv_one_div_selbergTerms d hd]
Proof state after:
no goals
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g l else 0) = ∑ l ∈ P.divisors, if l ∣ d then g (d / l) else 0
Tactic:
rw [← sum_over_dvd_ite s.prodPrimes_ne_zero hd,
  ← Nat.sum_divisorsAntidiagonal fun x _ => g x, Nat.sum_divisorsAntidiagonal' fun x _ => g x,
  sum_over_dvd_ite s.prodPrimes_ne_zero hd]
Proof state after:
no goals
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g (d / l) else 0) = g d * ∑ l ∈ P.divisors, if l ∣ d then 1 / g l else 0
Tactic:
rw [mul_sum]
Proof state after:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g (d / l) else 0) = ∑ i ∈ P.divisors, g d * if i ∣ d then 1 / g i else 0
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g (d / l) else 0) = ∑ i ∈ P.divisors, g d * if i ∣ d then 1 / g i else 0
Tactic:
apply sum_congr rfl
Proof state after:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ ∀ x ∈ P.divisors, (if x ∣ d then g (d / x) else 0) = g d * if x ∣ d then 1 / g x else 0
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ ∀ x ∈ P.divisors, (if x ∣ d then g (d / x) else 0) = g d * if x ∣ d then 1 / g x else 0
Tactic:
intro l hl
Proof state after:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ (if l ∣ d then g (d / l) else 0) = g d * if l ∣ d then 1 / g l else 0
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ (if l ∣ d then g (d / l) else 0) = g d * if l ∣ d then 1 / g l else 0
Tactic:
rw [mul_ite_zero]
Proof state after:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ (if l ∣ d then g (d / l) else 0) = if l ∣ d then g d * (1 / g l) else 0
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ (if l ∣ d then g (d / l) else 0) = if l ∣ d then g d * (1 / g l) else 0
Tactic:
apply if_ctx_congr Iff.rfl _ (fun _ => rfl)
Proof state after:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ l ∣ d → g (d / l) = g d * (1 / g l)
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ l ∣ d → g (d / l) = g d * (1 / g l)
Tactic:
intro h
Proof state after:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g (d / l) = g d * (1 / g l)
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g (d / l) = g d * (1 / g l)
Tactic:
rw [← div_mult_of_dvd_squarefree g s.selbergTerms_mult d l]
Proof state after:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g d / g l = g d * (1 / g l)

case hdl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ l ∣ d

case hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ Squarefree d

case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0
Theorem: Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Proof state before:
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g d / g l = g d * (1 / g l)

case hdl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ l ∣ d

case hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ Squarefree d

case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0
Tactic:
ring
Proof state after:
case hdl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ l ∣ d

case hl
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ Squarefree d

case hd
s : Sieve
d : ℕ
hd : d ∣ P
l : ℕ
hl : l ∈ P.divisors
h : l ∣ d
⊢ g l ≠ 0