Source indexedtheorem · leanprover/lean4:v4.32.0

Sieve.boundingSum_ge_log

PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean:496 to 507

Mathematical statement

Exact Lean statement

theorem boundingSum_ge_log (s : SelbergSieve) (hnu : s.nu = (ζ : ArithmeticFunction ℝ).pdiv .id)
  (hP : ∀ p:ℕ, p.Prime → (p:ℝ) ≤ s.level → p ∣ s.prodPrimes)  :
    s.selbergBoundingSum ≥ Real.log (s.level) / 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem boundingSum_ge_log (s : SelbergSieve) (hnu : s.nu = (ζ : ArithmeticFunction ℝ).pdiv .id)  (hP : ∀ p:ℕ, p.Prime → (p:ℝ) ≤ s.level → p ∣ s.prodPrimes)  :    s.selbergBoundingSum ≥ Real.log (s.level) / 2 := by  trans (∑ m ∈ Finset.Icc 1 (Nat.floor <| Real.sqrt s.level), 1 / (m:ℝ))  · exact boundingSum_ge_sum s hnu hP  trans (Real.log <| Real.sqrt s.level)  · rw [ge_iff_le]; simp_rw[one_div]    apply Aux.log_le_sum_inv (Real.sqrt s.level)    rw [Real.le_sqrt] <;> linarith[s.one_le_level]  · apply ge_of_eq    refine Real.log_sqrt ?h.hx    linarith[s.one_le_level]