Source indexedlemma · leanprover/lean4:v4.32.0

bound_sum_log0

PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1626 to 1635

Mathematical statement

Exact Lean statement

lemma bound_sum_log0 {C : ℝ} (hf : chebyWith C f) {x : ℝ} (hx : 1 ≤ x) :
    ∑' i, ‖f i‖ / i * (1 + (1 / (2 * π) * log (i / x)) ^ 2)⁻¹ ≤
      C * (1 + ∫ t in Ioi 0, hh (1 / (2 * π)) t)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma bound_sum_log0 {C : ℝ} (hf : chebyWith C f) {x : ℝ} (hx : 1 ≤ x) :    ∑' i, ‖f i‖ / i * (1 + (1 / (2 * π) * log (i / x)) ^ 2)⁻¹ ≤      C * (1 + ∫ t in Ioi 0, hh (1 / (2 * π)) t) := by   let f0 i := if i = 0 then 0 else f i  have l1 : chebyWith C f0 := by    intro n ; refine Finset.sum_le_sum (fun i _ => ?_) |>.trans (hf n)    by_cases hi : i = 0 <;> simp [hi, f0]  have l2 i : ‖f i‖ / i = ‖f0 i‖ / i := by by_cases hi : i = 0 <;> simp [hi, f0]  simp_rw [l2] ; apply bound_sum_log rfl l1 hx