Countably generated measurable spaces

We say a measurable space is countably generated if it can be generated by a countable set of sets.

In such a space, we can also build a sequence of finer and finer finite measurable partitions of the space such that the measurable space is generated by the union of all partitions.

Main definitions

• MeasurableSpace.CountablyGenerated: class stating that a measurable space is countably generated.
• MeasurableSpace.countableGeneratingSet: a countable set of sets that generates the σ-algebra.
• MeasurableSpace.countablePartition: sequences of finer and finer partitions of a countably generated space, defined by taking the memPartition of an enumeration of the sets in countableGeneratingSet.
• MeasurableSpace.SeparatesPoints : class stating that a measurable space separates points.

Main statements

• MeasurableSpace.measurableEquiv_nat_bool_of_countablyGenerated: if a measurable space is countably generated and separates points, it is measure equivalent to a subset of the Cantor Space ℕ → Bool (equipped with the product sigma algebra).
• MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated: If a measurable space admits a countable sequence of measurable sets separating points, it admits a measurable injection into the Cantor space ℕ → Bool ℕ → Bool (equipped with the product sigma algebra).

The file also contains measurability results about memPartition, from which the properties of countablePartition are deduced.

class MeasurableSpace.CountablyGenerated (α : Type u_3) [m : MeasurableSpace α] : Prop

We say a measurable space is countably generated if it can be generated by a countable set of sets.

• isCountablyGenerated : ∃ (b : Set (Set α)), b.Countable ∧ m = generateFrom b

def MeasurableSpace.countableGeneratingSet (α : Type u_3) [MeasurableSpace α] [h : CountablyGenerated α] : Set (Set α)

A countable set of sets that generate the measurable space. We insert ∅ to ensure it is nonempty.

Equations

• MeasurableSpace.countableGeneratingSet α = insert ∅ ⋯.choose

theorem MeasurableSpace.countable_countableGeneratingSet {α : Type u_1} [MeasurableSpace α] [h : CountablyGenerated α] : (countableGeneratingSet α).Countable

theorem MeasurableSpace.generateFrom_countableGeneratingSet {α : Type u_1} [m : MeasurableSpace α] [h : CountablyGenerated α] : generateFrom (countableGeneratingSet α) = m

theorem MeasurableSpace.empty_mem_countableGeneratingSet {α : Type u_1} [MeasurableSpace α] [CountablyGenerated α] : ∅ ∈ countableGeneratingSet α

theorem MeasurableSpace.nonempty_countableGeneratingSet {α : Type u_1} [MeasurableSpace α] [CountablyGenerated α] : (countableGeneratingSet α).Nonempty

theorem MeasurableSpace.measurableSet_countableGeneratingSet {α : Type u_1} [MeasurableSpace α] [CountablyGenerated α] {s : Set α} (hs : s ∈ countableGeneratingSet α) : MeasurableSet s

def MeasurableSpace.natGeneratingSequence (α : Type u_3) [MeasurableSpace α] [CountablyGenerated α] : ℕ → Set α

A countable sequence of sets generating the measurable space.

Equations

• MeasurableSpace.natGeneratingSequence α = Set.enumerateCountable ⋯ ∅

theorem MeasurableSpace.generateFrom_natGeneratingSequence (α : Type u_3) [m : MeasurableSpace α] [CountablyGenerated α] : generateFrom (Set.range (natGeneratingSequence α)) = m

theorem MeasurableSpace.measurableSet_natGeneratingSequence {α : Type u_1} [MeasurableSpace α] [CountablyGenerated α] (n : ℕ) : MeasurableSet (natGeneratingSequence α n)

theorem MeasurableSpace.CountablyGenerated.comap {α : Type u_1} {β : Type u_2} [m : MeasurableSpace β] [h : CountablyGenerated β] (f : α → β) : CountablyGenerated α

theorem MeasurableSpace.CountablyGenerated.sup {β : Type u_2} {m₁ m₂ : MeasurableSpace β} (h₁ : CountablyGenerated β) (h₂ : CountablyGenerated β) : CountablyGenerated β

@[instance 100]

instance MeasurableSpace.instCountablyGeneratedOfCountable {α : Type u_1} [MeasurableSpace α] [Countable α] : CountablyGenerated α

Any measurable space structure on a countable space is countably generated.

instance MeasurableSpace.instCountablyGeneratedSubtype {α : Type u_1} [MeasurableSpace α] [CountablyGenerated α] {p : α → Prop} : CountablyGenerated { x : α // p x }

instance MeasurableSpace.instCountablyGeneratedProd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [CountablyGenerated α] [MeasurableSpace β] [CountablyGenerated β] : CountablyGenerated (α × β)

def MeasurableSpace.countablyGeneratedAtom (α : Type u_3) [MeasurableSpace α] [CountablyGenerated α] : (ℕ → Prop) → Set α

The atoms in a countably generated measurable space.

Some of those sets may be empty, but the nonempty ones are the atoms of the measurable space. See measurableAtom_eq_countablyGeneratedAtom_natGeneratingSequence.

Equations

• MeasurableSpace.countablyGeneratedAtom α p = ⋂ (n : ℕ), if p n then MeasurableSpace.natGeneratingSequence α n else (MeasurableSpace.natGeneratingSequence α n)ᶜ

theorem MeasurableSpace.measurableSet_countablyGeneratedAtom {α : Type u_1} {mα : MeasurableSpace α} [CountablyGenerated α] (p : ℕ → Prop) : MeasurableSet (countablyGeneratedAtom α p)

theorem MeasurableSpace.disjoint_countablyGeneratedAtom {α : Type u_1} {mα : MeasurableSpace α} [CountablyGenerated α] : Pairwise (Function.onFun Disjoint (countablyGeneratedAtom α))

theorem MeasurableSpace.iUnion_countablyGeneratedAtom {α : Type u_1} {mα : MeasurableSpace α} [CountablyGenerated α] : ⋃ (p : ℕ → Prop), countablyGeneratedAtom α p = Set.univ

theorem MeasurableSpace.mem_countablyGeneratedAtom_natGeneratingSequence {α : Type u_1} {mα : MeasurableSpace α} [CountablyGenerated α] (x : α) : x ∈ countablyGeneratedAtom α fun (x_1 : ℕ) => x ∈ natGeneratingSequence α x_1

theorem MeasurableSpace.exists_eq_iUnion_countablyGeneratedAtom {α : Type u_1} {mα : MeasurableSpace α} [CountablyGenerated α] {s : Set α} (hs : MeasurableSet s) : ∃ (q : (ℕ → Prop) → Prop), s = ⋃ (p : ℕ → Prop), if q p then countablyGeneratedAtom α p else ∅

Any measurable set in a countably generated measurable space can be expressed as a union of atoms.

theorem MeasurableSpace.measurableAtom_eq_countablyGeneratedAtom_natGeneratingSequence {α : Type u_1} {mα : MeasurableSpace α} [CountablyGenerated α] (x : α) : measurableAtom x = countablyGeneratedAtom α fun (x_1 : ℕ) => x ∈ natGeneratingSequence α x_1

The measurable atom of a point in a countably generated measurable space is given by a countablyGeneratedAtom.

theorem MeasurableSpace.measurableSet_measurableAtom {α : Type u_1} {mα : MeasurableSpace α} [CountablyGenerated α] (x : α) : MeasurableSet (measurableAtom x)

In a countably generated measurable space, the atoms are measurable.

class MeasurableSpace.SeparatesPoints (α : Type u_3) [m : MeasurableSpace α] : Prop

We say that a measurable space separates points if for any two distinct points, there is a measurable set containing one but not the other.

• separates (x y : α) : (∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s) → x = y

theorem MeasurableSpace.separatesPoints_def {α : Type u_1} [MeasurableSpace α] [hs : SeparatesPoints α] {x y : α} (h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s) : x = y

theorem MeasurableSpace.exists_measurableSet_of_ne {α : Type u_1} [MeasurableSpace α] [SeparatesPoints α] {x y : α} (h : x ≠ y) : ∃ (s : Set α), MeasurableSet s ∧ x ∈ s ∧ y ∉ s

theorem MeasurableSpace.separatesPoints_iff {α : Type u_1} [MeasurableSpace α] : SeparatesPoints α ↔ ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y

theorem MeasurableSpace.separating_of_generateFrom {α : Type u_1} (S : Set (Set α)) [h : SeparatesPoints α] (x y : α) : (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

If the measurable space generated by S separates points, then this is witnessed by sets in S.

theorem MeasurableSpace.SeparatesPoints.mono {α : Type u_1} {m m' : MeasurableSpace α} [hsep : SeparatesPoints α] (h : m ≤ m') : SeparatesPoints α

theorem eq_const_of_measurable_bot {α : Type u_1} {β : Type u_2} [MeasurableSpace β] [Nonempty β] [MeasurableSpace.SeparatesPoints β] {f : α → β} (hf : Measurable f) : ∃ (c : β), f = fun (x : α) => c

class MeasurableSpace.CountablySeparated (α : Type u_3) [MeasurableSpace α] : Prop

We say that a measurable space is countably separated if there is a countable sequence of measurable sets separating points.

• countably_separated : HasCountableSeparatingOn α MeasurableSet Set.univ

instance MeasurableSpace.countablySeparated_of_hasCountableSeparatingOn {α : Type u_1} [MeasurableSpace α] [h : HasCountableSeparatingOn α MeasurableSet Set.univ] : CountablySeparated α

instance MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated {α : Type u_1} [MeasurableSpace α] [h : CountablySeparated α] : HasCountableSeparatingOn α MeasurableSet Set.univ

theorem MeasurableSpace.countablySeparated_def {α : Type u_1} [MeasurableSpace α] : CountablySeparated α ↔ HasCountableSeparatingOn α MeasurableSet Set.univ

theorem MeasurableSpace.CountablySeparated.mono {α : Type u_1} {m m' : MeasurableSpace α} [hsep : CountablySeparated α] (h : m ≤ m') : CountablySeparated α

theorem MeasurableSpace.CountablySeparated.subtype_iff {α : Type u_1} [MeasurableSpace α] {s : Set α} : CountablySeparated ↑s ↔ HasCountableSeparatingOn α MeasurableSet s

@[instance 100]

instance MeasurableSpace.Subtype.separatesPoints {α : Type u_1} [MeasurableSpace α] [h : SeparatesPoints α] {s : Set α} : SeparatesPoints ↑s

@[instance 100]

instance MeasurableSpace.Subtype.countablySeparated {α : Type u_1} [MeasurableSpace α] [h : CountablySeparated α] {s : Set α} : CountablySeparated ↑s

@[instance 100]

instance MeasurableSpace.separatesPoints_of_measurableSingletonClass {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] : SeparatesPoints α

@[instance 50]

instance MeasurableSpace.MeasurableSingletonClass.of_separatesPoints {α : Type u_1} [MeasurableSpace α] [Countable α] [SeparatesPoints α] : MeasurableSingletonClass α

instance MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated_subtype {α : Type u_1} [MeasurableSpace α] {s : Set α} [h : CountablySeparated ↑s] : HasCountableSeparatingOn α MeasurableSet s

instance MeasurableSpace.countablySeparated_subtype_of_hasCountableSeparatingOn {α : Type u_1} [MeasurableSpace α] {s : Set α} [h : HasCountableSeparatingOn α MeasurableSet s] : CountablySeparated ↑s

instance MeasurableSpace.countablySeparated_of_separatesPoints {α : Type u_1} [MeasurableSpace α] [h : CountablyGenerated α] [SeparatesPoints α] : CountablySeparated α

theorem MeasurableSpace.exists_countablyGenerated_le_of_countablySeparated (α : Type u_1) [m : MeasurableSpace α] [h : CountablySeparated α] : ∃ (m' : MeasurableSpace α), CountablyGenerated α ∧ SeparatesPoints α ∧ m' ≤ m

If a measurable space admits a countable separating family of measurable sets, there is a countably generated coarser space which still separates points.

noncomputable def MeasurableSpace.mapNatBool (α : Type u_1) [MeasurableSpace α] [CountablyGenerated α] (x : α) (n : ℕ) : Bool

A map from a measurable space to the Cantor space ℕ → Bool induced by a countable sequence of sets generating the measurable space.

Equations

• MeasurableSpace.mapNatBool α x n = decide (x ∈ MeasurableSpace.natGeneratingSequence α n)

theorem MeasurableSpace.measurable_mapNatBool (α : Type u_1) [MeasurableSpace α] [CountablyGenerated α] : Measurable (mapNatBool α)

theorem MeasurableSpace.injective_mapNatBool (α : Type u_1) [MeasurableSpace α] [CountablyGenerated α] [SeparatesPoints α] : Function.Injective (mapNatBool α)

theorem MeasurableSpace.measurableEquiv_nat_bool_of_countablyGenerated (α : Type u_1) [MeasurableSpace α] [CountablyGenerated α] [SeparatesPoints α] : ∃ (s : Set (ℕ → Bool)), Nonempty (α ≃ᵐ ↑s)

If a measurable space is countably generated and separates points, it is measure equivalent to some subset of the Cantor space ℕ → Bool (equipped with the product sigma algebra). Note: s need not be measurable, so this map need not be a MeasurableEmbedding to the Cantor Space.

theorem MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated (α : Type u_1) [MeasurableSpace α] [CountablySeparated α] : ∃ (f : α → ℕ → Bool), Measurable f ∧ Function.Injective f

If a measurable space admits a countable sequence of measurable sets separating points, it admits a measurable injection into the Cantor space ℕ → Bool (equipped with the product sigma algebra).

theorem MeasurableSpace.measurableSingletonClass_of_countablySeparated {α : Type u_1} [MeasurableSpace α] [CountablySeparated α] : MeasurableSingletonClass α

theorem MeasurableSpace.measurableSet_succ_memPartition {α : Type u_1} (t : ℕ → Set α) (n : ℕ) {s : Set α} (hs : s ∈ memPartition t n) : MeasurableSet s

theorem MeasurableSpace.generateFrom_memPartition_le_succ {α : Type u_1} (t : ℕ → Set α) (n : ℕ) : generateFrom (memPartition t n) ≤ generateFrom (memPartition t (n + 1))

theorem MeasurableSpace.measurableSet_generateFrom_memPartition_iff {α : Type u_1} (t : ℕ → Set α) (n : ℕ) (s : Set α) : MeasurableSet s ↔ ∃ (S : Finset (Set α)), ↑S ⊆ memPartition t n ∧ s = ⋃₀ ↑S

theorem MeasurableSpace.measurableSet_generateFrom_memPartition {α : Type u_1} (t : ℕ → Set α) (n : ℕ) : MeasurableSet (t n)

theorem MeasurableSpace.generateFrom_iUnion_memPartition {α : Type u_1} (t : ℕ → Set α) : generateFrom (⋃ (n : ℕ), memPartition t n) = generateFrom (Set.range t)

theorem MeasurableSpace.generateFrom_memPartition_le_range {α : Type u_1} (t : ℕ → Set α) (n : ℕ) : generateFrom (memPartition t n) ≤ generateFrom (Set.range t)

theorem MeasurableSpace.generateFrom_iUnion_memPartition_le {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) : generateFrom (⋃ (n : ℕ), memPartition t n) ≤ m

theorem MeasurableSpace.generateFrom_memPartition_le {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) : generateFrom (memPartition t n) ≤ m

theorem MeasurableSpace.measurableSet_memPartition {α : Type u_1} [MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) {s : Set α} (hs : s ∈ memPartition t n) : MeasurableSet s

theorem MeasurableSpace.measurableSet_memPartitionSet {α : Type u_1} [MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) (a : α) : MeasurableSet (memPartitionSet t n a)

def MeasurableSpace.countablePartition (α : Type u_3) [MeasurableSpace α] [CountablyGenerated α] : ℕ → Set (Set α)

For each n : ℕ, countablePartition α n is a partition of the space in at most 2^n sets. Each partition is finer than the preceding one. The measurable space generated by the union of all those partitions is the measurable space on α.

Equations

• MeasurableSpace.countablePartition α = memPartition (Set.enumerateCountable ⋯ ∅)

theorem MeasurableSpace.measurableSet_enumerateCountable_countableGeneratingSet (α : Type u_3) [MeasurableSpace α] [CountablyGenerated α] (n : ℕ) : MeasurableSet (Set.enumerateCountable ⋯ ∅ n)

theorem MeasurableSpace.finite_countablePartition (α : Type u_3) [MeasurableSpace α] [CountablyGenerated α] (n : ℕ) : (countablePartition α n).Finite

instance MeasurableSpace.instFinite_countablePartition {α : Type u_1} [m : MeasurableSpace α] [h : CountablyGenerated α] (n : ℕ) : Finite ↑(countablePartition α n)

theorem MeasurableSpace.disjoint_countablePartition {α : Type u_1} [m : MeasurableSpace α] [h : CountablyGenerated α] {n : ℕ} {s t : Set α} (hs : s ∈ countablePartition α n) (ht : t ∈ countablePartition α n) (hst : s ≠ t) : Disjoint s t

theorem MeasurableSpace.sUnion_countablePartition (α : Type u_3) [MeasurableSpace α] [CountablyGenerated α] (n : ℕ) : ⋃₀ countablePartition α n = Set.univ

theorem MeasurableSpace.measurableSet_generateFrom_countablePartition_iff {α : Type u_1} [m : MeasurableSpace α] [h : CountablyGenerated α] (n : ℕ) (s : Set α) : MeasurableSet s ↔ ∃ (S : Finset (Set α)), ↑S ⊆ countablePartition α n ∧ s = ⋃₀ ↑S

theorem MeasurableSpace.measurableSet_succ_countablePartition {α : Type u_1} [m : MeasurableSpace α] [h : CountablyGenerated α] (n : ℕ) {s : Set α} (hs : s ∈ countablePartition α n) : MeasurableSet s

theorem MeasurableSpace.generateFrom_countablePartition_le_succ (α : Type u_3) [MeasurableSpace α] [CountablyGenerated α] (n : ℕ) : generateFrom (countablePartition α n) ≤ generateFrom (countablePartition α (n + 1))

theorem MeasurableSpace.generateFrom_iUnion_countablePartition (α : Type u_3) [m : MeasurableSpace α] [CountablyGenerated α] : generateFrom (⋃ (n : ℕ), countablePartition α n) = m

theorem MeasurableSpace.generateFrom_countablePartition_le (α : Type u_3) [m : MeasurableSpace α] [CountablyGenerated α] (n : ℕ) : generateFrom (countablePartition α n) ≤ m

theorem MeasurableSpace.measurableSet_countablePartition {α : Type u_1} [m : MeasurableSpace α] [h : CountablyGenerated α] (n : ℕ) {s : Set α} (hs : s ∈ countablePartition α n) : MeasurableSet s

def MeasurableSpace.countablePartitionSet {α : Type u_1} [m : MeasurableSpace α] [h : CountablyGenerated α] (n : ℕ) (a : α) : Set α

The set in countablePartition α n to which a : α belongs.

Equations

• MeasurableSpace.countablePartitionSet n a = memPartitionSet (Set.enumerateCountable ⋯ ∅) n a

theorem MeasurableSpace.countablePartitionSet_mem {α : Type u_1} [m : MeasurableSpace α] [h : CountablyGenerated α] (n : ℕ) (a : α) : countablePartitionSet n a ∈ countablePartition α n

theorem MeasurableSpace.mem_countablePartitionSet {α : Type u_1} [m : MeasurableSpace α] [h : CountablyGenerated α] (n : ℕ) (a : α) : a ∈ countablePartitionSet n a

theorem MeasurableSpace.countablePartitionSet_eq_iff {α : Type u_1} [m : MeasurableSpace α] [h : CountablyGenerated α] {n : ℕ} (a : α) {s : Set α} (hs : s ∈ countablePartition α n) : countablePartitionSet n a = s ↔ a ∈ s

theorem MeasurableSpace.countablePartitionSet_of_mem {α : Type u_1} [m : MeasurableSpace α] [h : CountablyGenerated α] {n : ℕ} {a : α} {s : Set α} (hs : s ∈ countablePartition α n) (ha : a ∈ s) : countablePartitionSet n a = s

theorem MeasurableSpace.measurableSet_countablePartitionSet {α : Type u_1} [m : MeasurableSpace α] [h : CountablyGenerated α] (n : ℕ) (a : α) : MeasurableSet (countablePartitionSet n a)

class MeasurableSpace.CountableOrCountablyGenerated (α : Type u_5) (β : Type u_6) [MeasurableSpace β] : Prop

A class registering that either α is countable or β is a countably generated measurable space.

• countableOrCountablyGenerated : Countable α ∨ CountablyGenerated β

instance MeasurableSpace.instCountableOrCountablyGeneratedOfCountable {β : Type u_2} {α : Type u_3} [h1 : Countable α] [MeasurableSpace β] : CountableOrCountablyGenerated α β

instance MeasurableSpace.instCountableOrCountablyGeneratedOfCountablyGenerated {β : Type u_2} {α : Type u_3} [MeasurableSpace β] [h : CountablyGenerated β] : CountableOrCountablyGenerated α β

instance MeasurableSpace.instCountableOrCountablyGeneratedProd {β : Type u_2} {α : Type u_3} {γ : Type u_4} [MeasurableSpace γ] [hα : CountableOrCountablyGenerated α γ] [hβ : CountableOrCountablyGenerated β γ] : CountableOrCountablyGenerated (α × β) γ

theorem MeasurableSpace.countableOrCountablyGenerated_left_of_prod_left_of_nonempty {β : Type u_2} {α : Type u_3} {γ : Type u_4} [MeasurableSpace γ] [Nonempty β] [h : CountableOrCountablyGenerated (α × β) γ] : CountableOrCountablyGenerated α γ

theorem MeasurableSpace.countableOrCountablyGenerated_right_of_prod_left_of_nonempty {β : Type u_2} {α : Type u_3} {γ : Type u_4} [MeasurableSpace γ] [Nonempty α] [h : CountableOrCountablyGenerated (α × β) γ] : CountableOrCountablyGenerated β γ

theorem MeasurableSpace.countableOrCountablyGenerated_prod_left_swap {β : Type u_2} {α : Type u_3} {γ : Type u_4} [MeasurableSpace γ] [h : CountableOrCountablyGenerated (α × β) γ] : CountableOrCountablyGenerated (β × α) γ