fourierIntegralInv_comp_linearIsometry

English

For an isometry A: W ≃ᵢ V, 𝓕⁻ (f ∘ A) w = (𝓕⁻ f)(A w).

Русский

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

LaTeX

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

Lean4

theorem fourierIntegralInv_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) : 𝓕⁻ (f ∘ A) w = (𝓕⁻ f) (A w) := by
  simp [fourierIntegralInv_eq_fourierIntegral_neg, fourierIntegral_comp_linearIsometry]

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