fourierIntegral_continuousMultilinearMap_apply'

English

Let f: V → ContinuousMultilinearMap ℝ M E be integrable. Then for each w ∈ W and m ∈ (i : ι) → M i, the Fourier integral of f at w and m equals the Fourier integral of the function x ↦ f(x) m at w.

Русский

Пусть f: V → ContinuousMultilinearMap ℝ M E интегрируема. Тогда для каждого w ∈ W и для каждого m: 𝓕 f w m = 𝓕 (x ↦ f(x) m) w.

LaTeX

$$$\\mathcal{F} f w m = \\mathcal{F}\\big(x \\mapsto f(x) m\\big) w$$$

Lean4

theorem fourierIntegral_continuousMultilinearMap_apply' {f : V → ContinuousMultilinearMap ℝ M E} {m : (i : ι) → M i}
    {w : W} (hf : Integrable f μ) :
    VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₁₂ f w m =
      VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun x ↦ f x m) w :=
  VectorFourier.fourierIntegral_continuousMultilinearMap_apply continuous_fourierChar hf

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