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 memPartion of an enumeration of the sets in countableGeneratingSet.
• MeasurableSpace.SeparatesPoints : class stating that a measurable space separates points.

Main statements

• MeasurableSpace.measurable_equiv_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_countablyGenerated: 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 α)), Set.Countable b ∧ m = MeasurableSpace.generateFrom b

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

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

Equations

• MeasurableSpace.countableGeneratingSet α = insert ∅ (Exists.choose ⋯)

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

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

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

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

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

def MeasurableSpace.natGeneratingSequence (α : Type u_3) [MeasurableSpace α] [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 α] [MeasurableSpace.CountablyGenerated α] : MeasurableSpace.generateFrom (Set.range (MeasurableSpace.natGeneratingSequence α)) = m

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

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

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

instance MeasurableSpace.instCountablyGenerated {α : Type u_1} [MeasurableSpace α] [Finite α] : MeasurableSpace.CountablyGenerated α

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 : MeasurableSpace.SeparatesPoints α] {x : α} {y : α} (h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s) : x = y

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

theorem MeasurableSpace.separating_of_generateFrom {α : Type u_1} (S : Set (Set α)) [h : MeasurableSpace.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 : MeasurableSpace α} {m' : MeasurableSpace α} [hsep : MeasurableSpace.SeparatesPoints α] (h : m ≤ m') : MeasurableSpace.SeparatesPoints α

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance MeasurableSpace.instHasCountableSeparatingOnMeasurableSet {α : Type u_1} [MeasurableSpace α] {s : Set α} [h : MeasurableSpace.CountablyGenerated ↑s] [MeasurableSpace.SeparatesPoints ↑s] : HasCountableSeparatingOn α MeasurableSet s

Equations

• ⋯ = ⋯

theorem MeasurableSpace.exists_countablyGenerated_le_of_hasCountableSeparatingOn (α : Type u_1) [m : MeasurableSpace α] [h : HasCountableSeparatingOn α MeasurableSet Set.univ] : ∃ (m' : MeasurableSpace α), MeasurableSpace.CountablyGenerated α ∧ MeasurableSpace.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 α] [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 α] [MeasurableSpace.CountablyGenerated α] : Measurable (MeasurableSpace.mapNatBool α)

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

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

If a measurable space is countably generated and separates points, it is measure equivalent to some 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_hasCountableSeparatingOn (α : Type u_1) [MeasurableSpace α] [HasCountableSeparatingOn α MeasurableSet Set.univ] : ∃ (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_hasCountableSeparatingOn {α : Type u_1} [MeasurableSpace α] [HasCountableSeparatingOn α MeasurableSet Set.univ] : MeasurableSingletonClass α

instance MeasurableSpace.instHasCountableSeparatingOnMeasurableSet_1 {α : Type u_1} [MeasurableSpace α] {s : Set α} [h : MeasurableSpace.CountablyGenerated ↑s] [MeasurableSingletonClass ↑s] : HasCountableSeparatingOn α MeasurableSet s

Equations

• ⋯ = ⋯

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 : ℕ) : MeasurableSpace.generateFrom (memPartition t n) ≤ MeasurableSpace.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 α) : MeasurableSpace.generateFrom (⋃ (n : ℕ), memPartition t n) = MeasurableSpace.generateFrom (Set.range t)

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

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

theorem MeasurableSpace.generateFrom_memPartition_le {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) : MeasurableSpace.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 α] [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 preceeding 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 α] [MeasurableSpace.CountablyGenerated α] (n : ℕ) : MeasurableSet (Set.enumerateCountable ⋯ ∅ n)

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

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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

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

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

def MeasurableSpace.countablePartitionSet {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.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 : MeasurableSpace.CountablyGenerated α] (n : ℕ) (a : α) : MeasurableSpace.countablePartitionSet n a ∈ MeasurableSpace.countablePartition α n

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

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

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

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