apply mul_nonneg
case ha.ha.ha
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ↑(μ d) ^ 2 * (ν d)⁻¹

case ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ g d

case ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ S

case hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0
case ha.ha.ha.ha
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ↑(μ d) ^ 2

case ha.ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ (ν d)⁻¹

case ha.ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ g d

case ha.hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ S

case hb
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0