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.

def MeasureTheory.IsTightMeasureSet {𝓧 : Type u_1} [TopologicalSpace 𝓧] {m𝓧 : MeasurableSpace 𝓧} (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} [TopologicalSpace 𝓧] {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} : 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ᶜ ≤ ε.

theorem MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRT {𝓧 : Type u_1} [TopologicalSpace 𝓧] {m𝓧 : MeasurableSpace 𝓧} {μ : Measure 𝓧} [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} [TopologicalSpace 𝓧] {m𝓧 : MeasurableSpace 𝓧} {μ : Measure 𝓧} [T2Space 𝓧] [OpensMeasurableSpace 𝓧] [IsFiniteMeasure μ] [h : μ.InnerRegular] : IsTightMeasureSet {μ}

Inner regular finite measures on T2 spaces are tight.

theorem MeasureTheory.isTightMeasureSet_singleton {α : Type u_3} {mα : MeasurableSpace α} [PseudoEMetricSpace α] [CompleteSpace α] [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} [TopologicalSpace 𝓧] {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} [CompactSpace 𝓧] : IsTightMeasureSet S

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

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

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

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

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