Rename history and step (#140)

Author: RemyDegenne

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]

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) :

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
 

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,47 +201,61 @@ 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]
     have hA := h.measurable_action
     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,49 +267,49 @@ 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)
 
 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)
 
 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
 

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)]