fourierIntegralInv_eq' — Mathlib

English

The inverse Fourier transform of f is equal to the integral of the exponential against f, i.e., 𝓕⁻ f w = ∫ 𝐞^{⟪v,w⟫} f(v).

Русский

Обратное Фурье-представление f равно интегралу по экспоненте против f.

LaTeX

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

Lean4

theorem fourierIntegralInv_eq' (f : V → E) (w : V) :
    𝓕⁻ f w = ∫ v, Complex.exp ((↑(2 * π * ⟪v, w⟫) * Complex.I)) • f v := by
  simp_rw [fourierIntegralInv_eq, Circle.smul_def, Real.fourierChar_apply]

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