Cardinal of sigma-algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 measurable_space.cardinal_generate_measurable_le and measurable_space.cardinal_measurable_set_le.

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

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

source

def measurable_space.generate_measurable_rec {α : Type u} (s : set (set α)) :

(quotient.out (cardinal.aleph 1).ord).α → 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 ordinal < ω₁, as this will be enough to generate all sets in the sigma-algebra.

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

Equations

measurable_space.generate_measurable_rec s i = let S : set (set α) := ⋃ (j : ↥(set.Iio i)), measurable_space.generate_measurable_rec s j.val in s ∪ {∅} ∪ has_compl.compl '' S ∪ set.range (λ (f : ℕ → ↥S), ⋃ (n : ℕ), (f n).val)

source

theorem measurable_space.self_subset_generate_measurable_rec {α : Type u} (s : set (set α)) (i : (quotient.out (cardinal.aleph 1).ord).α) :

s ⊆ measurable_space.generate_measurable_rec s i

source

theorem measurable_space.empty_mem_generate_measurable_rec {α : Type u} (s : set (set α)) (i : (quotient.out (cardinal.aleph 1).ord).α) :

∅ ∈ measurable_space.generate_measurable_rec s i

source

theorem measurable_space.compl_mem_generate_measurable_rec {α : Type u} {s : set (set α)} {i j : (quotient.out (cardinal.aleph 1).ord).α} (h : j < i) {t : set α} (ht : t ∈ measurable_space.generate_measurable_rec s j) :

tᶜ ∈ measurable_space.generate_measurable_rec s i

source

theorem measurable_space.Union_mem_generate_measurable_rec {α : Type u} {s : set (set α)} {i : (quotient.out (cardinal.aleph 1).ord).α} {f : ℕ → set α} (hf : ∀ (n : ℕ), ∃ (j : (quotient.out (cardinal.aleph 1).ord).α) (H : j < i), f n ∈ measurable_space.generate_measurable_rec s j) :

(⋃ (n : ℕ), f n) ∈ measurable_space.generate_measurable_rec s i

source

theorem measurable_space.generate_measurable_rec_subset {α : Type u} (s : set (set α)) {i j : (quotient.out (cardinal.aleph 1).ord).α} (h : i ≤ j) :

measurable_space.generate_measurable_rec s i ⊆ measurable_space.generate_measurable_rec s j

source

theorem measurable_space.cardinal_generate_measurable_rec_le {α : Type u} (s : set (set α)) (i : (quotient.out (cardinal.aleph 1).ord).α) :

cardinal.mk ↥(measurable_space.generate_measurable_rec s i) ≤ linear_order.max (cardinal.mk ↥s) 2 ^ cardinal.aleph_0

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

source

theorem measurable_space.generate_measurable_eq_rec {α : Type u} (s : set (set α)) :

{t : set α | measurable_space.generate_measurable s t} = ⋃ (i : (quotient.out (cardinal.aleph 1).ord).α), measurable_space.generate_measurable_rec s i

generate_measurable_rec s generates precisely the smallest sigma-algebra containing s.

source

theorem measurable_space.cardinal_generate_measurable_le {α : Type u} (s : set (set α)) :

cardinal.mk ↥{t : set α | measurable_space.generate_measurable s t} ≤ linear_order.max (cardinal.mk ↥s) 2 ^ cardinal.aleph_0

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

source

theorem measurable_space.cardinal_measurable_set_le {α : Type u} (s : set (set α)) :

cardinal.mk ↥{t : set α | measurable_set t} ≤ linear_order.max (cardinal.mk ↥s) 2 ^ cardinal.aleph_0

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

source

theorem measurable_space.cardinal_generate_measurable_le_continuum {α : Type u} {s : set (set α)} (hs : cardinal.mk ↥s ≤ cardinal.continuum) :

cardinal.mk ↥{t : set α | measurable_space.generate_measurable 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.

source

theorem measurable_space.cardinal_measurable_set_le_continuum {α : Type u} {s : set (set α)} :

cardinal.mk ↥s ≤ cardinal.continuum → cardinal.mk ↥{t : set α | measurable_set 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.