fourierIntegral_real_eq_integral_exp_smul

English

For real-valued f: ℝ → E, the forward transform equals ∫ℝ e^{−2π i v w} f(v) dv after matching the kernel.

Русский

Для вещественно-значной f: ℝ → E преобразование Фурье равно ∫ℝ e^{−2π i v w} f(v) dv.

LaTeX

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

Lean4

theorem fourierIntegral_real_eq_integral_exp_smul (f : ℝ → E) (w : ℝ) :
    𝓕 f w = ∫ v : ℝ, Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v := by
  simp_rw [fourierIntegral_real_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul, mul_assoc]

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