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.
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 ν)
:
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 α)
(hfin : ∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i))
:
A family of finite measures indexed by a finite type has tight range.