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 α)), b.Countable ∧ m = MeasurableSpace.generateFrom b

theorem MeasurableSpace.CountablyGenerated.isCountablyGenerated {α : Type u_3} {m : MeasurableSpace α} [self : MeasurableSpace.CountablyGenerated α] : ∃ (b : Set (Set α)), b.Countable ∧ 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 ∅ ⋯.choose

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

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 α] : (MeasurableSpace.countableGeneratingSet α).Nonempty

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 100]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance MeasurableSpace.instCountablyGeneratedProd {α : 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.separates {α : Type u_3} {m : MeasurableSpace α} [self : MeasurableSpace.SeparatesPoints α] (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.separatesPoints_iff {α : Type u_1} [MeasurableSpace α] : 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 : 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 α

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

theorem MeasurableSpace.CountablySeparated.countably_separated {α : Type u_3} : ∀ {inst : MeasurableSpace α} [self : MeasurableSpace.CountablySeparated α], HasCountableSeparatingOn α MeasurableSet Set.univ

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 50]

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem MeasurableSpace.exists_countablyGenerated_le_of_countablySeparated (α : Type u_1) [m : MeasurableSpace α] [h : MeasurableSpace.CountablySeparated α] : ∃ (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 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 α] [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 α] [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 : ℕ) : 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 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 α] [MeasurableSpace.CountablyGenerated α] (n : ℕ) : MeasurableSet (Set.enumerateCountable ⋯ ∅ n)

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

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)

class MeasurableSpace.CountableOrCountablyGenerated (α : Type u_3) (β : Type u_4) [MeasurableSpace α] [MeasurableSpace β] : Prop

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

• countableOrCountablyGenerated : Countable α ∨ MeasurableSpace.CountablyGenerated β

theorem MeasurableSpace.CountableOrCountablyGenerated.countableOrCountablyGenerated {α : Type u_3} {β : Type u_4} : ∀ {inst : MeasurableSpace α} {inst_1 : MeasurableSpace β} [self : MeasurableSpace.CountableOrCountablyGenerated α β], Countable α ∨ MeasurableSpace.CountablyGenerated β

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯