Prokhorov compactness lemmas for sequences of measures

This file contains generic consequences of Mathlib's Prokhorov compactness theorem. For finite measures, tightness and a uniform mass bound give a weak cluster limit without a real-line support condition or normalization step. For probability measures on a Polish space, a weakly convergent sequence is tight.

Main declarations

• TauCeti.finite_measure_cluster_limit: a tight, mass-bounded sequence of finite measures has a weak cluster limit along an ultrafilter below atTop.
• TauCeti.finite_measure_subseq_limit: the corresponding subsequence form when the weak topology on FiniteMeasure α is first-countable.
• TauCeti.isTightMeasureSet_range_of_tendsto: a weakly convergent sequence of probability measures on a Polish space is tight.

References

• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part B (Bernstein theorem milestone).
• Roadmap: TauCetiRoadmap/OptimalTransport/README.md, Layer 1, item 6 (stability).

theorem TauCeti.finite_measure_cluster_limit {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [T2Space α] [BorelSpace α] (σ : ℕ → MeasureTheory.Measure α) (C : NNReal) (hmass : ∀ (n : ℕ), (σ n) Set.univ ≤ ↑C) (hTight : MeasureTheory.IsTightMeasureSet (Set.range σ)) : ∃ (μ₀ : MeasureTheory.Measure α) (U : Ultrafilter ℕ), ↑U ≤ Filter.atTop ∧ MeasureTheory.IsFiniteMeasure μ₀ ∧ μ₀ Set.univ ≤ ↑C ∧ ∀ (g : BoundedContinuousFunction α ℝ), Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), g x ∂σ n) (↑U) (nhds (∫ (x : α), g x ∂μ₀))

A tight, uniformly mass-bounded sequence of finite measures has a weak cluster limit.

Given tightness of the sequence and a common total-mass bound, the conclusion is a finite limiting measure with the same mass bound and weak convergence of all bounded-continuous test-function integrals along an ultrafilter U ≤ atTop; no first-countability assumption on FiniteMeasure α is needed.

theorem TauCeti.finite_measure_subseq_limit {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [T2Space α] [BorelSpace α] [FirstCountableTopology (MeasureTheory.FiniteMeasure α)] (σ : ℕ → MeasureTheory.Measure α) (C : NNReal) (hmass : ∀ (n : ℕ), (σ n) Set.univ ≤ ↑C) (hTight : MeasureTheory.IsTightMeasureSet (Set.range σ)) : ∃ (μ₀ : MeasureTheory.Measure α) (φ : ℕ → ℕ), MeasureTheory.IsFiniteMeasure μ₀ ∧ StrictMono φ ∧ μ₀ Set.univ ≤ ↑C ∧ ∀ (g : BoundedContinuousFunction α ℝ), Filter.Tendsto (fun (k : ℕ) => ∫ (x : α), g x ∂σ (φ k)) Filter.atTop (nhds (∫ (x : α), g x ∂μ₀))

Sequential form of finite_measure_cluster_limit when FiniteMeasure α is first-countable.

theorem TauCeti.isTightMeasureSet_range_of_tendsto {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [BorelSpace α] [PolishSpace α] {μs : ℕ → MeasureTheory.ProbabilityMeasure α} {μ : MeasureTheory.ProbabilityMeasure α} (hμ : Filter.Tendsto μs Filter.atTop (nhds μ)) : MeasureTheory.IsTightMeasureSet (Set.range fun (n : ℕ) => ↑(μs n))

A weakly convergent sequence of probability measures on a Polish space is tight.