vector_fourierIntegral_eq_integral_exp_smul

English

Under mild regularity, the Fourier integral with complex-valued outputs is continuous in frequency.

Русский

При умеренной регулярности преобразование Фурье с комплексными значениями непрерывно по частоте.

LaTeX

$$$$ \\text{Continuous}(w \\mapsto \\mathrm{fourierIntegral}(e, μ, L, f)(w)). $$$$

Lean4

theorem vector_fourierIntegral_eq_integral_exp_smul {V : Type*} [AddCommGroup V] [Module ℝ V] [MeasurableSpace V]
    {W : Type*} [AddCommGroup W] [Module ℝ W] (L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ) (μ : Measure V) (f : V → E) (w : W) :
    VectorFourier.fourierIntegral fourierChar μ L f w = ∫ v : V, Complex.exp (↑(-2 * π * L v w) * Complex.I) • f v ∂μ :=
  by simp_rw [VectorFourier.fourierIntegral, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul]

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