zero_at_infty_vector_fourierIntegral

English

The Riemann-Lebesgue lemma holds for vector-valued Fourier integrals: the integral of e^{-w·v} against f(v) tends to 0 as w → ∞ in the appropriate cocompact sense.

Русский

Лемма Римана-Лебега для векторного Фурье: интеграл e^{-w·v} f(v) dv стремится к 0 при w→∞.

LaTeX

$$$\\lim_{\\|w\\|\\to\\infty} \\int_V e^{-⟨w,v⟩} f(v) dv = 0$.$$

Lean4

/-- The Riemann-Lebesgue lemma, formulated in terms of `VectorFourier.fourierIntegral` (with the
pairing in the definition of `fourierIntegral` taken to be the canonical pairing between `V` and
its dual space). -/
theorem zero_at_infty_vector_fourierIntegral (μ : Measure V) [μ.IsAddHaarMeasure] :
    Tendsto (VectorFourier.fourierIntegral 𝐞 μ (topDualPairing ℝ V).flip f) (cocompact (StrongDual ℝ V)) (𝓝 0) :=
  _root_.tendsto_integral_exp_smul_cocompact f μ

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