have l1 : ∫ (v : ℝ), ‖f v‖ ≤ π * A := by
  apply decay_bounds_aux f.continuous.aestronglyMeasurable
  simp_rw [← div_eq_mul_inv] ; exact hA
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
⊢ ‖𝓕 f.toFun u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
⊢ ‖𝓕 f.toFun u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)