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.

Main statements

• MeasurableSpace.measurable_injection_nat_bool_of_countablyGenerated: if a measurable space is countably generated and separates points, it admits a measurable injection into the Cantor space ℕ → 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 α] : 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

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

• ⋯ = ⋯

instance MeasurableSpace.instHasCountableSeparatingOnMeasurableSet {α : 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)

theorem MeasurableSpace.measurable_injection_nat_bool_of_countablyGenerated (α : Type u_1) [MeasurableSpace α] [HasCountableSeparatingOn α MeasurableSet Set.univ] : ∃ (f : α → ℕ → Bool), Measurable f ∧ Function.Injective f

If a measurable space is countably generated and separates points, it admits a measurable injection into the Cantor space ℕ → Bool (equipped with the product sigma algebra).