Continuity sets, null-boundary thickenings and finite partitions

The portmanteau theorem makes the masses of a set converge along weak convergence as soon as the limit law does not charge the boundary of the set. Mathlib's exists_null_frontier_thickening supplies, for one set, thickening radii in any interval whose thickenings have null boundary. This file chooses a single radius that works simultaneously for countably many sets. It then uses this to cut a separable space into finitely many continuity sets of small diameter, apart from one set of arbitrarily small probability.

Weak convergence of finite measures also implies convergence of their masses on sets with null boundary, including when the limit measure is zero. This extends the probability-measure portmanteau API and is useful when localizing locally finite measures.

Main statements

• MeasureTheory.FiniteMeasure.tendsto_measure_of_null_frontier_of_tendsto — weak convergence of finite measures implies convergence on every continuity set of the limit measure.

• MeasureTheory.Measure.exists_forall_null_frontier_thickening — for countably many sets, some radius in any nonempty open interval gives thickenings whose boundaries are all null.

• MeasureTheory.Measure.exists_partition_null_frontier_small_last — a finite measure on a separable pseudometric space admits a finite measurable partition into null-boundary sets, all but the last lying in balls of a prescribed radius and the last having arbitrarily small measure.

theorem MeasureTheory.Measure.exists_forall_null_frontier_thickening {Ω : Type u_1} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ : Measure Ω) [SFinite μ] {ι : Type u_2} [Countable ι] (s : ι → Set Ω) {a b : ℝ} (hab : a < b) : ∃ r ∈ Set.Ioo a b, ∀ (k : ι), μ (frontier (Metric.thickening r (s k))) = 0

For countably many sets s k and an s-finite measure μ, some radius in any nonempty open interval gives thickenings whose boundaries are all μ-null: for each set only countably many radii fail, and a nonempty open interval of reals is uncountable.

theorem MeasureTheory.Measure.tendsto_measure_compl_biUnion_lt_ball {X : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (μ : Measure X) [IsFiniteMeasure μ] {u : ℕ → X} (hu : DenseRange u) {ρ : ℝ} (hρ0 : 0 < ρ) : Filter.Tendsto (fun (N : ℕ) => μ (⋃ (k : ℕ), ⋃ (_ : k < N), Metric.ball (u k) ρ)ᶜ) Filter.atTop (nhds 0)

For a dense sequence u and a radius ρ > 0, the complement of the union of the first N balls of radius ρ around the points u k has measure tending to 0 as N → ∞.

theorem MeasureTheory.Measure.exists_partition_null_frontier_small_last {X : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [TopologicalSpace.SeparableSpace X] (μ : Measure X) [IsFiniteMeasure μ] {r : ℝ} (hr : 0 < r) {ε : ENNReal} (hε : 0 < ε) : ∃ (N : ℕ) (A : Fin (N + 1) → Set X), (∀ (i : Fin (N + 1)), MeasurableSet (A i)) ∧ Pairwise (Function.onFun Disjoint A) ∧ ⋃ (i : Fin (N + 1)), A i = Set.univ ∧ (∀ (i : Fin (N + 1)), μ (frontier (A i)) = 0) ∧ (∀ (i : Fin (N + 1)), i ≠ Fin.last N → ∃ (x : X), A i ⊆ Metric.ball x r) ∧ μ (A (Fin.last N)) ≤ ε

A finite partition of X into pieces of μ-null boundary: all but the last piece lie in balls of radius r, and the last piece has μ-mass at most ε.

theorem MeasureTheory.FiniteMeasure.tendsto_measure_of_null_frontier_of_tendsto {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [HasOuterApproxClosed X] {l : Filter ι} {μs : ι → FiniteMeasure X} {μ : FiniteMeasure X} (h : Filter.Tendsto μs l (nhds μ)) {s : Set X} (hs : ↑μ (frontier s) = 0) : Filter.Tendsto (fun (i : ι) => ↑(μs i) s) l (nhds (↑μ s))

Weak convergence of finite measures gives convergence on every continuity set of the limit measure. No measurability assumption on the set is needed.