Source indexedlemma · leanprover/lean4:v4.32.0

W21.integrable_fourier

PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:462 to 470

Mathematical statement

Exact Lean statement

lemma W21.integrable_fourier (ψ : W21) (hc : c ≠ 0) :
    Integrable fun u ↦ 𝓕 (ψ : ℝ → ℂ) (u / c)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma W21.integrable_fourier (ψ : W21) (hc : c ≠ 0) :    Integrable fun u ↦ 𝓕 (ψ : ℝ → ℂ) (u / c) := by  have l1 (C) : Integrable (fun u ↦ C / (1 + (u / c) ^ 2)) volume := by    simpa using! (integrable_inv_one_add_sq.comp_div hc).const_mul C  have l2 : AEStronglyMeasurable (fun u ↦ 𝓕 (ψ : ℝ → ℂ) (u / c)) volume := by    apply Continuous.aestronglyMeasurable ; fun_prop  obtain ⟨C, h⟩ := decay_bounds_cor ψ  apply @Integrable.mono' ℝ ℂ _ volume _ _ (fun u => C / (1 + (u / c) ^ 2)) (l1 C) l2 ?_  apply Eventually.of_forall (fun x => h _)