English
If f is a family of linear maps, then the Fourier integral applied to the function returning the value at each parameter is equal to the function that maps the parameter to the Fourier integral of the corresponding linear map applied to the parameter.
Русский
Если функция принимает значения линейных отображений, то преобразование Фурье применяется по значениям и эквивалентно соответствующему отображению параметра.
LaTeX
$$$$ \\mathrm{fourierIntegral}(e,\\mu,L.toLinearMap_{12}, f)(w) = \\mathrm{fourierIntegral}(e,\\mu,L.toLinearMap_{12}, (\\lambda x. f(x) \\, a))(w). $$$$
Lean4
theorem fourierIntegral_continuousMultilinearMap_apply {f : V → (ContinuousMultilinearMap ℝ M E)} {m : (i : ι) → M i}
{w : W} (he : Continuous e) (hf : Integrable f μ) :
fourierIntegral e μ L.toLinearMap₁₂ f w m = fourierIntegral e μ L.toLinearMap₁₂ (fun x ↦ f x m) w :=
by
rw [fourierIntegral, ContinuousMultilinearMap.integral_apply]
· rfl
· apply (fourierIntegral_convergent_iff he _ _).2 hf
exact L.continuous₂
