English
For a family of multilinear maps M, the Fourier integral respects multilinear structure: applying the transform to a multilinear map-valued function reduces to applying the transform componentwise.
Русский
Преобразование Фурье сохраняет мультилинейную структуру: если функция принимает значения в линейных картах, то преобразование действует по компонентам.
LaTeX
$$$$ \\mathrm{fourierIntegral}(e, \\mu, L, f)(w) \\text{ preserves multilinear structure in } f. $$$$
Lean4
/-- The Fourier integral of an `L^1` function is a continuous function. -/
theorem fourierIntegral_continuous [FirstCountableTopology W] (he : Continuous e)
(hL : Continuous fun p : V × W ↦ L p.1 p.2) {f : V → E} (hf : Integrable f μ) :
Continuous (fourierIntegral e μ L f) := by
apply continuous_of_dominated
· exact fun w ↦ ((fourierIntegral_convergent_iff he hL w).2 hf).1
· exact fun w ↦ ae_of_all _ fun v ↦ le_of_eq (Circle.norm_smul _ _)
· exact hf.norm
· refine ae_of_all _ fun v ↦ (he.comp ?_).smul continuous_const
exact (hL.comp (.prodMk_right _)).neg
