trans ∑ m in Finset.Icc 1 (Nat.floor $ Real.sqrt s.level), (ζ : ArithmeticFunction ℝ).pdiv .id m
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m

s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, ((↑ζ).pdiv ↑ArithmeticFunction.id) m ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m