Tight sets of measures

A set of measures is tight if for all 0 < ε, there exists a compact set K such that for all measures in the set, the complement of K has measure at most ε.

Main definitions

• MeasureTheory.IsTightMeasureSet: A set of measures S is tight if for all 0 < ε, there exists a compact set K such that for all μ ∈ S, μ Kᶜ ≤ ε. The definition uses an equivalent formulation with filters: ⨆ μ ∈ S, μ tends to 0 along the filter of cocompact sets. isTightMeasureSet_iff_exists_isCompact_measure_compl_le establishes equivalence between the two definitions.

Main statements

• isTightMeasureSet_singleton_of_innerRegularWRT: every finite, inner-regular measure is tight.
• isTightMeasureSet_of_isCompact_closure: every relatively compact set of measures is tight.

def MeasureTheory.IsTightMeasureSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} [TopologicalSpace 𝓧] (S : Set (Measure 𝓧)) : Prop

A set of measures S is tight if for all 0 < ε, there exists a compact set K such that for all μ ∈ S, μ Kᶜ ≤ ε. This is formulated in terms of filters, and proven equivalent to the definition above in IsTightMeasureSet_iff_exists_isCompact_measure_compl_le.

Equations

• MeasureTheory.IsTightMeasureSet S = Filter.Tendsto (⨆ μ ∈ S, ⇑μ) (Filter.cocompact 𝓧).smallSets (nhds 0)

theorem MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} [TopologicalSpace 𝓧] : IsTightMeasureSet S ↔ ∀ (ε : ENNReal), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε

A set of measures S is tight if for all 0 < ε, there exists a compact set K such that for all μ ∈ S, μ Kᶜ ≤ ε.

@[deprecated MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le (since := "2025-12-13")]

theorem MeasureTheory.IsTightMeasureSet_iff_exists_isCompact_measure_compl_le {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} [TopologicalSpace 𝓧] : IsTightMeasureSet S ↔ ∀ (ε : ENNReal), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε

Alias of MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le.

---

A set of measures S is tight if for all 0 < ε, there exists a compact set K such that for all μ ∈ S, μ Kᶜ ≤ ε.

theorem MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRT {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : Measure 𝓧} [TopologicalSpace 𝓧] [OpensMeasurableSpace 𝓧] [IsFiniteMeasure μ] (h : μ.InnerRegularWRT (fun (s : Set 𝓧) => IsCompact s ∧ IsClosed s) MeasurableSet) : IsTightMeasureSet {μ}

Finite measures that are inner regular with respect to closed compact sets are tight.

theorem MeasureTheory.isTightMeasureSet_singleton_of_innerRegular {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : Measure 𝓧} [TopologicalSpace 𝓧] [T2Space 𝓧] [OpensMeasurableSpace 𝓧] [IsFiniteMeasure μ] [h : μ.InnerRegular] : IsTightMeasureSet {μ}

Inner regular finite measures on T2 spaces are tight.

theorem MeasureTheory.isTightMeasureSet_singleton {α : Type u_3} [MeasurableSpace α] [TopologicalSpace α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [SecondCountableTopology α] [BorelSpace α] {μ : Measure α} [IsFiniteMeasure μ] : IsTightMeasureSet {μ}

In a complete second-countable pseudo-metric space, finite measures are tight.

theorem MeasureTheory.IsTightMeasureSet.of_compactSpace {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} [TopologicalSpace 𝓧] [CompactSpace 𝓧] : IsTightMeasureSet S

In a compact space, every set of measures is tight.

theorem MeasureTheory.IsTightMeasureSet.subset {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S T : Set (Measure 𝓧)} [TopologicalSpace 𝓧] (hT : IsTightMeasureSet T) (hST : S ⊆ T) : IsTightMeasureSet S

theorem MeasureTheory.IsTightMeasureSet.union {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S T : Set (Measure 𝓧)} [TopologicalSpace 𝓧] (hS : IsTightMeasureSet S) (hT : IsTightMeasureSet T) : IsTightMeasureSet (S ∪ T)

theorem MeasureTheory.IsTightMeasureSet.inter {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} [TopologicalSpace 𝓧] (hS : IsTightMeasureSet S) (T : Set (Measure 𝓧)) : IsTightMeasureSet (S ∩ T)

theorem MeasureTheory.IsTightMeasureSet.map {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} [TopologicalSpace 𝓧] [TopologicalSpace 𝓨] [MeasurableSpace 𝓨] [OpensMeasurableSpace 𝓨] [T2Space 𝓨] (hS : IsTightMeasureSet S) {f : 𝓧 → 𝓨} (hf : Continuous f) : IsTightMeasureSet (Measure.map f '' S)

theorem MeasureTheory.exists_measure_iUnion_gt_of_isCompact_closure {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} [PseudoMetricSpace 𝓧] [OpensMeasurableSpace 𝓧] [SecondCountableTopology 𝓧] {S : Set (ProbabilityMeasure 𝓧)} (U : ℕ → Set 𝓧) (O : ∀ (i : ℕ), IsOpen (U i)) (Cov : ⋃ (i : ℕ), U i = Set.univ) (hcomp : IsCompact (closure S)) (ε : ENNReal) (hε : 0 < ε) (hεbound : ε ≤ 1) : ∃ (k : ℕ), ∀ μ ∈ S, 1 - ε < ↑(μ (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i))

theorem MeasureTheory.isTightMeasureSet_of_isCompact_closure {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} [PseudoMetricSpace 𝓧] [OpensMeasurableSpace 𝓧] [SecondCountableTopology 𝓧] {S : Set (ProbabilityMeasure 𝓧)} [CompleteSpace 𝓧] (hcomp : IsCompact (closure S)) : IsTightMeasureSet {x : Measure 𝓧 | ∃ μ ∈ S, ↑μ = x}

In a second countable complete metric space, a set of probability measures with compact closure is tight.