Tightness of probability measures

DefinitionTight family of probability measures#✓fully proved

Let \(\alpha\) be a space carrying a σ-algebra and a topology. A family \((\mu_i)_{i \in \iota}\) of probability measures on \(\alpha\) is tight if its range \(\{\mu_i : i \in \iota\}\) is a tight set of measures: for every \(\varepsilon \in (0, \infty]\) there is a compact set \(K \subseteq \alpha\) such that \(\mu_i(\alpha \setminus K) \le \varepsilon\) for every index \(i\).

def IsTightFamily {α : Type*} [MeasurableSpace α] [TopologicalSpace α]
    {ι : Type*} (μ : ι → Measure α) [∀ i, IsProbabilityMeasure (μ i)] : Prop :=
  IsTightMeasureSet (Set.range μ)

Used by 4

Used byReal-line tightness implies tightness · Tightness of a family is tightness of its range · Constant families on the real line are tight · Tight families on the real line concentrate on bounded intervals

DefinitionTightness on the real line#✓fully proved

A family \((\mu_i)_{i \in \iota}\) of probability measures on \(\mathbb{R}\) is tight in the real-line sense if for every \(\varepsilon \in (0, \infty]\) there is \(M \in \mathbb{R}\) such that \(\mu_i([-M, M]) \ge 1 - \varepsilon\) for every index \(i\).

def IsTightFamilyReal {ι : Type*} (μ : ι → Measure ℝ)
    [∀ i, IsProbabilityMeasure (μ i)] : Prop :=
  ∀ ε : ℝ≥0∞, 0 < ε → ∃ M : ℝ, ∀ i, μ i (Set.Icc (-M) M) ≥ 1 - ε

Used by 2

Used byReal-line tightness implies tightness · Tight families on the real line concentrate on bounded intervals

TheoremReal-line tightness implies tightness#✓fully proved

Let \((\mu_i)_{i \in \iota}\) be a family of probability measures on \(\mathbb{R}\). If the family is tight in the real-line sense, that is, for every \(\varepsilon \in (0, \infty]\) there is \(M \in \mathbb{R}\) with \(\mu_i([-M, M]) \ge 1 - \varepsilon\) for every \(i\), then the family is tight, that is, for every \(\varepsilon \in (0, \infty]\) there is a compact set \(K \subseteq \mathbb{R}\) with \(\mu_i(\mathbb{R} \setminus K) \le \varepsilon\) for every \(i\).

The interval \([-M, M]\) is compact.

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

Uses 2

Statement usesTight family of probability measures · Tightness on the real line

TheoremTight families on the real line concentrate on bounded intervals#✓fully proved

Let \((\mu_i)_{i \in \iota}\) be a family of probability measures on \(\mathbb{R}\). If the family is tight, that is, for every \(\varepsilon \in (0, \infty]\) there is a compact set \(K \subseteq \mathbb{R}\) with \(\mu_i(\mathbb{R} \setminus K) \le \varepsilon\) for every \(i\), then it is tight in the real-line sense: for every \(\varepsilon \in (0, \infty]\) there is \(M \in \mathbb{R}\) with \(\mu_i([-M, M]) \ge 1 - \varepsilon\) for every \(i\).

The proof encloses the compact set in a closed ball.

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

Uses 2

Statement usesTight family of probability measures · Tightness on the real line

TheoremTightness of a family is tightness of its range#✓fully proved

Let \(\alpha\) be a space carrying a σ-algebra and a topology. A family \((\mu_i)_{i \in \iota}\) of probability measures on \(\alpha\) is tight exactly when its range \(\{\mu_i : i \in \iota\}\) is a tight set of measures.

theorem isTightFamily_iff_isTightMeasureSet {α : Type*}
    [MeasurableSpace α] [TopologicalSpace α] {ι : Type*} {μ : ι → Measure α}
    [∀ i, IsProbabilityMeasure (μ i)] :
    IsTightFamily μ ↔ IsTightMeasureSet (Set.range μ)

Uses 1 · Used by 1

Statement usesTight family of probability measures

Used byConstant families on the real line are tight

TheoremConstant families on the real line are tight#✓fully proved

For every index type \(\iota\) and every probability measure \(\mu\) on \(\mathbb{R}\), the constant family \((\mu)_{i \in \iota}\) is tight.

theorem isTightFamily_of_singleton {ι : Type*} {μ : Measure ℝ}
    [IsProbabilityMeasure μ] :
    IsTightFamily (fun _ : ι => μ)

Uses 2

Statement usesTight family of probability measures

Proof usesTightness of a family is tightness of its range

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.