have l3 : ‖1 / ((4 : ℂ) * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹ := by simp
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹