fourierIntegralInv_eq — Mathlib

English

Applying the inverse transform to f and then using negation is equivalent to applying inverse transform to f negated, i.e., 𝓕⁻ f = 𝓕⁻ (f ∘ (−I)).

Русский

Применение обратного преобразования к f и затем отрицание аргумента даёт то же, что и применение обратного преобразования к f, композиированному с −I.

LaTeX

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

Lean4

theorem fourierIntegralInv_eq (f : V → E) (w : V) : 𝓕⁻ f w = ∫ v, 𝐞 ⟪v, w⟫ • f v := by
  simp [fourierIntegralInv, VectorFourier.fourierIntegral]

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