fourierIntegral_comp_linearIsometry

English

For an isometry A: W ≃ᵢ V, the Fourier transform of f ∘ A equals the Fourier transform of f evaluated at Aw.

Русский

Для линейной изометрии A: W ≃ᵢ V выполнено 𝓕 (f ∘ A) w = 𝓕 f (A w).

LaTeX

$$$\\mathcal{F} (f \\circ A) w = (\\mathcal{F} f)(A w)$$$

Lean4

theorem fourierIntegral_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) : 𝓕 (f ∘ A) w = (𝓕 f) (A w) := by
  simp only [fourierIntegral_eq, ← A.inner_map_map, Function.comp_apply,
    ← MeasurePreserving.integral_comp A.measurePreserving A.toHomeomorph.measurableEmbedding]

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