SelbergSieve.lambdaSquared_mainSum_eq_quad_form

theorem lambdaSquared_mainSum_eq_quad_form (w : ℕ → ℝ) :    mainSum (s := s) (lambdaSquared w) =      ∑ d1 ∈ divisors P, ∑ d2 ∈ divisors P,        ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ := by  dsimp only [mainSum, lambdaSquared]  trans (∑ d ∈ divisors P, ∑ d1 ∈ divisors d, ∑ d2 ∈ divisors d,          if d = d1.lcm d2 then w d1 * w d2 * ν d else 0)  · rw [sum_congr rfl]; intro d _    rw [sum_mul, sum_congr rfl]; intro d1 _    rw [sum_mul, sum_congr rfl]; intro d2 _    rw [ite_zero_mul]   trans (∑ d ∈ divisors P, ∑ d1 ∈ divisors P, ∑ d2 ∈ divisors P,          if d = d1.lcm d2 then w d1 * w d2 * ν d else 0)  · apply conv_lambda_sq_larger_sum  rw [sum_comm, sum_congr rfl]; intro d1 hd1  rw [sum_comm, sum_congr rfl]; intro d2 hd2  have h : d1.lcm d2 ∣ P :=    Nat.lcm_dvd_iff.mpr ⟨dvd_of_mem_divisors hd1, dvd_of_mem_divisors hd2⟩  rw [sum_ite_eq_of_mem' (divisors P) (d1.lcm d2) _ (mem_divisors.mpr ⟨h, prodPrimes_ne_zero⟩)]  rw [s.nu_mult.map_lcm]  · ring  refine _root_.ne_of_gt (nu_pos_of_dvd_prodPrimes ?_)  trans d1  · exact Nat.gcd_dvd_left d1 d2  · exact dvd_of_mem_divisors hd1