zero_at_infty_fourierIntegral — Mathlib

English

In a finite-dimensional setting, RL-type limit holds for Fourier-type integrals when expressed in terms of dual (strong dual) space, via an isomorphism with a real inner-product space.

Русский

В конечномерном случае лимит RL для интегралов Фурье выражается через двойственное пространство и изоморфизм с вещественным внутренним произведением.

LaTeX

$$$\\forall f, \\; \\mathrm{tendsto}_{{cocompact}} \\; \\int_V e^{-w(v)} f(v) dv = 0$.$$

Lean4

/-- The Riemann-Lebesgue lemma for functions on `ℝ`, formulated via `Real.fourierIntegral`. -/
theorem zero_at_infty_fourierIntegral (f : ℝ → E) : Tendsto (𝓕 f) (cocompact ℝ) (𝓝 0) :=
  tendsto_integral_exp_inner_smul_cocompact f

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