English
If f is integrable and decays suitably, then the Fourier-type integral tends to zero as the dual variable tends to infinity in cocompact fashion. This formalizes the standard RL lemma in a vector-valued setting.
Русский
Если f интегрируема и удовлетворяет распаду, то интеграл Фурье стремится к нулю при возрастании двойственного аргумента по кокомпактному направлению.
LaTeX
$$$\\lim_{\\|w\\|\\to\\infty} \\int_V e^{-⟨v,w⟩} f(v) dv = 0$ (in cocompact sense).$$
Lean4
/-- Riemann-Lebesgue lemma for functions on a real inner-product space: the integral
`∫ v, exp (-2 * π * ⟪w, v⟫ * I) • f v` tends to 0 as `w → ∞`. -/
theorem tendsto_integral_exp_inner_smul_cocompact : Tendsto (fun w : V => ∫ v, 𝐞 (-⟪v, w⟫) • f v) (cocompact V) (𝓝 0) :=
by
by_cases hfi : Integrable f; swap
· convert tendsto_const_nhds (x := (0 : E)) with w
apply integral_undef
rwa [Real.fourierIntegral_convergent_iff]
refine Metric.tendsto_nhds.mpr fun ε hε => ?_
obtain ⟨g, hg_supp, hfg, hg_cont, -⟩ := hfi.exists_hasCompactSupport_integral_sub_le (div_pos hε two_pos)
refine
((Metric.tendsto_nhds.mp (tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support hg_cont hg_supp))
_ (div_pos hε two_pos)).mp
(Eventually.of_forall fun w hI => ?_)
rw [dist_eq_norm] at hI ⊢
have : ‖(∫ v, 𝐞 (-⟪v, w⟫) • f v) - ∫ v, 𝐞 (-⟪v, w⟫) • g v‖ ≤ ε / 2 :=
by
refine le_trans ?_ hfg
simp_rw [←
integral_sub ((Real.fourierIntegral_convergent_iff w).2 hfi)
((Real.fourierIntegral_convergent_iff w).2 (hg_cont.integrable_of_hasCompactSupport hg_supp)),
← smul_sub, ← Pi.sub_apply]
exact VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 _ bilinFormOfRealInner (f - g) w
replace := add_lt_add_of_le_of_lt this hI
rw [add_halves] at this
refine ((le_of_eq ?_).trans (norm_add_le _ _)).trans_lt this
simp only [sub_zero, sub_add_cancel]
