Theorems · Theorem · measure theory

isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_le

∀ {E : Type u_1} [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  {u : ℕ → NNReal} {K : ℕ → Set E} (C : NNReal),
  Filter.Tendsto u Filter.atTop (nhds 0) →
    (∀ (n : ℕ), IsCompact (K n)) → NormalSpace E ∨ Monotone K → IsCompact {μ | μ.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.

Defined in

Mathlib.MeasureTheory.Measure.Prokhorov

Cited by

2 results in Mathlib

Foundations

Depth 264 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceT2SpaceBorelSpace