fourierIntegralInv_eq_fourierIntegral_comp_neg

English

The Fourier transform of the inverse of f equals the Fourier transform of f composed with negation, i.e., 𝓕⁻ f = 𝓕 (f ∘ (− Id)).

Русский

Фурье-преобразование обратного f равно Фурье-преобразованию f после отрицания аргумента.

LaTeX

$$$\\mathcal{F}^{-} f = \\mathcal{F} (f \\circ (-\\mathrm{id}))$$$

Lean4

theorem fourierIntegralInv_eq_fourierIntegral_comp_neg (f : V → E) : 𝓕⁻ f = 𝓕 (fun x ↦ f (-x)) :=
  by
  ext y
  rw [fourierIntegralInv_eq_fourierIntegral_neg]
  change 𝓕 f (LinearIsometryEquiv.neg ℝ y) = 𝓕 (f ∘ LinearIsometryEquiv.neg ℝ) y
  exact (fourierIntegral_comp_linearIsometry _ _ _).symm

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