SelbergSieve.selberg_bound_weights

theorem selberg_bound_weights (d : ℕ) : |γ d| ≤ 1 := by  by_cases hdP : d ∣ P  swap  · rw [s.selbergWeights_eq_zero_of_not_dvd hdP]; simp only [zero_le_one, abs_zero]  have : 1*S ≥ γ d * ↑(μ d) * S := by    rw[one_mul]    exact s.selbergBoundingSum_ge hdP  replace this : γ d * μ d ≤ 1 := by    apply le_of_mul_le_mul_of_pos_right this (s.selbergBoundingSum_pos)  convert this using 1  rw [← abs_of_nonneg <| s.selbergWeights_mul_mu_nonneg d hdP,    abs_mul, ←Int.cast_abs, abs_moebius_eq_one_of_squarefree <|    (s.prodPrimes_squarefree.squarefree_of_dvd hdP), Int.cast_one, mul_one]