English
A tendsto statement for powers with peak weights on a finite measure subset.
Русский
Сходимость степеней с весами пика на ограниченной мере подмножество.
LaTeX
$$$\\text{Tendsto}(n \\mapsto ∫ φ^n g)\\to a$ as n→∞ under peak normalization$$
Lean4
/-- If a sequence of peak functions `φᵢ` converges uniformly to zero away from a point `x₀` and its
integral on some finite-measure neighborhood of `x₀` converges to `1`, and `g` is integrable and
has a limit `a` at `x₀`, then `∫ φᵢ • g` converges to `a`. -/
theorem tendsto_integral_peak_smul_of_integrable_of_tendsto {t : Set α} (ht : MeasurableSet t) (h'ts : t ∈ 𝓝 x₀)
(h't : μ t ≠ ∞) (hnφ : ∀ᶠ i in l, ∀ x, 0 ≤ φ i x)
(hlφ : ∀ u : Set α, IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ)
(hiφ : Tendsto (fun i ↦ ∫ x in t, φ i x ∂μ) l (𝓝 1)) (h'iφ : ∀ᶠ i in l, AEStronglyMeasurable (φ i) μ)
(hmg : Integrable g μ) (hcg : Tendsto g (𝓝 x₀) (𝓝 a)) : Tendsto (fun i : ι ↦ ∫ x, φ i x • g x ∂μ) l (𝓝 a) :=
by
suffices Tendsto (fun i : ι ↦ ∫ x in univ, φ i x • g x ∂μ) l (𝓝 a) by simpa
exact
tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto MeasurableSet.univ ht (x₀ := x₀) (subset_univ _)
(by simpa [nhdsWithin_univ]) h't (by simpa) (by simpa [← compl_eq_univ_diff] using hlφ) hiφ (by simpa) (by simpa)
(by simpa [nhdsWithin_univ])
