Tightness of a finite family of finite measures

Mathlib's MeasureTheory.isTightMeasureSet_singleton says that a single finite measure on a complete second-countable pseudo-metrizable space is tight, and IsTightMeasureSet.union says that tightness survives a binary union. Together they give tightness of any finite set of finite measures, which is the form the Prokhorov extraction arguments need in order to discard the finitely many exceptional members of a family for which a uniform tail bound is unavailable.

Main declarations

• TauCeti.isTightMeasureSet_of_finite: a finite set of finite measures is tight.
• TauCeti.isTightMeasureSet_range_of_finite: a family of finite measures indexed by a finite type has tight range.
• TauCeti.isTightMeasureSet_range_of_eventually_eq: a family of finite measures that is equal to a fixed measure off finitely many indices has tight range.

References

• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part B (Bernstein theorem milestone), "measure extraction via Prokhorov tightness".

theorem TauCeti.isTightMeasureSet_of_finite {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [SecondCountableTopology α] [BorelSpace α] {S : Set (MeasureTheory.Measure α)} (hS : S.Finite) (hfin : ∀ ν ∈ S, MeasureTheory.IsFiniteMeasure ν) : MeasureTheory.IsTightMeasureSet S

A finite set of finite measures is tight. Singletons are tight and tightness is closed under unions; the empty case routes through an arbitrary singleton, as Mathlib has no dedicated empty-set tightness lemma.

theorem TauCeti.isTightMeasureSet_range_of_finite {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [SecondCountableTopology α] [BorelSpace α] {ι : Type u_2} [Finite ι] (μ : ι → MeasureTheory.Measure α) [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] : MeasureTheory.IsTightMeasureSet (Set.range μ)

A family of finite measures indexed by a finite type has tight range.

theorem TauCeti.isTightMeasureSet_range_of_eventually_eq {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [SecondCountableTopology α] [BorelSpace α] {ι : Type u_2} {μ : ι → MeasureTheory.Measure α} [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] {ν : MeasureTheory.Measure α} (h : ∀ᶠ (i : ι) in Filter.cofinite, μ i = ν) : MeasureTheory.IsTightMeasureSet (Set.range μ)

Eventually constant families of finite measures are tight. A family of finite measures that equals a fixed measure ν off finitely many indices has finite range, so it is tight. No finiteness assumption on ν is needed: ν lies in the range only if it is one of the μ i.