fourierIntegral_continuousLinearMap_apply

English

For a family of vector-valued functions taking values in a multilinear space, the Fourier transform is continuous as a map from the parameter to the transform value, provided integrability holds.

Русский

Для набора функциях с многолинейной структурой преобразование Фурье непрерывно как отображение параметра в значение преобразования, при условии интегрируемости.

LaTeX

$$$$ \\text{continuous}(w) : w \\mapsto \\mathrm{fourierIntegral}(e,\\mu,L,f)(w) \\text{ is continuous}. $$$$

Lean4

theorem fourierIntegral_continuousLinearMap_apply {f : V → (F →L[ℝ] E)} {a : F} {w : W} (he : Continuous e)
    (hf : Integrable f μ) :
    fourierIntegral e μ L.toLinearMap₁₂ f w a = fourierIntegral e μ L.toLinearMap₁₂ (fun x ↦ f x a) w :=
  by
  rw [fourierIntegral, ContinuousLinearMap.integral_apply]
  · rfl
  · apply (fourierIntegral_convergent_iff he _ _).2 hf
    exact L.continuous₂

Похожие утверждения