feat(probability/stopping): add properties of the measurable space ge…

…nerated by a stopping time (#13909)

- add lemmas stating that various sets are measurable with respect to that space
- describe the sigma algebra generated by the minimum of two stopping times
- use the results to generalize `is_stopping_time.measurable_set_eq_const` from nat to first countable linear orders and rename it to `is_stopping_time.measurable_space_eq'` to have a name similar to `is_stopping_time.measurable_set_eq`.

src/probability/martingale.lean

@@ -392,7 +392,7 @@ begin
   classical,
   specialize hf (s.piecewise (λ _, i) (λ _, j)) _
     (is_stopping_time_piecewise_const hij hs)
-    (is_stopping_time_const j) (λ x, (ite_le_sup _ _ _).trans (max_eq_right hij).le)
+    (is_stopping_time_const 𝒢 j) (λ x, (ite_le_sup _ _ _).trans (max_eq_right hij).le)
     ⟨j, λ x, le_rfl⟩,
   rwa [stopped_value_const, stopped_value_piecewise_const,
     integral_piecewise (𝒢.le _ _ hs) (hint _).integrable_on (hint _).integrable_on,

src/probability/stopping.lean

@@ -388,7 +388,7 @@ Intuitively, the stopping time `τ` describes some stopping rule such that at ti
 def is_stopping_time [preorder ι] (f : filtration ι m) (τ : α → ι) :=
 ∀ i : ι, measurable_set[f i] $ {x | τ x ≤ i}
 
-lemma is_stopping_time_const [preorder ι] {f : filtration ι m} (i : ι) :
+lemma is_stopping_time_const [preorder ι] (f : filtration ι m) (i : ι) :
   is_stopping_time f (λ x, i) :=
 λ j, by simp only [measurable_set.const]
 
@@ -397,7 +397,7 @@ section measurable_set
 section preorder
 variables [preorder ι] {f : filtration ι m} {τ : α → ι}
 
-lemma is_stopping_time.measurable_set_le (hτ : is_stopping_time f τ) (i : ι) :
+protected lemma is_stopping_time.measurable_set_le (hτ : is_stopping_time f τ) (i : ι) :
   measurable_set[f i] {x | τ x ≤ i} :=
 hτ i
 
@@ -531,6 +531,11 @@ begin
   exact (hτ i).inter (hπ i),
 end
 
+protected lemma max_const [linear_order ι] {f : filtration ι m} {τ : α → ι}
+  (hτ : is_stopping_time f τ) (i : ι) :
+  is_stopping_time f (λ x, max (τ x) i) :=
+hτ.max (is_stopping_time_const f i)
+
 protected lemma min [linear_order ι] {f : filtration ι m} {τ π : α → ι}
   (hτ : is_stopping_time f τ) (hπ : is_stopping_time f π) :
   is_stopping_time f (λ x, min (τ x) (π x)) :=
@@ -540,6 +545,11 @@ begin
   exact (hτ i).union (hπ i),
 end
 
+protected lemma min_const [linear_order ι] {f : filtration ι m} {τ : α → ι}
+  (hτ : is_stopping_time f τ) (i : ι) :
+  is_stopping_time f (λ x, min (τ x) i) :=
+hτ.min (is_stopping_time_const f i)
+
 lemma add_const [add_group ι] [preorder ι] [covariant_class ι ι (function.swap (+)) (≤)]
   [covariant_class ι ι (+) (≤)]
   {f : filtration ι m} {τ : α → ι} (hτ : is_stopping_time f τ) {i : ι} (hi : 0 ≤ i) :
@@ -584,11 +594,10 @@ end
 
 section preorder
 
-variables [preorder ι] {f : filtration ι m}
+variables [preorder ι] {f : filtration ι m} {τ π : α → ι}
 
 /-- The associated σ-algebra with a stopping time. -/
-protected def measurable_space
-  {τ : α → ι} (hτ : is_stopping_time f τ) : measurable_space α :=
+protected def measurable_space (hτ : is_stopping_time f τ) : measurable_space α :=
 { measurable_set' := λ s, ∀ i : ι, measurable_set[f i] (s ∩ {x | τ x ≤ i}),
   measurable_set_empty :=
     λ i, (set.empty_inter {x | τ x ≤ i}).symm ▸ @measurable_set.empty _ (f i),
@@ -609,14 +618,13 @@ protected def measurable_space
       exact measurable_set.Union (hs i),
     end }
 
-@[protected]
-lemma measurable_set {τ : α → ι} (hτ : is_stopping_time f τ) (s : set α) :
+protected lemma measurable_set (hτ : is_stopping_time f τ) (s : set α) :
   measurable_set[hτ.measurable_space] s ↔
   ∀ i : ι, measurable_set[f i] (s ∩ {x | τ x ≤ i}) :=
 iff.rfl
 
 lemma measurable_space_mono
-  {τ π : α → ι} (hτ : is_stopping_time f τ) (hπ : is_stopping_time f π) (hle : τ ≤ π) :
+  (hτ : is_stopping_time f τ) (hπ : is_stopping_time f π) (hle : τ ≤ π) :
   hτ.measurable_space ≤ hπ.measurable_space :=
 begin
   intros s hs i,
@@ -628,7 +636,7 @@ begin
     exact le_trans (hle _) hle' },
 end
 
-lemma measurable_space_le [encodable ι] {τ : α → ι} (hτ : is_stopping_time f τ) :
+lemma measurable_space_le [encodable ι] (hτ : is_stopping_time f τ) :
   hτ.measurable_space ≤ m :=
 begin
   intros s hs,
@@ -641,49 +649,172 @@ begin
       exact hx } }
 end
 
-section nat
+@[simp] lemma measurable_space_const (f : filtration ι m) (i : ι) :
+  (is_stopping_time_const f i).measurable_space = f i :=
+begin
+  ext1 s,
+  change measurable_set[(is_stopping_time_const f i).measurable_space] s ↔ measurable_set[f i] s,
+  rw is_stopping_time.measurable_set,
+  split; intro h,
+  { specialize h i,
+    simpa only [le_refl, set.set_of_true, set.inter_univ] using h, },
+  { intro j,
+    by_cases hij : i ≤ j,
+    { simp only [hij, set.set_of_true, set.inter_univ],
+      exact f.mono hij _ h, },
+    { simp only [hij, set.set_of_false, set.inter_empty, measurable_set.empty], }, },
+end
 
-lemma measurable_set_eq_const {f : filtration ℕ m}
-  {τ : α → ℕ} (hτ : is_stopping_time f τ) (i : ℕ) :
-  measurable_set[hτ.measurable_space] {x | τ x = i} :=
+lemma measurable_set_inter_eq_iff (hτ : is_stopping_time f τ) (s : set α) (i : ι) :
+  measurable_set[hτ.measurable_space] (s ∩ {x | τ x = i})
+    ↔ measurable_set[f i] (s ∩ {x | τ x = i}) :=
 begin
-  rw hτ.measurable_set,
-  intro j,
-  by_cases i ≤ j,
-  { rw (_ : {x | τ x = i} ∩ {x | τ x ≤ j} = {x | τ x = i}),
-    { exact hτ.measurable_set_eq_le h },
-    { ext,
-      simp only [set.mem_inter_eq, and_iff_left_iff_imp, set.mem_set_of_eq],
-      rintro rfl,
-      assumption } },
-  { rw (_ : {x | τ x = i} ∩ {x | τ x ≤ j} = ∅),
-    { exact @measurable_set.empty _ (f j) },
-    { ext,
-      simp only [set.mem_empty_eq, set.mem_inter_eq, not_and, not_le, set.mem_set_of_eq, iff_false],
-      rintro rfl,
-      rwa not_le at h } }
+  have : ∀ j, ({x : α | τ x = i} ∩ {x : α | τ x ≤ j}) = {x : α | τ x = i} ∩ {x | i ≤ j},
+  { intro j,
+    ext1 x,
+    simp only [set.mem_inter_eq, set.mem_set_of_eq, and.congr_right_iff],
+    intro hxi,
+    rw hxi, },
+  split; intro h,
+  { specialize h i,
+    simpa only [set.inter_assoc, this, le_refl, set.set_of_true, set.inter_univ] using h, },
+  { intro j,
+    rw [set.inter_assoc, this],
+    by_cases hij : i ≤ j,
+    { simp only [hij, set.set_of_true, set.inter_univ],
+      exact f.mono hij _ h, },
+    { simp [hij], }, },
 end
 
-end nat
+lemma measurable_space_le_of_le_const (hτ : is_stopping_time f τ) {i : ι} (hτ_le : ∀ x, τ x ≤ i) :
+  hτ.measurable_space ≤ f i :=
+(measurable_space_mono hτ _ hτ_le).trans (is_stopping_time.measurable_space_const _ _).le
+
+lemma le_measurable_space_of_const_le (hτ : is_stopping_time f τ) {i : ι} (hτ_le : ∀ x, i ≤ τ x) :
+  f i ≤ hτ.measurable_space :=
+(is_stopping_time.measurable_space_const _ _).symm.le.trans (measurable_space_mono _ hτ hτ_le)
 
 end preorder
 
 section linear_order
 
-variable [linear_order ι]
+variables [linear_order ι] {f : filtration ι m} {τ π : α → ι}
+
+protected lemma measurable_set_le' (hτ : is_stopping_time f τ) (i : ι) :
+  measurable_set[hτ.measurable_space] {x | τ x ≤ i} :=
+begin
+  intro j,
+  have : {x : α | τ x ≤ i} ∩ {x : α | τ x ≤ j} = {x : α | τ x ≤ min i j},
+  { ext1 x, simp only [set.mem_inter_eq, set.mem_set_of_eq, le_min_iff], },
+  rw this,
+  exact f.mono (min_le_right i j) _ (hτ _),
+end
+
+protected lemma measurable_set_gt' (hτ : is_stopping_time f τ) (i : ι) :
+  measurable_set[hτ.measurable_space] {x | i < τ x} :=
+begin
+  have : {x : α | i < τ x} = {x : α | τ x ≤ i}ᶜ, by { ext1 x, simp, },
+  rw this,
+  exact (hτ.measurable_set_le' i).compl,
+end
+
+protected lemma measurable_set_eq' [topological_space ι] [order_topology ι]
+  [first_countable_topology ι]
+  (hτ : is_stopping_time f τ) (i : ι) :
+  measurable_set[hτ.measurable_space] {x | τ x = i} :=
+begin
+  rw [← set.univ_inter {x | τ x = i}, measurable_set_inter_eq_iff, set.univ_inter],
+  exact hτ.measurable_set_eq i,
+end
 
-lemma measurable [topological_space ι] [measurable_space ι]
+protected lemma measurable_set_ge' [topological_space ι] [order_topology ι]
+  [first_countable_topology ι]
+  (hτ : is_stopping_time f τ) (i : ι) :
+  measurable_set[hτ.measurable_space] {x | i ≤ τ x} :=
+begin
+  have : {x | i ≤ τ x} = {x | τ x = i} ∪ {x | i < τ x},
+  { ext1 x,
+    simp only [le_iff_lt_or_eq, set.mem_set_of_eq, set.mem_union_eq],
+    rw [@eq_comm _ i, or_comm], },
+  rw this,
+  exact (hτ.measurable_set_eq' i).union (hτ.measurable_set_gt' i),
+end
+
+protected lemma measurable_set_lt' [topological_space ι] [order_topology ι]
+  [first_countable_topology ι]
+  (hτ : is_stopping_time f τ) (i : ι) :
+  measurable_set[hτ.measurable_space] {x | τ x < i} :=
+begin
+  have : {x | τ x < i} = {x | τ x ≤ i} \ {x | τ x = i},
+  { ext1 x,
+    simp only [lt_iff_le_and_ne, set.mem_set_of_eq, set.mem_diff], },
+  rw this,
+  exact (hτ.measurable_set_le' i).diff (hτ.measurable_set_eq' i),
+end
+
+protected lemma measurable [topological_space ι] [measurable_space ι]
   [borel_space ι] [order_topology ι] [second_countable_topology ι]
-  {f : filtration ι m} {τ : α → ι} (hτ : is_stopping_time f τ) :
+  (hτ : is_stopping_time f τ) :
   measurable[hτ.measurable_space] τ :=
+@measurable_of_Iic ι α _ _ _ hτ.measurable_space _ _ _ _ (λ i, hτ.measurable_set_le' i)
+
+protected lemma measurable_of_le [topological_space ι] [measurable_space ι]
+  [borel_space ι] [order_topology ι] [second_countable_topology ι]
+  (hτ : is_stopping_time f τ) {i : ι} (hτ_le : ∀ x, τ x ≤ i) :
+  measurable[f i] τ :=
+hτ.measurable.mono (measurable_space_le_of_le_const _ hτ_le) le_rfl
+
+lemma measurable_space_min (hτ : is_stopping_time f τ) (hπ : is_stopping_time f π) :
+  (hτ.min hπ).measurable_space = hτ.measurable_space ⊓ hπ.measurable_space :=
 begin
-  refine @measurable_of_Iic ι α _ _ _ hτ.measurable_space _ _ _ _ _,
-  simp_rw [hτ.measurable_set, set.preimage, set.mem_Iic],
-  intros i j,
-  rw (_ : {x | τ x ≤ i} ∩ {x | τ x ≤ j} = {x | τ x ≤ min i j}),
-  { exact f.mono (min_le_right i j) _ (hτ (min i j)) },
-  { ext,
-    simp only [set.mem_inter_eq, iff_self, le_min_iff, set.mem_set_of_eq] }
+  refine le_antisymm _ _,
+  { exact le_inf (is_stopping_time.measurable_space_mono _ hτ (λ _, min_le_left _ _))
+      (is_stopping_time.measurable_space_mono _ hπ (λ _, min_le_right _ _)), },
+  { intro s,
+    change measurable_set[hτ.measurable_space] s ∧ measurable_set[hπ.measurable_space] s
+      → measurable_set[(hτ.min hπ).measurable_space] s,
+    simp_rw is_stopping_time.measurable_set,
+    have : ∀ i, {x | min (τ x) (π x) ≤ i} = {x | τ x ≤ i} ∪ {x | π x ≤ i},
+    { intro i, ext1 x, simp, },
+    simp_rw [this, set.inter_union_distrib_left],
+    exact λ h i, (h.left i).union (h.right i), },
+end
+
+lemma measurable_set_min_iff (hτ : is_stopping_time f τ) (hπ : is_stopping_time f π) (s : set α) :
+  measurable_set[(hτ.min hπ).measurable_space] s
+    ↔ measurable_set[hτ.measurable_space] s ∧ measurable_set[hπ.measurable_space] s :=
+by { rw measurable_space_min, refl, }
+
+lemma measurable_set_inter_le [topological_space ι] [second_countable_topology ι] [order_topology ι]
+  [measurable_space ι] [borel_space ι]
+  (hτ : is_stopping_time f τ) (hπ : is_stopping_time f π) (s : set α)
+  (hs : measurable_set[hτ.measurable_space] s) :
+  measurable_set[(hτ.min hπ).measurable_space] (s ∩ {x | τ x ≤ π x}) :=
+begin
+  simp_rw is_stopping_time.measurable_set at ⊢ hs,
+  intro i,
+  have : (s ∩ {x | τ x ≤ π x} ∩ {x | min (τ x) (π x) ≤ i})
+    = (s ∩ {x | τ x ≤ i}) ∩ {x | min (τ x) (π x) ≤ i} ∩ {x | min (τ x) i ≤ min (min (τ x) (π x)) i},
+  { ext1 x,
+    simp only [min_le_iff, set.mem_inter_eq, set.mem_set_of_eq, le_min_iff, le_refl, true_and,
+      and_true, true_or, or_true],
+    by_cases hτi : τ x ≤ i,
+    { simp only [hτi, true_or, and_true, and.congr_right_iff],
+      intro hx,
+      split; intro h,
+      { exact or.inl h, },
+      { cases h,
+        { exact h, },
+        { exact hτi.trans h, }, }, },
+    simp only [hτi, false_or, and_false, false_and, iff_false, not_and, not_le, and_imp],
+    refine λ hx hτ_le_π, lt_of_lt_of_le _ hτ_le_π,
+    rw ← not_le,
+    exact hτi, },
+  rw this,
+  refine ((hs i).inter ((hτ.min hπ) i)).inter _,
+  apply measurable_set_le,
+  { exact (hτ.min_const i).measurable_of_le (λ _, min_le_right _ _), },
+  { exact ((hτ.min hπ).min_const i).measurable_of_le (λ _, min_le_right _ _),  },
 end
 
 end linear_order
@@ -772,7 +903,7 @@ lemma prog_measurable.adapted_stopped_process
   adapted f (stopped_process u τ) :=
 (h.stopped_process hτ).adapted
 
-lemma prog_measurable.measurable_stopped_process
+lemma prog_measurable.strongly_measurable_stopped_process
   (hu : prog_measurable f u) (hτ : is_stopping_time f τ) (i : ι) :
   strongly_measurable (stopped_process u τ i) :=
 (hu.adapted_stopped_process hτ i).mono (f.le _)
@@ -846,10 +977,11 @@ lemma adapted.stopped_process_of_nat [topological_space β] [has_continuous_add
   adapted f (stopped_process u τ) :=
 (hu.prog_measurable_of_nat.stopped_process hτ).adapted
 
-lemma adapted.measurable_stopped_process_of_nat [topological_space β] [has_continuous_add β]
+lemma adapted.strongly_measurable_stopped_process_of_nat [topological_space β]
+  [has_continuous_add β]
   (hτ : is_stopping_time f τ) (hu : adapted f u) (n : ℕ) :
   strongly_measurable (stopped_process u τ n) :=
-hu.prog_measurable_of_nat.measurable_stopped_process hτ n
+hu.prog_measurable_of_nat.strongly_measurable_stopped_process hτ n
 
 lemma stopped_value_eq {N : ℕ} (hbdd : ∀ x, τ x ≤ N) :
   stopped_value u τ =
@@ -961,7 +1093,8 @@ end
 
 lemma is_stopping_time_piecewise_const (hij : i ≤ j) (hs : measurable_set[𝒢 i] s) :
   is_stopping_time 𝒢 (s.piecewise (λ _, i) (λ _, j)) :=
-(is_stopping_time_const i).piecewise_of_le (is_stopping_time_const j) (λ x, le_rfl) (λ _, hij) hs
+(is_stopping_time_const 𝒢 i).piecewise_of_le (is_stopping_time_const 𝒢 j)
+  (λ x, le_rfl) (λ _, hij) hs
 
 lemma stopped_value_piecewise_const {ι' : Type*} {i j : ι'} {f : ι' → α → ℝ} :
   stopped_value f (s.piecewise (λ _, i) (λ _, j)) = s.piecewise (f i) (f j) :=