fourierIntegral_continuousLinearMap_apply'

English

Let f: V → (F →L[ℝ] E) be integrable. Then for every w ∈ W and every a ∈ F, the Fourier transform of f at w evaluated at a equals the Fourier transform of the function x ↦ f(x)(a) at w.

Русский

Пусть f: V → (F →L[ℝ] E) интегрируема. Тогда для любых w ∈ W и a ∈ F верно: 𝓕 f w a = 𝓕 (x ↦ f(x) a) w.

LaTeX

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

Lean4

theorem fourierIntegral_continuousLinearMap_apply' {f : V → (F →L[ℝ] E)} {a : F} {w : W} (hf : Integrable f μ) :
    VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₁₂ f w a =
      VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun x ↦ f x a) w :=
  VectorFourier.fourierIntegral_continuousLinearMap_apply continuous_fourierChar hf

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