SelbergSieve.lambdaSquared_mainSum_eq_diag_quad_form

theorem lambdaSquared_mainSum_eq_diag_quad_form (w : ℕ → ℝ) :    mainSum (s := s) (lambdaSquared w) =      ∑ l ∈ divisors P,        1 / g l * (∑ d ∈ divisors P, if l ∣ d then ν d * w d else 0) ^ 2 :=  by  rw [lambdaSquared_mainSum_eq_quad_form s w]  trans (∑ d1 ∈ divisors P, ∑ d2 ∈ divisors P, (∑ l ∈ divisors P,          if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0))  · apply sum_congr rfl; intro d1 hd1; apply sum_congr rfl; intro d2 _    have hgcd_dvd: d1.gcd d2 ∣ P := Trans.trans (Nat.gcd_dvd_left d1 d2) (dvd_of_mem_divisors hd1)    rw [nu_eq_conv_one_div_selbergTerms s _ hgcd_dvd, mul_sum]    apply sum_congr rfl; intro l _    rw [mul_ite_zero]; apply if_congr Iff.rfl _ rfl    ring  trans (∑ l ∈ divisors P, ∑ d1 ∈ divisors P, ∑ d2 ∈ divisors P,        if l ∣ Nat.gcd d1 d2 then 1 / selbergTerms s l * (ν d1 * w d1) * (ν d2 * w d2) else 0)  · apply symm; rw [sum_comm, sum_congr rfl]; intro d1 _    rw [sum_comm]  apply sum_congr rfl; intro l _  rw [sq, sum_mul, mul_sum, sum_congr rfl]; intro d1 _  rw [mul_sum, mul_sum, sum_congr rfl]; intro d2 _  rw [ite_zero_mul_ite_zero, mul_ite_zero]  apply if_congr (Nat.dvd_gcd_iff) _ rfl;  ring