Carathéodory's extension theorem

TheoremEvery algebra of sets is a semiring of sets#✓fully proved

If \(\mathcal{A}\) is an algebra of sets on \(\alpha\), then \(\mathcal{A}\) is a semiring of sets: \(\emptyset \in \mathcal{A}\), \(s \cap t \in \mathcal{A}\) for all \(s, t \in \mathcal{A}\), and for all \(s, t \in \mathcal{A}\) the difference \(s \setminus t\) is the union of finitely many pairwise disjoint members of \(\mathcal{A}\).

theorem isSetSemiring_of_isSetAlgebra {α : Type*} {𝒜 : Set (Set α)} (h : IsSetAlgebra 𝒜) :
    IsSetSemiring 𝒜

Used by 1

Used byExistence of the Carathéodory extension

LemmaEvery algebra of sets is a π-system#✓fully proved

If \(\mathcal{A}\) is an algebra of sets on \(\alpha\), then \(\mathcal{A}\) is a \(\pi\)-system: for all \(s, t \in \mathcal{A}\) with \(s \cap t\) nonempty, we have \(s \cap t \in \mathcal{A}\).

lemma isSetAlgebra_isPiSystem {α : Type*} {𝒜 : Set (Set α)} (h : IsSetAlgebra 𝒜) :
    IsPiSystem 𝒜

Used by 1

Used byCarathéodory extension theorem

LemmaExistence of the Carathéodory extension#✓fully proved

Let \(\mathcal{A}\) be an algebra of sets on \(\alpha\) and let \(\mu_0\) be an additive content on \(\mathcal{A}\) with values in \([0, \infty]\) that is \(\sigma\)-subadditive: whenever \(s_0, s_1, \dots \in \mathcal{A}\) and \(\bigcup_i s_i \in \mathcal{A}\), we have \(\mu_0(\bigcup_i s_i) \le \sum_i \mu_0(s_i)\). Then there is a measure \(\mu\) on the \(\sigma\)-algebra \(\sigma(\mathcal{A})\) generated by \(\mathcal{A}\) such that \(\mu(s) = \mu_0(s)\) for every \(s \in \mathcal{A}\).

lemma exists_measure_extension
    {α : Type*}
    (𝒜 : Set (Set α))
    (h𝒜 : IsSetAlgebra 𝒜)
    (μ₀ : AddContent ℝ≥0∞ 𝒜)
    (hμ₀_sigma : μ₀.IsSigmaSubadditive) :
    ∃ μ : @Measure α (generateFrom 𝒜), ∀ s ∈ 𝒜, μ s = μ₀ s

Uses 1 · Used by 1

Proof usesEvery algebra of sets is a semiring of sets

Used byCarathéodory extension theorem

TheoremCarathéodory extension theorem#✓fully proved

Let \(\mathcal{A}\) be an algebra of sets on \(\alpha\) and let \(\mu_0\) be an additive content on \(\mathcal{A}\) with values in \([0, \infty]\) that is \(\sigma\)-subadditive: whenever \(s_0, s_1, \dots \in \mathcal{A}\) and \(\bigcup_i s_i \in \mathcal{A}\), we have \(\mu_0(\bigcup_i s_i) \le \sum_i \mu_0(s_i)\). Suppose there are sets \(B_0, B_1, \dots \in \mathcal{A}\) with \(\bigcup_i B_i = \alpha\) and \(\mu_0(B_i) < \infty\) for every \(i\). Then there is exactly one measure \(\mu\) on the \(\sigma\)-algebra \(\sigma(\mathcal{A})\) generated by \(\mathcal{A}\) such that \(\mu(s) = \mu_0(s)\) for every \(s \in \mathcal{A}\).

theorem caratheodory_extension_theorem
    {α : Type*}
    (𝒜 : Set (Set α))
    (h𝒜 : IsSetAlgebra 𝒜)
    (μ₀ : AddContent ℝ≥0∞ 𝒜)
    (hμ₀_sigma : μ₀.IsSigmaSubadditive)
    (B : ℕ → Set α)
    (hB_mem : ∀ i, B i ∈ 𝒜)
    (hB_cover : ⋃ i, B i = univ)
    (hB_fin : ∀ i, μ₀ (B i) ≠ ⊤) :
    ∃! μ : @Measure α (generateFrom 𝒜), ∀ s ∈ 𝒜, μ s = μ₀ s

Uses 2

Proof usesExistence of the Carathéodory extension · Every algebra of sets is a π-system

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.