feat(Probability): Countable infimum of stopping times is a stopping time

Mathlib/Probability/Process/Filtration.lean

@@ -22,6 +22,9 @@ This file defines filtrations of a measurable space and σ-finite filtrations.
   `μ` if for all `i`, `μ.trim (f.le i)` is σ-finite.
 * `MeasureTheory.Filtration.natural`: the smallest filtration that makes a process adapted. That
   notion `adapted` is not defined yet in this file. See `MeasureTheory.adapted`.
+* `MeasureTheory.Filtration.rightCont`: the right-continuation of a filtration.
+* `MeasureTheory.Filtration.IsRightContinuous`: a filtration is right-continuous if it is equal
+  to its right-continuation.
 
 ## Main results
 
@@ -245,6 +248,166 @@ end OfSet
 
 namespace Filtration
 
+section IsRightContinuous
+
+open scoped Classical in
+/-- Given a filtration `𝓕`, its **right continuation** is the filtration `𝓕₊` defined as follows:
+- If `i` is isolated on the right, then `𝓕₊ i := 𝓕 i`;
+- Otherwise, `𝓕₊ i := ⨅ j > i, 𝓕 j`.
+It is sometimes simply defined as `𝓕₊ i := ⨅ j > i, 𝓕 j` when the index type is `ℝ`. In the
+general case this is not ideal however. If `i` is maximal for instance, then `𝓕₊ i = ⊤`, which
+is inconvenient because `𝓕₊` is not  a `Filtration ι m` anymore. If the index type
+is discrete (such as `ℕ`), then we would have `𝓕 = 𝓕₊` (i.e. `𝓕` is right-continuous) only if
+`𝓕` is constant.
+
+To avoid requiring a `TopologicalSpace` instance on `ι` in the definition, we endow `ι` with
+the order topology `Preorder.topology` inside the definition. Say you write a statement about
+`𝓕₊` which does not require a `TopologicalSpace` structure on `ι`,
+but you wish to use a statement which requires a topology (such as `rightCont_def`).
+Then you can endow `ι` with
+the order topology by writing
+```lean
+  letI := Preorder.topology ι
+  haveI : OrderTopology ι := ⟨rfl⟩
+``` -/
+noncomputable def rightCont [PartialOrder ι] (𝓕 : Filtration ι m) : Filtration ι m :=
+  letI : TopologicalSpace ι := Preorder.topology ι
+  { seq i := if (𝓝[>] i).NeBot then ⨅ j > i, 𝓕 j else 𝓕 i
+    mono' i j hij := by
+      simp only [gt_iff_lt]
+      split_ifs with hi hj hj
+      · exact le_iInf₂ fun k hkj ↦ iInf₂_le k (hij.trans_lt hkj)
+      · obtain rfl | hj := eq_or_ne j i
+        · contradiction
+        · exact iInf₂_le j (lt_of_le_of_ne hij hj.symm)
+      · exact le_iInf₂ fun k hk ↦ 𝓕.mono (hij.trans hk.le)
+      · exact 𝓕.mono hij
+    le' i := by
+      split_ifs with hi
+      · obtain ⟨j, hj⟩ := (frequently_gt_nhds i).exists
+        exact iInf₂_le_of_le j hj (𝓕.le j)
+      · exact 𝓕.le i }
+
+@[inherit_doc] scoped postfix:max "₊" => rightCont
+
+open scoped Classical in
+lemma rightCont_def [PartialOrder ι] [TopologicalSpace ι] [OrderTopology ι]
+    (𝓕 : Filtration ι m) (i : ι) :
+    𝓕₊ i = if (𝓝[>] i).NeBot then ⨅ j > i, 𝓕 j else 𝓕 i := by
+  simp only [rightCont, OrderTopology.topology_eq_generate_intervals]
+
+lemma rightCont_eq_of_nhdsGT_eq_bot [PartialOrder ι] [TopologicalSpace ι] [OrderTopology ι]
+    (𝓕 : Filtration ι m) {i : ι} (hi : 𝓝[>] i = ⊥) :
+    𝓕₊ i = 𝓕 i := by
+  rw [rightCont_def, hi, neBot_iff, ne_self_iff_false, if_false]
+
+/-- If the index type is a `SuccOrder`, then `𝓕₊ = 𝓕`. -/
+lemma rightCont_eq_self [LinearOrder ι] [SuccOrder ι] (𝓕 : Filtration ι m) :
+    𝓕₊ = 𝓕 := by
+  letI := Preorder.topology ι; haveI : OrderTopology ι := ⟨rfl⟩
+  ext _
+  rw [rightCont_eq_of_nhdsGT_eq_bot _ SuccOrder.nhdsGT]
+
+lemma rightCont_eq_of_isMax [PartialOrder ι] (𝓕 : Filtration ι m) {i : ι} (hi : IsMax i) :
+    𝓕₊ i = 𝓕 i := by
+  letI := Preorder.topology ι; haveI : OrderTopology ι := ⟨rfl⟩
+  exact rightCont_eq_of_nhdsGT_eq_bot _ (hi.Ioi_eq ▸ nhdsWithin_empty i)
+
+lemma rightCont_eq_of_exists_gt [LinearOrder ι] (𝓕 : Filtration ι m) {i : ι}
+    (hi : ∃ j > i, Set.Ioo i j = ∅) :
+    𝓕₊ i = 𝓕 i := by
+  letI := Preorder.topology ι; haveI : OrderTopology ι := ⟨rfl⟩
+  obtain ⟨j, hij, hIoo⟩ := hi
+  have hcov : i ⋖ j := covBy_iff_Ioo_eq.mpr ⟨hij, hIoo⟩
+  exact rightCont_eq_of_nhdsGT_eq_bot _ <| CovBy.nhdsGT hcov
+
+/-- If `i` is not isolated on the right, then `𝓕₊ i = ⨅ j > i, 𝓕 j`. This is for instance the case
+when `ι` is a densely ordered linear order with no maximal elements and equipped with the order
+topology, see `rightCont_eq`. -/
+lemma rightCont_eq_of_neBot_nhdsGT [PartialOrder ι] [TopologicalSpace ι] [OrderTopology ι]
+    (𝓕 : Filtration ι m) (i : ι) [(𝓝[>] i).NeBot] :
+    𝓕₊ i = ⨅ j > i, 𝓕 j := by
+  rw [rightCont_def, if_pos ‹(𝓝[>] i).NeBot›]
+
+lemma rightCont_eq_of_not_isMax [LinearOrder ι] [DenselyOrdered ι]
+    (𝓕 : Filtration ι m) {i : ι} (hi : ¬IsMax i) :
+    𝓕₊ i = ⨅ j > i, 𝓕 j := by
+  letI := Preorder.topology ι; haveI : OrderTopology ι := ⟨rfl⟩
+  have : (𝓝[>] i).NeBot := nhdsGT_neBot_of_exists_gt (not_isMax_iff.mp hi)
+  exact rightCont_eq_of_neBot_nhdsGT _ _
+
+/-- If `ι` is a densely ordered linear order with no maximal elements, then no point is isolated
+on the right, so that `𝓕₊ i = ⨅ j > i, 𝓕 j` holds for all `i`. This is in particular the
+case when `ι := ℝ≥0`. -/
+lemma rightCont_eq [LinearOrder ι] [DenselyOrdered ι] [NoMaxOrder ι]
+    (𝓕 : Filtration ι m) (i : ι) :
+    𝓕₊ i = ⨅ j > i, 𝓕 j := 𝓕.rightCont_eq_of_not_isMax (not_isMax i)
+
+variable [PartialOrder ι]
+
+lemma le_rightCont (𝓕 : Filtration ι m) : 𝓕 ≤ 𝓕₊ := by
+  letI := Preorder.topology ι; haveI : OrderTopology ι := ⟨rfl⟩
+  intro i
+  by_cases hne : (𝓝[>] i).NeBot
+  · rw [rightCont_eq_of_neBot_nhdsGT]
+    exact le_iInf₂ fun _ he => 𝓕.mono he.le
+  · rw [rightCont_def, if_neg hne]
+
+lemma rightCont_self (𝓕 : Filtration ι m) : 𝓕₊₊ = 𝓕₊ := by
+  letI := Preorder.topology ι; haveI : OrderTopology ι := ⟨rfl⟩
+  apply le_antisymm _ 𝓕₊.le_rightCont
+  intro i
+  by_cases hne : (𝓝[>] i).NeBot
+  · have hineq : (⨅ j > i, 𝓕₊ j) ≤ ⨅ j > i, 𝓕 j := by
+      apply le_iInf₂ fun u hu => ?_
+      have hiou : Set.Ioo i u ∈ 𝓝[>] i := by
+        rw [mem_nhdsWithin_iff_exists_mem_nhds_inter]
+        exact ⟨Set.Iio u, (isOpen_Iio' u).mem_nhds hu, fun _ hx ↦ ⟨hx.2, hx.1⟩⟩
+      obtain ⟨v, hv⟩ := hne.nonempty_of_mem hiou
+      have hle₁ : (⨅ j > i, 𝓕₊ j) ≤ 𝓕₊ v := iInf₂_le_of_le v hv.1 le_rfl
+      have hle₂ : 𝓕₊ v ≤ 𝓕 u := by
+        by_cases hnv : (𝓝[>] v).NeBot
+        · simpa [rightCont_eq_of_neBot_nhdsGT] using iInf₂_le_of_le u hv.2 le_rfl
+        · simpa [rightCont_def, hnv] using 𝓕.mono hv.2.le
+      exact hle₁.trans hle₂
+    simpa [rightCont_eq_of_neBot_nhdsGT] using hineq
+  · rw [rightCont_def, if_neg hne]
+
+/-- A filtration `𝓕` is right continuous if it is equal to its right continuation `𝓕₊`. -/
+class IsRightContinuous (𝓕 : Filtration ι m) where
+    /-- The right continuity property. -/
+    RC : 𝓕₊ ≤ 𝓕
+
+lemma IsRightContinuous.eq {𝓕 : Filtration ι m} [h : IsRightContinuous 𝓕] :
+    𝓕 = 𝓕₊ := le_antisymm 𝓕.le_rightCont h.RC
+
+lemma isRightContinuous_rightCont (𝓕 : Filtration ι m) : 𝓕₊.IsRightContinuous :=
+  ⟨(rightCont_self 𝓕).le⟩
+
+lemma IsRightContinuous.measurableSet {𝓕 : Filtration ι m} [IsRightContinuous 𝓕] {i : ι}
+    {s : Set Ω} (hs : MeasurableSet[𝓕₊ i] s) :
+    MeasurableSet[𝓕 i] s := IsRightContinuous.eq (𝓕 := 𝓕) ▸ hs
+
+/-- A filtration `𝓕` is said to satisfy the usual conditions if it is right continuous and `𝓕 0`
+  and consequently `𝓕 t` is complete (i.e. contains all null sets) for all `t`. -/
+class HasUsualConditions [OrderBot ι] (𝓕 : Filtration ι m) (μ : Measure Ω := by volume_tac)
+    extends IsRightContinuous 𝓕 where
+    /-- `𝓕 ⊥` contains all the null sets. -/
+    IsComplete ⦃s : Set Ω⦄ (hs : μ s = 0) : MeasurableSet[𝓕 ⊥] s
+
+variable [OrderBot ι]
+
+instance {𝓕 : Filtration ι m} {μ : Measure Ω} [u : HasUsualConditions 𝓕 μ] {i : ι} :
+    @Measure.IsComplete Ω (𝓕 i) (μ.trim <| 𝓕.le _) :=
+  ⟨fun _ hs ↦ 𝓕.mono bot_le _ <| u.2 (measure_eq_zero_of_trim_eq_zero (Filtration.le 𝓕 _) hs)⟩
+
+lemma HasUsualConditions.measurableSet_of_null
+    (𝓕 : Filtration ι m) {μ : Measure Ω} [u : HasUsualConditions 𝓕 μ] (s : Set Ω) (hs : μ s = 0) :
+    MeasurableSet[𝓕 ⊥] s :=
+  u.2 hs
+
+end IsRightContinuous
+
 variable {β : ι → Type*} [∀ i, TopologicalSpace (β i)] [∀ i, MetrizableSpace (β i)]
   [mβ : ∀ i, MeasurableSpace (β i)] [∀ i, BorelSpace (β i)]
   [Preorder ι]

Mathlib/Probability/Process/Stopping.lean

@@ -270,6 +270,104 @@ theorem isStoppingTime_of_measurableSet_eq [Preorder ι] [Countable ι] {f : Fil
 
 end Countable
 
+section IsRightContinuous
+
+open Filtration
+
+variable [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι]
+    [DenselyOrdered ι] [FirstCountableTopology ι] {f : Filtration ι m}
+
+lemma isStoppingTime_of_measurableSet_lt_of_isRightContinuous [NoMaxOrder ι]
+    {τ : Ω → WithTop ι} [hf : f.IsRightContinuous] (hτ : ∀ i, MeasurableSet[f i] {ω | τ ω < i}) :
+    IsStoppingTime f τ := by
+  intro i
+  obtain ⟨u, hu₁, hu₂, hu₃⟩ := exists_seq_strictAnti_tendsto i
+  refine MeasurableSet.of_compl ?_
+  rw [(_ : {ω | τ ω ≤ i}ᶜ = ⋃ n, {ω | u n ≤ τ ω})]
+  · refine hf.measurableSet ?_
+    simp_rw [f.rightCont_eq, MeasurableSpace.measurableSet_iInf]
+    intros j hj
+    obtain ⟨N, hN⟩ := (hu₃.eventually_le_const hj).exists
+    rw [(_ : ⋃ n, {ω | u n ≤ τ ω} = ⋃ n ≥ N, {ω | u n ≤ τ ω})]
+    · refine MeasurableSet.iUnion <| fun n ↦ MeasurableSet.iUnion <| fun hn ↦
+        f.mono ((hu₁.antitone hn).trans hN) _ <| MeasurableSet.of_compl ?_
+      rw [(by ext; simp : {ω | u n ≤ τ ω}ᶜ = {ω | τ ω < u n})]
+      exact hτ (u n)
+    · ext ω
+      simp only [Set.mem_iUnion, Set.mem_setOf_eq, ge_iff_le, exists_prop]
+      constructor
+      · rintro ⟨i, hle⟩
+        refine ⟨i + N, N.le_add_left i, le_trans ?_ hle⟩
+        norm_cast
+        exact hu₁.antitone <| i.le_add_right N
+      · rintro ⟨i, -, hi⟩
+        exact ⟨i, hi⟩
+  · ext ω
+    simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le, Set.mem_iUnion]
+    constructor
+    · intro h
+      by_cases hτ : τ ω = ⊤
+      · exact ⟨0, hτ ▸ le_top⟩
+      · have hlt : i < (τ ω).untop hτ := by
+          rwa [WithTop.lt_untop_iff]
+        obtain ⟨N, hN⟩ := (hu₃.eventually_le_const hlt).exists
+        refine ⟨N, WithTop.coe_le_iff.2 <| fun n hn ↦ hN.trans ?_⟩
+        simp [hn, WithTop.untop_coe]
+    · rintro ⟨j, hj⟩
+      refine lt_of_lt_of_le ?_ hj
+      norm_cast
+      exact hu₂ _
+
+lemma isStoppingTime_of_measurableSet_lt_of_isRightContinuous'
+    {τ : Ω → WithTop ι} [hf : f.IsRightContinuous]
+    (hτ1 : ∀ i, ¬ IsMax i → MeasurableSet[f i] {ω | τ ω < i})
+    (hτ2 : ∀ i, IsMax i → MeasurableSet[f i] {ω | τ ω ≤ i}) :
+    IsStoppingTime f τ := by
+  intro i
+  by_cases hmax : IsMax i
+  · rw [hf.eq, f.rightCont_eq_of_isMax hmax]
+    exact hτ2 i hmax
+  rw [hf.eq, f.rightCont_eq_of_not_isMax hmax]
+  rw [not_isMax_iff] at hmax
+  obtain ⟨j, hj⟩ := hmax
+  obtain ⟨u, hu₁, hu₂, hu₃⟩ := exists_seq_strictAnti_tendsto' hj
+  refine MeasurableSet.of_compl ?_
+  rw [(_ : {ω | τ ω ≤ i}ᶜ = ⋃ n, {ω | u n ≤ τ ω})]
+  · simp_rw [MeasurableSpace.measurableSet_iInf]
+    intros j hj
+    obtain ⟨N, hN⟩ := (hu₃.eventually_le_const hj).exists
+    rw [(_ : ⋃ n, {ω | u n ≤ τ ω} = ⋃ n > N, {ω | u n ≤ τ ω})]
+    · refine MeasurableSet.iUnion <| fun n ↦ MeasurableSet.iUnion <| fun hn ↦
+        f.mono ((hu₁ hn).le.trans hN) _ <| MeasurableSet.of_compl ?_
+      rw [(by ext; simp : {ω | u n ≤ τ ω}ᶜ = {ω | τ ω < u n})]
+      refine hτ1 (u n) <| not_isMax_iff.2 ⟨u N, hu₁ hn⟩
+    · ext ω
+      simp only [Set.mem_iUnion, Set.mem_setOf_eq, gt_iff_lt, exists_prop]
+      constructor
+      · rintro ⟨i, hle⟩
+        refine ⟨i + N + 1, by linarith, le_trans ?_ hle⟩
+        norm_cast
+        exact hu₁.antitone (by linarith)
+      · rintro ⟨i, -, hi⟩
+        exact ⟨i, hi⟩
+  · ext ω
+    simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le, Set.mem_iUnion]
+    constructor
+    · intro h
+      by_cases hτ : τ ω = ⊤
+      · exact ⟨0, hτ ▸ le_top⟩
+      · have hlt : i < (τ ω).untop hτ := by
+          rwa [WithTop.lt_untop_iff]
+        obtain ⟨N, hN⟩ := (hu₃.eventually_le_const hlt).exists
+        refine ⟨N, WithTop.coe_le_iff.2 <| fun n hn ↦ hN.trans ?_⟩
+        simp [hn, WithTop.untop_coe]
+    · rintro ⟨j, hj⟩
+      refine lt_of_lt_of_le ?_ hj
+      norm_cast
+      exact (hu₂ j).1
+
+end IsRightContinuous
+
 end MeasurableSet
 
 namespace IsStoppingTime
@@ -296,6 +394,26 @@ protected theorem min_const [LinearOrder ι] {f : Filtration ι m} {τ : Ω →
     (hτ : IsStoppingTime f τ) (i : ι) : IsStoppingTime f fun ω => min (τ ω) i :=
   hτ.min (isStoppingTime_const f i)
 
+protected lemma biInf [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι]
+    [OrderTopology ι] [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι]
+    {κ : Type*} {f : Filtration ι m} {τ : κ → Ω → WithTop ι} {s : Set κ} (hs : s.Countable)
+    [f.IsRightContinuous] (hτ : ∀ n ∈ s, IsStoppingTime f (τ n)) :
+    IsStoppingTime f (fun ω ↦ ⨅ (n) (_ : n ∈ s), τ n ω) := by
+  refine isStoppingTime_of_measurableSet_lt_of_isRightContinuous <|
+    fun i ↦ MeasurableSet.of_compl ?_
+  rw [(_ : {ω | ⨅ n ∈ s, τ n ω < i}ᶜ = ⋂ n ∈ s, {ω | i ≤ τ n ω})]
+  · exact MeasurableSet.biInter hs <| fun n hn ↦ (hτ n hn).measurableSet_ge i
+  · ext ω
+    simp
+
+protected lemma iInf [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι]
+    [OrderTopology ι] [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι]
+    {κ : Type*} [Countable κ] {f : Filtration ι m} {τ : κ → Ω → WithTop ι}
+    [f.IsRightContinuous] (hτ : ∀ n, IsStoppingTime f (τ n)) :
+    IsStoppingTime f (fun ω ↦ ⨅ n, τ n ω) := by
+  convert IsStoppingTime.biInf (κ := κ) Set.countable_univ (fun n _ => hτ n) using 2
+  simp
+
 theorem add_const [AddGroup ι] [Preorder ι] [AddRightMono ι]
     [AddLeftMono ι] {f : Filtration ι m} {τ : Ω → WithTop ι} (hτ : IsStoppingTime f τ)
     {i : ι} (hi : 0 ≤ i) : IsStoppingTime f fun ω => τ ω + i := by