tendsto_integral_exp_smul_cocompact

English

For a function f: V → E on a finite-dimensional real inner-product space, the integral of exp(-⟨w,v⟩) f(v) against the Haar measure tends to 0 as w goes to infinity in the dual space.

Русский

Для функции f на конечномерном внутреннем произведении интеграл exp(-⟨w,v⟩) f(v) по Гааровской мере стремится к нулю при ||w||→∞.

LaTeX

$$$\\lim_{\\|w\\|\\to\\infty} \\int_V e^{-\\langle w,v\\rangle} f(v) dv = 0$ in cocompact dual space.$$

Lean4

/-- The Riemann-Lebesgue lemma for functions on `ℝ`. -/
theorem tendsto_integral_exp_smul_cocompact (f : ℝ → E) :
    Tendsto (fun w : ℝ => ∫ v : ℝ, 𝐞 (-(v * w)) • f v) (cocompact ℝ) (𝓝 0) :=
  by
  simp_rw [mul_comm]
  exact tendsto_integral_exp_inner_smul_cocompact f

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