Cardinal of sigma-algebras

If a sigma-algebra is generated by a set of sets s, then the cardinality of the sigma-algebra is bounded by (max #s 2) ^ ℵ₀. This is stated in MeasurableSpace.cardinal_generate_measurable_le and MeasurableSpace.cardinalMeasurableSet_le.

In particular, if #s ≤ 𝔠, then the generated sigma-algebra has cardinality at most 𝔠, see MeasurableSpace.cardinal_measurableSet_le_continuum.

For the proof, we rely on an explicit inductive construction of the sigma-algebra generated by s (instead of the inductive predicate GenerateMeasurable). This transfinite inductive construction is parameterized by an ordinal < ω₁, and the cardinality bound is preserved along each step of the construction. We show in MeasurableSpace.generateMeasurable_eq_rec that this indeed generates this sigma-algebra.

@[irreducible]

def MeasurableSpace.generateMeasurableRec {α : Type u} (s : Set (Set α)) (i : Ordinal.{u_1}) : Set (Set α)

Transfinite induction construction of the sigma-algebra generated by a set of sets s. At each step, we add all elements of s, the empty set, the complements of already constructed sets, and countable unions of already constructed sets.

We index this construction by an arbitrary ordinal for simplicity, but by ω₁ we will have generated all the sets in the sigma-algebra.

This construction is very similar to that of the Borel hierarchy.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasurableSpace.self_subset_generateMeasurableRec {α : Type u} (s : Set (Set α)) (i : Ordinal.{u_1}) : s ⊆ generateMeasurableRec s i

theorem MeasurableSpace.empty_mem_generateMeasurableRec {α : Type u} (s : Set (Set α)) (i : Ordinal.{u_1}) : ∅ ∈ generateMeasurableRec s i

theorem MeasurableSpace.compl_mem_generateMeasurableRec {α : Type u} {s : Set (Set α)} {i j : Ordinal.{u_1}} (h : j < i) {t : Set α} (ht : t ∈ generateMeasurableRec s j) : tᶜ ∈ generateMeasurableRec s i

theorem MeasurableSpace.iUnion_mem_generateMeasurableRec {α : Type u} {s : Set (Set α)} {i : Ordinal.{u_1}} {f : ℕ → Set α} (hf : ∀ (n : ℕ), ∃ j < i, f n ∈ generateMeasurableRec s j) : ⋃ (n : ℕ), f n ∈ generateMeasurableRec s i

theorem MeasurableSpace.generateMeasurableRec_mono {α : Type u} (s : Set (Set α)) : Monotone (generateMeasurableRec s)

theorem MeasurableSpace.generateMeasurableRec_induction {α : Type u} {s : Set (Set α)} {i : Ordinal.{u_1}} {t : Set α} {p : Set α → Prop} (hs : ∀ t ∈ s, p t) (h0 : p ∅) (hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ) (hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ (n : ℕ), f n)) : t ∈ generateMeasurableRec s i → p t

An inductive principle for the elements of generateMeasurableRec.

theorem MeasurableSpace.generateMeasurableRec_omega1 {α : Type u} (s : Set (Set α)) : generateMeasurableRec s (Ordinal.omega 1) = ⋃ (i : Ordinal.{v}), ⋃ (_ : i < Ordinal.omega 1), generateMeasurableRec s i

theorem MeasurableSpace.generateMeasurableRec_subset {α : Type u} (s : Set (Set α)) (i : Ordinal.{u_1}) : generateMeasurableRec s i ⊆ {t : Set α | GenerateMeasurable s t}

theorem MeasurableSpace.generateMeasurable_eq_rec {α : Type u} (s : Set (Set α)) : {t : Set α | GenerateMeasurable s t} = generateMeasurableRec s (Ordinal.omega 1)

generateMeasurableRec s ω₁ generates precisely the smallest sigma-algebra containing s.

theorem MeasurableSpace.generateMeasurableRec_of_omega1_le {α : Type u} (s : Set (Set α)) {i : Ordinal.{v}} (hi : Ordinal.omega 1 ≤ i) : generateMeasurableRec s i = generateMeasurableRec s (Ordinal.omega 1)

generateMeasurableRec is constant for ordinals ≥ ω₁.

theorem MeasurableSpace.cardinal_generateMeasurableRec_le {α : Type u} (s : Set (Set α)) (i : Ordinal.{v}) : Cardinal.mk ↑(generateMeasurableRec s i) ≤ max (Cardinal.mk ↑s) 2 ^ Cardinal.aleph0

At each step of the inductive construction, the cardinality bound ≤ #s ^ ℵ₀ holds.

theorem MeasurableSpace.cardinal_generateMeasurable_le {α : Type u} (s : Set (Set α)) : Cardinal.mk ↑{t : Set α | GenerateMeasurable s t} ≤ max (Cardinal.mk ↑s) 2 ^ Cardinal.aleph0

If a sigma-algebra is generated by a set of sets s, then the sigma-algebra has cardinality at most max #s 2 ^ ℵ₀.

theorem MeasurableSpace.cardinal_measurableSet_le {α : Type u} (s : Set (Set α)) : Cardinal.mk ↑{t : Set α | MeasurableSet t} ≤ max (Cardinal.mk ↑s) 2 ^ Cardinal.aleph0

If a sigma-algebra is generated by a set of sets s, then the sigma algebra has cardinality at most max #s 2 ^ ℵ₀.

theorem MeasurableSpace.cardinal_generateMeasurable_le_continuum {α : Type u} {s : Set (Set α)} (hs : Cardinal.mk ↑s ≤ Cardinal.continuum) : Cardinal.mk ↑{t : Set α | GenerateMeasurable s t} ≤ Cardinal.continuum

If a sigma-algebra is generated by a set of sets s with cardinality at most the continuum, then the sigma algebra has the same cardinality bound.

theorem MeasurableSpace.cardinal_measurableSet_le_continuum {α : Type u} {s : Set (Set α)} : Cardinal.mk ↑s ≤ Cardinal.continuum → Cardinal.mk ↑{t : Set α | MeasurableSet t} ≤ Cardinal.continuum

If a sigma-algebra is generated by a set of sets s with cardinality at most the continuum, then the sigma algebra has the same cardinality bound.