Sieve.boundingSum_ge_sum

theorem boundingSum_ge_sum (s : SelbergSieve) (hnu : s.nu = (ζ : ArithmeticFunction ℝ).pdiv .id)  (hP : ∀ p:ℕ, p.Prime → (p:ℝ) ≤ s.level → p ∣ s.prodPrimes) :    s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 (Nat.floor <| Real.sqrt s.level), 1 / (m:ℝ) := by  trans ∑ m ∈ Finset.Icc 1 (Nat.floor <| Real.sqrt s.level), (ζ : ArithmeticFunction ℝ).pdiv .id m  · rw[←hnu]    apply selbergBoundingSum_ge_sum_div    · intro p hpp hple      apply hP p hpp hple    · rw[hnu]      exact CompletelyMultiplicative.zeta.pdiv CompletelyMultiplicative.id    · intro n      rw[hnu]      apply div_nonneg      · by_cases h : n = 0 <;> simp[h]      simp    · intro p hpp _      rw[hnu]      simp only [ArithmeticFunction.pdiv_apply, ArithmeticFunction.natCoe_apply,        ArithmeticFunction.zeta_apply, Nat.cast_ite, CharP.cast_eq_zero, Nat.cast_one,        ArithmeticFunction.id_apply]      rw [if_neg, one_div]      · apply inv_lt_one_of_one_lt₀; norm_cast        exact hpp.one_lt      exact hpp.ne_zero  apply le_of_eq  apply Finset.sum_congr rfl  intro m hm  rw [Finset.mem_Icc] at hm  simp only [one_div, ArithmeticFunction.pdiv_apply, ArithmeticFunction.natCoe_apply,    ArithmeticFunction.zeta_apply_ne (show m ≠ 0 by omega), Nat.cast_one,    ArithmeticFunction.id_apply];