fourierIntegral_continuousMultilinearMap_apply

English

Let f: V → ContinuousMultilinearMap ℝ M E be integrable; then 𝓕 f v m = 𝓕 (x ↦ f x m) v for all v and m.

Русский

Пусть f: V → ContinuousMultilinearMap ℝ M E интегрируема; тогда 𝓕 f v m = 𝓕 (x ↦ f x m) v для всех v,m.

LaTeX

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

Lean4

theorem fourierIntegral_continuousMultilinearMap_apply {ι : Type*} [Fintype ι] {M : ι → Type*}
    [∀ i, NormedAddCommGroup (M i)] [∀ i, NormedSpace ℝ (M i)] {f : V → ContinuousMultilinearMap ℝ M E}
    {m : (i : ι) → M i} {v : V} (hf : Integrable f) : 𝓕 f v m = 𝓕 (fun x ↦ f x m) v :=
  fourierIntegral_continuousMultilinearMap_apply' (L := innerSL ℝ) hf

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