decay_bounds_key

lemma decay_bounds_key (f : W21) (u : ℝ) : ‖𝓕 (f : ℝ → ℂ) u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹ := by  have l1 : 0 < 1 + u ^ 2 := one_add_sq_pos _  have l2 : 1 + u ^ 2 = ‖(1 : ℂ) + u ^ 2‖ := by    norm_cast ; simp only [Real.norm_eq_abs, abs_eq_self.2 l1.le]  have l3 : ‖1 / ((4 : ℂ) * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹ := by simp  have key := fourierIntegral_self_add_deriv_deriv f u  simp only [Function.iterate_succ _ 1, Function.iterate_one, Function.comp_apply] at key  rw [F_sub f.hf (f.hf''.const_mul (1 / (4 * ↑π ^ 2)))] at key  rw [← div_eq_mul_inv, le_div_iff₀ l1, mul_comm, l2, ← norm_mul, key, sub_eq_add_neg]  apply norm_add_le _ _ |>.trans  change _ ≤ W21.norm _  rw [norm_neg, F_mul, norm_mul, W21.norm]  gcongr <;> apply VectorFourier.norm_fourierIntegral_le_integral_norm