Source indexedlemma · leanprover/lean4:v4.32.0

bound_I1

PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1660 to 1671

Mathematical statement

Exact Lean statement

lemma bound_I1 (x : ℝ) (hx : 0 < x) (ψ : W21) (hcheby : cheby f) :
    ‖∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * log (n / x))‖ ≤
    W21.norm ψ • ∑' i, ‖f i‖ / i * (1 + (1 / (2 * π) * log (i / x)) ^ 2)⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma bound_I1 (x : ℝ) (hx : 0 < x) (ψ : W21) (hcheby : cheby f) :    ‖∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * log (n / x))‖ ≤    W21.norm ψ • ∑' i, ‖f i‖ / i * (1 + (1 / (2 * π) * log (i / x)) ^ 2)⁻¹ := by   have l5 : Summable fun i ↦ ‖f i‖ / ↑i * ((1 + (1 / (2 * ↑π) * ↑(Real.log (↑i / x))) ^ 2)⁻¹) := by    simpa using limiting_fourier_lim1_aux hcheby hx 1 (zero_le_one' ℝ)  have l6 := summable_fourier_aux x f ψ  have l1 : Summable fun i ↦ ‖f i / ↑i * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * Real.log (↑i / x))‖ := by    exact summable_fourier x hx ψ hcheby  apply (norm_tsum_le_tsum_norm l1).trans  simpa only [← Summable.tsum_const_smul _ l5] using!    Summable.tsum_mono l1 (by simpa using l5.const_smul (W21.norm ψ)) l6