diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
index 6d93ccc6..9bdda650 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
@@ -86,7 +86,7 @@ lemma arm_zero [Nonempty (Fin K)]
 
 lemma arm_ae_eq_etcNextArm [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) (n : ℕ) :
-    A (n + 1) =ᵐ[P] fun ω ↦ nextArm hK m n (IsAlgEnvSeq.hist A R n ω) := by
+    A (n + 1) =ᵐ[P] fun ω ↦ nextArm hK m n (history A R n ω) := by
   have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
   exact h.action_detAlgorithm_ae_eq n
 
@@ -101,7 +101,7 @@ phase. -/
 lemma arm_mul [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) (hm : m ≠ 0) :
     A (K * m) =ᵐ[P] fun ω ↦ measurableArgmax (empMean' (K * m - 1))
-      (IsAlgEnvSeq.hist A R (K * m - 1) ω) := by
+      (history A R (K * m - 1) ω) := by
   have : K * m = (K * m - 1) + 1 := by
     have : 0 < K * m := Nat.mul_pos hK hm.bot_lt
     grind
@@ -176,7 +176,7 @@ lemma sumRewards_bestArm_le_of_arm_mul_eq [Nonempty (Fin K)]
       sumRewards A R a (K * m) h := by
   filter_upwards [arm_mul h hm, pullCount_mul h a, pullCount_mul h (bestArm ν)]
     with h h_arm ha h_best h_eq
-  have h_max := isMaxOn_measurableArgmax (empMean' (K * m - 1)) (IsAlgEnvSeq.hist A R (K * m - 1) h)
+  have h_max := isMaxOn_measurableArgmax (empMean' (K * m - 1)) (history A R (K * m - 1) h)
     (bestArm ν)
   rw [← h_arm, h_eq] at h_max
   rw [sumRewards_eq_pullCount_mul_empMean, sumRewards_eq_pullCount_mul_empMean, ha, h_best]
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
index 94adc7c3..2d1e2fb7 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
@@ -90,7 +90,7 @@ lemma measurable_ucbWidth (hA : ∀ n, Measurable (A n)) (c : ℝ) (a : Fin K) :
   fun_prop
 
 lemma ucbWidth_eq_ucbWidth' (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) (hn : n ≠ 0) :
-    ucbWidth A c a n ω = ucbWidth' c (n - 1) (IsAlgEnvSeq.hist A R (n - 1) ω) a := by
+    ucbWidth A c a n ω = ucbWidth' c (n - 1) (history A R (n - 1) ω) a := by
   simp only [ucbWidth, pullCount_eq_pullCount' (A := A) (R' := R) hn, Nat.cast_nonneg, sqrt_div',
     ucbWidth']
   congr 4
@@ -104,13 +104,13 @@ lemma arm_zero [Nonempty (Fin K)]
 
 lemma arm_ae_eq_ucbNextArm [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (n : ℕ) :
-    A (n + 1) =ᵐ[P] fun ω ↦ nextArm hK c n (IsAlgEnvSeq.hist A R n ω) := by
+    A (n + 1) =ᵐ[P] fun ω ↦ nextArm hK c n (history A R n ω) := by
   have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
   exact h.action_detAlgorithm_ae_eq n
 
 lemma arm_ae_all_eq [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
-    ∀ᵐ h ∂P, A 0 h = ⟨0, hK⟩ ∧ ∀ n, A (n + 1) h = nextArm hK c n (IsAlgEnvSeq.hist A R n h) := by
+    ∀ᵐ h ∂P, A 0 h = ⟨0, hK⟩ ∧ ∀ n, A (n + 1) h = nextArm hK c n (history A R n h) := by
   rw [eventually_and, ae_all_iff]
   exact ⟨arm_zero h, arm_ae_eq_ucbNextArm h⟩
 
@@ -126,7 +126,7 @@ lemma ucbIndex_le_ucbIndex_arm [Nonempty (Fin K)]
   simp_rw [h_arm, empMean_eq_empMean' (by grind : n ≠ 0),
     ucbWidth_eq_ucbWidth' (A := A) (R := R) _ _ _ _ (by grind : n ≠ 0)]
   exact isMaxOn_measurableArgmax (fun h a ↦ empMean' (n - 1) h a + ucbWidth' c (n - 1) h a)
-    (IsAlgEnvSeq.hist A R (n - 1) h) a
+    (history A R (n - 1) h) a
 
 lemma forall_arm_eq_mod_of_lt [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
diff --git a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
index 0b615176..0ac59b3e 100644
--- a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
+++ b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
@@ -95,8 +95,8 @@ lemma condIndepFun_reward_stepsUntil_action' [StandardBorelSpace Ω]
     simp only [hn]
     refine h_indep.of_measurable_right (hX := hA 0) ?_
     exact measurable_comap_indicator_stepsUntil_eq_zero a m
-  · have h_indep : R n ⟂ᵢ[A n, hA n; P] fun ω ↦ (IsAlgEnvSeq.hist A R (n - 1) ω, A n ω) :=
-      IsAlgEnvSeq.condIndepFun_feedback_hist_action_action' h n (by grind)
+  · have h_indep : R n ⟂ᵢ[A n, hA n; P] fun ω ↦ (history A R (n - 1) ω, A n ω) :=
+      IsAlgEnvSeq.condIndepFun_feedback_history_action_action' h n (by grind)
     refine h_indep.of_measurable_right (hX := hA n) ?_
     exact measurable_comap_indicator_stepsUntil_eq hA hR a m n
 
diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean
index 4a47a8d6..ff4f58db 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithm.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean
@@ -97,14 +97,13 @@ variable {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 
     {P : Measure Ω} [IsFiniteMeasure P] {N : ℕ}
 
 /-- Step of the algorithm-environment sequence: the action-feedback pair at time `n`. -/
-def IsAlgEnvSeq.step (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : 𝓐 × 𝓨 :=
+def step (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : 𝓐 × 𝓨 :=
   (A n ω, Y n ω)
 
 @[fun_prop]
-lemma IsAlgEnvSeq.measurable_step (n : ℕ) (hA : Measurable (A n))
-    (hY : Measurable (Y n)) :
-    Measurable (IsAlgEnvSeq.step A Y n) := by
-  unfold IsAlgEnvSeq.step
+lemma measurable_step (n : ℕ) (hA : Measurable (A n)) (hY : Measurable (Y n)) :
+    Measurable (step A Y n) := by
+  unfold step
   fun_prop
 
 /-- A random variable that gives the sequence of action-feedback pairs. -/
@@ -117,24 +116,24 @@ lemma measurable_trajectory {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
   fun_prop
 
 /-- History of the algorithm-environment sequence up to time `n`. -/
-def IsAlgEnvSeq.hist (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : Iic n → 𝓐 × 𝓨 :=
+def history (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : Iic n → 𝓐 × 𝓨 :=
   fun i ↦ (A i ω, Y i ω)
 
 @[fun_prop]
-lemma IsAlgEnvSeq.measurable_hist (hA : ∀ n, Measurable (A n))
+lemma measurable_history (hA : ∀ n, Measurable (A n))
     (hY : ∀ n, Measurable (Y n)) (n : ℕ) :
-    Measurable (IsAlgEnvSeq.hist A Y n) := by
-  unfold IsAlgEnvSeq.hist
+    Measurable (history A Y n) := by
+  unfold history
   fun_prop
 
-lemma IsAlgEnvSeq.eval_comp_hist (n : ℕ) :
-    (fun x ↦ x ⟨n, by simp⟩) ∘ (hist A Y n) = step A Y n := rfl
+lemma eval_comp_history (n : ℕ) :
+    (fun x ↦ x ⟨n, by simp⟩) ∘ (history A Y n) = step A Y n := rfl
 
-lemma IsAlgEnvSeq.fst_eval_comp_hist (n : ℕ) :
-    (fun x ↦ (x ⟨n, by simp⟩).1) ∘ (hist A Y n) = A n := rfl
+lemma fst_eval_comp_history (n : ℕ) :
+    (fun x ↦ (x ⟨n, by simp⟩).1) ∘ (history A Y n) = A n := rfl
 
-lemma IsAlgEnvSeq.snd_eval_comp_hist (n : ℕ) :
-    (fun x ↦ (x ⟨n, by simp⟩).2) ∘ (hist A Y n) = Y n := rfl
+lemma snd_eval_comp_history (n : ℕ) :
+    (fun x ↦ (x ⟨n, by simp⟩).2) ∘ (history A Y n) = Y n := rfl
 
 section IsAlgEnvSeq
 
@@ -155,11 +154,11 @@ structure IsAlgEnvSeq
   hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (A 0) env.ν0 P
   /-- The next action has the correct conditional distribution given the history. -/
   hasCondDistrib_action n :
-    HasCondDistrib (A (n + 1)) (IsAlgEnvSeq.hist A Y n) (alg.policy n) P
+    HasCondDistrib (A (n + 1)) (history A Y n) (alg.policy n) P
   /-- The next feedback has the correct conditional distribution given the history and
   next action. -/
   hasCondDistrib_feedback n :
-    HasCondDistrib (Y (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A Y n ω, A (n + 1) ω))
+    HasCondDistrib (Y (n + 1)) (fun ω ↦ (history A Y n ω, A (n + 1) ω))
       (env.feedback n) P
 
 /-- An algorithm-environment sequence: a sequence of actions and feedbacks generated
@@ -177,11 +176,11 @@ structure IsAlgEnvSeqUntil
   hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (A 0) env.ν0 P
   /-- The next action has the correct conditional distribution given the history. -/
   hasCondDistrib_action n (hn : n < N) :
-    HasCondDistrib (A (n + 1)) (IsAlgEnvSeq.hist A Y n) (alg.policy n) P
+    HasCondDistrib (A (n + 1)) (history A Y n) (alg.policy n) P
   /-- The next feedback has the correct conditional distribution given the history and
   next action. -/
   hasCondDistrib_feedback n (hn : n < N) :
-    HasCondDistrib (Y (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A Y n ω, A (n + 1) ω))
+    HasCondDistrib (Y (n + 1)) (fun ω ↦ (history A Y n ω, A (n + 1) ω))
       (env.feedback n) P
 
 lemma IsAlgEnvSeqUntil.mono (h : IsAlgEnvSeqUntil A Y alg env P N) {N' : ℕ} (hN : N' ≤ N) :
@@ -202,30 +201,44 @@ lemma IsAlgEnvSeq.isAlgEnvSeqUntil (h : IsAlgEnvSeq A Y alg env P) (N : ℕ) :
   hasCondDistrib_action n _ := h.hasCondDistrib_action n
   hasCondDistrib_feedback n _ := h.hasCondDistrib_feedback n
 
+@[fun_prop]
+lemma IsAlgEnvSeq.measurable_step (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
+    Measurable (step A Y n) := by
+  have hA := h.measurable_action
+  have hY := h.measurable_feedback
+  fun_prop
+
+@[fun_prop]
+lemma IsAlgEnvSeq.measurable_history (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
+    Measurable (history A Y n) := by
+  have hA := h.measurable_action
+  have hY := h.measurable_feedback
+  fun_prop
+
 lemma IsAlgEnvSeq.hasLaw_step_zero (h : IsAlgEnvSeq A Y alg env P) :
     HasLaw (step A Y 0) (alg.p0 ⊗ₘ env.ν0) P :=
   HasLaw.prod_of_hasCondDistrib h.hasLaw_action_zero h.hasCondDistrib_feedback_zero
 
 lemma IsAlgEnvSeqUntil.hasLaw_step_zero (h : IsAlgEnvSeqUntil A Y alg env P N) :
-    HasLaw (IsAlgEnvSeq.step A Y 0) (alg.p0 ⊗ₘ env.ν0) P :=
+    HasLaw (step A Y 0) (alg.p0 ⊗ₘ env.ν0) P :=
   HasLaw.prod_of_hasCondDistrib h.hasLaw_action_zero h.hasCondDistrib_feedback_zero
 
 lemma IsAlgEnvSeq.hasCondDistrib_step (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
-    HasCondDistrib (step A Y (n + 1)) (hist A Y n) (stepKernel alg env n) P :=
+    HasCondDistrib (step A Y (n + 1)) (history A Y n) (stepKernel alg env n) P :=
   HasCondDistrib.prod (h.hasCondDistrib_action n) (h.hasCondDistrib_feedback n)
 
 lemma IsAlgEnvSeqUntil.hasCondDistrib_step (h : IsAlgEnvSeqUntil A Y alg env P N)
     (n : ℕ) (hn : n < N) :
-    HasCondDistrib (IsAlgEnvSeq.step A Y (n + 1)) (IsAlgEnvSeq.hist A Y n)
+    HasCondDistrib (step A Y (n + 1)) (history A Y n)
       (stepKernel alg env n) P :=
   HasCondDistrib.prod (h.hasCondDistrib_action n hn) (h.hasCondDistrib_feedback n hn)
 
-lemma IsAlgEnvSeq.hasLaw_hist_zero (h : IsAlgEnvSeq A Y alg env P) : HasLaw (hist A Y 0)
+lemma IsAlgEnvSeq.hasLaw_history_zero (h : IsAlgEnvSeq A Y alg env P) : HasLaw (history A Y 0)
     ((P.map (step A Y 0)).map (MeasurableEquiv.piUnique (fun _ : Iic 0 ↦ 𝓐 × 𝓨)).symm) P where
-  aemeasurable := (measurable_hist h.measurable_action h.measurable_feedback 0).aemeasurable
+  aemeasurable := (h.measurable_history 0).aemeasurable
   map_eq := by
     have he : (MeasurableEquiv.piUnique (fun _ : Iic 0 ↦ 𝓐 × 𝓨)).symm ∘ step A Y 0 =
-        hist A Y 0 := by
+        history A Y 0 := by
       funext _ ⟨0, _⟩
       rfl
     rw [← he]
@@ -233,16 +246,16 @@ lemma IsAlgEnvSeq.hasLaw_hist_zero (h : IsAlgEnvSeq A Y alg env P) : HasLaw (his
     have hY := h.measurable_feedback
     exact (Measure.map_map (by fun_prop) (by fun_prop)).symm
 
-lemma IsAlgEnvSeq.hasLaw_hist_succ (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
-  HasLaw (hist A Y (n + 1))
-    ((P.map (hist A Y n) ⊗ₘ condDistrib (step A Y (n + 1)) (hist A Y n) P).map
+lemma IsAlgEnvSeq.hasLaw_history_succ (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
+  HasLaw (history A Y (n + 1))
+    ((P.map (history A Y n) ⊗ₘ condDistrib (step A Y (n + 1)) (history A Y n) P).map
         (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm) P where
-  aemeasurable := (measurable_hist h.measurable_action h.measurable_feedback (n + 1)).aemeasurable
+  aemeasurable := (h.measurable_history (n + 1)).aemeasurable
   map_eq := by
     have he : (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm ∘
-        (fun ω ↦ (hist A Y n ω, step A Y (n + 1) ω)) = hist A Y (n + 1) := by
+        (fun ω ↦ (history A Y n ω, step A Y (n + 1) ω)) = history A Y (n + 1) := by
       funext ω
-      exact (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm_apply_apply (hist A Y (n + 1) ω)
+      exact (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm_apply_apply (history A Y (n + 1) ω)
     have hA := h.measurable_action
     have hY := h.measurable_feedback
     rw [← he, ← Measure.map_map (by fun_prop) (by fun_prop)]
@@ -254,29 +267,29 @@ end IsAlgEnvSeq
 /-- Filtration generated by the history up to time `n`. -/
 def IsAlgEnvSeq.filtration (hA : ∀ n, Measurable (A n)) (hY : ∀ n, Measurable (Y n)) :
     Filtration ℕ mΩ where
-  seq i := MeasurableSpace.comap (hist A Y i) inferInstance
+  seq i := MeasurableSpace.comap (history A Y i) inferInstance
   mono' i j hij := by
     simp only
     rw [← measurable_iff_comap_le]
-    have : hist A Y i = (fun h k ↦ h ⟨k.1, by grind⟩) ∘ hist A Y j := rfl
+    have : history A Y i = (fun h k ↦ h ⟨k.1, by grind⟩) ∘ history A Y j := rfl
     rw [this]
     exact measurable_comp_comap _ (by fun_prop)
   le' i := by
     rw [← measurable_iff_comap_le]
-    exact measurable_hist hA hY i
+    exact Learning.measurable_history hA hY i
 
-lemma IsAlgEnvSeq.adapted_hist
+lemma IsAlgEnvSeq.adapted_history
     (hA : ∀ n, Measurable (A n)) (hY : ∀ n, Measurable (Y n)) :
-    Adapted (filtration hA hY) (IsAlgEnvSeq.hist A Y) :=
+    Adapted (filtration hA hY) (history A Y) :=
   fun _ ↦ measurable_iff_comap_le.mpr le_rfl
 
 lemma IsAlgEnvSeq.adapted_step
     (hA : ∀ n, Measurable (A n)) (hY : ∀ n, Measurable (Y n)) :
     Adapted (filtration hA hY) (step A Y) := by
   intro n
-  have : step A Y n = (fun h ↦ (h ⟨n, by simp⟩)) ∘ (hist A Y n) := by
+  have : step A Y n = (fun h ↦ (h ⟨n, by simp⟩)) ∘ (history A Y n) := by
     ext ω : 1
-    simp [hist, step]
+    simp [history, step]
   rw [this]
   exact measurable_comp_comap _ (by fun_prop)
 
@@ -284,9 +297,9 @@ lemma IsAlgEnvSeq.adapted_action
     (hA : ∀ n, Measurable (A n)) (hY : ∀ n, Measurable (Y n)) :
     Adapted (filtration hA hY) A := by
   intro n
-  have : A n = (fun h ↦ (h ⟨n, by simp⟩).1) ∘ (hist A Y n) := by
+  have : A n = (fun h ↦ (h ⟨n, by simp⟩).1) ∘ (history A Y n) := by
     ext ω : 1
-    simp [IsAlgEnvSeq.hist]
+    simp [history]
   rw [this]
   exact measurable_comp_comap _ (by fun_prop)
 
@@ -294,9 +307,9 @@ lemma IsAlgEnvSeq.adapted_feedback
     (hA : ∀ n, Measurable (A n)) (hY : ∀ n, Measurable (Y n)) :
     Adapted (filtration hA hY) Y := by
   intro n
-  have : Y n = (fun h ↦ (h ⟨n, by simp⟩).2) ∘ (hist A Y n) := by
+  have : Y n = (fun h ↦ (h ⟨n, by simp⟩).2) ∘ (history A Y n) := by
     ext ω : 1
-    simp [IsAlgEnvSeq.hist]
+    simp [history]
   rw [this]
   exact measurable_comp_comap _ (by fun_prop)
 
@@ -351,7 +364,7 @@ lemma IsAlgEnvSeq.filtrationAction_zero_eq_comap
 lemma IsAlgEnvSeq.filtrationAction_eq_comap
     {hA : ∀ n, Measurable (A n)} {hY : ∀ n, Measurable (Y n)} (n : ℕ) (hn : n ≠ 0) :
     filtrationAction hA hY n =
-      MeasurableSpace.comap (fun ω ↦ (hist A Y (n - 1) ω, A n ω)) inferInstance := by
+      MeasurableSpace.comap (fun ω ↦ (history A Y (n - 1) ω, A n ω)) inferInstance := by
   simp only [filtrationAction, filtration, ← MeasurableSpace.comap_prodMk, hn, ↓reduceIte]
   rfl
 
diff --git a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean
index 50a5ef43..120f0fd9 100644
--- a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean
+++ b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean
@@ -32,7 +32,7 @@ concept that we also introduce here.
 * `absolutelyContinuous_map_hist`: the law of the history at time `n` under `alg` is absolutely
   continuous with respect to the law of the history at time `n` under `alg₀` when they
   are interacting with the same environment and `alg ≪ₐ alg₀`.
-* `hasLaw_hist_withDensity`: the law of the history at time `n` under `alg` is the law of the
+* `hasLaw_history_withDensity`: the law of the history at time `n` under `alg` is the law of the
   history at time `n` under `alg₀` with density `alg.density alg₀ n` when they are interacting
   with the same environment and `alg ≪ₐ alg₀`.
 
@@ -94,32 +94,31 @@ variable {alg₀ : Algorithm 𝓐 𝓨}
 variable {A₀ : ℕ → Ω₀ → 𝓐} {Y₀ : ℕ → Ω₀ → 𝓨}
 variable {P₀ : Measure Ω₀} [IsProbabilityMeasure P₀]
 
-lemma absolutelyContinuous_map_hist (h : IsAlgEnvSeq A Y alg env P)
+lemma absolutelyContinuous_map_history (h : IsAlgEnvSeq A Y alg env P)
     (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
-    P.map (IsAlgEnvSeq.hist A Y n) ≪ P₀.map (IsAlgEnvSeq.hist A₀ Y₀ n) := by
+    P.map (history A Y n) ≪ P₀.map (history A₀ Y₀ n) := by
   induction n with
   | zero =>
-    rw [h.hasLaw_hist_zero.map_eq, h₀.hasLaw_hist_zero.map_eq]
+    rw [h.hasLaw_history_zero.map_eq, h₀.hasLaw_history_zero.map_eq]
     apply Measure.AbsolutelyContinuous.map _ (by fun_prop)
     rw [h.hasLaw_step_zero.map_eq, h₀.hasLaw_step_zero.map_eq]
     exact Measure.AbsolutelyContinuous.compProd_left hc.p0 _
   | succ n ih =>
-    rw [(h.hasLaw_hist_succ n).map_eq, (h₀.hasLaw_hist_succ n).map_eq]
+    rw [(h.hasLaw_history_succ n).map_eq, (h₀.hasLaw_history_succ n).map_eq]
     apply Measure.AbsolutelyContinuous.map _ (by fun_prop)
     rw [Measure.compProd_congr (h.hasCondDistrib_step n).condDistrib_eq,
         Measure.compProd_congr (h₀.hasCondDistrib_step n).condDistrib_eq]
     apply Measure.AbsolutelyContinuous.compProd ih
     filter_upwards with h' using Measure.AbsolutelyContinuous.compProd_left_apply (hc.policy n h') _
 
-lemma hasLaw_hist_withDensity (h : IsAlgEnvSeq A Y alg env P) (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀)
-   (hc : alg ≪ₐ alg₀) (n : ℕ) : HasLaw (IsAlgEnvSeq.hist A Y n)
-      ((P₀.map (IsAlgEnvSeq.hist A₀ Y₀ n)).withDensity (alg.density alg₀ n)) P where
-  aemeasurable :=
-    (IsAlgEnvSeq.measurable_hist h.measurable_action h.measurable_feedback n).aemeasurable
+lemma hasLaw_history_withDensity (h : IsAlgEnvSeq A Y alg env P)
+    (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) : HasLaw (history A Y n)
+      ((P₀.map (history A₀ Y₀ n)).withDensity (alg.density alg₀ n)) P where
+  aemeasurable := (h.measurable_history n).aemeasurable
   map_eq := by
     induction n with
     | zero =>
-      rw [h.hasLaw_hist_zero.map_eq, h₀.hasLaw_hist_zero.map_eq, h.hasLaw_step_zero.map_eq,
+      rw [h.hasLaw_history_zero.map_eq, h₀.hasLaw_history_zero.map_eq, h.hasLaw_step_zero.map_eq,
         h₀.hasLaw_step_zero.map_eq]
       rw [← Measure.withDensity_rnDeriv_eq _ _ hc.p0,
         Measure.compProd_withDensity_left (by fun_prop)]
@@ -132,7 +131,7 @@ lemma hasLaw_hist_withDensity (h : IsAlgEnvSeq A Y alg env P) (h₀ : IsAlgEnvSe
       have : IsMarkovKernel ((stepKernel alg₀ env n).withDensity ρ) := by
         rw [← hs]
         infer_instance
-      rw [(h.hasLaw_hist_succ n).map_eq, (h₀.hasLaw_hist_succ n).map_eq,
+      rw [(h.hasLaw_history_succ n).map_eq, (h₀.hasLaw_history_succ n).map_eq,
           Measure.compProd_congr (h.hasCondDistrib_step n).condDistrib_eq,
           Measure.compProd_congr (h₀.hasCondDistrib_step n).condDistrib_eq, ih, hs,
           Measure.compProd_withDensity_withDensity (by fun_prop) (by fun_prop)]
diff --git a/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean b/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean
index 42f381b7..8acca0dd 100644
--- a/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean
+++ b/LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean
@@ -23,10 +23,10 @@ Let `h : IsBayesAlgEnvSeq Q κ alg E A Y P`, `h₀ : IsBayesAlgEnvSeq Q κ alg
   the history at time `n` under `P₀` with density `alg.density alg₀ n`. Intuitively, the law of the
   history under `alg` can be obtained from the law of the history under `alg₀` when they are
   interacting with underlying stationary environments drawn from the same distribution.
-* `hasCondDistrib_env_hist h h₀ hc n`: the conditional distribution of `E` given the history at time
-  `n` under `P` is almost everywhere equal to the conditional distribution of `E₀` given the history
-  at time `n` under `P₀`. Intuitively, the posterior is independent of the algorithm used to observe
-  the history.
+* `hasCondDistrib_env_history h h₀ hc n`: the conditional distribution of `E` given the history
+  at time `n` under `P` is almost everywhere equal to the conditional distribution of `E₀` given
+  the history at time `n` under `P₀`. Intuitively, the posterior is independent of the algorithm
+  used to observe the history.
 
 -/
 
@@ -56,22 +56,21 @@ variable {E₀ : Ω₀ → 𝓔} {A₀ : ℕ → Ω₀ → 𝓐} {Y₀ : ℕ →
 variable {alg₀ : Algorithm 𝓐 𝓨}
 variable {P₀ : Measure Ω₀} [IsProbabilityMeasure P₀]
 
-lemma condDistrib_hist_eq_condDistrib_hist_withDensity (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
+lemma condDistrib_history_eq_condDistrib_hist_withDensity (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
     (h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
-    condDistrib (IsAlgEnvSeq.hist A Y n) E P =ᵐ[Q]
-      ((condDistrib (IsAlgEnvSeq.hist A₀ Y₀ n) E₀ P₀).withDensity
+    condDistrib (history A Y n) E P =ᵐ[Q]
+      ((condDistrib (history A₀ Y₀ n) E₀ P₀).withDensity
         (fun _ ↦ alg.density alg₀ n)) := by
     filter_upwards [h.ae_IsAlgEnvSeq, h₀.ae_IsAlgEnvSeq, h.hasLaw_IT_hist n, h₀.hasLaw_IT_hist n]
       with _ hae hae₀ he he₀
     rw [Kernel.withDensity_apply _ (by fun_prop), ← he.map_eq, ← he₀.map_eq]
-    exact (hae.hasLaw_hist_withDensity hae₀ hc n).map_eq
+    exact (hae.hasLaw_history_withDensity hae₀ hc n).map_eq
 
-lemma hasLaw_hist_withDensity (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
+lemma hasLaw_history_withDensity (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
     (h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
-    HasLaw (IsAlgEnvSeq.hist A Y n)
-      ((P₀.map (IsAlgEnvSeq.hist A₀ Y₀ n)).withDensity (alg.density alg₀ n)) P where
-  aemeasurable :=
-    (IsAlgEnvSeq.measurable_hist h.measurable_action h.measurable_feedback n).aemeasurable
+    HasLaw (history A Y n)
+      ((P₀.map (history A₀ Y₀ n)).withDensity (alg.density alg₀ n)) P where
+  aemeasurable := (measurable_history h.measurable_action h.measurable_feedback n).aemeasurable
   map_eq := by
     have hA := h.measurable_action
     have hY := h.measurable_feedback
@@ -80,20 +79,19 @@ lemma hasLaw_hist_withDensity (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
     have hE := h.measurable_param
     have hE₀ := h₀.measurable_param
     rw [← condDistrib_comp_map hE.aemeasurable (by fun_prop), h.hasLaw_env.map_eq,
-          Measure.bind_congr_right (h.condDistrib_hist_eq_condDistrib_hist_withDensity h₀ hc n),
+          Measure.bind_congr_right (h.condDistrib_history_eq_condDistrib_hist_withDensity h₀ hc n),
           Kernel.comp_withDensity_eq_withDensity_comp (by fun_prop),
           ← h₀.hasLaw_env.map_eq, condDistrib_comp_map hE₀.aemeasurable (by fun_prop)]
 
 variable [StandardBorelSpace 𝓔] [Nonempty 𝓔]
 variable [IsProbabilityMeasure Q]
 
-lemma hasCondDistrib_env_hist (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
+lemma hasCondDistrib_env_history (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
     (h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
-    HasCondDistrib E (IsAlgEnvSeq.hist A Y n)
-      (condDistrib E₀ (IsAlgEnvSeq.hist A₀ Y₀ n) P₀) P where
+    HasCondDistrib E (history A Y n) (condDistrib E₀ (history A₀ Y₀ n) P₀) P where
   aemeasurable_fst := h.measurable_param.aemeasurable
   aemeasurable_snd :=
-    (IsAlgEnvSeq.measurable_hist h.measurable_action h.measurable_feedback n).aemeasurable
+    (measurable_history h.measurable_action h.measurable_feedback n).aemeasurable
   condDistrib_eq := by
     have hA := h.measurable_action
     have hY := h.measurable_feedback
@@ -104,12 +102,12 @@ lemma hasCondDistrib_env_hist (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
     rw [condDistrib_ae_eq_iff_measure_eq_compProd _ h.measurable_param.aemeasurable,
       ← map_swap_compProd_map_condDistrib (by fun_prop), h.hasLaw_env.map_eq,
       Measure.compProd_eq_compProd_withDensity_comp_snd (by fun_prop)
-        (h.condDistrib_hist_eq_condDistrib_hist_withDensity h₀ hc n),
+        (h.condDistrib_history_eq_condDistrib_hist_withDensity h₀ hc n),
       map_swap_withDensity_comp_snd (by fun_prop),
       ← h₀.hasLaw_env.map_eq, map_swap_compProd_map_condDistrib (by fun_prop),
       ← compProd_map_condDistrib (by fun_prop),
       ← Measure.compProd_withDensity_left (by fun_prop),
-      ← (hasLaw_hist_withDensity h h₀ hc n).map_eq]
+      ← (hasLaw_history_withDensity h h₀ hc n).map_eq]
 
 end IsBayesAlgEnvSeq
 
diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean
index 63c69644..8f25f41e 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean
@@ -72,7 +72,7 @@ lemma iIndep_action (h : IsAlgEnvSeq A Y (randomSampling μ) env P) :
   · have meas_fst : Measurable (fun (f : Iic n → 𝓐 × 𝓨) ↦ (fun i ↦ (f i).1)) := by
       fun_prop
     exact (condDistrib_eq.comp meas_fst measurable_id).symm
-  · exact (IsAlgEnvSeq.measurable_hist (h.measurable_action) (h.measurable_feedback) n).aemeasurable
+  · exact (h.measurable_history n).aemeasurable
 
 end randomSampling
 
diff --git a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean
index 00fb411a..c5b8b039 100644
--- a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean
+++ b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean
@@ -67,10 +67,10 @@ structure IsBayesAlgEnvSeq
   hasCondDistrib_action_zero : HasCondDistrib (A 0) E (Kernel.const _ alg.p0) P
   hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (fun ω ↦ (E ω, A 0 ω)) κ P
   hasCondDistrib_action n :
-    HasCondDistrib (A (n + 1)) (fun ω ↦ (E ω, IsAlgEnvSeq.hist A Y n ω))
+    HasCondDistrib (A (n + 1)) (fun ω ↦ (E ω, history A Y n ω))
       ((alg.policy n).prodMkLeft _) P
   hasCondDistrib_feedback n :
-    HasCondDistrib (Y (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A Y n ω, E ω, A (n + 1) ω))
+    HasCondDistrib (Y (n + 1)) (fun ω ↦ (history A Y n ω, E ω, A (n + 1) ω))
       (κ.prodMkLeft _) P
 
 namespace IsBayesAlgEnvSeq
@@ -84,7 +84,7 @@ lemma hasLaw_action_zero [IsProbabilityMeasure P] (h : IsBayesAlgEnvSeq Q κ alg
     HasLaw (A 0) alg.p0 P := h.hasCondDistrib_action_zero.hasLaw_of_const
 
 lemma hasCondDistrib_action' (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) :
-    HasCondDistrib (A (n + 1)) (IsAlgEnvSeq.hist A Y n) (alg.policy n) P :=
+    HasCondDistrib (A (n + 1)) (history A Y n) (alg.policy n) P :=
   (h.hasCondDistrib_action n).comp_right' (by fun_prop)
 
 lemma hasCondDistrib_feedback' [IsFiniteKernel κ] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) :
@@ -125,7 +125,7 @@ lemma hasCondDistrib_IT_feedback [IsFiniteKernel κ] (h : IsBayesAlgEnvSeq Q κ
       ((κ.sectR e).prodMkLeft _) (condDistrib (trajectory A Y) E P e) := by
   rw [← h.hasLaw_env.map_eq]
   have hc : HasCondDistrib (Y (n + 1))
-      (fun ω ↦ (E ω, IsAlgEnvSeq.hist A Y n ω, A (n + 1) ω))
+      (fun ω ↦ (E ω, history A Y n ω, A (n + 1) ω))
       (κ.comap (fun (e, _, a) ↦ (e, a)) (by fun_prop)) P :=
     (h.hasCondDistrib_feedback n).comp_right (MeasurableEquiv.prodAssoc.symm.trans
       ((MeasurableEquiv.prodCongr .prodComm (.refl _)).trans .prodAssoc))
@@ -134,9 +134,9 @@ lemma hasCondDistrib_IT_feedback [IsFiniteKernel κ] (h : IsBayesAlgEnvSeq Q κ
     (measurable_trajectory h.measurable_action h.measurable_feedback).aemeasurable
 
 lemma hasLaw_IT_hist (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) :
-    ∀ᵐ e ∂Q, HasLaw (IT.hist n) (condDistrib (IsAlgEnvSeq.hist A Y n) E P e)
+    ∀ᵐ e ∂Q, HasLaw (IT.hist n) (condDistrib (history A Y n) E P e)
       (condDistrib (trajectory A Y) E P e) := by
-  rw [← h.hasLaw_env.map_eq, show IsAlgEnvSeq.hist A Y n = IT.hist n ∘ trajectory A Y from rfl]
+  rw [← h.hasLaw_env.map_eq, show history A Y n = IT.hist n ∘ trajectory A Y from rfl]
   filter_upwards [condDistrib_comp E
     (measurable_trajectory h.measurable_action h.measurable_feedback).aemeasurable
     (IT.measurable_hist n)] with _ he
@@ -190,7 +190,7 @@ lemma IsAlgEnvSeq.isBayesAlgEnvSeq
   hasCondDistrib_action n := by
     let f : (Iic n → 𝓐 × 𝓔 × 𝓨) → 𝓔 × (Iic n → 𝓐 × 𝓨) :=
       fun h ↦ ((h ⟨0, by simp⟩).2.1, fun i ↦ ((h i).1, (h i).2.2))
-    have hc : HasCondDistrib (A (n + 1)) (IsAlgEnvSeq.hist A Y n)
+    have hc : HasCondDistrib (A (n + 1)) (history A Y n)
         (((alg.policy n).comap Prod.snd (by fun_prop)).comap f (by fun_prop)) P :=
       h.hasCondDistrib_action n
     exact hc.comp_right' (f := f)
@@ -198,7 +198,7 @@ lemma IsAlgEnvSeq.isBayesAlgEnvSeq
     let f : (Iic n → 𝓐 × 𝓔 × 𝓨) × 𝓐 → (Iic n → 𝓐 × 𝓨) × 𝓔 × 𝓐 :=
       fun p ↦ ((fun i ↦ ((p.1 i).1, (p.1 i).2.2)), (p.1 ⟨0, by simp⟩).2.1, p.2)
     have hc : HasCondDistrib (fun ω ↦ (Y (n + 1) ω).2)
-        (fun ω ↦ (IsAlgEnvSeq.hist A Y n ω, A (n + 1) ω))
+        (fun ω ↦ (history A Y n ω, A (n + 1) ω))
         ((Kernel.prodMkLeft ((Iic n) → 𝓐 × 𝓨) κ).comap f (by fun_prop)) P := by
       simpa [bayesStationaryEnv, Kernel.prodMkLeft, ← Kernel.comap_comp_right, Function.comp_def]
         using (h.hasCondDistrib_feedback n).snd
@@ -230,7 +230,7 @@ noncomputable
 def bayesTrajMeasurePosterior [StandardBorelSpace 𝓔] [Nonempty 𝓔]
     (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (𝓔 × 𝓐) 𝓨) [IsMarkovKernel κ]
     (alg : Algorithm 𝓐 𝓨) (n : ℕ) : Kernel (Iic n → 𝓐 × 𝓨) 𝓔 :=
-  condDistrib (fun ω ↦ (ω 0).2.1) (IsAlgEnvSeq.hist action (fun n ω ↦ (ω n).2.2) n)
+  condDistrib (fun ω ↦ (ω 0).2.1) (history action (fun n ω ↦ (ω n).2.2) n)
     (bayesTrajMeasure Q κ alg)
 deriving IsMarkovKernel
 
diff --git a/LeanMachineLearning/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean
index 60f4929b..70e0346e 100644
--- a/LeanMachineLearning/SequentialLearning/Deterministic.lean
+++ b/LeanMachineLearning/SequentialLearning/Deterministic.lean
@@ -103,7 +103,7 @@ lemma action_zero_of_IsAlgEnvSeqUntil [h_det : IsDeterministicAlg alg]
 
 lemma action_ae_eq_of_IsAlgEnvSeqUntil [h_det : IsDeterministicAlg alg]
     (h : IsAlgEnvSeqUntil A Y alg env P N) (hn : n < N) :
-    A (n + 1) =ᵐ[P] fun ω ↦ nextAction alg n (IsAlgEnvSeq.hist A Y n ω) := by
+    A (n + 1) =ᵐ[P] fun ω ↦ nextAction alg n (history A Y n ω) := by
   have hA := h.measurable_action
   have hY := h.measurable_feedback
   have h_eq := (h.hasCondDistrib_action n hn).condDistrib_eq
@@ -121,12 +121,12 @@ lemma action_zero_ae_eq [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A Y al
   action_zero_of_IsAlgEnvSeqUntil (h.isAlgEnvSeqUntil 0)
 
 lemma action_ae_eq [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
-    A (n + 1) =ᵐ[P] fun ω ↦ nextAction alg n (IsAlgEnvSeq.hist A Y n ω) :=
+    A (n + 1) =ᵐ[P] fun ω ↦ nextAction alg n (history A Y n ω) :=
   action_ae_eq_of_IsAlgEnvSeqUntil (h.isAlgEnvSeqUntil (n + 1)) (by simp)
 
 lemma action_ae_all_eq [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A Y alg env P) :
     ∀ᵐ ω ∂P, A 0 ω = actionZero alg ∧
-      ∀ n, A (n + 1) ω = nextAction alg n (IsAlgEnvSeq.hist A Y n ω) := by
+      ∀ n, A (n + 1) ω = nextAction alg n (history A Y n ω) := by
   rw [eventually_and, ae_all_iff]
   exact ⟨action_zero_ae_eq h, action_ae_eq h⟩
 
@@ -186,7 +186,7 @@ lemma hasCondDistrib_feedback_zero [h_det : IsDeterministicEnv env]
 
 lemma hasCondDistrib_feedback [h_det : IsDeterministicEnv env]
     (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
-    HasCondDistrib (Y (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A Y n ω, A (n + 1) ω))
+    HasCondDistrib (Y (n + 1)) (fun ω ↦ (history A Y n ω, A (n + 1) ω))
       (Kernel.deterministic (feedbackFun env n) (measurable_feedbackFun env n)) P := by
   rw [← feedback_eq_deterministic]
   exact h.hasCondDistrib_feedback n
@@ -267,12 +267,12 @@ lemma action_zero_detAlgorithm
 
 lemma action_detAlgorithm_ae_eq
     (h : IsAlgEnvSeq A Y (detAlgorithm nextA h_next action0) env P) (n : ℕ) :
-    A (n + 1) =ᵐ[P] fun ω ↦ nextA n (hist A Y n ω) :=
+    A (n + 1) =ᵐ[P] fun ω ↦ nextA n (history A Y n ω) :=
   (IsDeterministicAlg.action_ae_eq h n).trans (by simp)
 
 lemma action_detAlgorithm_ae_all_eq
     (h : IsAlgEnvSeq A Y (detAlgorithm nextA h_next action0) env P) :
-    ∀ᵐ ω ∂P, A 0 ω = action0 ∧ ∀ n, A (n + 1) ω = nextA n (hist A Y n ω) := by
+    ∀ᵐ ω ∂P, A 0 ω = action0 ∧ ∀ n, A (n + 1) ω = nextA n (history A Y n ω) := by
   filter_upwards [IsDeterministicAlg.action_ae_all_eq h] with ω hω using by simp [hω]
 
 end IsAlgEnvSeq
@@ -296,7 +296,7 @@ lemma action_zero_detAlgorithm
 
 lemma action_detAlgorithm_ae_eq
     (h : IsAlgEnvSeqUntil A Y (detAlgorithm nextA h_next action0) env P N) (hn : n < N) :
-    A (n + 1) =ᵐ[P] fun ω ↦ nextA n (IsAlgEnvSeq.hist A Y n ω) :=
+    A (n + 1) =ᵐ[P] fun ω ↦ nextA n (history A Y n ω) :=
   (IsDeterministicAlg.action_ae_eq_of_IsAlgEnvSeqUntil h hn).trans (by simp)
 
 end IsAlgEnvSeqUntil
diff --git a/LeanMachineLearning/SequentialLearning/FiniteActions.lean b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
index 369e862b..8a13a8e7 100644
--- a/LeanMachineLearning/SequentialLearning/FiniteActions.lean
+++ b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
@@ -225,7 +225,7 @@ lemma adapted_pullCount_add_one [MeasurableSingletonClass 𝓐]
     Adapted (IsAlgEnvSeq.filtration hA hR') (fun n ↦ pullCount A a (n + 1)) := by
   intro n
   have : pullCount A a (n + 1) = (fun h : Iic n → 𝓐 × R ↦ pullCount' n h a) ∘
-      (IsAlgEnvSeq.hist A R' n) := by
+      (history A R' n) := by
     ext
     exact pullCount_add_one_eq_pullCount'
   rw [measurable_iff_comap_le]
@@ -564,7 +564,7 @@ lemma measurable_stepsUntil' [MeasurableSingletonClass 𝓐]
 lemma measurable_comap_indicator_stepsUntil_eq [MeasurableSingletonClass 𝓐]
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (m n : ℕ) :
     Measurable[MeasurableSpace.comap
-        (fun ω : Ω ↦ (IsAlgEnvSeq.hist A R' (n-1) ω, A n ω)) inferInstance]
+        (fun ω : Ω ↦ (history A R' (n-1) ω, A n ω)) inferInstance]
       ({ω | stepsUntil A a m ω = ↑n}.indicator fun _ ↦ 1) := by
   by_cases hm : m = 0
   · simp only [hm]
@@ -631,11 +631,11 @@ lemma measurable_comap_indicator_stepsUntil_eq_zero [MeasurableSingletonClass 
 
 lemma measurableSet_stepsUntil_eq [MeasurableSingletonClass 𝓐]
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : 𝓐) (m n : ℕ) :
-    MeasurableSet[MeasurableSpace.comap (fun ω : Ω ↦ (IsAlgEnvSeq.hist A R' (n-1) ω, A n ω))
+    MeasurableSet[MeasurableSpace.comap (fun ω : Ω ↦ (history A R' (n-1) ω, A n ω))
         inferInstance]
       {ω : Ω | stepsUntil A a m ω = ↑n} := by
   let mProd := MeasurableSpace.comap
-    (fun ω : Ω ↦ (IsAlgEnvSeq.hist A R' (n-1) ω, A n ω)) inferInstance
+    (fun ω : Ω ↦ (history A R' (n-1) ω, A n ω)) inferInstance
   suffices Measurable[mProd] ({ω | stepsUntil A a m ω = ↑n}.indicator fun x ↦ 1) by
     rwa [measurable_indicator_const_iff] at this
   exact measurable_comap_indicator_stepsUntil_eq hA hR' a m n
diff --git a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
index a479ca1e..1efdce54 100644
--- a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
+++ b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
@@ -89,7 +89,7 @@ lemma hasCondDistrib_feedback [IsObliviousEnv env] (h : IsAlgEnvSeq A Y alg env
     have h_eq := (h.hasCondDistrib_feedback n).condDistrib_eq
     rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h_eq ⊢
     have : P.map (A (n + 1)) =
-        (P.map (fun x ↦ (IsAlgEnvSeq.hist A Y n x, A (n + 1) x))).snd := by
+        (P.map (fun x ↦ (history A Y n x, A (n + 1) x))).snd := by
       rw [Measure.snd_map_prodMk (by fun_prop)]
     simp only [feedback_eq_feedbackCondAction] at h_eq
     rw [this, ← Measure.snd_prodAssoc_compProd_prodMkLeft, ← h_eq,
@@ -98,9 +98,9 @@ lemma hasCondDistrib_feedback [IsObliviousEnv env] (h : IsAlgEnvSeq A Y alg env
 
 /-- The feedback at time `n + 1` is conditionally independent of the history up to time `n`
 given the action at time `n + 1`. -/
-lemma condIndepFun_feedback_hist_action [StandardBorelSpace Ω]
+lemma condIndepFun_feedback_history_action [StandardBorelSpace Ω]
         [IsObliviousEnv env] (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
-    Y (n + 1) ⟂ᵢ[A (n + 1), h.measurable_action _ ; P] IsAlgEnvSeq.hist A Y n := by
+    Y (n + 1) ⟂ᵢ[A (n + 1), h.measurable_action _ ; P] history A Y n := by
   have hA := h.measurable_action
   have hY := h.measurable_feedback
   refine condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft
@@ -110,20 +110,20 @@ lemma condIndepFun_feedback_hist_action [StandardBorelSpace Ω]
   rw [← feedback_eq_feedbackCondAction]
   exact h.hasCondDistrib_feedback n
 
-lemma condIndepFun_feedback_hist_action_action [StandardBorelSpace Ω]
+lemma condIndepFun_feedback_history_action_action [StandardBorelSpace Ω]
     [IsObliviousEnv env] (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
     Y (n + 1) ⟂ᵢ[A (n + 1), h.measurable_action (n + 1); P]
-      (fun ω ↦ (IsAlgEnvSeq.hist A Y n ω, A (n + 1) ω)) := by
-  have h_indep : Y (n + 1) ⟂ᵢ[A (n + 1), h.measurable_action (n + 1); P] IsAlgEnvSeq.hist A Y n :=
-    condIndepFun_feedback_hist_action h n
+      (fun ω ↦ (history A Y n ω, A (n + 1) ω)) := by
+  have h_indep : Y (n + 1) ⟂ᵢ[A (n + 1), h.measurable_action (n + 1); P] history A Y n :=
+    condIndepFun_feedback_history_action h n
   have hA := h.measurable_action
   have hY := h.measurable_feedback
   exact h_indep.prod_right (by fun_prop) (by fun_prop) (by fun_prop)
 
-lemma condIndepFun_feedback_hist_action_action' [StandardBorelSpace Ω]
+lemma condIndepFun_feedback_history_action_action' [StandardBorelSpace Ω]
         [IsObliviousEnv env] (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) (hn : n ≠ 0) :
-    Y n ⟂ᵢ[A n, h.measurable_action n; P] (fun ω ↦ (IsAlgEnvSeq.hist A Y (n - 1) ω, A n ω)) := by
-  have := condIndepFun_feedback_hist_action_action h (n - 1)
+    Y n ⟂ᵢ[A n, h.measurable_action n; P] (fun ω ↦ (history A Y (n - 1) ω, A n ω)) := by
+  have := condIndepFun_feedback_history_action_action h (n - 1)
   grind
 
 end IsObliviousEnv
@@ -206,21 +206,21 @@ lemma condDistrib_feedback_stationaryEnv
 
 /-- The feedback at time `n + 1` is conditionally independent of the history up to time `n`
 given the action at time `n + 1`. -/
-lemma condIndepFun_feedback_hist_action [StandardBorelSpace Ω]
+lemma condIndepFun_feedback_history_action [StandardBorelSpace Ω]
     (h : IsAlgEnvSeq A Y alg (stationaryEnv ν) P) (n : ℕ) :
-    Y (n + 1) ⟂ᵢ[A (n + 1), h.measurable_action _ ; P] hist A Y n :=
-  IsObliviousEnv.condIndepFun_feedback_hist_action h n
+    Y (n + 1) ⟂ᵢ[A (n + 1), h.measurable_action _ ; P] history A Y n :=
+  IsObliviousEnv.condIndepFun_feedback_history_action h n
 
-lemma condIndepFun_feedback_hist_action_action [StandardBorelSpace Ω]
+lemma condIndepFun_feedback_history_action_action [StandardBorelSpace Ω]
     (h : IsAlgEnvSeq A Y alg (stationaryEnv ν) P) (n : ℕ) :
     Y (n + 1) ⟂ᵢ[A (n + 1), h.measurable_action (n + 1); P]
-      (fun ω ↦ (hist A Y n ω, A (n + 1) ω)) :=
-  IsObliviousEnv.condIndepFun_feedback_hist_action_action h n
+      (fun ω ↦ (history A Y n ω, A (n + 1) ω)) :=
+  IsObliviousEnv.condIndepFun_feedback_history_action_action h n
 
-lemma condIndepFun_feedback_hist_action_action' [StandardBorelSpace Ω]
+lemma condIndepFun_feedback_history_action_action' [StandardBorelSpace Ω]
     (h : IsAlgEnvSeq A Y alg (stationaryEnv ν) P) (n : ℕ) (hn : n ≠ 0) :
-    Y n ⟂ᵢ[A n, h.measurable_action n; P] (fun ω ↦ (hist A Y (n - 1) ω, A n ω)) :=
-  IsObliviousEnv.condIndepFun_feedback_hist_action_action' h n hn
+    Y n ⟂ᵢ[A n, h.measurable_action n; P] (fun ω ↦ (history A Y (n - 1) ω, A n ω)) :=
+  IsObliviousEnv.condIndepFun_feedback_history_action_action' h n hn
 
 end IsAlgEnvSeq