rw [s.lambdaSquared_mainSum_eq_quad_form w]
s : Sieve
w : ℕ → ℝ
⊢ s.mainSum (lambdaSquared w) = ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2
s : Sieve
w : ℕ → ℝ
⊢ ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * w d else 0) ^ 2