tendsto_measure_of_null_frontier_of_tendsto

English

There exists a sequence rs with rs(n) > 0, rs(n) → 0, and frontier(thickening(rs(n), E)) has measure zero for all n.

Русский

Существует последовательность rs(n) > 0, rs(n) → 0, и для каждого n фронтир толщины rs(n) множества E имеет меру ноль.

LaTeX

$$$\exists rs:\mathbb{N}\to\mathbb{R},\ Tendsto rs\to 0,\forall n\; 0

Lean4

/-- One implication of the portmanteau theorem:
Weak convergence of probability measures implies that if the boundary of a Borel set
carries no probability mass under the limit measure, then the limit of the measures of the set
equals the measure of the set under the limit probability measure.

A version with coercions to ordinary `ℝ≥0∞`-valued measures is
`MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto'`.
-/
theorem tendsto_measure_of_null_frontier_of_tendsto {Ω ι : Type*} {L : Filter ι} [MeasurableSpace Ω]
    [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : ProbabilityMeasure Ω}
    {μs : ι → ProbabilityMeasure Ω} (μs_lim : Tendsto μs L (𝓝 μ)) {E : Set Ω} (E_nullbdry : μ (frontier E) = 0) :
    Tendsto (fun i ↦ μs i E) L (𝓝 (μ E)) :=
  by
  have key := tendsto_measure_of_null_frontier_of_tendsto' μs_lim (by simpa using E_nullbdry)
  exact (ENNReal.tendsto_toNNReal (measure_ne_top (↑μ) E)).comp key

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