Theorem: SchwartzMap.Real.norm_fourierIntegral_le_integral_norm (ForML/SchwartzRealFourier.lean)

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖𝓕 (fun x => f x) ξ‖ ≤ ∫ (x : ℝ), ‖f x‖
Tactic:
simpa [Real.fourierIntegral_def] using
  norm_integral_le_of_norm_le f.integrable.norm
    (Filter.eventually_of_forall (by simp [norm_smul]))
State after:
no goals

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ∀ (x : ℝ), ‖↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x‖ ≤ ‖f x‖
Tactic:
simp [norm_smul]
State after:
no goals