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.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)