fourierIntegral_real_eq — Mathlib

English

On the real line, the Fourier transform takes the form 𝓕 f(w) = ∫ℝ e^{− i 2π v w} f(v) dv, i.e., with the standard one-dimensional kernel.

Русский

На линии Реальных Фурье-преобразование имеет вид 𝓕 f(w) = ∫ℝ e^{− i 2π v w} f(v) dv.

LaTeX

$$$\\mathcal{F} f w = \\int_{\\mathbb{R}} e^{-{2\\pi i v w}} f(v) \\, dv$$$

Lean4

theorem fourierIntegral_real_eq (f : ℝ → E) (w : ℝ) : fourierIntegral f w = ∫ v : ℝ, 𝐞 (-(v * w)) • f v :=
  by
  simp_rw [mul_comm _ w]
  rfl

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