fourierIntegralInv — Mathlib

English

The inverse Fourier transform is defined with the opposite sign in the exponent, i.e., 𝓕⁻ f w uses +⟪v,w⟫ inside the exponential.

Русский

Обратное Фурье-преобразование задаётся с обратным знаком в экспоненте: 𝓕⁻ f w действует с +⟪v,w⟫ внутри экспоненты.

LaTeX

$$$\\mathcal{F}^{-} f w = \\int_V 𝐞^{+⟨v,w⟩} \\cdot f(v) \\, d\\mu(v)$$$

Lean4

/-- The inverse Fourier transform of a function on an inner product space, defined as the Fourier
transform but with opposite sign in the exponential.
Denoted as `𝓕⁻¹` within the `Real.FourierTransform` namespace. -/
def fourierIntegralInv (f : V → E) (w : V) : E :=
  VectorFourier.fourierIntegral 𝐞 volume (-innerₗ V) f w

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