def MeasureTheory.Measure.IsTightFamily {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {ι : Type u_2} (μ : ι → Measure α) [∀ (i : ι), IsProbabilityMeasure (μ i)] : Prop

A family of probability measures μ : ι → Measure α is tight if for every ε > 0 there exists a compact set K such that μ i K ≥ 1 - ε for every index i.

def MeasureTheory.Measure.IsTightFamilyReal {ι : Type u_1} (μ : ι → Measure ℝ) [∀ (i : ι), IsProbabilityMeasure (μ i)] : Prop

A family of probability measures on ℝ is tight if for every ε > 0 there exists M > 0 such that μ i [-M, M] ≥ 1 - ε for every index i. This is the textbook definition specialised to the real line.

theorem MeasureTheory.Measure.IsTightFamilyReal.isTightFamily {ι : Type u_1} {μ : ι → Measure ℝ} [∀ (i : ι), IsProbabilityMeasure (μ i)] (h : IsTightFamilyReal μ) : IsTightFamily μ

Tightness in the real-line sense ([-M, M] exhausts mass uniformly) implies tightness in the general topological sense (a compact set exhausts mass uniformly), since [-M, M] is compact.

theorem MeasureTheory.Measure.IsTightFamily.isTightFamilyReal {ι : Type u_1} {μ : ι → Measure ℝ} [∀ (i : ι), IsProbabilityMeasure (μ i)] (h : IsTightFamily μ) : IsTightFamilyReal μ

Converse direction: tightness in the general topological sense for measures on ℝ implies the real-line [-M, M] formulation, by enclosing the compact set in a closed ball.