simp only [Function.iterate_succ _ 1, Function.iterate_one, Function.comp_apply] at key
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 = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) 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
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) u) u
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹