SelbergSieve.selbergWeights_mul_mu_nonneg

@[aesop safe]theorem selbergWeights_mul_mu_nonneg (d : ℕ) (hdP : d ∣ P) :    0 ≤ γ d * μ d := by  dsimp only [selbergWeights]  rw [if_pos hdP, mul_assoc]  trans ((μ d :ℝ)^2 * (ν d)⁻¹ * g d * S⁻¹ * ∑ m ∈ divisors P,          if (d * m) ^ 2 ≤ y ∧ Coprime m d then g m else 0)  swap  · apply le_of_eq; ring  refine mul_nonneg (div_nonneg (mul_nonneg (mul_nonneg ?_ ?_) ?_) ?_) ?_  · apply sq_nonneg  · rw [inv_nonneg]    exact le_of_lt <| nu_pos_of_dvd_prodPrimes hdP  · exact le_of_lt <| selbergTerms_pos _ d hdP  · exact s.selbergBoundingSum_nonneg  apply sum_nonneg; intro m hm  split_ifs with h  · exact le_of_lt <| selbergTerms_pos _ m (dvd_of_mem_divisors hm)  · rfl