fourierIntegral — Mathlib

English

The Fourier transform of a function f: V → E at w is the integral of the exponential character against f, i.e., 𝓕 f w = ∫_V 𝐞^{−⟪v,w⟫} · f(v) dμ(v).

Русский

Фурье-преобразование функции f: V → E в точке w равно интегралу по V экспоненциального характера: 𝓕 f w = ∫ 𝐞^{−⟪v,w⟫} · f(v) dμ(v).

LaTeX

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

Lean4

/-- The Fourier transform of a function on an inner product space, with respect to the standard
additive character `ω ↦ exp (2 i π ω)`.
Denoted as `𝓕` within the `Real.FourierTransform` namespace. -/
def fourierIntegral (f : V → E) (w : V) : E :=
  VectorFourier.fourierIntegral 𝐞 volume (innerₗ V) f w

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