English
A tendsto result for smoothed products with c^n weights and a fixed target g.
Русский
Сходимость с весами c^n в комбинации со сглаженными пиковыми функциями.
LaTeX
$$$\\text{tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn}$: convergence of ∫ (c^n) φ_n × g$$
Lean4
/-- If a continuous function `c` realizes its maximum at a unique point `x₀` in a compact set `s`,
then the sequence of functions `(c x) ^ n / ∫ (c x) ^ n` is a sequence of peak functions
concentrating around `x₀`. Therefore, `∫ (c x) ^ n * g / ∫ (c x) ^ n` converges to `g x₀` if `g` is
continuous on `s`. -/
theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn [MetrizableSpace α]
[IsLocallyFiniteMeasure μ] [IsOpenPosMeasure μ] (hs : IsCompact s) {c : α → ℝ} (hc : ContinuousOn c s)
(h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀) (hnc : ∀ x ∈ s, 0 ≤ c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ ∈ closure (interior s))
(hmg : ContinuousOn g s) :
Tendsto (fun n : ℕ => (∫ x in s, c x ^ n ∂μ)⁻¹ • ∫ x in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀)) :=
haveI : x₀ ∈ s := by rw [← hs.isClosed.closure_eq]; exact closure_mono interior_subset h₀
tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn hs hc h'c hnc hnc₀ h₀
(hmg.integrableOn_compact hs) (hmg x₀ this)
