diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanBandits/Bandit/Bandit.lean
index 8c81862f..a53c2b60 100644
--- a/LeanBandits/Bandit/Bandit.lean
+++ b/LeanBandits/Bandit/Bandit.lean
@@ -273,47 +273,6 @@ lemma hist_add_one_eq_IicSuccProd' [DecidableEq α] (alg : Algorithm α R) (ω :
     Equiv.coe_fn_mk, Prod.map_apply, id_eq]
   rfl
 
-lemma measurable_action_add_one' [DecidableEq α] {alg : Algorithm α R}
-    (n : ℕ) (h : Measurable (hist alg · n)) :
-    Measurable (fun x ↦ algFunction alg n (hist alg x n) (x.1 (n + 1))) := by fun_prop
-
-lemma measurable_pullCount'_action_add_one [DecidableEq α] {alg : Algorithm α R}
-    (n : ℕ) (h_hist : Measurable (hist alg · n)) :
-    Measurable (fun x ↦
-      pullCount' n (hist alg x n) (algFunction alg n (hist alg x n) (x.1 (n + 1)))) := by
-  have h_alg_meas : Measurable (fun x ↦ algFunction alg n (hist alg x n) (x.1 (n + 1))) :=
-    measurable_action_add_one' n h_hist
-  exact (measurable_uncurry_pullCount' (α := α) n).comp (h_hist.prodMk h_alg_meas)
-
-@[fun_prop]
-lemma measurable_hist [DecidableEq α] [Countable α] (alg : Algorithm α R) (n : ℕ) :
-    Measurable (fun ω ↦ hist alg ω n) := by
-  induction n with
-  | zero =>
-    simp_rw [hist_zero, measurable_pi_iff]
-    refine fun _ ↦ Measurable.prodMk (by fun_prop) ?_
-    change Measurable ((fun x : α × ((ℕ → I) × (ℕ → α → R)) ↦ x.2.2 0 x.1) ∘
-        (fun x : (ℕ → I) × (ℕ → α → R) ↦ (initAlgFunction alg (x.1 0), x)))
-    have : Measurable (fun x : α × ((ℕ → I) × (ℕ → α → R)) ↦ x.2.2 0 x.1) :=
-      measurable_from_prod_countable_right fun p ↦ by simp only; fun_prop
-    exact Measurable.comp (by fun_prop) (Measurable.prodMk (by fun_prop) (by fun_prop))
-  | succ n hn =>
-    refine measurable_pi_iff.mpr fun i ↦ ?_
-    by_cases hin : i ≤ n
-    · simp only [hist, hin, ↓reduceDIte]
-      rw [measurable_pi_iff] at hn
-      exact hn ⟨i.1, by simp [hin]⟩
-    · simp only [hist, hin, ↓reduceDIte]
-      refine Measurable.prodMk (by fun_prop) ?_
-      change Measurable ((fun (x : (ℕ → α → R) × ℕ × α) ↦ x.1 x.2.1 x.2.2) ∘
-        (fun x ↦ (x.2, pullCount' n (hist alg x n) (algFunction alg n (hist alg x n) (x.1 (n + 1))),
-          (algFunction alg n (hist alg x n) (x.1 (n + 1))))))
-      have h1 : Measurable (fun (x : (ℕ → α → R) × ℕ × α) ↦ x.1 x.2.1 x.2.2) :=
-        measurable_from_prod_countable_left fun p : ℕ × α ↦ (by simp only; fun_prop)
-      refine Measurable.comp (by fun_prop) (Measurable.prodMk (by fun_prop) ?_)
-      refine Measurable.prodMk ?_ (by fun_prop)
-      exact measurable_pullCount'_action_add_one n hn
-
 /-- Action taken at time `n` in the array model. -/
 noncomputable
 def action [DecidableEq α] (alg : Algorithm α R) (n : ℕ) (ω : probSpace α R) : α :=
@@ -330,10 +289,6 @@ lemma action_add_one_eq [DecidableEq α] (alg : Algorithm α R) (n : ℕ) :
   rw [action, hist_add_one]
   simp only [add_le_iff_nonpos_right, nonpos_iff_eq_zero, one_ne_zero, ↓reduceDIte]
 
-@[fun_prop]
-lemma measurable_action [DecidableEq α] [Countable α] (alg : Algorithm α R) (n : ℕ) :
-    Measurable (action alg n) := by unfold action; fun_prop
-
 /-- Reward received at time `n` in the array model. -/
 noncomputable
 def reward [DecidableEq α] (alg : Algorithm α R) (n : ℕ) (ω : probSpace α R) : R :=
@@ -363,6 +318,53 @@ lemma reward_eq [DecidableEq α] (alg : Algorithm α R) (n : ℕ) :
     rw [hist_eq]
     rfl
 
+section Measurability
+
+lemma measurable_action_add_one' [DecidableEq α] {alg : Algorithm α R}
+    (n : ℕ) (h : Measurable (hist alg · n)) :
+    Measurable (fun x ↦ algFunction alg n (hist alg x n) (x.1 (n + 1))) := by fun_prop
+
+lemma measurable_pullCount'_action_add_one [DecidableEq α] {alg : Algorithm α R}
+    (n : ℕ) (h_hist : Measurable (hist alg · n)) :
+    Measurable (fun x ↦
+      pullCount' n (hist alg x n) (algFunction alg n (hist alg x n) (x.1 (n + 1)))) := by
+  have h_alg_meas : Measurable (fun x ↦ algFunction alg n (hist alg x n) (x.1 (n + 1))) :=
+    measurable_action_add_one' n h_hist
+  exact (measurable_uncurry_pullCount' (α := α) n).comp (h_hist.prodMk h_alg_meas)
+
+@[fun_prop]
+lemma measurable_hist [DecidableEq α] [Countable α] (alg : Algorithm α R) (n : ℕ) :
+    Measurable (fun ω ↦ hist alg ω n) := by
+  induction n with
+  | zero =>
+    simp_rw [hist_zero, measurable_pi_iff]
+    refine fun _ ↦ Measurable.prodMk (by fun_prop) ?_
+    change Measurable ((fun x : α × ((ℕ → I) × (ℕ → α → R)) ↦ x.2.2 0 x.1) ∘
+        (fun x : (ℕ → I) × (ℕ → α → R) ↦ (initAlgFunction alg (x.1 0), x)))
+    have : Measurable (fun x : α × ((ℕ → I) × (ℕ → α → R)) ↦ x.2.2 0 x.1) :=
+      measurable_from_prod_countable_right fun p ↦ by simp only; fun_prop
+    exact Measurable.comp (by fun_prop) (Measurable.prodMk (by fun_prop) (by fun_prop))
+  | succ n hn =>
+    refine measurable_pi_iff.mpr fun i ↦ ?_
+    by_cases hin : i ≤ n
+    · simp only [hist, hin, ↓reduceDIte]
+      rw [measurable_pi_iff] at hn
+      exact hn ⟨i.1, by simp [hin]⟩
+    · simp only [hist, hin, ↓reduceDIte]
+      refine Measurable.prodMk (by fun_prop) ?_
+      change Measurable ((fun (x : (ℕ → α → R) × ℕ × α) ↦ x.1 x.2.1 x.2.2) ∘
+        (fun x ↦ (x.2, pullCount' n (hist alg x n) (algFunction alg n (hist alg x n) (x.1 (n + 1))),
+          (algFunction alg n (hist alg x n) (x.1 (n + 1))))))
+      have h1 : Measurable (fun (x : (ℕ → α → R) × ℕ × α) ↦ x.1 x.2.1 x.2.2) :=
+        measurable_from_prod_countable_left fun p : ℕ × α ↦ (by simp only; fun_prop)
+      refine Measurable.comp (by fun_prop) (Measurable.prodMk (by fun_prop) ?_)
+      refine Measurable.prodMk ?_ (by fun_prop)
+      exact measurable_pullCount'_action_add_one n hn
+
+@[fun_prop]
+lemma measurable_action [DecidableEq α] [Countable α] (alg : Algorithm α R) (n : ℕ) :
+    Measurable (action alg n) := by unfold action; fun_prop
+
 @[fun_prop]
 lemma measurable_reward [DecidableEq α] [Countable α] (alg : Algorithm α R) (n : ℕ) :
     Measurable (reward alg n) := by unfold reward; fun_prop
@@ -374,6 +376,16 @@ lemma hist_add_one_eq_IicSuccProd [DecidableEq α] (alg : Algorithm α R) (ω :
         (hist alg ω n, (action alg (n + 1) ω, reward alg (n + 1) ω)) := by
   rw [hist_add_one_eq_IicSuccProd', reward_add_one, action_add_one_eq]
 
+@[fun_prop]
+lemma measurable_pullCount_action_add_one [DecidableEq α] [Countable α] (alg : Algorithm α R)
+    (n : ℕ) :
+    Measurable (fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω) := by
+  change Measurable ((fun p : (probSpace α R) × α ↦ pullCount (action alg) p.2 (n + 1) p.1) ∘
+    (fun ω : probSpace α R ↦ (ω, action alg (n + 1) ω)))
+  exact (measurable_uncurry_pullCount (by fun_prop) _).comp (by fun_prop)
+
+end Measurability
+
 end HistoryActionReward
 
 variable [DecidableEq α]
@@ -460,35 +472,133 @@ lemma stepsUntil_indicator_congr (alg : Algorithm α R) (a : α) (m n : ℕ) {ω
 
 end Congruence
 
-section Laws
+section MeasurabilityAdvanced
 
-variable [Countable α]
+lemma measurable_hist_todo [Countable α] (alg : Algorithm α R) (n : ℕ) :
+    Measurable[MeasurableSpace.comap (fun ω ↦ (fun (i : Iic n) ↦ ω.1 i, ω.2)) inferInstance]
+      (hist alg · n) := by
+  have h_eq : (hist alg · n) =
+      ((hist alg · n) ∘ (fun p ↦ (fun i : ℕ ↦ p.1 ⟨min i n, by grind⟩, p.2))) ∘
+        (fun ω ↦ (fun (i : Iic n) ↦ ω.1 i, ω.2)) := by
+    ext ω : 1
+    exact hist_congr alg n (by grind) (by simp)
+  rw [h_eq]
+  refine measurable_comp_comap _ (Measurable.comp (by fun_prop) ?_)
+  refine Measurable.prodMk ?_ (by fun_prop)
+  rw [measurable_pi_iff]
+  intro i
+  change Measurable ((fun p ↦ p ⟨min i n, by simp⟩) ∘ (fun x : (Iic n → I) × (ℕ → α → R) ↦ x.1))
+  exact Measurable.comp (by fun_prop) measurable_fst
 
-lemma hasLaw_action_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] :
-    HasLaw (action alg 0) alg.p0 (arrayMeasure ν) where
-  map_eq := by
-    calc (arrayMeasure ν).map (fun ω ↦ initAlgFunction alg (ω.1 0))
-    _ = ((arrayMeasure ν).fst.map (Function.eval 0)).map (initAlgFunction alg) := by
-      rw [Measure.fst, Measure.map_map (by fun_prop) (by fun_prop),
-        Measure.map_map (by fun_prop) (by fun_prop)]
-      rfl
-    _ = (volume : Measure I).map (initAlgFunction alg) := by
-      simp only [arrayMeasure, Measure.fst_prod]
-      rw [(measurePreserving_eval_infinitePi (fun _ ↦ volume) 0).map_eq]
-    _ = alg.p0 := initAlgFunction_map alg
+variable [Nonempty R]
 
-omit [Nonempty α] [StandardBorelSpace α] [DecidableEq α] [Countable α] in
-lemma indepFun_fst_snd (ν : Kernel α R) [IsMarkovKernel ν] :
-    IndepFun Prod.fst Prod.snd (arrayMeasure ν) :=
-  indepFun_prod measurable_id measurable_id
+-- very bad name
+/-- All random variables in the space, except for the unseen rewards for action `a` after
+time `n`. -/
+noncomputable
+def truePast (alg : Algorithm α R) (a : α) (n : ℕ) (ω : probSpace α R) :
+    probSpace α R :=
+  (ω.1, fun i b ↦ if b = a then if pullCount (action alg) a (n + 1) ω ≠ 0 then
+      ω.2 (min i ((pullCount (action alg) a (n + 1) ω) - 1)) a else Nonempty.some inferInstance
+    else ω.2 i b)
 
-omit [Nonempty α] [StandardBorelSpace α] [DecidableEq α] [Countable α] in
-lemma indepFun_fst_zero_snd_zero_action (ν : Kernel α R) [IsMarkovKernel ν] (a : α) :
-    IndepFun (fun ω ↦ ω.1 0) (fun ω ↦ ω.2 0 a) (arrayMeasure ν) :=
-  indepFun_prod (X := fun ω : ℕ → I ↦ ω 0) (Y := fun ω : ℕ → α → R ↦ ω 0 a)
-    (by fun_prop) (by fun_prop)
+lemma truePast_eq_of_pullCount_eq (alg : Algorithm α R)
+    (a : α) (n m : ℕ) (ω : probSpace α R)
+    (h_pc : pullCount (action alg) a (n + 1) ω = m) :
+    truePast alg a n ω = (ω.1, fun i b ↦ if b = a then if m ≠ 0 then
+      ω.2 (min i (m - 1)) a else Nonempty.some inferInstance else ω.2 i b) := by
+  simp [truePast, h_pc]
+
+lemma truePast_eq_of_pullCount_eq_of_ne_zero (alg : Algorithm α R)
+    (a : α) (n m : ℕ) (ω : probSpace α R)
+    (h_pc : pullCount (action alg) a (n + 1) ω = m) (hm : m ≠ 0) :
+    truePast alg a n ω = (ω.1, fun i b ↦ if b = a then
+      ω.2 (min i (m - 1)) a else ω.2 i b) := by
+  simp [truePast, h_pc, hm]
+
+lemma measurable_hist_truePast [Countable α] (alg : Algorithm α R)
+    (a : α) (n : ℕ) :
+    Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance] (hist alg · n) := by
+  have h_eq : (hist alg · n) = (hist alg · n) ∘ (truePast alg a n) := by
+    ext ω : 1
+    refine hist_congr alg n (fun _ _ ↦ rfl) fun i b hi ↦ ?_
+    by_cases hb : b = a
+    · subst hb
+      simp only [truePast, ↓reduceIte]
+      rw [min_eq_left, if_pos (by grind)]
+      grind
+    · simp [truePast, hb]
+  rw [h_eq]
+  refine Measurable.comp ?_ (Measurable.of_comap_le le_rfl)
+  fun_prop
+
+lemma measurable_action_add_one_truePast [Countable α] (alg : Algorithm α R)
+    (a : α) (n : ℕ) :
+    Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance]
+      (action alg (n + 1)) := by
+  rw [action_add_one_eq]
+  change Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance]
+    ((fun p ↦ algFunction alg n p.1 p.2) ∘ (fun ω ↦ (hist alg ω n, ω.1 (n + 1))))
+  refine (measurable_algFunction alg n).comp (Measurable.prodMk ?_ ?_)
+  · exact measurable_hist_truePast alg a n
+  · have : (fun ω ↦ ω.1 (n + 1)) =
+      (fun (p : probSpace α R) ↦ p.1 (n + 1)) ∘ (truePast alg a n) := rfl
+    rw [this]
+    exact Measurable.comp (by fun_prop) (Measurable.of_comap_le le_rfl)
+
+lemma measurable_pullCount_add_one_truePast [Countable α] (alg : Algorithm α R) (a : α) (n : ℕ) :
+    Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance]
+      (pullCount (action alg) a (n + 1)) := by
+  change Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance]
+    (fun ω ↦ pullCount (action alg) a (n + 1) ω)
+  simp_rw [pullCount_eq_sum]
+  refine measurable_sum _ fun i hi ↦ Measurable.ite ?_ (by fun_prop) (by fun_prop)
+  refine (measurableSet_singleton _).preimage ?_
+  have h_meas := measurable_hist_truePast alg a n
+  simp_rw [hist_eq _ _ n, @measurable_pi_iff] at h_meas
+  exact (h_meas ⟨i, by grind⟩).fst
+
+lemma measurable_stepsUntil [Countable α] (alg : Algorithm α R) (a : α) (m n : ℕ) :
+    Measurable[MeasurableSpace.comap
+        (fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
+          else Nonempty.some inferInstance else ω.2 k b)) inferInstance]
+      (({ω | action alg (n + 1) ω = a ∧
+        pullCount (action alg) a (n + 1) ω = m}).indicator (fun _ ↦ 1)) := by
+  let f := ({ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m}).indicator
+    (fun _ ↦ 1)
+  have h_eq : f = f ∘
+      fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
+        else Nonempty.some inferInstance else ω.2 k b) := by
+    ext ω
+    exact stepsUntil_indicator_congr alg a m n (by grind) (by grind) (by grind)
+  change Measurable[MeasurableSpace.comap
+    (fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
+      else Nonempty.some inferInstance else ω.2 k b)) inferInstance] f
+  rw [h_eq]
+  refine Measurable.comp ?_ (Measurable.of_comap_le le_rfl)
+  refine Measurable.indicator (by fun_prop) ?_
+  exact MeasurableSet.inter ((measurableSet_singleton _).preimage (by fun_prop))
+    ((measurableSet_singleton _).preimage (by fun_prop))
+
+omit [Nonempty R] in
+lemma measurable_pullCount_action_add_one_hist (alg : Algorithm α R) (n : ℕ) :
+    Measurable[MeasurableSpace.comap (fun ω ↦ (action alg (n + 1) ω, hist alg ω n)) inferInstance]
+      (fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω) := by
+  simp_rw [pullCount_eq_sum]
+  refine measurable_sum _ fun i hi ↦ Measurable.ite ?_ (by fun_prop) (by fun_prop)
+  refine measurableSet_eq_fun ?_ (measurable_comp_comap _ measurable_fst)
+  simp_rw [hist_eq _ _ n]
+  unfold action
+  refine Measurable.fst (mγ := inferInstance) ?_
+  have : (hist alg · i ⟨i, by grind⟩) =
+      (fun ω : α × (Iic n → α × R) ↦ ω.2 ⟨i, by grind⟩) ∘
+        (fun ω ↦ (action alg (n + 1) ω, fun i : Iic n ↦ hist alg ω i ⟨i, by grind⟩)) := rfl
+  rw [this]
+  exact measurable_comp_comap _ (Measurable.prodMk (by fun_prop) (by fun_prop))
+
+end MeasurabilityAdvanced
 
-omit [Nonempty α] [StandardBorelSpace α] [DecidableEq α] [Countable α] in
+omit [Nonempty α] [StandardBorelSpace α] [DecidableEq α] in
 lemma map_snd_apply_arrayMeasure {ν : Kernel α R} [IsMarkovKernel ν] (n : ℕ) (a : α) :
     (arrayMeasure ν).map (fun ω ↦ ω.2 n a) = ν a := by
   calc (arrayMeasure ν).map (fun ω ↦ ω.2 n a)
@@ -501,37 +611,21 @@ lemma map_snd_apply_arrayMeasure {ν : Kernel α R} [IsMarkovKernel ν] (n : ℕ
     rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), Measure.infinitePi_map_eval,
       Measure.infinitePi_map_eval]
 
-variable [StandardBorelSpace R] [Nonempty R]
+section Independence
 
-lemma hasCondDistrib_reward_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] :
-    HasCondDistrib (reward alg 0) (action alg 0) ν (arrayMeasure ν) where
-  condDistrib_eq := by
-    refine (condDistrib_ae_eq_cond (by fun_prop) (by fun_prop)).trans ?_
-    rw [Filter.EventuallyEq, ae_iff_of_countable]
-    intro a ha
-    simp only [reward_zero]
-    calc ((arrayMeasure ν)[|action alg 0 ⁻¹' {a}]).map (fun ω ↦ ω.2 0 (action alg 0 ω))
-    _ = ((arrayMeasure ν)[|action alg 0 ⁻¹' {a}]).map (fun ω ↦ ω.2 0 a) := by
-      refine Measure.map_congr
-        (ae_cond_of_forall_mem ((measurableSet_singleton _).preimage (by fun_prop)) ?_)
-      intro x hx
-      simp only [Set.mem_preimage, Set.mem_singleton_iff] at hx
-      simp [hx]
-    _ = ν a := by
-      rw [cond_of_indepFun]
-      · exact map_snd_apply_arrayMeasure 0 a
-      · have : (fun ω ↦ ω.1 0) ⟂ᵢ[arrayMeasure ν] fun ω ↦ ω.2 0 a :=
-          indepFun_fst_zero_snd_zero_action ν a
-        rw [action_zero]
-        exact this.comp (φ := initAlgFunction alg) (by fun_prop) measurable_id
-      · fun_prop
-      · fun_prop
-      · simp
-      · rwa [Measure.map_apply (by fun_prop) (by simp)] at ha
+omit [Nonempty α] [StandardBorelSpace α] [DecidableEq α] in
+lemma indepFun_fst_snd (ν : Kernel α R) [IsMarkovKernel ν] :
+    IndepFun Prod.fst Prod.snd (arrayMeasure ν) :=
+  indepFun_prod measurable_id measurable_id
+
+omit [Nonempty α] [StandardBorelSpace α] [DecidableEq α] in
+lemma indepFun_fst_zero_snd_zero_action (ν : Kernel α R) [IsMarkovKernel ν] (a : α) :
+    IndepFun (fun ω ↦ ω.1 0) (fun ω ↦ ω.2 0 a) (arrayMeasure ν) :=
+  indepFun_prod (X := fun ω : ℕ → I ↦ ω 0) (Y := fun ω : ℕ → α → R ↦ ω 0 a)
+    (by fun_prop) (by fun_prop)
 
 -- proved by Claude, then slightly golfed
-omit [DecidableEq α] [Nonempty α] [StandardBorelSpace α] [Countable α] [StandardBorelSpace R]
-  [Nonempty R] in
+omit [DecidableEq α] [Nonempty α] [StandardBorelSpace α] in
 lemma indepFun_fst_add_one_aux (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
     (fun ω ↦ ω.1 (n + 1)) ⟂ᵢ[arrayMeasure ν] (fun ω ↦ (fun (i : Iic n) ↦ ω.1 i, ω.2)) := by
   let μ₁ : Measure (ℕ → I) := Measure.infinitePi fun _ ↦ volume
@@ -578,154 +672,15 @@ lemma indepFun_fst_add_one_aux (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ)
   simp_rw [h_eq]
   exact lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun hf_meas (by fun_prop) hindep_fg
 
-omit [StandardBorelSpace R] [Nonempty R] in
-lemma measurable_hist_todo (alg : Algorithm α R) (n : ℕ) :
-    Measurable[MeasurableSpace.comap (fun ω ↦ (fun (i : Iic n) ↦ ω.1 i, ω.2)) inferInstance]
-      (hist alg · n) := by
-  have h_eq : (hist alg · n) =
-      ((hist alg · n) ∘ (fun p ↦ (fun i : ℕ ↦ p.1 ⟨min i n, by grind⟩, p.2))) ∘
-        (fun ω ↦ (fun (i : Iic n) ↦ ω.1 i, ω.2)) := by
-    ext ω : 1
-    exact hist_congr alg n (by grind) (by simp)
-  rw [h_eq]
-  refine measurable_comp_comap _ (Measurable.comp (by fun_prop) ?_)
-  refine Measurable.prodMk ?_ (by fun_prop)
-  rw [measurable_pi_iff]
-  intro i
-  change Measurable ((fun p ↦ p ⟨min i n, by simp⟩) ∘ (fun x : (Iic n → I) × (ℕ → α → R) ↦ x.1))
-  exact Measurable.comp (by fun_prop) measurable_fst
+variable [StandardBorelSpace R] [Nonempty R]
 
-lemma indepFun_fst_add_one_hist (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
+lemma indepFun_fst_add_one_hist [Countable α] (alg : Algorithm α R)
+    (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
     IndepFun (fun ω ↦ ω.1 (n + 1)) (hist alg · n) (arrayMeasure ν) :=
   (indepFun_fst_add_one_aux ν n).of_measurable_right (measurable_hist_todo alg n)
 
-lemma hasCondDistrib_action' (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
-    HasCondDistrib (action alg (n + 1)) (hist alg · n) (alg.policy n) (arrayMeasure ν) := by
-  rw [action_add_one_eq]
-  have h_fun ω := algFunction_map alg n (hist alg ω n)
-  refine ⟨by fun_prop, by fun_prop, ?_⟩
-  refine condDistrib_ae_eq_of_measure_eq_compProd _ (by fun_prop) ?_
-  have h_indep : (arrayMeasure ν).map (fun ω ↦ (ω.1 (n + 1), hist alg ω n)) =
-      (ℙ).prod ((arrayMeasure ν).map (hist alg · n)) := by
-    have h_indep' := indepFun_fst_add_one_hist alg ν n
-    rw [indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop)] at h_indep'
-    rw [h_indep']
-    congr
-    simp only [arrayMeasure]
-    calc ((Measure.infinitePi fun x ↦ ℙ).prod (Bandit.streamMeasure ν)).map (fun ω ↦ ω.1 (n + 1))
-    _ = (Measure.infinitePi fun x ↦ ℙ).map (Function.eval (n + 1)) := by
-      nth_rw 2 [← Measure.fst_prod (μ := Measure.infinitePi fun x ↦ ℙ)
-        (ν := Bandit.streamMeasure ν)]
-      rw [Measure.fst, Measure.map_map (by fun_prop) (by fun_prop)]
-      rfl
-    _ = ℙ := by rw [Measure.infinitePi_map_eval]
-  have : (fun x ↦ (hist alg x n, algFunction alg n (hist alg x n) (x.1 (n + 1)))) =
-      (fun p ↦ (p.2, algFunction alg n (p.2) (p.1))) ∘ (fun x ↦ (x.1 (n + 1), hist alg x n)) := rfl
-  rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), h_indep]
-  have : (ℙ : Measure I).prod ((arrayMeasure ν).map (hist alg · n)) =
-      ((Kernel.const _ ℙ) ×ₖ Kernel.id) ∘ₘ ((arrayMeasure ν).map (hist alg · n)) := by
-    have h := Measure.compProd_const (μ := (arrayMeasure ν).map (hist alg · n))
-      (ν := (ℙ : Measure I))
-    rw [Measure.compProd_eq_comp_prod] at h
-    rw [← Measure.prod_swap, ← h, ← Measure.deterministic_comp_eq_map (by fun_prop),
-      Measure.comp_assoc, ← Kernel.swap, Kernel.swap_prod]
-  rw [this, ← Measure.deterministic_comp_eq_map (by fun_prop),
-    ← Measure.deterministic_comp_eq_map (by fun_prop), Measure.compProd_eq_comp_prod,
-    Measure.comp_assoc, Measure.comp_assoc, Measure.comp_assoc]
-  congr 2
-  ext ω : 1
-  simp only [Kernel.deterministic_comp_eq_map, Kernel.comp_deterministic_eq_comap, Kernel.coe_comap,
-    Function.comp_apply]
-  rw [Kernel.map_apply _ (by fun_prop), Kernel.prod_apply, Kernel.const_apply, Kernel.id_apply,
-    Kernel.prod_apply, Kernel.id_apply, ← h_fun]
-  calc (((ℙ).prod (Measure.dirac (hist alg ω n)))).map (fun p ↦ (p.2, algFunction alg n p.2 p.1))
-  _ = (((ℙ).prod (Measure.dirac (hist alg ω n))).map Prod.swap).map
-      (fun p ↦ (p.1, algFunction alg n p.1 p.2)) := by
-    rw [Measure.map_map (by fun_prop) (by fun_prop)]
-    rfl
-  _ = ((Measure.dirac (hist alg ω n)).prod ℙ).map (fun p ↦ (p.1, algFunction alg n p.1 p.2)) := by
-    rw [Measure.prod_swap]
-  _ = (Measure.dirac (hist alg ω n)).prod ((ℙ).map (algFunction alg n (hist alg ω n))) := by
-    ext s hs
-    rw [Measure.map_apply (by fun_prop) hs, Measure.prod_apply, lintegral_dirac, Measure.prod_apply,
-      lintegral_dirac, Measure.map_apply (by fun_prop)]
-    · congr
-    · exact hs.preimage (by fun_prop)
-    · exact hs
-    · exact hs.preimage (by fun_prop)
-
--- very bad name
-/-- All random variables in the space, except for the unseen rewards for action `a` after
-time `n`. -/
-noncomputable
-def truePast (alg : Algorithm α R) (a : α) (n : ℕ) (ω : probSpace α R) :
-    probSpace α R :=
-  (ω.1, fun i b ↦ if b = a then if pullCount (action alg) a (n + 1) ω ≠ 0 then
-      ω.2 (min i ((pullCount (action alg) a (n + 1) ω) - 1)) a else Nonempty.some inferInstance
-    else ω.2 i b)
-
-omit [Countable α] [StandardBorelSpace R] in
-lemma truePast_eq_of_pullCount_eq (alg : Algorithm α R)
-    (a : α) (n m : ℕ) (ω : probSpace α R)
-    (h_pc : pullCount (action alg) a (n + 1) ω = m) :
-    truePast alg a n ω = (ω.1, fun i b ↦ if b = a then if m ≠ 0 then
-      ω.2 (min i (m - 1)) a else Nonempty.some inferInstance else ω.2 i b) := by
-  simp [truePast, h_pc]
-
-omit [Countable α] [StandardBorelSpace R] in
-lemma truePast_eq_of_pullCount_eq_of_ne_zero (alg : Algorithm α R)
-    (a : α) (n m : ℕ) (ω : probSpace α R)
-    (h_pc : pullCount (action alg) a (n + 1) ω = m) (hm : m ≠ 0) :
-    truePast alg a n ω = (ω.1, fun i b ↦ if b = a then
-      ω.2 (min i (m - 1)) a else ω.2 i b) := by
-  simp [truePast, h_pc, hm]
-
-omit [StandardBorelSpace R] in
-lemma measurable_hist_truePast (alg : Algorithm α R)
-    (a : α) (n : ℕ) :
-    Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance] (hist alg · n) := by
-  have h_eq : (hist alg · n) = (hist alg · n) ∘ (truePast alg a n) := by
-    ext ω : 1
-    refine hist_congr alg n (fun _ _ ↦ rfl) fun i b hi ↦ ?_
-    by_cases hb : b = a
-    · subst hb
-      simp only [truePast, ↓reduceIte]
-      rw [min_eq_left, if_pos (by grind)]
-      grind
-    · simp [truePast, hb]
-  rw [h_eq]
-  refine Measurable.comp ?_ (Measurable.of_comap_le le_rfl)
-  fun_prop
-
-omit [StandardBorelSpace R] in
-lemma measurable_action_add_one_truePast (alg : Algorithm α R)
-    (a : α) (n : ℕ) :
-    Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance]
-      (action alg (n + 1)) := by
-  rw [action_add_one_eq]
-  change Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance]
-    ((fun p ↦ algFunction alg n p.1 p.2) ∘ (fun ω ↦ (hist alg ω n, ω.1 (n + 1))))
-  refine (measurable_algFunction alg n).comp (Measurable.prodMk ?_ ?_)
-  · exact measurable_hist_truePast alg a n
-  · have : (fun ω ↦ ω.1 (n + 1)) =
-      (fun (p : probSpace α R) ↦ p.1 (n + 1)) ∘ (truePast alg a n) := rfl
-    rw [this]
-    exact Measurable.comp (by fun_prop) (Measurable.of_comap_le le_rfl)
-
-omit [StandardBorelSpace R] in
-lemma measurable_pullCount_add_one_truePast (alg : Algorithm α R) (a : α) (n : ℕ) :
-    Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance]
-      (pullCount (action alg) a (n + 1)) := by
-  change Measurable[MeasurableSpace.comap (truePast alg a n) inferInstance]
-    (fun ω ↦ pullCount (action alg) a (n + 1) ω)
-  simp_rw [pullCount_eq_sum]
-  refine measurable_sum _ fun i hi ↦ Measurable.ite ?_ (by fun_prop) (by fun_prop)
-  refine (measurableSet_singleton _).preimage ?_
-  have h_meas := measurable_hist_truePast alg a n
-  simp_rw [hist_eq _ _ n, @measurable_pi_iff] at h_meas
-  exact (h_meas ⟨i, by grind⟩).fst
-
-omit [Nonempty α] [StandardBorelSpace α] [Countable α] [StandardBorelSpace R] in
+-- proved by Claude
+omit [Nonempty α] [StandardBorelSpace α] [StandardBorelSpace R] in
 lemma indepFun_snd_apply_aux (ν : Kernel α R) [IsMarkovKernel ν] (a : α) (m : ℕ) :
     (fun ω ↦ ω.2 m a) ⟂ᵢ[arrayMeasure ν]
       (fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
@@ -934,45 +889,174 @@ lemma indepFun_snd_apply_aux (ν : Kernel α R) [IsMarkovKernel ν] (a : α) (m
   rw [lintegral_const_mul _ (measurable_measure_prodMk_left_finite ht),
     lintegral_const, measure_univ, mul_one]
 
-
-omit [StandardBorelSpace R] in
-lemma measurable_stepsUntil (alg : Algorithm α R) (a : α) (m n : ℕ) :
-    Measurable[MeasurableSpace.comap
-        (fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
-          else Nonempty.some inferInstance else ω.2 k b)) inferInstance]
-      (({ω | action alg (n + 1) ω = a ∧
-        pullCount (action alg) a (n + 1) ω = m}).indicator (fun _ ↦ 1)) := by
-  let f := ({ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m}).indicator
-    (fun _ ↦ 1)
-  have h_eq : f = f ∘
-      fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
-        else Nonempty.some inferInstance else ω.2 k b) := by
-    ext ω
-    exact stepsUntil_indicator_congr alg a m n (by grind) (by grind) (by grind)
-  change Measurable[MeasurableSpace.comap
-    (fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
-      else Nonempty.some inferInstance else ω.2 k b)) inferInstance] f
-  rw [h_eq]
-  refine Measurable.comp ?_ (Measurable.of_comap_le le_rfl)
-  refine Measurable.indicator (by fun_prop) ?_
-  exact MeasurableSet.inter ((measurableSet_singleton _).preimage (by fun_prop))
-    ((measurableSet_singleton _).preimage (by fun_prop))
-
 omit [StandardBorelSpace R] in
-lemma indepFun_snd_apply_pullCount_action (alg : Algorithm α R)
+lemma indepFun_snd_apply_pullCount_action [Countable α] (alg : Algorithm α R)
     (ν : Kernel α R) [IsMarkovKernel ν] (a : α) (m n : ℕ) :
     (fun ω ↦ ω.2 m a) ⟂ᵢ[arrayMeasure ν]
       ({ω | action alg (n + 1) ω = a ∧
         pullCount (action alg) a (n + 1) ω = m}).indicator (fun _ ↦ 1) :=
   (indepFun_snd_apply_aux ν a m).of_measurable_right (measurable_stepsUntil alg a m n)
 
-omit [StandardBorelSpace R] [Nonempty R] in
-@[fun_prop]
-lemma measurable_pullCount_action_add_one (alg : Algorithm α R) (n : ℕ) :
-    Measurable (fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω) := by
-  change Measurable ((fun p : (probSpace α R) × α ↦ pullCount (action alg) p.2 (n + 1) p.1) ∘
-    (fun ω : probSpace α R ↦ (ω, action alg (n + 1) ω)))
-  exact (measurable_uncurry_pullCount (by fun_prop) _).comp (by fun_prop)
+lemma indepFun_todo {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
+    {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} [MeasurableSingletonClass δ] {μ : Measure α}
+    {X : α → β} {Y : α → γ} (hXY : X ⟂ᵢ[μ] Y) (hY : Measurable Y)
+    {Z : γ → δ} (hZ : Measurable Z) (z : δ) :
+    X ⟂ᵢ[μ[|(Z ∘ Y) ⁻¹' {z}]] Y := by
+  have h_preim : (Z ∘ Y) ⁻¹' {z} = Y ⁻¹' (Z ⁻¹' {z}) := by grind
+  simp_rw [h_preim]
+  exact indepFun_cond_of_indepFun hXY hY (hZ (measurableSet_singleton z))
+
+lemma indepFun_snd_hist_cond [Countable α] (alg : Algorithm α R)
+    (ν : Kernel α R) [IsMarkovKernel ν] (a : α) (n m : ℕ) :
+    (fun ω ↦ ω.2 m a) ⟂ᵢ[(arrayMeasure ν)[|(fun ω ↦ (action alg (n + 1) ω,
+      pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ⁻¹' {(a, m)}]]
+    (hist alg · n) := by
+  have h_meas := measurable_hist_truePast alg a n
+  refine IndepFun.of_measurable_right ?_ h_meas
+  have h_ae_eq : truePast alg a n =ᵐ[(arrayMeasure ν)[|(fun ω ↦ (action alg (n + 1) ω,
+        pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ⁻¹' {(a, m)}]]
+      (fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
+        else Nonempty.some inferInstance else ω.2 k b)) := by
+    refine ae_cond_of_forall_mem ?_ fun x hx ↦ ?_
+    · refine (measurableSet_singleton _).preimage ?_
+      have h_meas_pc : Measurable fun ω ↦
+          pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω := by
+        change Measurable ((fun p : (probSpace α R) × α ↦ pullCount (action alg) p.2 (n + 1) p.1) ∘
+          (fun ω : probSpace α R ↦ (ω, action alg (n + 1) ω)))
+        exact (measurable_uncurry_pullCount (by fun_prop) _).comp (by fun_prop)
+      fun_prop
+    simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq] at hx
+    simp only [truePast]
+    congr with i b
+    by_cases hb : b = a
+    · simp only [hb, ↓reduceIte]
+      simp only [hx.1, true_and] at hx
+      congr!
+    · simp [hb]
+  refine IndepFun.congr ?_ EventuallyEq.rfl h_ae_eq.symm
+  suffices (fun ω ↦ ω.2 m a) ⟂ᵢ[(arrayMeasure ν)[|(({ω | action alg (n + 1) ω = a ∧
+        pullCount (action alg) a (n + 1) ω = m}).indicator (fun _ ↦ 1)) ⁻¹' {1}]]
+      fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
+        else Nonempty.some inferInstance else ω.2 k b) by
+    convert this
+    ext ω
+    simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq, Set.indicator_apply,
+      Set.mem_setOf_eq, ite_eq_left_iff, not_and, zero_ne_one, imp_false,
+      Classical.not_imp, Decidable.not_not, and_congr_right_iff]
+    intro ha
+    simp [ha]
+  have h_meas := measurable_stepsUntil alg a m n
+  obtain ⟨f, hf, hf_eq⟩ := h_meas.exists_eq_measurable_comp
+  simp_rw [hf_eq]
+  refine indepFun_todo (Z := f) (z := 1) ?_ ?_ hf
+  · exact indepFun_snd_apply_aux ν a m
+  · refine Measurable.prodMk (by fun_prop) ?_
+    simp_rw [measurable_pi_iff]
+    intro i b
+    refine Measurable.ite (MeasurableSet.const _) ?_ (by fun_prop)
+    refine Measurable.ite (MeasurableSet.const _) (by fun_prop) (by fun_prop)
+
+end Independence
+
+section Laws
+
+variable [Countable α]
+
+lemma hasLaw_action_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] :
+    HasLaw (action alg 0) alg.p0 (arrayMeasure ν) where
+  map_eq := by
+    calc (arrayMeasure ν).map (fun ω ↦ initAlgFunction alg (ω.1 0))
+    _ = ((arrayMeasure ν).fst.map (Function.eval 0)).map (initAlgFunction alg) := by
+      rw [Measure.fst, Measure.map_map (by fun_prop) (by fun_prop),
+        Measure.map_map (by fun_prop) (by fun_prop)]
+      rfl
+    _ = (volume : Measure I).map (initAlgFunction alg) := by
+      simp only [arrayMeasure, Measure.fst_prod]
+      rw [(measurePreserving_eval_infinitePi (fun _ ↦ volume) 0).map_eq]
+    _ = alg.p0 := initAlgFunction_map alg
+
+variable [StandardBorelSpace R] [Nonempty R]
+
+lemma hasCondDistrib_reward_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] :
+    HasCondDistrib (reward alg 0) (action alg 0) ν (arrayMeasure ν) where
+  condDistrib_eq := by
+    refine (condDistrib_ae_eq_cond (by fun_prop) (by fun_prop)).trans ?_
+    rw [Filter.EventuallyEq, ae_iff_of_countable]
+    intro a ha
+    simp only [reward_zero]
+    calc ((arrayMeasure ν)[|action alg 0 ⁻¹' {a}]).map (fun ω ↦ ω.2 0 (action alg 0 ω))
+    _ = ((arrayMeasure ν)[|action alg 0 ⁻¹' {a}]).map (fun ω ↦ ω.2 0 a) := by
+      refine Measure.map_congr
+        (ae_cond_of_forall_mem ((measurableSet_singleton _).preimage (by fun_prop)) ?_)
+      intro x hx
+      simp only [Set.mem_preimage, Set.mem_singleton_iff] at hx
+      simp [hx]
+    _ = ν a := by
+      rw [cond_of_indepFun]
+      · exact map_snd_apply_arrayMeasure 0 a
+      · have : (fun ω ↦ ω.1 0) ⟂ᵢ[arrayMeasure ν] fun ω ↦ ω.2 0 a :=
+          indepFun_fst_zero_snd_zero_action ν a
+        rw [action_zero]
+        exact this.comp (φ := initAlgFunction alg) (by fun_prop) measurable_id
+      · fun_prop
+      · fun_prop
+      · simp
+      · rwa [Measure.map_apply (by fun_prop) (by simp)] at ha
+
+lemma hasCondDistrib_action' (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
+    HasCondDistrib (action alg (n + 1)) (hist alg · n) (alg.policy n) (arrayMeasure ν) := by
+  rw [action_add_one_eq]
+  have h_fun ω := algFunction_map alg n (hist alg ω n)
+  refine ⟨by fun_prop, by fun_prop, ?_⟩
+  refine condDistrib_ae_eq_of_measure_eq_compProd _ (by fun_prop) ?_
+  have h_indep : (arrayMeasure ν).map (fun ω ↦ (ω.1 (n + 1), hist alg ω n)) =
+      (ℙ).prod ((arrayMeasure ν).map (hist alg · n)) := by
+    have h_indep' := indepFun_fst_add_one_hist alg ν n
+    rw [indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop)] at h_indep'
+    rw [h_indep']
+    congr
+    simp only [arrayMeasure]
+    calc ((Measure.infinitePi fun x ↦ ℙ).prod (Bandit.streamMeasure ν)).map (fun ω ↦ ω.1 (n + 1))
+    _ = (Measure.infinitePi fun x ↦ ℙ).map (Function.eval (n + 1)) := by
+      nth_rw 2 [← Measure.fst_prod (μ := Measure.infinitePi fun x ↦ ℙ)
+        (ν := Bandit.streamMeasure ν)]
+      rw [Measure.fst, Measure.map_map (by fun_prop) (by fun_prop)]
+      rfl
+    _ = ℙ := by rw [Measure.infinitePi_map_eval]
+  have : (fun x ↦ (hist alg x n, algFunction alg n (hist alg x n) (x.1 (n + 1)))) =
+      (fun p ↦ (p.2, algFunction alg n (p.2) (p.1))) ∘ (fun x ↦ (x.1 (n + 1), hist alg x n)) := rfl
+  rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), h_indep]
+  have : (ℙ : Measure I).prod ((arrayMeasure ν).map (hist alg · n)) =
+      ((Kernel.const _ ℙ) ×ₖ Kernel.id) ∘ₘ ((arrayMeasure ν).map (hist alg · n)) := by
+    have h := Measure.compProd_const (μ := (arrayMeasure ν).map (hist alg · n))
+      (ν := (ℙ : Measure I))
+    rw [Measure.compProd_eq_comp_prod] at h
+    rw [← Measure.prod_swap, ← h, ← Measure.deterministic_comp_eq_map (by fun_prop),
+      Measure.comp_assoc, ← Kernel.swap, Kernel.swap_prod]
+  rw [this, ← Measure.deterministic_comp_eq_map (by fun_prop),
+    ← Measure.deterministic_comp_eq_map (by fun_prop), Measure.compProd_eq_comp_prod,
+    Measure.comp_assoc, Measure.comp_assoc, Measure.comp_assoc]
+  congr 2
+  ext ω : 1
+  simp only [Kernel.deterministic_comp_eq_map, Kernel.comp_deterministic_eq_comap, Kernel.coe_comap,
+    Function.comp_apply]
+  rw [Kernel.map_apply _ (by fun_prop), Kernel.prod_apply, Kernel.const_apply, Kernel.id_apply,
+    Kernel.prod_apply, Kernel.id_apply, ← h_fun]
+  calc (((ℙ).prod (Measure.dirac (hist alg ω n)))).map (fun p ↦ (p.2, algFunction alg n p.2 p.1))
+  _ = (((ℙ).prod (Measure.dirac (hist alg ω n))).map Prod.swap).map
+      (fun p ↦ (p.1, algFunction alg n p.1 p.2)) := by
+    rw [Measure.map_map (by fun_prop) (by fun_prop)]
+    rfl
+  _ = ((Measure.dirac (hist alg ω n)).prod ℙ).map (fun p ↦ (p.1, algFunction alg n p.1 p.2)) := by
+    rw [Measure.prod_swap]
+  _ = (Measure.dirac (hist alg ω n)).prod ((ℙ).map (algFunction alg n (hist alg ω n))) := by
+    ext s hs
+    rw [Measure.map_apply (by fun_prop) hs, Measure.prod_apply, lintegral_dirac, Measure.prod_apply,
+      lintegral_dirac, Measure.map_apply (by fun_prop)]
+    · congr
+    · exact hs.preimage (by fun_prop)
+    · exact hs
+    · exact hs.preimage (by fun_prop)
 
 /-- The conditional distribution of the reward at time `n + 1`, given the action at time `n + 1`
 and the number of times that action has been pulled before time `n + 1`, is equal to
@@ -1048,65 +1132,6 @@ lemma reward_ae_eq_cond (alg : Algorithm α R) (ν : Kernel α R) (a : α) (n m
   simp only [hω.2]
   simp [hω.1]
 
-lemma indepFun_todo {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
-    {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} [MeasurableSingletonClass δ] {μ : Measure α}
-    {X : α → β} {Y : α → γ} (hXY : X ⟂ᵢ[μ] Y) (hY : Measurable Y)
-    {Z : γ → δ} (hZ : Measurable Z) (z : δ) :
-    X ⟂ᵢ[μ[|(Z ∘ Y) ⁻¹' {z}]] Y := by
-  have h_preim : (Z ∘ Y) ⁻¹' {z} = Y ⁻¹' (Z ⁻¹' {z}) := by grind
-  simp_rw [h_preim]
-  exact indepFun_cond_of_indepFun hXY hY (hZ (measurableSet_singleton z))
-
-lemma indepFun_snd_hist_cond (alg : Algorithm α R)
-    (ν : Kernel α R) [IsMarkovKernel ν] (a : α) (n m : ℕ) :
-    (fun ω ↦ ω.2 m a) ⟂ᵢ[(arrayMeasure ν)[|(fun ω ↦ (action alg (n + 1) ω,
-      pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ⁻¹' {(a, m)}]]
-    (hist alg · n) := by
-  have h_meas := measurable_hist_truePast alg a n
-  refine IndepFun.of_measurable_right ?_ h_meas
-  have h_ae_eq : truePast alg a n =ᵐ[(arrayMeasure ν)[|(fun ω ↦ (action alg (n + 1) ω,
-        pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω)) ⁻¹' {(a, m)}]]
-      (fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
-        else Nonempty.some inferInstance else ω.2 k b)) := by
-    refine ae_cond_of_forall_mem ?_ fun x hx ↦ ?_
-    · refine (measurableSet_singleton _).preimage ?_
-      have h_meas_pc : Measurable fun ω ↦
-          pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω := by
-        change Measurable ((fun p : (probSpace α R) × α ↦ pullCount (action alg) p.2 (n + 1) p.1) ∘
-          (fun ω : probSpace α R ↦ (ω, action alg (n + 1) ω)))
-        exact (measurable_uncurry_pullCount (by fun_prop) _).comp (by fun_prop)
-      fun_prop
-    simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq] at hx
-    simp only [truePast]
-    congr with i b
-    by_cases hb : b = a
-    · simp only [hb, ↓reduceIte]
-      simp only [hx.1, true_and] at hx
-      congr!
-    · simp [hb]
-  refine IndepFun.congr ?_ EventuallyEq.rfl h_ae_eq.symm
-  suffices (fun ω ↦ ω.2 m a) ⟂ᵢ[(arrayMeasure ν)[|(({ω | action alg (n + 1) ω = a ∧
-        pullCount (action alg) a (n + 1) ω = m}).indicator (fun _ ↦ 1)) ⁻¹' {1}]]
-      fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
-        else Nonempty.some inferInstance else ω.2 k b) by
-    convert this
-    ext ω
-    simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq, Set.indicator_apply,
-      Set.mem_setOf_eq, ite_eq_left_iff, not_and, zero_ne_one, imp_false,
-      Classical.not_imp, Decidable.not_not, and_congr_right_iff]
-    intro ha
-    simp [ha]
-  have h_meas := measurable_stepsUntil alg a m n
-  obtain ⟨f, hf, hf_eq⟩ := h_meas.exists_eq_measurable_comp
-  simp_rw [hf_eq]
-  refine indepFun_todo (Z := f) (z := 1) ?_ ?_ hf
-  · exact indepFun_snd_apply_aux ν a m
-  · refine Measurable.prodMk (by fun_prop) ?_
-    simp_rw [measurable_pi_iff]
-    intro i b
-    refine Measurable.ite (MeasurableSet.const _) ?_ (by fun_prop)
-    refine Measurable.ite (MeasurableSet.const _) (by fun_prop) (by fun_prop)
-
 /-- The conditional distribution of the reward at time `n + 1`, given the history up to time `n`,
 the action at time `n + 1`, and the number of times that action has been pulled before time `n + 1`,
 is equal to the kernel `ν`. -/
@@ -1166,22 +1191,6 @@ lemma condIndepFun_reward_hist (alg : Algorithm α R) (ν : Kernel α R) [IsMark
     h_cond.condDistrib_eq
   exact Measurable.prodMk (by fun_prop) (measurable_pullCount_action_add_one alg n)
 
-omit [Countable α] [StandardBorelSpace R] [Nonempty R] in
-lemma measurable_pullCount_action_add_one_hist (alg : Algorithm α R) (n : ℕ) :
-    Measurable[MeasurableSpace.comap (fun ω ↦ (action alg (n + 1) ω, hist alg ω n)) inferInstance]
-      (fun ω ↦ pullCount (action alg) (action alg (n + 1) ω) (n + 1) ω) := by
-  simp_rw [pullCount_eq_sum]
-  refine measurable_sum _ fun i hi ↦ Measurable.ite ?_ (by fun_prop) (by fun_prop)
-  refine measurableSet_eq_fun ?_ (measurable_comp_comap _ measurable_fst)
-  simp_rw [hist_eq _ _ n]
-  unfold action
-  refine Measurable.fst (mγ := inferInstance) ?_
-  have : (hist alg · i ⟨i, by grind⟩) =
-      (fun ω : α × (Iic n → α × R) ↦ ω.2 ⟨i, by grind⟩) ∘
-        (fun ω ↦ (action alg (n + 1) ω, fun i : Iic n ↦ hist alg ω i ⟨i, by grind⟩)) := rfl
-  rw [this]
-  exact measurable_comp_comap _ (Measurable.prodMk (by fun_prop) (by fun_prop))
-
 /-- The conditional distribution of the reward at time `n + 1`, given the history up to time `n`
 and the action at time `n + 1`, is equal to the kernel `ν`. -/
 lemma hasCondDistrib_reward' (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
diff --git a/blueprint/lean_decls b/blueprint/lean_decls
index 54612c19..b9510cbe 100644
--- a/blueprint/lean_decls
+++ b/blueprint/lean_decls
@@ -57,6 +57,33 @@ Bandits.ArrayModel.probSpace
 Bandits.ArrayModel.arrayMeasure
 Bandits.ArrayModel.algFunction
 Bandits.ArrayModel.initAlgFunction
+Bandits.ArrayModel.hist
+Bandits.ArrayModel.action
+Bandits.ArrayModel.reward
+Bandits.ArrayModel.measurable_hist
+Bandits.ArrayModel.measurable_action
+Bandits.ArrayModel.measurable_reward
+Bandits.ArrayModel.hist_congr
+Bandits.ArrayModel.stepsUntil_congr
+Bandits.ArrayModel.truePast
+Bandits.ArrayModel.measurable_hist_todo
+Bandits.ArrayModel.measurable_hist_truePast
+Bandits.ArrayModel.measurable_action_add_one_truePast
+Bandits.ArrayModel.measurable_pullCount_add_one_truePast
+Bandits.ArrayModel.measurable_stepsUntil
+Bandits.ArrayModel.measurable_pullCount_action_add_one_hist
+Bandits.ArrayModel.indepFun_fst_add_one_aux
+Bandits.ArrayModel.indepFun_fst_add_one_hist
+Bandits.ArrayModel.indepFun_snd_apply_aux
+Bandits.ArrayModel.indepFun_snd_apply_pullCount_action
+Bandits.ArrayModel.indepFun_snd_hist_cond
+Bandits.ArrayModel.hasLaw_action_zero
+Bandits.ArrayModel.hasCondDistrib_reward_zero
+Bandits.ArrayModel.hasCondDistrib_action
+Bandits.ArrayModel.hasCondDistrib_reward_pullCount_action
+Bandits.ArrayModel.hasCondDistrib_reward_hist_action_pullCount
+Bandits.ArrayModel.condIndepFun_reward_hist
+Bandits.ArrayModel.hasCondDistrib_reward
 Bandits.ArrayModel.isAlgEnvSeq_arrayMeasure
 Learning.measurable_comap_indicator_stepsUntil_eq
 Bandits.condIndepFun_reward_stepsUntil_action
diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex
index e89628b6..576e03b2 100644
--- a/blueprint/src/chapters/bandit.tex
+++ b/blueprint/src/chapters/bandit.tex
@@ -41,6 +41,8 @@ \section{The array model of rewards}
 Nonetheless, we now build an alternative model of the rewards, on which it will be easier to prove concentration inequalities.
 By the uniqueness of the law, these statements will then transfer to any algorithm-environment interaction.
 
+In the ``array model'', we consider a probability space on which we have an infinite array of rewards from each arm, independent from each other.
+When pulling an arm, the algorithm sees the next previously unseen reward from that arm in the array.
 
 \begin{definition}\label{def:arrayMeasure}
   \leanok
@@ -59,7 +61,8 @@ \section{The array model of rewards}
   \uses{def:algorithm}
   \leanok
   \lean{Bandits.ArrayModel.algFunction, Bandits.ArrayModel.initAlgFunction}
-Since $\mathcal{A}$ and $\mathcal{R}$ are standard Borel spaces, there exists jointly measurable functions $f'_0 : I \to \mathcal{A}$ and $f_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times I \to \mathcal{A}$ such that
+Let $\mathfrak{A}$ be an algorithm with action space $\mathcal{A}$ and reward space $\mathcal{R}$, policy $\pi$ and initial distribution $P_0$.
+For $\mathcal{A}$ and $\mathcal{R}$ standard Borel spaces, there exists jointly measurable functions $f'_0 : I \to \mathcal{A}$ and $f_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times I \to \mathcal{A}$ such that
 \begin{itemize}
   \item the law of $f'_0$ is $P_0$,
   \item for all history $h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$, the law of $f_t(h_t, \cdot)$ is $\pi_t(h_t)$.
@@ -67,18 +70,351 @@ \section{The array model of rewards}
 \end{definition}
 
 
-TODO: lots of results
+\begin{definition}\label{def:AM.history}
+  \uses{def:algFunction, def:arrayMeasure, def:pullCount}
+  \leanok
+  \lean{Bandits.ArrayModel.hist, Bandits.ArrayModel.action, Bandits.ArrayModel.reward}
+The history, actions and rewards on the array model probability space $(\Omega_{\mathcal{A}}, P_{\mathcal{A}})$ are defined as follows:
+\begin{itemize}
+  \item the action at time $0$ is $A_0(\omega) = f'_0(\omega_{1,0})$, the reward at time $0$ is $R_0(\omega) = \omega_{2,0,A_0(\omega)}$, and the history at time $0$ is $H_0(\omega) = (A_0(\omega), R_0(\omega))$,
+  \item for $t \ge 0$, the action at time $t+1$ is $A_{t+1}(\omega) = f_t(H_t(\omega), \omega_{1,t+1})$, the reward at time $t+1$ is $R_{t+1}(\omega) = \omega_{2,N_{t+1,A_{t+1}(\omega)},A_{t+1}(\omega)}$, and the history at time $t+1$ is $H_{t+1}(\omega) = (H_t(\omega), (A_{t+1}(\omega), R_{t+1}(\omega)))$.
+\end{itemize}
+\end{definition}
+
+
+The goal of this section is to show that $(\Omega_{\mathcal{A}}, P_{\mathcal{A}})$ with the actions and rewards defined above is an algorithm-environment sequence as in Definition~\ref{def:IsAlgEnvSeq}.
+
+
+\subsection{Measurability}
+
+TODO: some of those results are proved for $\mathcal{A}$ countable. Add that assumption where needed.
+
+\begin{remark}[Proving measurability with respect to a sub-sigma-algebra]
+In this section, we often need to prove that a random variable $X$ is measurable with respect to the sigma-algebra generated by a subset of the independent random variables defining the probability space $\Omega_{\mathcal{A}}$.
+We want to prove that $X : \Omega_{\mathcal{A}} \to \mathcal{X}$ is measurable with respect to the sigma-algebra $\sigma((\omega_p)_{p \in S})$, where $S$ is a subset of the indices of the independent random variables defining $\Omega_{\mathcal{A}}$.
+In most cases, this is due to $X$ being defined (possibly recursively in a complicated way) only using those random variables.
+However, it might be difficult to exhibit an explicit function $f$ such that $X = f((\omega_p)_{p \in S})$.
+
+Here is a general strategy to prove such measurability results in Lean:
+\begin{enumerate}
+  \item Prove that $X$ is measurable with respect to the full sigma-algebra on $\Omega_{\mathcal{A}}$.
+  \item Prove a congruence lemma: for any $\omega, \omega' \in \Omega_{\mathcal{A}}$, if $\omega_p = \omega'_p$ for all $p \in S$, then $X(\omega) = X(\omega')$.
+  \item Define $g : (\prod_{p \in S} \Omega_p) \to \Omega$ by $g((\omega_p)_{p \in S}) = \omega'$, where $\omega'_p = \omega_p$ for $p \in S$ and $\omega'_p$ is some fixed value for $p \notin S$.
+  \item Write $X = X \circ g \circ \mathrm{proj}_S$, where $\mathrm{proj}_S : \Omega_{\mathcal{A}} \to \prod_{p \in S} \Omega_p$ is the projection on the coordinates in $S$.
+  \item Conclude that $X$ is the composition of a measurable function $(X \circ g)$ and the random variable generating the sub-sigma-algebra, and thus is measurable with respect to that sub-sigma-algebra.
+\end{enumerate}
+\end{remark}
+
+\begin{lemma}[Measurability]\label{lem:AM.measurable_hist}
+  \uses{def:AM.history}
+  \leanok
+  \lean{Bandits.ArrayModel.measurable_hist, Bandits.ArrayModel.measurable_action, Bandits.ArrayModel.measurable_reward}
+$H_t$, $N_{t,A_t}$, $A_t$ and $R_t$ are measurable for all $t \in \mathbb{N}$.
+\end{lemma}
+
+\begin{proof}\leanok
+
+\end{proof}
+
+
+\begin{lemma}[Congruence for the history]\label{lem:AM.hist_congr}
+  \uses{def:AM.history}
+  \leanok
+  \lean{Bandits.ArrayModel.hist_congr}
+Let $\omega, \omega' \in \Omega_{\mathcal{A}}$ and $t \in \mathbb{N}$.
+Suppose that
+\begin{align*}
+  \forall s \le t, \ \omega_{1,s} &= \omega'_{1,s}
+  \: , \\
+  \forall a \in \mathcal{A}, \forall s < N_{t+1,a}, \ \omega_{2,s,a} &= \omega'_{2,s,a}
+  \: .
+\end{align*}
+Then $H_t(\omega) = H_t(\omega')$.
+\end{lemma}
+
+\begin{proof}\leanok
 
+\end{proof}
+
+
+\begin{lemma}[Congruence for the number of pulls and action]\label{lem:AM.stepsUntil_congr}
+  \uses{def:AM.history, def:pullCount}
+  \leanok
+  \lean{Bandits.ArrayModel.stepsUntil_congr}
+Let $\omega, \omega' \in \Omega_{\mathcal{A}}$, $t, m \in \mathbb{N}$ and $a \in \mathcal{A}$.
+Suppose that
+\begin{align*}
+  \omega_{1} &= \omega'_{1}
+  \: , \\
+  \forall s < m, \ \omega_{2,s,a} &= \omega'_{2,s,a}
+  \: , \\
+  \forall b \ne a, \forall s \in \mathbb{N}, \ \omega_{2,s,b} &= \omega'_{2,s,b}
+  \: .
+\end{align*}
+Then $(N_{t+1, a}(\omega) = m \wedge A_{t+1}(\omega) = a) \iff (N_{t+1, a}(\omega') = m \wedge A_{t+1}(\omega') = a)$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.hist_congr}
+
+\end{proof}
+
+
+\begin{definition}\label{def:AM.probSpaceSubsets}
+  \leanok
+  \lean{Bandits.ArrayModel.truePast}
+We define the following functions on $\Omega_{\mathcal{A}}$:
+\begin{align*}
+  F_{1, t}(\omega) &= ((\omega_{1,s})_{s \le t}, (\omega_{2,s})_{s \in \mathbb{N}})
+  \: , \\
+  F_{2, a, t}(\omega) &= ((\omega_{1,s})_{s \in \mathbb{N}}, (\omega_{2, \min\{s,N_{t+1,a}(\omega)-1\}, a})_{s \in \mathbb{N}}, (\omega_{2, s, b})_{s \in \mathbb{N}, b \ne a})
+  \: , \\
+  F_{2, a}^m(\omega) &= ((\omega_{1,s})_{s \in \mathbb{N}}, (\omega_{2, \min\{s,m-1\}, a})_{s \in \mathbb{N}}, (\omega_{2, s, b})_{s \in \mathbb{N}, b \ne a})
+  \: .
+\end{align*}
+In the definition of $F_{2, a, t}$ and $F_{2, a}^m$, if $N_{t+1,a}(\omega) = 0$ (resp. $m = 0$), then the second component is a constant sequence equal to an arbitrary value.
+
+$F_{1, t}(\omega)$ contains all the information in $\omega$ except for the action selection randomness after time $t$.
+
+$F_{2, a, t}(\omega)$ contains all the information in $\omega$ except the rewards for arm $a$ indexed by $N_{t+1,a}(\omega)$ or more.
+$F_{2, a}^m(\omega)$ is similar, but removes the rewards for arm $a$ indexed by $m$ or more.
+\end{definition}
+
+
+\begin{lemma}\label{lem:AM.measurable_hist_todo}
+  \uses{def:AM.probSpaceSubsets, def:AM.history}
+  \leanok
+  \lean{Bandits.ArrayModel.measurable_hist_todo, Bandits.ArrayModel.measurable_hist_truePast}
+For all $t \in \mathbb{N}$, $H_t$ is measurable with respect to the sigma-algebra generated by $F_{1, t}$, and with respect to the sigma-algebra generated by $F_{2, a, t}$ for any arm $a \in \mathcal{A}$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.measurable_hist, lem:AM.hist_congr}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.measurable_action_add_one_truePast}
+  \uses{def:AM.probSpaceSubsets, def:AM.history}
+  \leanok
+  \lean{Bandits.ArrayModel.measurable_action_add_one_truePast}
+$A_{t+1}$ is measurable with respect to the sigma-algebra generated by $F_{2, a, t}$ for any arm $a \in \mathcal{A}$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.measurable_hist_todo}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.measurable_pullCount_add_one_truePast}
+  \uses{def:AM.probSpaceSubsets, def:pullCount}
+  \leanok
+  \lean{Bandits.ArrayModel.measurable_pullCount_add_one_truePast}
+$N_{t+1,a}$ is measurable with respect to the sigma-algebra generated by $F_{2, a, t}$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.measurable_hist_todo}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.measurable_stepsUntil}
+  \uses{def:AM.probSpaceSubsets, def:pullCount}
+  \leanok
+  \lean{Bandits.ArrayModel.measurable_stepsUntil}
+For $t, m \in \mathbb{N}$ and $a \in \mathcal{A}$, the indicator function $\mathbb{I}\{N_{t+1,a} = m \wedge A_{t+1} = a\} : \Omega_{\mathcal{A}} \to \{0, 1\}$ is measurable with respect to the sigma-algebra generated by $F_{2, a}^m$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.stepsUntil_congr, lem:AM.measurable_hist}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.measurable_pullCount_action_add_one_hist}
+  \uses{def:AM.history, def:pullCount}
+  \leanok
+  \lean{Bandits.ArrayModel.measurable_pullCount_action_add_one_hist}
+For $t \in \mathbb{N}$, the function $N_{t+1, A_{t+1}}$ is measurable with respect to the sigma-algebra generated by $H_t$ and $A_{t+1}$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:pullCount_basic}
+
+\end{proof}
+
+
+\subsection{Independence}
+
+
+\begin{lemma}\label{lem:AM.indepFun_fst_add_one_aux}
+  \uses{def:AM.probSpaceSubsets}
+  \leanok
+  \lean{Bandits.ArrayModel.indepFun_fst_add_one_aux}
+$\omega \mapsto \omega_{1, t+1}$ is independent of $F_{1, t}$.
+\end{lemma}
+
+\begin{proof}\leanok
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.indepFun_fst_add_one_hist}
+  \uses{def:AM.history, def:AM.probSpaceSubsets}
+  \leanok
+  \lean{Bandits.ArrayModel.indepFun_fst_add_one_hist}
+$\omega \mapsto \omega_{1, t+1}$ is independent of $H_t$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.measurable_hist_todo, lem:AM.indepFun_fst_add_one_aux}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.indepFun_snd_apply_aux}
+  \uses{def:AM.probSpaceSubsets}
+  \leanok
+  \lean{Bandits.ArrayModel.indepFun_snd_apply_aux}
+For $a \in \mathcal{A}$ and $m \in \mathbb{N}$, $\omega \mapsto \omega_{2, m, a}$ is independent of $F_{2, a}^m$.
+\end{lemma}
+
+\begin{proof}\leanok
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.indepFun_snd_apply_pullCount_action}
+  \uses{def:AM.history, def:pullCount, def:AM.probSpaceSubsets}
+  \leanok
+  \lean{Bandits.ArrayModel.indepFun_snd_apply_pullCount_action}
+For $a \in \mathcal{A}$, $\omega \mapsto \omega_{2, m, a}$ is independent of the indicator function $\mathbb{I}\{N_{t+1,a} = m \wedge A_{t+1} = a\}$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.measurable_stepsUntil, lem:AM.indepFun_snd_apply_aux}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.indepFun_snd_hist_cond}
+  \uses{def:AM.history, def:pullCount}
+  \leanok
+  \lean{Bandits.ArrayModel.indepFun_snd_hist_cond}
+For $a \in \mathcal{A}$ and $t, m \in \mathbb{N}$, $\omega \mapsto \omega_{2, m, a}$ is independent of $H_t$ given that $N_{t+1,a} = m$ and $A_{t+1} = a$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.measurable_stepsUntil, lem:AM.measurable_hist_todo, lem:AM.indepFun_snd_apply_aux}
+
+\end{proof}
+
+
+\subsection{Laws}
+
+
+\begin{lemma}\label{lem:AM.hasLaw_action_zero}
+  \uses{def:AM.history, def:algFunction}
+  \leanok
+  \lean{Bandits.ArrayModel.hasLaw_action_zero}
+The law of $A_0$ in the array model is $P_0$.
+\end{lemma}
+
+\begin{proof}\leanok
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.hasCondDistrib_reward_zero}
+  \uses{def:AM.history}
+  \leanok
+  \lean{Bandits.ArrayModel.hasCondDistrib_reward_zero}
+In the array model, $P_{\mathcal{A}}[R_0 \mid A_0] = \nu$.
+\end{lemma}
+
+\begin{proof}\leanok
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.hasCondDistrib_action}
+  \uses{def:AM.history}
+  \leanok
+  \lean{Bandits.ArrayModel.hasCondDistrib_action}
+In the array model, $P_{\mathcal{A}}[A_{t+1} \mid H_t] = \pi_t$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.indepFun_fst_add_one_hist, def:algFunction}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.hasCondDistrib_reward_pullCount_action}
+  \uses{def:AM.history, def:pullCount}
+  \leanok
+  \lean{Bandits.ArrayModel.hasCondDistrib_reward_pullCount_action}
+In the array model, $P_{\mathcal{A}}[R_{t+1} \mid N_{t+1,A_{t+1}}, A_{t+1}] = \nu$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.indepFun_snd_apply_pullCount_action}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.hasCondDistrib_reward_hist_action_pullCount}
+  \uses{def:AM.history, def:pullCount}
+  \leanok
+  \lean{Bandits.ArrayModel.hasCondDistrib_reward_hist_action_pullCount}
+In the array model, $P_{\mathcal{A}}[R_{t+1} \mid H_t, A_{t+1}, N_{t+1,A_{t+1}}] = \nu$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.indepFun_snd_hist_cond, lem:AM.indepFun_snd_apply_pullCount_action}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.condIndepFun_reward_hist}
+  \uses{def:AM.history}
+  \leanok
+  \lean{Bandits.ArrayModel.condIndepFun_reward_hist}
+For $t \ge 0$, $R_{t+1} \ind H_t \mid A_{t+1}, N_{t+1, A_{t+1}}$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.hasCondDistrib_reward_hist_action_pullCount}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.hasCondDistrib_reward}
+  \uses{def:AM.history}
+  \leanok
+  \lean{Bandits.ArrayModel.hasCondDistrib_reward}
+In the array model, $P_{\mathcal{A}}[R_{t+1} \mid H_t, A_{t+1}] = \nu$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.measurable_pullCount_action_add_one_hist, lem:AM.condIndepFun_reward_hist,
+  lem:AM.hasCondDistrib_reward_pullCount_action}
+
+\end{proof}
 
 \begin{theorem}\label{thm:isAlgEnvSeq_arrayMeasure}
-  \uses{def:bandit, def:arrayMeasure}
+  \uses{def:bandit, def:arrayMeasure, def:IsAlgEnvSeq}
   \leanok
   \lean{Bandits.ArrayModel.isAlgEnvSeq_arrayMeasure}
-TODO
+The actions and rewards defined on the array model probability space $(\Omega_{\mathcal{A}}, P_{\mathcal{A}})$ form an algorithm-environment sequence for the algorithm $\mathfrak{A}$ and bandit $\nu$.
 \end{theorem}
 
-\begin{proof}
-
+\begin{proof}\leanok
+  \uses{lem:AM.hasLaw_action_zero, lem:AM.hasCondDistrib_reward_zero,
+  lem:AM.hasCondDistrib_action, lem:AM.hasCondDistrib_reward}
+The four conditions of Definition~\ref{def:IsAlgEnvSeq} are satisfied by Lemmas~\ref{lem:AM.hasLaw_action_zero}, \ref{lem:AM.hasCondDistrib_reward_zero}, \ref{lem:AM.hasCondDistrib_action} and \ref{lem:AM.hasCondDistrib_reward}.
 \end{proof}