have l1 : 0 < 1 + u ^ 2 := one_add_sq_pos _
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
⊢ ‖𝓕 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
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹