SelbergSieve.selberg_bound_simple_mainSum

theorem selberg_bound_simple_mainSum :    mainSum (s := s.toBoundingSieve) μ⁺ = S⁻¹ := by  rw [mainSum_eq_diag_quad_form]  trans (∑ l ∈ divisors P, (if l ^ 2 ≤ y then g l * (S⁻¹) ^ 2 else 0))  · apply sum_congr rfl; intro l hl    rw [s.selbergWeights_diagonalisation l hl, ite_pow, zero_pow two_ne_zero, mul_ite_zero]    apply if_congr Iff.rfl _ rfl    trans (1/g l * g l * g l * (μ l:ℝ)^2  * (S⁻¹) ^ 2)    · ring    norm_cast; rw [moebius_sq_eq_one_of_squarefree <| squarefree_of_mem_divisors_prodPrimes hl]    rw [one_div_mul_cancel <| _root_.ne_of_gt <| selbergTerms_pos _ l <| dvd_of_mem_divisors hl]    ring  conv => {lhs; congr; {skip}; {ext i; rw [← ite_zero_mul]}}  dsimp only [selbergBoundingSum]  rw [←sum_mul, sq, ←mul_assoc, mul_inv_cancel₀]  · ring  · apply _root_.ne_of_gt; apply selbergBoundingSum_pos