Convergence of nonnegative weights with mass one #
Scheffé's argument uses dominated convergence for the minimum of the two weights. Convergence in measure is reduced to almost everywhere convergence on subsequences.
Reference: J.-F. Le Gall, Random trees and applications, Probab. Surveys 2 (2005), Section 1.
theorem
BGW.StableTrees.tendsto_integral_abs_sub_of_massOne
{Ω : Type u_1}
[MeasurableSpace Ω]
{P : MeasureTheory.Measure Ω}
{w : ℕ → Ω → ℝ}
{w₀ : Ω → ℝ}
(hw : ∀ (k : ℕ), Measurable (w k))
(hw₀ : Measurable w₀)
(hnn : ∀ (k : ℕ) (ω : Ω), 0 ≤ w k ω)
(hnn₀ : ∀ (ω : Ω), 0 ≤ w₀ ω)
(h1 : ∀ (k : ℕ), ∫ (ω : Ω), w k ω ∂P = 1)
(h10 : ∫ (ω : Ω), w₀ ω ∂P = 1)
(hconv : MeasureTheory.TendstoInMeasure P w Filter.atTop w₀)
:
Filter.Tendsto (fun (k : ℕ) => ∫ (ω : Ω), |w k ω - w₀ ω| ∂P) Filter.atTop (nhds 0)
Scheffé for nonnegative mass-one weights (generic helper). If w_k ≥ 0,
w ≥ 0, all with integral one and w_k → w in measure, then w_k → w in L¹.
theorem
BGW.StableTrees.tendsto_integral_mul_of_massOne
{Ω : Type u_1}
[MeasurableSpace Ω]
{P : MeasureTheory.Measure Ω}
{w : ℕ → Ω → ℝ}
{w₀ : Ω → ℝ}
(hw : ∀ (k : ℕ), Measurable (w k))
(hw₀ : Measurable w₀)
(hnn : ∀ (k : ℕ) (ω : Ω), 0 ≤ w k ω)
(hnn₀ : ∀ (ω : Ω), 0 ≤ w₀ ω)
(h1 : ∀ (k : ℕ), ∫ (ω : Ω), w k ω ∂P = 1)
(h10 : ∫ (ω : Ω), w₀ ω ∂P = 1)
(hconv : MeasureTheory.TendstoInMeasure P w Filter.atTop w₀)
{F : ℕ → Ω → ℝ}
{F₀ : Ω → ℝ}
{C : ℝ}
(hF : ∀ (k : ℕ), Measurable (F k))
(hF₀ : Measurable F₀)
(hC : ∀ (k : ℕ) (ω : Ω), |F k ω| ≤ C)
(hC₀ : ∀ (ω : Ω), |F₀ ω| ≤ C)
(hFc : MeasureTheory.TendstoInMeasure P F Filter.atTop F₀)
:
Weighted convergence (consequence): uniformly bounded measurable F_k → F in measure
and weights as above give ∫ F_k w_k → ∫ F w₀.