diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean
index f64d7306..46ad1617 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithm.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean
@@ -143,9 +143,6 @@ lemma history_succ (n : ℕ) :
   symm
   exact (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm_apply_apply (history A Y (n + 1) ω)
 
-section IsAlgEnvSeq
-
-
 /-- An algorithm-environment sequence: a sequence of actions and feedbacks generated
 by an algorithm interacting with an environment. -/
 structure IsAlgEnvSeq
@@ -253,10 +250,12 @@ lemma IsAlgEnvSeq.hasLaw_history_zero (h : IsAlgEnvSeq A Y alg env P) : HasLaw (
     have hY := h.measurable_feedback
     exact (Measure.map_map (by fun_prop) (by fun_prop)).symm
 
-end IsAlgEnvSeq
+section Filtration
+
+namespace IsAlgEnvSeq
 
 /-- Filtration generated by the history up to time `n`. -/
-def IsAlgEnvSeq.filtration (h : IsAlgEnvSeq A Y alg env P) :
+def filtration (h : IsAlgEnvSeq A Y alg env P) :
     Filtration ℕ mΩ where
   seq i := MeasurableSpace.comap (history A Y i) inferInstance
   mono' i j hij := by
@@ -269,11 +268,11 @@ def IsAlgEnvSeq.filtration (h : IsAlgEnvSeq A Y alg env P) :
     rw [← measurable_iff_comap_le]
     exact Learning.measurable_history h.measurable_action h.measurable_feedback i
 
-lemma IsAlgEnvSeq.adapted_history (h : IsAlgEnvSeq A Y alg env P) :
+lemma adapted_history (h : IsAlgEnvSeq A Y alg env P) :
     Adapted h.filtration (history A Y) :=
   fun _ ↦ measurable_iff_comap_le.mpr le_rfl
 
-lemma IsAlgEnvSeq.adapted_step (h : IsAlgEnvSeq A Y alg env P) :
+lemma adapted_step (h : IsAlgEnvSeq A Y alg env P) :
     Adapted h.filtration (step A Y) := by
   intro n
   have : step A Y n = (fun h ↦ (h ⟨n, by simp⟩)) ∘ (history A Y n) := by
@@ -282,7 +281,7 @@ lemma IsAlgEnvSeq.adapted_step (h : IsAlgEnvSeq A Y alg env P) :
   rw [this]
   exact measurable_comp_comap _ (by fun_prop)
 
-lemma IsAlgEnvSeq.adapted_action (h : IsAlgEnvSeq A Y alg env P) :
+lemma adapted_action (h : IsAlgEnvSeq A Y alg env P) :
     Adapted h.filtration A := by
   intro n
   have : A n = (fun h ↦ (h ⟨n, by simp⟩).1) ∘ (history A Y n) := by
@@ -291,7 +290,7 @@ lemma IsAlgEnvSeq.adapted_action (h : IsAlgEnvSeq A Y alg env P) :
   rw [this]
   exact measurable_comp_comap _ (by fun_prop)
 
-lemma IsAlgEnvSeq.adapted_feedback (h : IsAlgEnvSeq A Y alg env P) :
+lemma adapted_feedback (h : IsAlgEnvSeq A Y alg env P) :
     Adapted h.filtration Y := by
   intro n
   have : Y n = (fun h ↦ (h ⟨n, by simp⟩).2) ∘ (history A Y n) := by
@@ -301,10 +300,10 @@ lemma IsAlgEnvSeq.adapted_feedback (h : IsAlgEnvSeq A Y alg env P) :
   exact measurable_comp_comap _ (by fun_prop)
 
 /-- Filtration generated by the history at time `n-1` together with the action at time `n`. -/
-def IsAlgEnvSeq.filtrationAction (h : IsAlgEnvSeq A Y alg env P) :
+def filtrationAction (h : IsAlgEnvSeq A Y alg env P) :
     Filtration ℕ mΩ where
   seq n := if n = 0 then MeasurableSpace.comap (A 0) inferInstance
-    else IsAlgEnvSeq.filtration h (n - 1) ⊔ MeasurableSpace.comap (A n) inferInstance
+    else h.filtration (n - 1) ⊔ MeasurableSpace.comap (A n) inferInstance
   mono' n m hnm := by
     simp only
     by_cases hn : n = 0
@@ -313,8 +312,8 @@ def IsAlgEnvSeq.filtrationAction (h : IsAlgEnvSeq A Y alg env P) :
       · simp only [hn, ↓reduceIte, hm]
         refine le_sup_of_le_left ?_
         rw [← measurable_iff_comap_le]
-        suffices Measurable[IsAlgEnvSeq.filtration h 0] (A 0) from
-          this.mono ((IsAlgEnvSeq.filtration h).mono zero_le) le_rfl
+        suffices Measurable[h.filtration 0] (A 0) from
+          this.mono ((h.filtration).mono zero_le) le_rfl
         exact adapted_action h 0
     have hm : m ≠ 0 := by grind
     simp only [hn, hm, ↓reduceIte]
@@ -322,14 +321,14 @@ def IsAlgEnvSeq.filtrationAction (h : IsAlgEnvSeq A Y alg env P) :
     simp only [sup_le_iff]
     constructor
     · refine le_sup_of_le_left ?_
-      exact (IsAlgEnvSeq.filtration h).mono hnm'
+      exact (h.filtration).mono hnm'
     · rcases eq_or_lt_of_le hnm with rfl | hlt
       · exact le_sup_of_le_right le_rfl
       refine le_sup_of_le_left ?_
       rw [← measurable_iff_comap_le]
       have h_le : n ≤ m - 1 := by grind
       suffices Measurable[h.filtration n] (A n) from
-        this.mono ((IsAlgEnvSeq.filtration h).mono h_le) le_rfl
+        this.mono ((h.filtration).mono h_le) le_rfl
       exact adapted_action h n
   le' n := by
     by_cases hn : n = 0
@@ -342,17 +341,56 @@ def IsAlgEnvSeq.filtrationAction (h : IsAlgEnvSeq A Y alg env P) :
     · rw [← measurable_iff_comap_le]
       exact h.measurable_action n
 
-lemma IsAlgEnvSeq.filtrationAction_zero_eq_comap {h : IsAlgEnvSeq A Y alg env P} :
+lemma filtrationAction_zero_eq_comap (h : IsAlgEnvSeq A Y alg env P) :
     h.filtrationAction 0 = MeasurableSpace.comap (A 0) inferInstance := by
   simp [filtrationAction]
 
-lemma IsAlgEnvSeq.filtrationAction_eq_comap
-    {h : IsAlgEnvSeq A Y alg env P} (n : ℕ) (hn : n ≠ 0) :
+lemma filtrationAction_eq_comap (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) (hn : n ≠ 0) :
     h.filtrationAction n =
       MeasurableSpace.comap (fun ω ↦ (history A Y (n - 1) ω, A n ω)) inferInstance := by
   simp only [filtrationAction, filtration, ← MeasurableSpace.comap_prodMk, hn, ↓reduceIte]
   rfl
 
+@[fun_prop]
+lemma measurable_history_filtrationAction_add_one (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
+    Measurable[h.filtrationAction (n + 1)] (history A Y n) := by
+  rw [h.filtrationAction_eq_comap (n + 1) (Nat.succ_ne_zero n)]
+  exact measurable_fst.comp (measurable_iff_comap_le.mpr le_rfl)
+
+lemma filtration_le_filtrationAction_succ (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
+    h.filtration n ≤ h.filtrationAction (n + 1) :=
+  measurable_iff_comap_le.mp (h.measurable_history_filtrationAction_add_one n)
+
+lemma filtrationAction_le_filtration (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
+    h.filtrationAction n ≤ h.filtration n := by
+  cases n with
+  | zero =>
+    rw [h.filtrationAction_zero_eq_comap]
+    exact measurable_iff_comap_le.mp (h.adapted_action 0)
+  | succ m =>
+    rw [h.filtrationAction_eq_comap (m + 1) (Nat.succ_ne_zero m), ← measurable_iff_comap_le]
+    exact ((h.adapted_history m).mono (h.filtration.mono m.le_succ) le_rfl).prodMk
+      (h.adapted_action (m + 1))
+
+lemma adapted_action_filtrationAction (h : IsAlgEnvSeq A Y alg env P) :
+    Adapted h.filtrationAction A := fun n ↦ by
+  cases n with
+  | zero => rw [h.filtrationAction_zero_eq_comap]; exact measurable_iff_comap_le.mpr le_rfl
+  | succ m =>
+    rw [h.filtrationAction_eq_comap (m + 1) (Nat.succ_ne_zero m)]
+    exact measurable_snd.comp (measurable_iff_comap_le.mpr le_rfl)
+
+lemma measurable_feedback_filtrationAction_of_lt (h : IsAlgEnvSeq 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
+
+end IsAlgEnvSeq
+
+end Filtration
+
 end IsAlgEnvSeq
 
 end Learning
diff --git a/LeanMachineLearning/SequentialLearning/FiniteActions.lean b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
index 3fb707ec..a1bb588d 100644
--- a/LeanMachineLearning/SequentialLearning/FiniteActions.lean
+++ b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
@@ -651,7 +651,7 @@ lemma isStoppingTime_stepsUntil_filtrationAction [MeasurableSingletonClass 𝓐]
   · subst hn
     simp only [WithTop.coe_zero]
     exact measurableSet_stepsUntil_eq_zero a m
-  · rw [IsAlgEnvSeq.filtrationAction_eq_comap _ hn]
+  · rw [h.filtrationAction_eq_comap _ hn]
     exact measurableSet_stepsUntil_eq h a m n
 
 end Measurability
@@ -767,6 +767,13 @@ lemma sum_comp_pullCount [Fintype 𝓐] [AddCommMonoid R] (f : ℕ → R) (t : 
     · simp [sum_range_succ]
     · simp
 
+lemma sum_pullCount' [Fintype 𝓐] (n : ℕ) (h : Iic n → 𝓐 × ℝ) : ∑ a, pullCount' n h a = n + 1 := by
+  simp_rw [pullCount'_eq_sum]
+  rw [Finset.sum_comm]
+  have hcol (s : Iic n) : ∑ a, (if (h s).1 = a then (1 : ℕ) else 0) = 1 := by
+    simp [Finset.sum_ite_eq univ (h s).1 (fun _ ↦ (1 : ℕ))]
+  simp [hcol]
+
 section SumRewards
 
 /-- Sum of rewards obtained when pulling action `a` up to time `t` (exclusive). -/