English
For a function f in an inner-product setting on a subspace, tendsto of the Fourier-type integral holds uniformly in the cocompact topology of the dual together with the inner-product pairing.
Русский
Для функции на подпространстве RL-лимит интеграла сохраняется по сопряжённой топологии двойственного пространства.
LaTeX
$$$\\text{tendsto } \\int_{V} e^{-⟨w,v⟩} f(v) dv = 0 \\quad (w\\to\\infty)$ in cocompact dual.$$
Lean4
/-- Riemann-Lebesgue lemma for functions on a finite-dimensional inner-product space, formulated
via dual space. **Do not use** -- it is only a stepping stone to
`tendsto_integral_exp_smul_cocompact` where the inner-product-space structure isn't required. -/
theorem tendsto_integral_exp_smul_cocompact_of_inner_product (μ : Measure V) [μ.IsAddHaarMeasure] :
Tendsto (fun w : StrongDual ℝ V => ∫ v, 𝐞 (-w v) • f v ∂μ) (cocompact (StrongDual ℝ V)) (𝓝 0) :=
by
rw [μ.isAddLeftInvariant_eq_smul volume]
simp_rw [integral_smul_nnreal_measure]
rw [← (smul_zero _ : Measure.addHaarScalarFactor μ volume • (0 : E) = 0)]
apply Tendsto.const_smul
let A := (InnerProductSpace.toDual ℝ V).symm
have : (fun w : StrongDual ℝ V ↦ ∫ v, 𝐞 (-w v) • f v) = (fun w : V ↦ ∫ v, 𝐞 (-⟪v, w⟫) • f v) ∘ A :=
by
ext1 w
congr 1 with v : 1
rw [← inner_conj_symm, RCLike.conj_to_real, InnerProductSpace.toDual_symm_apply]
rw [this]
exact (tendsto_integral_exp_inner_smul_cocompact f).comp A.toHomeomorph.toCocompactMap.cocompact_tendsto'
