fourierIntegral — Mathlib

English

The Fourier integral is defined by integrating the input function against the additive character with a bilinear form in the exponent, i.e., a standard integral representation.

Русский

Преобразование Фурье задается как интеграл от функции по аддитивному характеру с билинейной формой в показателе степени, т.е. стандартная интегральная запись.

LaTeX

$$$$ \\mathrm{fourierIntegral}(e, \\mu, f, w) = \\int v \\in V \\; e(-L(v,w)) \\cdot f(v) \\, d\\mu(v). $$$$

Lean4

/-- The Fourier transform integral for `f : 𝕜 → E`, with respect to the measure `μ` and additive
character `e`. -/
def fourierIntegral (e : AddChar 𝕜 𝕊) (μ : Measure 𝕜) (f : 𝕜 → E) (w : 𝕜) : E :=
  VectorFourier.fourierIntegral e μ (LinearMap.mul 𝕜 𝕜) f w

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