Theorem: Sieve.lambdaSquared_mainSum_eq_quad_form (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean)

State before:
s : Sieve
w : ℕ → ℝ
⊢ s.mainSum (lambdaSquared w) = ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
dsimp only [mainSum, lambdaSquared]
State after:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d ∈ P.divisors, (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹

State before:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d ∈ P.divisors, (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
trans (∑ d in divisors P, ∑ d1 in divisors d, ∑ d2 in divisors d,
        if d = d1.lcm d2 then w d1 * w d2 * ν d else 0)
State after:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d ∈ P.divisors, (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0

s : Sieve
w : ℕ → ℝ
⊢ (∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0) =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹

State before:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0) =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
trans (∑ d in divisors P, ∑ d1 in divisors P, ∑ d2 in divisors P,
        if d = d1.lcm d2 then w d1 * w d2 * ν d else 0)
State after:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0) =
    ∑ d ∈ P.divisors, ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0

s : Sieve
w : ℕ → ℝ
⊢ (∑ d ∈ P.divisors, ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0) =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹

State before:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d ∈ P.divisors, ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0) =
    ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
rw [sum_comm, sum_congr rfl]
State after:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x_1 = x.lcm d2 then w x * w d2 * ν x_1 else 0) =
      ∑ d2 ∈ P.divisors, ν x * w x * ν d2 * w d2 * (ν (x.gcd d2))⁻¹

State before:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x_1 = x.lcm d2 then w x * w d2 * ν x_1 else 0) =
      ∑ d2 ∈ P.divisors, ν x * w x * ν d2 * w d2 * (ν (x.gcd d2))⁻¹
Tactic:
intro d1 hd1
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, ∑ d2 ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) =
    ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, ∑ d2 ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) =
    ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
rw [sum_comm, sum_congr rfl]
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, if x_1 = d1.lcm x then w d1 * w x * ν x_1 else 0) = ν d1 * w d1 * ν x * w x * (ν (d1.gcd x))⁻¹

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, if x_1 = d1.lcm x then w d1 * w x * ν x_1 else 0) = ν d1 * w d1 * ν x * w x * (ν (d1.gcd x))⁻¹
Tactic:
intro d2 hd2
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
have h : d1.lcm d2 ∣ P := Nat.lcm_dvd_iff.mpr ⟨dvd_of_mem_divisors hd1, dvd_of_mem_divisors hd2⟩
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ (∑ x ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ (∑ x ∈ P.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
rw [←sum_intro (divisors P) (d1.lcm d2) (mem_divisors.mpr ⟨h, s.prodPrimes_ne_zero⟩ )]
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ w d1 * w d2 * ν (d1.lcm d2) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ w d1 * w d2 * ν (d1.lcm d2) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
Tactic:
rw [s.nu_mult.mult_lcm_eq_of_ne_zero]
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ w d1 * w d2 * (ν d1 * ν d2 / ν (d1.gcd d2)) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹

case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ ν (d1.gcd d2) ≠ 0

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ w d1 * w d2 * (ν d1 * ν d2 / ν (d1.gcd d2)) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹

case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ ν (d1.gcd d2) ≠ 0
Tactic:
ring
State after:
case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ ν (d1.gcd d2) ≠ 0

State before:
case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ ν (d1.gcd d2) ≠ 0
Tactic:
refine _root_.ne_of_gt (s.nu_pos_of_dvd_prodPrimes ?_)
State after:
case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ d1.gcd d2 ∣ P

State before:
case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ d1.gcd d2 ∣ P
Tactic:
trans d1
State after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ d1.gcd d2 ∣ d1

s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ d1 ∣ P

State before:
s : Sieve
w : ℕ → ℝ
⊢ ∑ d ∈ P.divisors, (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Tactic:
rw [sum_congr rfl]
State after:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then w d1 * w d2 else 0) * ν x =
      ∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0

State before:
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then w d1 * w d2 else 0) * ν x =
      ∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then w d1 * w d2 * ν x else 0
Tactic:
intro d _
State after:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝ : d ∈ P.divisors
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0

State before:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝ : d ∈ P.divisors
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Tactic:
rw [sum_mul, sum_congr rfl]
State after:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ d.divisors,
    (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) * ν d =
      ∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 * ν d else 0

State before:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ d.divisors,
    (∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 else 0) * ν d =
      ∑ d2 ∈ d.divisors, if d = x.lcm d2 then w x * w d2 * ν d else 0
Tactic:
intro d1 _
State after:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝¹ : d ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0

State before:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝¹ : d ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ (∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d =
    ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Tactic:
rw [sum_mul, sum_congr rfl]
State after:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝¹ : d ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ ∀ x ∈ d.divisors, (if d = d1.lcm x then w d1 * w x else 0) * ν d = if d = d1.lcm x then w d1 * w x * ν d else 0

State before:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝¹ : d ∈ P.divisors
d1 : ℕ
a✝ : d1 ∈ d.divisors
⊢ ∀ x ∈ d.divisors, (if d = d1.lcm x then w d1 * w x else 0) * ν d = if d = d1.lcm x then w d1 * w x * ν d else 0
Tactic:
intro d2 _
State after:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝² : d ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d = if d = d1.lcm d2 then w d1 * w d2 * ν d else 0

State before:
s : Sieve
w : ℕ → ℝ
d : ℕ
a✝² : d ∈ P.divisors
d1 : ℕ
a✝¹ : d1 ∈ d.divisors
d2 : ℕ
a✝ : d2 ∈ d.divisors
⊢ (if d = d1.lcm d2 then w d1 * w d2 else 0) * ν d = if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Tactic:
rw [ite_zero_mul]
State after:
no goals

State before:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d ∈ P.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0) =
    ∑ d ∈ P.divisors, ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if d = d1.lcm d2 then w d1 * w d2 * ν d else 0
Tactic:
apply conv_lambda_sq_larger_sum
State after:
no goals

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ d1.gcd d2 ∣ d1
Tactic:
exact Nat.gcd_dvd_left d1 d2
State after:
no goals

State before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ d1 ∣ P
Tactic:
exact dvd_of_mem_divisors hd1
State after:
no goals