SelbergSieve.selbergBoundingSum_ge

theorem selbergBoundingSum_ge {d : ℕ} (hdP : d ∣ P) :    S ≥ γ d * ↑(μ d) * S := by  calc  _ = (∑ k ∈ divisors P, ∑ l ∈ divisors P, if k = d.gcd l ∧ l ^ 2 ≤ y then g l else 0) := by    dsimp only [selbergBoundingSum]    rw [sum_comm, sum_congr rfl]; intro l _    simp_rw [ite_and]    rw [sum_ite_eq_of_mem']    · rw [mem_divisors]      exact ⟨(Nat.gcd_dvd_left d l).trans (hdP), prodPrimes_ne_zero⟩  _ = (∑ k ∈ divisors P,          if k ∣ d then            g k * ∑ m ∈ divisors P, if (k * m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0          else 0) := by    apply sum_congr rfl; intro k hk    rw [mul_sum]    split_ifs with hkd    swap    · rw [sum_eq_zero]; intro l _      rw [if_neg]      push Not; intro h; exfalso      rw [h] at hkd      exact hkd <| Nat.gcd_dvd_left d l    rw [sum_mul_subst k P, sum_congr rfl]    · intro m hm      rw [mul_ite_zero, ← ite_and]      apply if_ctx_congr _ _ fun _ => rfl      · exact_mod_cast s._helper hkd hk hm      · intro h        apply (selbergTerms_mult _).map_mul_of_coprime        rw [gcd_comm]; apply h.2.coprime_dvd_right hkd    · intro l _ hkl; apply if_neg      push Not; intro h; exfalso      rw [h] at hkl; exact hkl (Nat.gcd_dvd_right d l)  _ ≥ (∑ k ∈ divisors P, if k ∣ d          then g k * ∑ m ∈ divisors P, if (d * m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0          else 0 ) := by    apply sum_le_sum; intro k _    split_ifs with hkd    swap    · rfl    apply mul_le_mul le_rfl _ _ (le_of_lt <| selbergTerms_pos _ k <| hkd.trans hdP)    · apply sum_le_sum; intro m hm      split_ifs with h h' h'      · rfl      · exfalso; apply h'        refine ⟨?_, h.2⟩        · trans ((d*m)^2:ℝ)          · norm_cast; gcongr            refine Nat.le_of_dvd ?_ hkd            apply Nat.pos_of_ne_zero; apply ne_zero_of_dvd_ne_zero prodPrimes_ne_zero hdP          exact h.1      · refine le_of_lt <| selbergTerms_pos _ m <| dvd_of_mem_divisors hm      · rfl    apply sum_nonneg; intro m hm    split_ifs    · apply le_of_lt <| selbergTerms_pos _ m <| dvd_of_mem_divisors hm    · rfl  _ = _ := by    conv => enter [1, 2, k]; rw [← ite_zero_mul]    rw [←sum_mul, conv_selbergTerms_eq_selbergTerms_mul_nu _ hdP]    trans (S * S⁻¹ * (μ d:ℝ)^2 * (ν d)⁻¹ * g d * (∑ m ∈ divisors P, if (d*m) ^ 2 ≤ y ∧      Coprime m d then g m else 0))    · rw [mul_inv_cancel₀, ←Int.cast_pow, moebius_sq_eq_one_of_squarefree]      · ring      · exact Squarefree.squarefree_of_dvd hdP s.prodPrimes_squarefree      · exact _root_.ne_of_gt <| s.selbergBoundingSum_pos    dsimp only [selbergWeights]; rw [if_pos hdP]    ring