tendsto_measure_iUnion_accumulate

English

Continuity from below: for any f : ι → Set Ω, μ(Accumulate f i) tends to μ(⋃ i, f i) as i → atTop.

Русский

Непрерывность снизу: μ(Accumulate f i) сходится к μ(⋃ i, f i) при i → atTop.

LaTeX

$$Tendsto (i ↦ μ(Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))$$

Lean4

/-- Continuity from below: the measure of the union of a sequence of (not necessarily measurable)
sets is the limit of the measures of the partial unions. -/
protected theorem tendsto_measure_iUnion_accumulate {ι : Type*} [Preorder ι] [IsCountablyGenerated (atTop : Filter ι)]
    {μ : ProbabilityMeasure Ω} {f : ι → Set Ω} : Tendsto (fun i ↦ μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i))) := by
  simpa [← ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.tendsto_coe] using
    tendsto_measure_iUnion_accumulate (μ := μ.toMeasure)

Похожие утверждения