feat: countable filtration in a countably generated measurable space (#10945)

In a countably generated measurable space `α`, we can 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.
This sequence of partitions (`countablePartition α n`) is defined in `MeasureTheory.MeasurableSpace.CountablyGenerated`. This is a new file in which we put the definition of `CountablyGenerated` (which was previously in MeasurableSpace.Basic).

In `Probability.Process.CountablyGenerated`, we build the filtration generated by `countablePartition α n` for all `n : ℕ`, which we call `countableFiltration α`.



Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

Author: RemyDegenne

Mathlib.lean

@@ -2092,6 +2092,7 @@ import Mathlib.Data.Set.Intervals.UnorderedInterval
 import Mathlib.Data.Set.Intervals.WithBotTop
 import Mathlib.Data.Set.Lattice
 import Mathlib.Data.Set.List
+import Mathlib.Data.Set.MemPartition
 import Mathlib.Data.Set.MulAntidiagonal
 import Mathlib.Data.Set.NAry
 import Mathlib.Data.Set.Opposite
@@ -2826,6 +2827,7 @@ import Mathlib.MeasureTheory.Integral.TorusIntegral
 import Mathlib.MeasureTheory.Integral.VitaliCaratheodory
 import Mathlib.MeasureTheory.MeasurableSpace.Basic
 import Mathlib.MeasureTheory.MeasurableSpace.Card
+import Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
 import Mathlib.MeasureTheory.MeasurableSpace.Defs
 import Mathlib.MeasureTheory.MeasurableSpace.Invariants
 import Mathlib.MeasureTheory.Measure.AEDisjoint
@@ -3206,6 +3208,7 @@ import Mathlib.Probability.ProbabilityMassFunction.Monad
 import Mathlib.Probability.Process.Adapted
 import Mathlib.Probability.Process.Filtration
 import Mathlib.Probability.Process.HittingTime
+import Mathlib.Probability.Process.PartitionFiltration
 import Mathlib.Probability.Process.Stopping
 import Mathlib.Probability.StrongLaw
 import Mathlib.Probability.Variance

Mathlib/Data/Set/MemPartition.lean

@@ -0,0 +1,150 @@
+/-
+Copyright (c) 2024 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+import Mathlib.Data.Set.Finite
+
+/-!
+# Partitions based on membership of a sequence of sets
+
+Let `f : ℕ → Set α` be a sequence of sets. For `n : ℕ`, we can form the set of points that are in
+`f 0 ∪ f 1 ∪ ... ∪ f (n-1)`; then the set of points in `(f 0)ᶜ ∪ f 1 ∪ ... ∪ f (n-1)` and so on for
+all 2^n choices of a set or its complement. The at most 2^n sets we obtain form a partition
+of `univ : Set α`. We call that partition `memPartition f n` (the membership partition of `f`).
+For `n = 0` we set `memPartition f 0 = {univ}`.
+
+The partition `memPartition f (n + 1)` is finer than `memPartition f n`.
+
+## Main definitions
+
+* `memPartition f n`: the membership partition of the first `n` sets in `f`.
+* `memPartitionSet`: `memPartitionSet f n x` is the set in the partition `memPartition f n` to
+  which `x` belongs.
+
+## Main statements
+
+* `disjoint_memPartition`: the sets in `memPartition f n` are disjoint
+* `sUnion_memPartition`: the union of the sets in `memPartition f n` is `univ`
+* `finite_memPartition`: `memPartition f n` is finite
+
+-/
+
+open Set
+
+variable {α : Type*}
+
+/-- `memPartition f n` is the partition containing at most `2^(n+1)` sets, where each set contains
+the points that for all `i` belong to one of `f i` or its complement. -/
+def memPartition (f : ℕ → Set α) : ℕ → Set (Set α)
+  | 0 => {univ}
+  | n + 1 => {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
+
+@[simp]
+lemma memPartition_zero (f : ℕ → Set α) : memPartition f 0 = {univ} := rfl
+
+lemma memPartition_succ (f : ℕ → Set α) (n : ℕ) :
+    memPartition f (n + 1) = {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} :=
+  rfl
+
+lemma disjoint_memPartition (f : ℕ → Set α) (n : ℕ) {u v : Set α}
+    (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v) :
+    Disjoint u v := by
+  revert u v
+  induction n with
+  | zero =>
+    intro u v hu hv huv
+    simp only [Nat.zero_eq, memPartition_zero, mem_insert_iff, mem_singleton_iff] at hu hv
+    rw [hu, hv] at huv
+    exact absurd rfl huv
+  | succ n ih =>
+    intro u v hu hv huv
+    rw [memPartition_succ] at hu hv
+    obtain ⟨u', hu', hu'_eq⟩ := hu
+    obtain ⟨v', hv', hv'_eq⟩ := hv
+    rcases hu'_eq with rfl | rfl <;> rcases hv'_eq with rfl | rfl
+    · refine Disjoint.mono (inter_subset_left _ _) (inter_subset_left _ _) (ih hu' hv' ?_)
+      exact fun huv' ↦ huv (huv' ▸ rfl)
+    · exact Disjoint.mono_left (inter_subset_right _ _) Set.disjoint_sdiff_right
+    · exact Disjoint.mono_right (inter_subset_right _ _) Set.disjoint_sdiff_left
+    · refine Disjoint.mono (diff_subset _ _) (diff_subset _ _) (ih hu' hv' ?_)
+      exact fun huv' ↦ huv (huv' ▸ rfl)
+
+@[simp]
+lemma sUnion_memPartition (f : ℕ → Set α) (n : ℕ) : ⋃₀ memPartition f n = univ := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [memPartition_succ]
+    ext x
+    have : x ∈ ⋃₀ memPartition f n := by simp [ih]
+    simp only [mem_sUnion, mem_iUnion, mem_insert_iff, mem_singleton_iff, exists_prop, mem_univ,
+      iff_true] at this ⊢
+    obtain ⟨t, ht, hxt⟩ := this
+    by_cases hxf : x ∈ f n
+    · exact ⟨t ∩ f n, ⟨t, ht, Or.inl rfl⟩, hxt, hxf⟩
+    · exact ⟨t \ f n, ⟨t, ht, Or.inr rfl⟩, hxt, hxf⟩
+
+lemma finite_memPartition (f : ℕ → Set α) (n : ℕ) : Set.Finite (memPartition f n) := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [memPartition_succ]
+    have : Finite (memPartition f n) := Set.finite_coe_iff.mp ih
+    rw [← Set.finite_coe_iff]
+    simp_rw [setOf_exists, ← exists_prop, setOf_exists, setOf_or]
+    refine Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)
+    rw [Set.finite_coe_iff]
+    simp
+
+instance instFinite_memPartition (f : ℕ → Set α) (n : ℕ) : Finite (memPartition f n) :=
+  Set.finite_coe_iff.mp (finite_memPartition _ _)
+
+open Classical in
+/-- The set in `memPartition f n` to which `a : α` belongs. -/
+def memPartitionSet (f : ℕ → Set α) : ℕ → α → Set α
+  | 0 => fun _ ↦ univ
+  | n + 1 => fun a ↦ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n
+
+@[simp]
+lemma memPartitionSet_zero (f : ℕ → Set α) (a : α) : memPartitionSet f 0 a = univ := by
+  simp [memPartitionSet]
+
+lemma memPartitionSet_succ (f : ℕ → Set α) (n : ℕ) (a : α) [Decidable (a ∈ f n)] :
+    memPartitionSet f (n + 1) a
+      = if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n := by
+  simp [memPartitionSet]
+
+lemma memPartitionSet_mem (f : ℕ → Set α) (n : ℕ) (a : α) :
+    memPartitionSet f n a ∈ memPartition f n := by
+  induction n with
+  | zero => simp [memPartitionSet]
+  | succ n ih =>
+    classical
+    rw [memPartitionSet_succ, memPartition_succ]
+    refine ⟨memPartitionSet f n a, ?_⟩
+    split_ifs <;> simp [ih]
+
+lemma mem_memPartitionSet (f : ℕ → Set α) (n : ℕ) (a : α) : a ∈ memPartitionSet f n a := by
+  induction n with
+  | zero => simp [memPartitionSet]
+  | succ n ih =>
+    classical
+    rw [memPartitionSet_succ]
+    split_ifs with h <;> exact ⟨ih, h⟩
+
+lemma memPartitionSet_eq_iff {f : ℕ → Set α} {n : ℕ} (a : α) {s : Set α}
+    (hs : s ∈ memPartition f n) :
+    memPartitionSet f n a = s ↔ a ∈ s := by
+  refine ⟨fun h ↦ h ▸ mem_memPartitionSet f n a, fun h ↦ ?_⟩
+  by_contra h_ne
+  have h_disj : Disjoint s (memPartitionSet f n a) :=
+    disjoint_memPartition f n hs (memPartitionSet_mem f n a) (Ne.symm h_ne)
+  refine absurd h_disj ?_
+  rw [not_disjoint_iff_nonempty_inter]
+  exact ⟨a, h, mem_memPartitionSet f n a⟩
+
+lemma memPartitionSet_of_mem {f : ℕ → Set α} {n : ℕ} {a : α} {s : Set α}
+    (hs : s ∈ memPartition f n) (ha : a ∈ s) :
+    memPartitionSet f n a = s :=
+  (memPartitionSet_eq_iff a hs).mpr ha

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -9,7 +9,6 @@ import Mathlib.GroupTheory.Coset
 import Mathlib.Logic.Equiv.Fin
 import Mathlib.MeasureTheory.MeasurableSpace.Defs
 import Mathlib.Order.Filter.SmallSets
-import Mathlib.Order.Filter.CountableSeparatingOn
 import Mathlib.Order.LiminfLimsup
 import Mathlib.Data.Set.UnionLift
 
@@ -1949,73 +1948,6 @@ theorem MeasurableSpace.comap_compl {m' : MeasurableSpace β} [BooleanAlgebra β
   MeasurableSpace.comap_compl (fun _ _ ↦ measurableSet_top) _
 #align measurable_space.comap_not MeasurableSpace.comap_not
 
-section CountablyGenerated
-
-namespace MeasurableSpace
-
-variable (α)
-
-/-- We say a measurable space is countably generated
-if it can be generated by a countable set of sets. -/
-class CountablyGenerated [m : MeasurableSpace α] : Prop where
-  isCountablyGenerated : ∃ b : Set (Set α), b.Countable ∧ m = generateFrom b
-#align measurable_space.countably_generated MeasurableSpace.CountablyGenerated
-
-variable {α}
-
-theorem CountablyGenerated.comap [m : MeasurableSpace β] [h : CountablyGenerated β] (f : α → β) :
-    @CountablyGenerated α (.comap f m) := by
-  rcases h with ⟨⟨b, hbc, rfl⟩⟩
-  rw [comap_generateFrom]
-  letI := generateFrom (preimage f '' b)
-  exact ⟨_, hbc.image _, rfl⟩
-
-theorem CountablyGenerated.sup {m₁ m₂ : MeasurableSpace β} (h₁ : @CountablyGenerated β m₁)
-    (h₂ : @CountablyGenerated β m₂) : @CountablyGenerated β (m₁ ⊔ m₂) := by
-  rcases h₁ with ⟨⟨b₁, hb₁c, rfl⟩⟩
-  rcases h₂ with ⟨⟨b₂, hb₂c, rfl⟩⟩
-  exact @mk _ (_ ⊔ _) ⟨_, hb₁c.union hb₂c, generateFrom_sup_generateFrom⟩
-
-instance (priority := 100) [MeasurableSpace α] [Finite α] : CountablyGenerated α where
-  isCountablyGenerated :=
-    ⟨{s | MeasurableSet s}, Set.to_countable _, generateFrom_measurableSet.symm⟩
-
-instance [MeasurableSpace α] [CountablyGenerated α] {p : α → Prop} :
-    CountablyGenerated { x // p x } := .comap _
-
-instance [MeasurableSpace α] [CountablyGenerated α] [MeasurableSpace β] [CountablyGenerated β] :
-    CountablyGenerated (α × β) :=
-  .sup (.comap Prod.fst) (.comap Prod.snd)
-
-instance [MeasurableSpace α] {s : Set α} [h : CountablyGenerated s] [MeasurableSingletonClass s] :
-    HasCountableSeparatingOn α MeasurableSet s := by
-  suffices HasCountableSeparatingOn s MeasurableSet univ from this.of_subtype fun _ ↦ id
-  rcases h.1 with ⟨b, hbc, hb⟩
-  refine ⟨⟨b, hbc, fun t ht ↦ hb.symm ▸ .basic t ht, fun x _ y _ h ↦ ?_⟩⟩
-  rw [← forall_generateFrom_mem_iff_mem_iff, ← hb] at h
-  simpa using h {y}
-
-variable (α)
-
-open scoped Classical
-
-/-- 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). -/
-theorem measurable_injection_nat_bool_of_countablyGenerated [MeasurableSpace α]
-    [HasCountableSeparatingOn α MeasurableSet univ] :
-    ∃ f : α → ℕ → Bool, Measurable f ∧ Function.Injective f := by
-  rcases exists_seq_separating α MeasurableSet.empty univ with ⟨e, hem, he⟩
-  refine ⟨(· ∈ e ·), ?_, ?_⟩
-  · rw [measurable_pi_iff]
-    refine fun n ↦ measurable_to_bool ?_
-    simpa only [preimage, mem_singleton_iff, Bool.decide_iff, setOf_mem_eq] using hem n
-  · exact fun x y h ↦ he x trivial y trivial fun n ↦ decide_eq_decide.1 <| congr_fun h _
-#align measurable_space.measurable_injection_nat_bool_of_countably_generated MeasurableSpace.measurable_injection_nat_bool_of_countablyGenerated
-
-end MeasurableSpace
-
-end CountablyGenerated
-
 namespace Filter
 
 variable [MeasurableSpace α]