Source indexedtheorem · leanprover/lean4:v4.32.0

decay_bounds_W21

PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:407 to 419

Mathematical statement

Exact Lean statement

theorem decay_bounds_W21 (f : W21) (hA : ∀ t, ‖f t‖ ≤ A / (1 + t ^ 2))
    (hA' : ∀ t, ‖deriv (deriv f) t‖ ≤ A / (1 + t ^ 2)) (u) :
    ‖𝓕 (f : ℝ → ℂ) u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem decay_bounds_W21 (f : W21) (hA : ∀ t, ‖f t‖ ≤ A / (1 + t ^ 2))    (hA' : ∀ t, ‖deriv (deriv f) t‖ ≤ A / (1 + t ^ 2)) (u) :    ‖𝓕 (f : ℝ → ℂ) u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2) := by  have l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A) := by field_simp  have l1 : ∫ (v : ℝ), ‖f v‖ ≤ π * A := by    apply decay_bounds_aux f.continuous.aestronglyMeasurable    simp_rw [← div_eq_mul_inv] ; exact hA  have l2 : ∫ (v : ℝ), ‖deriv (deriv f) v‖ ≤ π * A := by    apply decay_bounds_aux f.deriv.deriv.continuous.aestronglyMeasurable    simp_rw [← div_eq_mul_inv] ; exact hA'  apply decay_bounds_key f u |>.trans  change W21.norm _ * _ ≤ _  simp_rw [W21.norm, div_eq_mul_inv, add_mul, l0] ; gcongr