Prokhorov theorem

We prove statements about the compactness of sets of finite measures or probability measures, notably several versions of Prokhorov theorem on tight sets of probability measures.

Main statements

• instCompactSpaceProbabilityMeasure proves that the space of probability measures on a compact space is itself compact
• isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le: Given a sequence of compact sets Kₙ and a sequence uₙ tending to zero, the probability measures giving mass at most uₙ to the complement of Kₙ form a compact set.
• isCompact_closure_of_isTightMeasureSet: Given a tight set of probability measures, its closure is compact.

Versions are also given for finite measures.

Implementation

We do not assume second-countability or metrizability.

For the compactness of the space of probability measures in a compact space, we argue that every ultrafilter converges, using the Riesz-Markov-Kakutani theorem to construct the limiting measure in terms of its integrals against continuous functions.

For Prokhorov theorem isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le, we rely on the compactness of the space of measures inside each compact set to get convergence of the restriction there, and argue that the full measure converges to the sum of the individual limits of the disjointed components. There is a subtlety that the space of finite measures giving mass uₙ to Kₙᶜ doesn't have to be closed in our general setting, but we only need to find a limit satisfying this condition. To ensure this, we need a technical condition (monotonicity of K or normality of the space). In the first case, the bound follows readily from the construction. In the second case, we modify the individual limits (again using Riesz-Markov-Kakutani) to make sure that they are inner-regular, and then one can check the condition.

theorem isCompact_setOf_finiteMeasure_le_of_compactSpace (E : Type u_1) [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] [CompactSpace E] (C : NNReal) : IsCompact {μ : MeasureTheory.FiniteMeasure E | μ.mass ≤ C}

In a compact space, the set of finite measures with mass at most C is compact.

theorem isCompact_setOf_finiteMeasure_eq_of_compactSpace (E : Type u_1) [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] [CompactSpace E] (C : NNReal) : IsCompact {μ : MeasureTheory.FiniteMeasure E | μ.mass = C}

In a compact space, the set of finite measures with mass C is compact.

instance instCompactSpaceProbabilityMeasure {E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] [CompactSpace E] : CompactSpace (MeasureTheory.ProbabilityMeasure E)

In a compact space, the space of probability measures is also compact.

theorem isCompact_setOf_finiteMeasure_le_of_isCompact {E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] (C : NNReal) {K : Set E} (hK : IsCompact K) : IsCompact {μ : MeasureTheory.FiniteMeasure E | μ.mass ≤ C ∧ μ Kᶜ = 0}

The set of finite measures of mass at most C supported on a given compact set K is compact.

theorem isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le {E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {u : ℕ → NNReal} {K : ℕ → Set E} (C : NNReal) (hu : Filter.Tendsto u Filter.atTop (nhds 0)) (hK : ∀ (n : ℕ), IsCompact (K n)) (h : NormalSpace E ∨ Monotone K) : IsCompact {μ : MeasureTheory.FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}

Prokhorov theorem: Given a sequence of compact sets Kₙ and a sequence uₙ tending to zero, the finite measures of mass at most C giving mass at most uₙ to the complement of Kₙ form a compact set.

theorem isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le {E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {u : ℕ → NNReal} {K : ℕ → Set E} (C : NNReal) (hu : Filter.Tendsto u Filter.atTop (nhds 0)) (hK : ∀ (n : ℕ), IsCompact (K n)) (h : NormalSpace E ∨ Monotone K) : IsCompact {μ : MeasureTheory.FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}

Prokhorov theorem: Given a sequence of compact sets Kₙ and a sequence uₙ tending to zero, the finite measures of mass C giving mass at most uₙ to the complement of Kₙ form a compact set.

theorem isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le {E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {u : ℕ → NNReal} {K : ℕ → Set E} (hu : Filter.Tendsto u Filter.atTop (nhds 0)) (hK : ∀ (n : ℕ), IsCompact (K n)) (h : NormalSpace E ∨ Monotone K) : IsCompact {μ : MeasureTheory.ProbabilityMeasure E | ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}

Prokhorov theorem: Given a sequence of compact sets Kₙ and a sequence uₙ tending to zero, the probability measures giving mass at most uₙ to the complement of Kₙ form a compact set.

theorem isCompact_closure_of_isTightMeasureSet {E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {S : Set (MeasureTheory.ProbabilityMeasure E)} (hS : MeasureTheory.IsTightMeasureSet {x : MeasureTheory.Measure E | ∃ μ ∈ S, ↑μ = x}) : IsCompact (closure S)

Prokhorov theorem: the closure of a tight set of probability measures is compact. We only require the space to be T2.