change _ ≤ W21.norm _
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)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 f.toFun u - 𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u
⊢ ‖𝓕 f.toFun u‖ + ‖-𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u‖ ≤ ‖f‖
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)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 f.toFun u - 𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u
⊢ ‖𝓕 f.toFun u‖ + ‖-𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u‖ ≤ W21.norm fun v => f.toFun v