Experiment: shift filtration

LeanMachineLearning/SequentialLearning/ActionIndicator.lean

@@ -24,7 +24,8 @@ at round `n`. It is the increment weight of every per-action sum attached to an
 
 * `Learning.sum_range_actionIndicator_eq_pullCount`, `Learning.sum_actionIndicator_mul` — the two
   partial-sum identities.
-* `Learning.adapted_actionIndicator`, `Learning.integrable_actionIndicator`.
+* `Learning.IsAlgEnvSeq.measurable_actionIndicator_filtration_succ`,
+  `Learning.integrable_actionIndicator`.
 -/
 
 @[expose] public section
@@ -92,12 +93,13 @@ lemma integrable_actionIndicator (P : Measure Ω) [IsFiniteMeasure P]
     Integrable (actionIndicator A k n) P :=
   (integrable_const (1 : ℝ)).indicator (hA (measurableSet_singleton k))
 
-/-- The action indicator is adapted to the history filtration: whether action `k` was chosen at `n`
-is known at time `n`. -/
-lemma IsAlgEnvSeq.adapted_actionIndicator {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨}
-    [IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (k : 𝓐) :
-    Adapted h.filtration (actionIndicator A k) :=
-  fun _ ↦ Measurable.indicator measurable_const (h.adapted_action _ (measurableSet_singleton k))
+/-- Whether action `k` was chosen at time `n` is known once the first `n + 1` rounds are known. -/
+lemma IsAlgEnvSeq.measurable_actionIndicator_filtration_succ {alg : Algorithm 𝓞 𝓐 𝓨}
+    {env : Environment 𝓞 𝓐 𝓨} [IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (k : 𝓐)
+    (n : ℕ) :
+    Measurable[h.filtration (n + 1)] (actionIndicator A k n) :=
+  Measurable.indicator measurable_const
+    (h.measurable_action_filtration_succ n (measurableSet_singleton k))
 
 /-- The action indicator is adapted to the history+action filtration: whether action `k` was chosen
 at `n` is known once we know the action at `n`. -/

LeanMachineLearning/SequentialLearning/Algorithm.lean

@@ -539,56 +539,75 @@ section Filtration
 
 namespace IsAlgEnvSeq
 
-/-- Filtration generated by the history up to time `n` (included): `h.filtration n` is the
-σ-algebra generated by `history O A Y (n + 1)`, that is by the rounds at times `0, ..., n`. -/
+/-- Filtration generated by the history: `h.filtration n` is the σ-algebra generated by
+`history O A Y n`, that is by the `n` rounds at times `0, ..., n - 1`. In particular
+`h.filtration 0` is the trivial σ-algebra, and the round at time `n` is measurable with respect
+to `h.filtration (n + 1)`. -/
 def filtration (h : IsAlgEnvSeq O A Y alg env P) :
     Filtration ℕ mΩ where
-  seq n := MeasurableSpace.comap (history O A Y (n + 1)) inferInstance
+  seq n := MeasurableSpace.comap (history O A Y n) inferInstance
   mono' i j hij := by
     simp only
-    rw [← measurable_iff_comap_le, history_eq_comp_history (Nat.succ_le_succ hij)]
+    rw [← measurable_iff_comap_le, history_eq_comp_history hij]
     exact measurable_comp_comap _ (by fun_prop)
   le' i := by
     rw [← measurable_iff_comap_le]
     exact Learning.measurable_history h.measurable_obs h.measurable_action h.measurable_feedback _
 
 lemma filtration_eq_comap (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
-    h.filtration n = MeasurableSpace.comap (history O A Y (n + 1)) inferInstance := rfl
+    h.filtration n = MeasurableSpace.comap (history O A Y n) inferInstance := rfl
 
-lemma measurable_history_succ_filtration (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
-    Measurable[h.filtration n] (history O A Y (n + 1)) :=
+lemma filtration_zero (h : IsAlgEnvSeq O A Y alg env P) : h.filtration 0 = ⊥ := by
+  rw [filtration_eq_comap, history_zero, MeasurableSpace.comap_const]
+
+lemma measurable_history_filtration (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    Measurable[h.filtration n] (history O A Y n) :=
   measurable_iff_comap_le.mpr le_rfl
 
 lemma adapted_history (h : IsAlgEnvSeq O A Y alg env P) :
-    Adapted h.filtration (history O A Y) := by
-  intro n
-  rw [history_eq_comp_history n.le_succ]
-  exact measurable_comp_comap _ (by fun_prop)
+    Adapted h.filtration (history O A Y) :=
+  h.measurable_history_filtration
 
-lemma adapted_step (h : IsAlgEnvSeq O A Y alg env P) :
-    Adapted h.filtration (step O A Y) := by
-  intro n
+lemma measurable_step_filtration_succ (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    Measurable[h.filtration (n + 1)] (step O A Y n) := by
   rw [← eval_comp_history]
   exact measurable_comp_comap _ (by fun_prop)
 
-lemma adapted_obs (h : IsAlgEnvSeq O A Y alg env P) :
-    Adapted h.filtration O := by
-  intro n
+lemma measurable_obs_filtration_succ (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    Measurable[h.filtration (n + 1)] (O n) := by
   rw [← obs_eval_comp_history (O := O) (A := A) (Y := Y) n]
   exact measurable_comp_comap _ (by fun_prop)
 
-lemma adapted_action (h : IsAlgEnvSeq O A Y alg env P) :
-    Adapted h.filtration A := by
-  intro n
+lemma measurable_action_filtration_succ (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    Measurable[h.filtration (n + 1)] (A n) := by
   rw [← action_eval_comp_history (O := O) (A := A) (Y := Y) n]
   exact measurable_comp_comap _ (by fun_prop)
 
-lemma adapted_feedback (h : IsAlgEnvSeq O A Y alg env P) :
-    Adapted h.filtration Y := by
-  intro n
+lemma measurable_feedback_filtration_succ (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    Measurable[h.filtration (n + 1)] (Y n) := by
   rw [← feedback_eval_comp_history (O := O) (A := A) (Y := Y) n]
   exact measurable_comp_comap _ (by fun_prop)
 
+/-- The step at time `m < n` is measurable with respect to the σ-algebra generated by the first
+`n` rounds. -/
+lemma measurable_step_filtration_of_lt (h : IsAlgEnvSeq O A Y alg env P) {m n : ℕ} (hmn : m < n) :
+    Measurable[h.filtration n] (step O A Y m) :=
+  (h.measurable_step_filtration_succ m).mono (h.filtration.mono hmn) le_rfl
+
+lemma measurable_obs_filtration_of_lt (h : IsAlgEnvSeq O A Y alg env P) {m n : ℕ} (hmn : m < n) :
+    Measurable[h.filtration n] (O m) :=
+  (h.measurable_obs_filtration_succ m).mono (h.filtration.mono hmn) le_rfl
+
+lemma measurable_action_filtration_of_lt (h : IsAlgEnvSeq O A Y alg env P) {m n : ℕ}
+    (hmn : m < n) :
+    Measurable[h.filtration n] (A m) :=
+  (h.measurable_action_filtration_succ m).mono (h.filtration.mono hmn) le_rfl
+
+lemma measurable_feedback_filtration_of_lt (h : IsAlgEnvSeq O A Y alg env P) {m n : ℕ}
+    (hmn : m < n) :
+    Measurable[h.filtration n] (Y m) :=
+  (h.measurable_feedback_filtration_succ m).mono (h.filtration.mono hmn) le_rfl
+
 /-- Filtration generated by the history before time `n` together with the observation at
 time `n`. -/
 def filtrationObs (h : IsAlgEnvSeq O A Y alg env P) :
@@ -677,22 +696,23 @@ lemma filtrationObs_le_filtrationAction (h : IsAlgEnvSeq O A Y alg env P) (n : 
   rw [filtrationObs_eq_comap, filtrationAction_eq_comap, ← measurable_iff_comap_le]
   exact measurable_fst.comp (measurable_iff_comap_le.mpr le_rfl)
 
-lemma filtration_le_filtrationObs_succ (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
-    h.filtration n ≤ h.filtrationObs (n + 1) :=
-  measurable_iff_comap_le.mp (h.measurable_history_filtrationObs (n + 1))
+lemma filtration_le_filtrationObs (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    h.filtration n ≤ h.filtrationObs n :=
+  measurable_iff_comap_le.mp (h.measurable_history_filtrationObs n)
 
-lemma filtration_le_filtrationAction_succ (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
-    h.filtration n ≤ h.filtrationAction (n + 1) :=
-  measurable_iff_comap_le.mp (h.measurable_history_filtrationAction (n + 1))
+lemma filtration_le_filtrationAction (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    h.filtration n ≤ h.filtrationAction n :=
+  measurable_iff_comap_le.mp (h.measurable_history_filtrationAction n)
 
-lemma filtrationAction_le_filtration (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
-    h.filtrationAction n ≤ h.filtration n := by
+lemma filtrationAction_le_filtration_succ (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    h.filtrationAction n ≤ h.filtration (n + 1) := by
   rw [filtrationAction_eq_comap, ← measurable_iff_comap_le]
-  exact ((h.adapted_history n).prodMk (h.adapted_obs n)).prodMk (h.adapted_action n)
+  exact ((h.adapted_history.measurable_le n.le_succ).prodMk
+    (h.measurable_obs_filtration_succ n)).prodMk (h.measurable_action_filtration_succ n)
 
-lemma filtrationObs_le_filtration (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
-    h.filtrationObs n ≤ h.filtration n :=
-  (h.filtrationObs_le_filtrationAction n).trans (h.filtrationAction_le_filtration n)
+lemma filtrationObs_le_filtration_succ (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    h.filtrationObs n ≤ h.filtration (n + 1) :=
+  (h.filtrationObs_le_filtrationAction n).trans (h.filtrationAction_le_filtration_succ n)
 
 lemma adapted_obs_filtrationObs (h : IsAlgEnvSeq O A Y alg env P) :
     Adapted h.filtrationObs O := fun _ ↦
@@ -708,17 +728,13 @@ lemma adapted_action_filtrationAction (h : IsAlgEnvSeq O A Y alg env P) :
 
 lemma measurable_feedback_filtrationObs_of_lt (h : IsAlgEnvSeq O A Y alg env P)
     {m n : ℕ} (hmn : m < n) :
-    Measurable[h.filtrationObs n] (Y m) := by
-  obtain ⟨j, rfl⟩ : ∃ j, n = j + 1 := ⟨n - 1, by lia⟩
-  exact (h.adapted_feedback.measurable_le (by lia)).mono
-    (filtration_le_filtrationObs_succ h j) le_rfl
+    Measurable[h.filtrationObs n] (Y m) :=
+  (h.measurable_feedback_filtration_of_lt hmn).mono (filtration_le_filtrationObs h n) le_rfl
 
 lemma measurable_feedback_filtrationAction_of_lt (h : IsAlgEnvSeq O A Y alg env P)
     {m n : ℕ} (hmn : m < n) :
-    Measurable[h.filtrationAction n] (Y m) := by
-  obtain ⟨j, rfl⟩ : ∃ j, n = j + 1 := ⟨n - 1, by lia⟩
-  exact (h.adapted_feedback.measurable_le (by lia)).mono
-    (filtration_le_filtrationAction_succ h j) le_rfl
+    Measurable[h.filtrationAction n] (Y m) :=
+  (h.measurable_feedback_filtration_of_lt hmn).mono (filtration_le_filtrationAction h n) le_rfl
 
 end IsAlgEnvSeq
 

LeanMachineLearning/SequentialLearning/FiniteActions.lean

@@ -219,27 +219,20 @@ lemma measurable_uncurry_pullCount' [MeasurableEq 𝓐] (n : ℕ) :
     exact measurableSet_eq_fun (by fun_prop) (by fun_prop)
   fun_prop
 
-lemma adapted_pullCount_add_one [MeasurableSingletonClass 𝓐]
+/-- The number of pulls of `a` before time `n` is a function of the first `n` rounds. -/
+lemma adapted_pullCount [MeasurableSingletonClass 𝓐]
     (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) :
-    Adapted h.filtration (fun n ↦ pullCount A a (n + 1)) := by
+    Adapted h.filtration (pullCount A a) := by
   intro n
-  change Measurable[h.filtration n] (pullCount A a (n + 1))
+  change Measurable[h.filtration n] (pullCount A a n)
   rw [measurable_iff_comap_le, h.filtration_eq_comap, pullCount_eq_comp_history (O := O) (R' := R'),
     ← measurable_iff_comap_le]
-  exact measurable_comp_comap _ (measurable_pullCount' (n + 1) a)
+  exact measurable_comp_comap _ (measurable_pullCount' n a)
 
-lemma stronglyAdapted_pullCount_add_one [MeasurableSingletonClass 𝓐]
+lemma stronglyAdapted_pullCount [MeasurableSingletonClass 𝓐]
     (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) :
-    StronglyAdapted h.filtration (fun n ↦ pullCount A a (n + 1)) :=
-  (adapted_pullCount_add_one h a).stronglyAdapted
-
-lemma isStronglyPredictable_pullCount [MeasurableSingletonClass 𝓐]
-    (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) :
-    IsStronglyPredictable h.filtration (pullCount A a) := by
-  rw [IsStronglyPredictable.iff_measurable_add_one]
-  refine ⟨?_, stronglyAdapted_pullCount_add_one h a⟩
-  simp only [pullCount_zero]
-  fun_prop
+    StronglyAdapted h.filtration (pullCount A a) :=
+  (adapted_pullCount h a).stronglyAdapted
 
 lemma measurableSet_action_eq_and_pullCount_eq [MeasurableSingletonClass 𝓐]
     (hA : ∀ n, Measurable (A n)) (t : ℕ) (b : 𝓐) (k : ℕ) :
@@ -529,16 +522,6 @@ lemma stepsUntil_eq_congr {ω' : Ω} (h_eq : ∀ i ≤ n, A i ω = A i ω') :
 
 section Measurability
 
-lemma isStoppingTime_stepsUntil [MeasurableSingletonClass 𝓐]
-    (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) (hm : m ≠ 0) :
-    IsStoppingTime h.filtration (stepsUntil A a m) := by
-  rw [stepsUntil_eq_leastGE _ hm]
-  refine StronglyAdapted.isStoppingTime_leastGE _ fun n ↦ ?_
-  suffices StronglyMeasurable[h.filtration n] (pullCount A a (n + 1)) by
-    fun_prop
-  refine Measurable.stronglyMeasurable ?_
-  exact adapted_pullCount_add_one h a n
-
 -- todo: get this from the stopping time property?
 @[fun_prop]
 lemma measurable_stepsUntil [MeasurableSingletonClass 𝓐]
@@ -644,6 +627,27 @@ lemma isStoppingTime_stepsUntil_filtrationAction [MeasurableSingletonClass 𝓐]
   rw [h.filtrationAction_eq_comap n]
   exact measurableSet_stepsUntil_eq O R' a m n
 
+/-- `stepsUntil a m + 1`, the number of rounds played until action `a` has been pulled `m`
+times, is a stopping time with respect to the history filtration (`stepsUntil a m` itself is the
+index of the round of the `m`-th pull, which is known only once that round is played). -/
+lemma isStoppingTime_stepsUntil_add_one [MeasurableSingletonClass 𝓐]
+    (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) (m : ℕ) :
+    IsStoppingTime h.filtration (fun ω ↦ (stepsUntil A a m ω + 1 : ℕ∞)) := by
+  intro n
+  change MeasurableSet[h.filtration n] {ω | stepsUntil A a m ω + 1 ≤ (n : ℕ∞)}
+  cases n with
+  | zero =>
+    convert @MeasurableSet.empty Ω (h.filtration 0) using 1
+    ext ω
+    simp only [Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false]
+    exact fun h' ↦ absurd (le_add_self.trans h') (by simp)
+  | succ j =>
+    convert h.filtrationAction_le_filtration_succ j _
+      (isStoppingTime_stepsUntil_filtrationAction h a m j) using 1
+    ext ω
+    simp only [Set.mem_ofPred_eq, ENat.some_eq_natCast, Nat.cast_add, Nat.cast_one]
+    exact ENat.add_le_add_iff_right (by simp)
+
 end Measurability
 
 end StepsUntil

LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean

@@ -189,49 +189,55 @@ end ModelEquivalence
 
 namespace IT
 
-/-- Filtration of the algorithm Seq: `IT.filtration 𝓞 𝓐 𝓨 n` is the σ-algebra generated by the
-rounds at times `0, ..., n`, that is by `hist (n + 1)`. -/
+/-- Filtration of the canonical space: `IT.filtration 𝓞 𝓐 𝓨 n` is the σ-algebra generated by
+`hist n`, that is by the `n` rounds at times `0, ..., n - 1`. -/
 protected def filtration (𝓞 𝓐 𝓨 : Type*) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐]
     [MeasurableSpace 𝓨] :
-    Filtration ℕ (inferInstance : MeasurableSpace (ℕ → Round 𝓞 𝓐 𝓨)) :=
-  MeasureTheory.Filtration.piLE (X := fun _ ↦ Round 𝓞 𝓐 𝓨)
+    Filtration ℕ (inferInstance : MeasurableSpace (ℕ → Round 𝓞 𝓐 𝓨)) where
+  seq n := MeasurableSpace.comap (hist n) inferInstance
+  mono' i j hij := by
+    simp only
+    rw [← measurable_iff_comap_le, hist_eq_comp_hist hij]
+    exact measurable_comp_comap _ (by fun_prop)
+  le' n := (measurable_hist n).comap_le
 
 lemma filtration_eq_comap (n : ℕ) :
-    IT.filtration 𝓞 𝓐 𝓨 n = MeasurableSpace.comap (hist (n + 1)) inferInstance := by
-  simp only [IT.filtration, Filtration.piLE_eq_comap_frestrictLe]
+    IT.filtration 𝓞 𝓐 𝓨 n = MeasurableSpace.comap (hist n) inferInstance := rfl
+
+/-- `IT.filtration 𝓞 𝓐 𝓨 (n + 1)` is the canonical filtration `Filtration.piLE` of the product
+space at time `n`, the σ-algebra generated by the coordinates `0, ..., n`. -/
+lemma filtration_succ_eq_piLE (n : ℕ) :
+    IT.filtration 𝓞 𝓐 𝓨 (n + 1) = Filtration.piLE (X := fun _ ↦ Round 𝓞 𝓐 𝓨) n := by
+  rw [filtration_eq_comap, Filtration.piLE_eq_comap_frestrictLe]
   refine le_antisymm ?_ ?_
-  · rw [← measurable_iff_comap_le, frestrictLe_eq_comp_hist]
-    exact measurable_comp_comap _ (by fun_prop)
   · rw [← measurable_iff_comap_le, hist_succ_eq_comp_frestrictLe]
     exact measurable_comp_comap _ (by fun_prop)
+  · rw [← measurable_iff_comap_le, frestrictLe_eq_comp_hist]
+    exact measurable_comp_comap _ (by fun_prop)
+
+lemma measurable_hist_filtration (n : ℕ) :
+    Measurable[IT.filtration 𝓞 𝓐 𝓨 n] (hist (𝓞 := 𝓞) (𝓐 := 𝓐) (𝓨 := 𝓨) n) :=
+  measurable_iff_comap_le.mpr le_rfl
+
+lemma adapted_hist : Adapted (IT.filtration 𝓞 𝓐 𝓨) hist := measurable_hist_filtration
 
-lemma adapted_step : Adapted (IT.filtration 𝓞 𝓐 𝓨) (step (𝓞 := 𝓞) (𝓐 := 𝓐) (𝓨 := 𝓨)) := by
-  intro n
+lemma measurable_step_filtration_succ (n : ℕ) :
+    Measurable[IT.filtration 𝓞 𝓐 𝓨 (n + 1)] (step (𝓞 := 𝓞) (𝓐 := 𝓐) (𝓨 := 𝓨) n) := by
   rw [filtration_eq_comap, step_eq_eval_comp_hist]
   exact measurable_comp_comap _ (by fun_prop)
 
-lemma adapted_obs : Adapted (IT.filtration 𝓞 𝓐 𝓨) obs := by
-  intro n
+lemma measurable_obs_filtration_succ (n : ℕ) :
+    Measurable[IT.filtration 𝓞 𝓐 𝓨 (n + 1)] (obs (𝓞 := 𝓞) (𝓐 := 𝓐) (𝓨 := 𝓨) n) := by
   rw [filtration_eq_comap, obs_eq_eval_comp_hist]
   exact measurable_comp_comap _ (by fun_prop)
 
-lemma measurable_hist_succ_filtration (n : ℕ) :
-    Measurable[IT.filtration 𝓞 𝓐 𝓨 n] (hist (n + 1)) := by
-  rw [filtration_eq_comap]
-  exact measurable_iff_comap_le.mpr le_rfl
-
-lemma adapted_hist : Adapted (IT.filtration 𝓞 𝓐 𝓨) hist := by
-  intro n
-  rw [filtration_eq_comap, hist_eq_comp_hist n.le_succ]
-  exact measurable_comp_comap _ (by fun_prop)
-
-lemma adapted_action : Adapted (IT.filtration 𝓞 𝓐 𝓨) action := by
-  intro n
+lemma measurable_action_filtration_succ (n : ℕ) :
+    Measurable[IT.filtration 𝓞 𝓐 𝓨 (n + 1)] (action (𝓞 := 𝓞) (𝓐 := 𝓐) (𝓨 := 𝓨) n) := by
   rw [filtration_eq_comap, action_eq_eval_comp_hist]
   exact measurable_comp_comap _ (by fun_prop)
 
-lemma adapted_feedback : Adapted (IT.filtration 𝓞 𝓐 𝓨) feedback := by
-  intro n
+lemma measurable_feedback_filtration_succ (n : ℕ) :
+    Measurable[IT.filtration 𝓞 𝓐 𝓨 (n + 1)] (feedback (𝓞 := 𝓞) (𝓐 := 𝓐) (𝓨 := 𝓨) n) := by
   rw [filtration_eq_comap, feedback_eq_eval_comp_hist]
   exact measurable_comp_comap _ (by fun_prop)
 
@@ -281,24 +287,23 @@ lemma measurable_hist_filtrationAction (n : ℕ) :
     Measurable[filtrationAction 𝓞 𝓐 𝓨 n] (hist n) :=
   (measurable_fst.comp measurable_fst).comp (measurable_iff_comap_le.mpr le_rfl)
 
-lemma filtration_le_filtrationAction_add_one (n : ℕ) :
-    IT.filtration 𝓞 𝓐 𝓨 n ≤ filtrationAction 𝓞 𝓐 𝓨 (n + 1) := by
-  rw [filtration_eq_comap]
-  exact measurable_iff_comap_le.mp (measurable_hist_filtrationAction (n + 1))
+lemma filtration_le_filtrationAction (n : ℕ) :
+    IT.filtration 𝓞 𝓐 𝓨 n ≤ filtrationAction 𝓞 𝓐 𝓨 n :=
+  measurable_iff_comap_le.mp (measurable_hist_filtrationAction n)
 
-lemma filtration_le_filtrationAction {m n : ℕ} (h : n < m) :
-    IT.filtration 𝓞 𝓐 𝓨 n ≤ filtrationAction 𝓞 𝓐 𝓨 m := by
-  have h' : n + 1 ≤ m := by grind
-  exact (filtration_le_filtrationAction_add_one n).trans ((filtrationAction 𝓞 𝓐 𝓨).mono h')
+lemma filtration_le_filtrationAction_of_le {m n : ℕ} (h : n ≤ m) :
+    IT.filtration 𝓞 𝓐 𝓨 n ≤ filtrationAction 𝓞 𝓐 𝓨 m :=
+  (filtration_le_filtrationAction n).trans ((filtrationAction 𝓞 𝓐 𝓨).mono h)
 
-lemma filtrationAction_le_filtration_self (n : ℕ) :
-    filtrationAction 𝓞 𝓐 𝓨 n ≤ IT.filtration 𝓞 𝓐 𝓨 n := by
+lemma filtrationAction_le_filtration_succ (n : ℕ) :
+    filtrationAction 𝓞 𝓐 𝓨 n ≤ IT.filtration 𝓞 𝓐 𝓨 (n + 1) := by
   rw [filtrationAction_eq_comap, ← measurable_iff_comap_le]
-  exact ((adapted_hist n).prodMk (adapted_obs n)).prodMk (adapted_action n)
+  exact ((Adapted.measurable_le adapted_hist n.le_succ).prodMk
+    (measurable_obs_filtration_succ n)).prodMk (measurable_action_filtration_succ n)
 
-lemma filtrationAction_le_filtration {m n : ℕ} (h : m ≤ n) :
+lemma filtrationAction_le_filtration_of_lt {m n : ℕ} (h : m < n) :
     filtrationAction 𝓞 𝓐 𝓨 m ≤ IT.filtration 𝓞 𝓐 𝓨 n :=
-  (filtrationAction_le_filtration_self m).trans ((IT.filtration 𝓞 𝓐 𝓨).mono h)
+  (filtrationAction_le_filtration_succ m).trans ((IT.filtration 𝓞 𝓐 𝓨).mono h)
 
 lemma measurable_obs_filtrationAction (n : ℕ) :
     Measurable[filtrationAction 𝓞 𝓐 𝓨 n] (obs n) :=