English
Riemann-Lebesgue holds in multiple variants: for inner-product spaces, duals, and vector-valued mappings under suitable decay and integrability hypotheses.
Русский
Лемма Римана-Лебега сохраняется в нескольких формах: для пространств с непрерывным скалярным произведением, двойственных пространств и векторнозначных функций под подходящими условиями распада и интегрируемости.
LaTeX
$$$\\text{tendsto } (w\\mapsto \\int e^{-⟨v,w⟩} f(v) dv) \\; \\text{to } 0 \\text{ as } w\\to\\infty.$$$
Lean4
/-- Riemann-Lebesgue lemma for functions on a finite-dimensional real vector space, formulated via
dual space. -/
theorem tendsto_integral_exp_smul_cocompact (μ : Measure V) [μ.IsAddHaarMeasure] :
Tendsto (fun w : StrongDual ℝ V => ∫ v, 𝐞 (-w v) • f v ∂μ) (cocompact (StrongDual ℝ V)) (𝓝 0) := by
-- We have already proved the result for inner-product spaces, formulated in a way which doesn't
-- refer to the inner product. So we choose an arbitrary inner-product space isomorphic to V
-- and port the result over from there.
let V' := EuclideanSpace ℝ (Fin (finrank ℝ V))
have A : V ≃L[ℝ] V' := toEuclidean
borelize V'
let Aₘ : MeasurableEquiv V V' := A.toHomeomorph.toMeasurableEquiv
let Adual : StrongDual ℝ V ≃L[ℝ] StrongDual ℝ V' := A.arrowCongrSL (.refl _ _)
have : (μ.map Aₘ).IsAddHaarMeasure := A.isAddHaarMeasure_map _
convert
(tendsto_integral_exp_smul_cocompact_of_inner_product (f ∘ A.symm) (μ.map Aₘ)).comp
Adual.toHomeomorph.toCocompactMap.cocompact_tendsto' with
w
suffices ∫ v, 𝐞 (-w v) • f v ∂μ = ∫ (x : V), 𝐞 (-w (A.symm (Aₘ x))) • f (A.symm (Aₘ x)) ∂μ by
simpa [Function.comp_apply, integral_map_equiv, Adual]
simp [Aₘ]
