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

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