English
Convergence of weighted integrals with a peak at a unique maximum point of the weight function.
Русский
Сходимость взвешенного интеграла с пиком в единственной максимальной точке весовой функции.
LaTeX
$$$\\text{tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn}$$$
Lean4
/-- Consider a nonnegative function `φ` with integral one, decaying quickly enough at infinity.
Then suitable renormalizations of `φ` form a sequence of peak functions around any point:
`∫ (c ^ d * φ (c • (x₀ - x)) • g x` converges to `g x₀` as `c → ∞` if `g` is continuous at `x₀`
and integrable. -/
theorem tendsto_integral_comp_smul_smul_of_integrable' {φ : F → ℝ} (hφ : ∀ x, 0 ≤ φ x) (h'φ : ∫ x, φ x ∂μ = 1)
(h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)) {g : F → E} {x₀ : F} (hg : Integrable g μ)
(h'g : ContinuousAt g x₀) :
Tendsto (fun (c : ℝ) ↦ ∫ x, (c ^ (finrank ℝ F) * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀)) :=
by
let f := fun x ↦ g (x₀ - x)
have If : Integrable f μ := by simpa [f, sub_eq_add_neg] using (hg.comp_add_left x₀).comp_neg
have : Tendsto (fun (c : ℝ) ↦ ∫ x, (c ^ (finrank ℝ F) * φ (c • x)) • f x ∂μ) atTop (𝓝 (f 0)) :=
by
apply tendsto_integral_comp_smul_smul_of_integrable hφ h'φ h If
have A : ContinuousAt g (x₀ - 0) := by simpa using h'g
exact A.comp <| by fun_prop
simp only [f, sub_zero] at this
convert this using 2 with c
conv_rhs =>
rw [← integral_add_left_eq_self x₀ (μ := μ) (f := fun x ↦ (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x)), ←
integral_neg_eq_self]
simp [sub_eq_add_neg]
