refactor: change the definition of the stopped sigma-algebra (leanprover-community#42021)

Change the definition of [MeasureTheory.IsStoppingTime.measurableSpace](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Process/Stopping.html#MeasureTheory.IsStoppingTime.measurableSpace) to require that it contains only sets that are measurable wrt `⨆ t, f t` where `f` is the filtration. This is what is done for instance in _Semimartingale Theory and Stochastic Calculus_ by He Wang Yan and is needed in the Brownian motion project.

Author: EtienneC30

Mathlib/Probability/Process/Stopping.lean

@@ -442,7 +442,7 @@ variable [Preorder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι}
 /-- The associated σ-algebra with a stopping time. -/
 @[instance_reducible]
 protected def measurableSpace (hτ : IsStoppingTime f τ) : MeasurableSpace Ω where
-  MeasurableSet' s := MeasurableSet s ∧ ∀ i : ι, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i})
+  MeasurableSet' s := MeasurableSet[⨆ t, f t] s ∧ ∀ i : ι, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i})
   measurableSet_empty := by simp
   measurableSet_compl s hs := by
     refine ⟨hs.1.compl, fun i ↦ ?_⟩
@@ -462,7 +462,7 @@ protected def measurableSpace (hτ : IsStoppingTime f τ) : MeasurableSpace Ω w
 
 protected theorem measurableSet (hτ : IsStoppingTime f τ) (s : Set Ω) :
     MeasurableSet[hτ.measurableSpace] s
-      ↔ MeasurableSet s ∧ ∀ i : ι, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i}) :=
+      ↔ MeasurableSet[⨆ t, f t] s ∧ ∀ i : ι, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i}) :=
   Iff.rfl
 
 theorem measurableSpace_mono (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) (hle : τ ≤ π) :
@@ -475,7 +475,11 @@ theorem measurableSpace_mono (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f
     intro hle' _
     exact le_trans (hle _) hle'
 
-theorem measurableSpace_le (hτ : IsStoppingTime f τ) : hτ.measurableSpace ≤ m := fun _ hs ↦ hs.1
+theorem measurableSpace_le' (hτ : IsStoppingTime f τ) :
+    hτ.measurableSpace ≤ ⨆ t, f t := fun _ hs ↦ hs.1
+
+theorem measurableSpace_le (hτ : IsStoppingTime f τ) : hτ.measurableSpace ≤ m :=
+  hτ.measurableSpace_le'.trans (iSup_le f.le)
 
 @[simp]
 theorem measurableSpace_const (f : Filtration ι m) (i : ι) :
@@ -485,7 +489,7 @@ theorem measurableSpace_const (f : Filtration ι m) (i : ι) :
   constructor <;> intro h
   · have h' := h.2 i
     simpa only [le_refl, Set.ofPred_true, Set.inter_univ] using h'
-  · refine ⟨f.le i _ h, fun j ↦ ?_⟩
+  · refine ⟨le_iSup f i s h, fun j ↦ ?_⟩
     by_cases hij : i ≤ j
     · norm_cast
       simp only [hij, Set.ofPred_true, Set.inter_univ]
@@ -504,7 +508,7 @@ theorem measurableSet_inter_eq_iff (hτ : IsStoppingTime f τ) (s : Set Ω) (i :
     rw [hxi]
   constructor <;> intro h
   · simpa [Set.inter_assoc, this] using h.2 i
-  · refine ⟨f.le i _ h, fun j ↦ ?_⟩
+  · refine ⟨le_iSup f i _ h, fun j ↦ ?_⟩
     rw [Set.inter_assoc, this]
     by_cases hij : i ≤ j
     · norm_cast
@@ -550,7 +554,7 @@ variable [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι}
 
 protected theorem measurableSet_le' (hτ : IsStoppingTime f τ) (i : ι) :
     MeasurableSet[hτ.measurableSpace] {ω | τ ω ≤ i} := by
-  refine ⟨f.le i _ (hτ i), fun j ↦ ?_⟩
+  refine ⟨le_iSup f i _ (hτ i), fun j ↦ ?_⟩
   have : {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | τ ω ≤ j} = {ω : Ω | τ ω ≤ min i j} := by
     ext1 ω
     simp [Set.mem_inter_iff, Set.mem_ofPred_eq]
@@ -649,11 +653,20 @@ protected theorem measurable' [TopologicalSpace ι]
     [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) :
     Measurable τ := hτ.measurable.mono (measurableSpace_le hτ) le_rfl
 
+protected theorem measurable_iSup [TopologicalSpace ι]
+    [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) :
+    Measurable[⨆ t, f t] τ := hτ.measurable.mono (measurableSpace_le' hτ) le_rfl
+
 protected lemma measurableSet_eq_top [TopologicalSpace ι]
     [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) :
     MeasurableSet {ω | τ ω = ⊤} :=
   (measurableSet_singleton _).preimage hτ.measurable'
 
+protected lemma measurableSet_eq_top' [TopologicalSpace ι]
+    [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) :
+    MeasurableSet[⨆ t, f t] {ω | τ ω = ⊤} :=
+  (measurableSet_singleton _).preimage hτ.measurable_iSup
+
 protected theorem measurable_of_le [TopologicalSpace ι]
     [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) {i : ι}
     (hτ_le : ∀ ω, τ ω ≤ i) : Measurable[f i] τ :=
@@ -698,7 +711,7 @@ theorem measurableSet_inter_le [TopologicalSpace ι] [SecondCountableTopology ι
     ext ω
     by_cases hτi : τ ω ≤ i <;> grind
   simp_rw [h_eq]
-  refine ⟨hs.1.inter (measurableSet_le hτ.measurable' hπ.measurable'), fun i ↦ ?_⟩
+  refine ⟨hs.1.inter (measurableSet_le hτ.measurable_iSup hπ.measurable_iSup), fun i ↦ ?_⟩
   refine ((hs.2 i).inter ((hτ.min hπ) i)).inter ?_
   apply @measurableSet_le _ _ _ _ _ (Filtration.seq f i) _ _ _ _ _ ?_ ?_
   · exact (hτ.min_const i).measurable_of_le fun _ => min_le_right _ _
@@ -730,7 +743,7 @@ theorem measurableSet_le_stopping_time [TopologicalSpace ι] [SecondCountableTop
     [OrderTopology ι] (hτ : IsStoppingTime f τ)
     (hπ : IsStoppingTime f π) : MeasurableSet[hτ.measurableSpace] {ω | τ ω ≤ π ω} := by
   rw [hτ.measurableSet]
-  refine ⟨measurableSet_le hτ.measurable' hπ.measurable', fun j ↦ ?_⟩
+  refine ⟨measurableSet_le hτ.measurable_iSup hπ.measurable_iSup, fun j ↦ ?_⟩
   have : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j ≤ min (π ω) j} ∩ {ω | τ ω ≤ j} := by
     ext
     simpa using fun a b ↦ Std.IsPreorder.le_trans _ _ _ a b
@@ -1056,7 +1069,7 @@ theorem measurable_stoppedValue [PseudoMetrizableSpace β] [MeasurableSpace β]
       exact (h_seq_tendsto t).exists
   rw [this]
   refine MeasurableSet.union ?_ ?_
-  · exact MeasurableSet.iUnion fun i ↦ f.le (seq i) _
+  · exact MeasurableSet.iUnion fun i ↦ le_iSup f (seq i) _
       (measurableSet_preimage_stoppedValue_inter hf_prog hτ ht (seq i))
   · have : stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤}
        = (fun ω ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω | τ ω = ⊤} := by
@@ -1066,9 +1079,9 @@ theorem measurable_stoppedValue [PseudoMetrizableSpace β] [MeasurableSpace β]
       intro h
       simp [h]
     rw [this]
-    refine MeasurableSet.inter (ht.preimage ?_) hτ.measurableSet_eq_top
+    refine MeasurableSet.inter (ht.preimage ?_) hτ.measurableSet_eq_top'
     exact (hf_prog.stronglyAdapted (Classical.arbitrary ι)).measurable.mono
-      (f.le (Classical.arbitrary ι)) le_rfl
+      (le_iSup f (Classical.arbitrary ι)) le_rfl
 
 end Progressive