Theorems · Theorem · measure theory

isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le

Deprecated since 2026-07-09Use isCompact_setOfPred_finiteMeasure_mass_eq_compl_isCompact_le instead.

• 1000+ list: Prokhorov's theorem

∀ {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}

Alias of isCompact_setOfPred_finiteMeasure_mass_eq_compl_isCompact_le. 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.

Defined in

Mathlib.MeasureTheory.Measure.Prokhorov

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceT2SpaceBorelSpace