fourierIntegralInv_comm — Mathlib

English

The inverse Fourier transform commutes with linear isometries in a symmetric way: 𝓕⁻ (f ∘ A) w = (𝓕⁻ f)(A w).

Русский

Обратное Фурье-преобразование коммутирует с линейной изометрией: 𝓕⁻ (f ∘ A) w = (𝓕⁻ f)(A w).

LaTeX

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

Lean4

theorem fourierIntegralInv_comm (f : V → E) : 𝓕 (𝓕⁻ f) = 𝓕⁻ (𝓕 f) :=
  by
  conv_rhs => rw [fourierIntegralInv_eq_fourierIntegral_comp_neg]
  simp_rw [← fourierIntegralInv_eq_fourierIntegral_neg]

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