Source indexedlemma · leanprover/lean4:v4.32.0

summable_fourier

PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1652 to 1658

Mathematical statement

Exact Lean statement

lemma summable_fourier (x : ℝ) (hx : 0 < x) (ψ : W21) (hcheby : cheby f) :
    Summable fun i ↦ ‖f i / ↑i * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * Real.log (↑i / x))‖

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma summable_fourier (x : ℝ) (hx : 0 < x) (ψ : W21) (hcheby : cheby f) :    Summable fun i ↦ ‖f i / ↑i * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * Real.log (↑i / x))‖ := 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 ψ  exact Summable.of_nonneg_of_le (fun _ => norm_nonneg _) l6    (by simpa using l5.const_smul (W21.norm ψ))