fourierIntegral_eq — Mathlib

English

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

Русский

Для функции f: V → E fурье-преобразование в точке w равно интегралу по V от 𝐞^{−⟪v,w⟫} f(v).

LaTeX

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

Lean4

theorem fourierIntegral_eq (f : V → E) (w : V) : 𝓕 f w = ∫ v, 𝐞 (-⟪v, w⟫) • f v :=
  rfl

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