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

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
ι : Type u_2
s : Finset ι
f : ι → 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => ∑ i in s, (f i) x) ξ = ∑ i in s, 𝓕 (fun x => (f i) x) ξ
Tactic:
simpa [Real.fourierIntegral_def, Finset.smul_sum] using
  integral_finset_sum s fun i _ ↦ Real.integrable_fourierIntegrand (f i) ξ
State after:
no goals