diff --git a/LeanBandits.lean b/LeanBandits.lean
index aa4d81cb..a5d8fef3 100644
--- a/LeanBandits.lean
+++ b/LeanBandits.lean
@@ -1,9 +1,11 @@
+import LeanBandits.Algorithm
 import LeanBandits.AlgorithmBuilding
 import LeanBandits.Bandit
 import LeanBandits.ETC
 import LeanBandits.ForMathlib.CondDistrib
 import LeanBandits.ForMathlib.KernelCompositionLemmas
 import LeanBandits.ForMathlib.KernelCompositionParallelComp
+import LeanBandits.ForMathlib.KernelSub
 import LeanBandits.ForMathlib.Traj
 import LeanBandits.Regret
 import LeanBandits.RewardByCountMeasure
diff --git a/LeanBandits/Algorithm.lean b/LeanBandits/Algorithm.lean
new file mode 100644
index 00000000..d886459d
--- /dev/null
+++ b/LeanBandits/Algorithm.lean
@@ -0,0 +1,232 @@
+/-
+Copyright (c) 2025 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne, Paulo Rauber
+-/
+import Mathlib
+import LeanBandits.ForMathlib.CondDistrib
+import LeanBandits.ForMathlib.KernelCompositionLemmas
+import LeanBandits.ForMathlib.Traj
+
+/-!
+# Bandit
+-/
+
+open MeasureTheory ProbabilityTheory Filter Real Finset
+
+open scoped ENNReal NNReal
+
+namespace Learning
+
+variable {α R : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R}
+
+/-- A stochastic, sequential algorithm. -/
+structure Algorithm (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] where
+  /-- Policy or sampling rule: distribution of the next action. -/
+  policy : (n : ℕ) → Kernel (Iic n → α × R) α
+  [h_policy : ∀ n, IsMarkovKernel (policy n)]
+  /-- Distribution of the first action. -/
+  p0 : Measure α
+  [hp0 : IsProbabilityMeasure p0]
+
+instance (alg : Algorithm α R) (n : ℕ) : IsMarkovKernel (alg.policy n) := alg.h_policy n
+instance (alg : Algorithm α R) : IsProbabilityMeasure alg.p0 := alg.hp0
+
+/-- A stochastic environment. -/
+structure Environment (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] where
+  /-- Distribution of the next observation as function of the past history. -/
+  feedback : (n : ℕ) → Kernel ((Iic n → α × R) × α) R
+  [h_feedback : ∀ n, IsMarkovKernel (feedback n)]
+  /-- Distribution of the first observation given the first action. -/
+  ν0 : Kernel α R
+  [hp0 : IsMarkovKernel ν0]
+
+instance (env : Environment α R) (n : ℕ) : IsMarkovKernel (env.feedback n) := env.h_feedback n
+instance (env : Environment α R) : IsMarkovKernel env.ν0 := env.hp0
+
+/-- A deterministic algorithm. -/
+noncomputable
+def detAlgorithm (nextaction : (n : ℕ) → (Iic n → α × R) → α)
+    (h_next : ∀ n, Measurable (nextaction n)) (action0 : α) :
+    Algorithm α R where
+  policy n := Kernel.deterministic (nextaction n) (h_next n)
+  p0 := Measure.dirac action0
+
+/-- A stationary environment, in which the distribution of the next reward depends only on the last
+action. -/
+@[simps]
+def stationaryEnv (ν : Kernel α R) [IsMarkovKernel ν] : Environment α R where
+  feedback _ := ν.prodMkLeft _
+  ν0 := ν
+
+/-- Kernel describing the distribution of the next action-reward pair given the history
+up to `n`. -/
+noncomputable
+def stepKernel (alg : Algorithm α R) (env : Environment α R) (n : ℕ) :
+    Kernel (Iic n → α × R) (α × R) :=
+  alg.policy n ⊗ₖ env.feedback n
+deriving IsMarkovKernel
+
+@[simp]
+lemma fst_stepKernel (alg : Algorithm α R) (env : Environment α R) (n : ℕ) :
+    (stepKernel alg env n).fst = alg.policy n := by
+  rw [stepKernel, Kernel.fst_compProd]
+
+/-- Kernel sending a partial trajectory of the bandit interaction `Iic n → α × ℝ` to a measure
+on `ℕ → α × ℝ`, supported on full trajectories that start with the partial one. -/
+noncomputable def traj (alg : Algorithm α R) (env : Environment α R) (n : ℕ) :
+    Kernel (Iic n → α × R) (ℕ → α × R) :=
+  ProbabilityTheory.Kernel.traj (X := fun _ ↦ α × R) (stepKernel alg env) n
+deriving IsMarkovKernel
+
+/-- Measure on the sequence of actions and observations generated by the algorithm/environment. -/
+noncomputable
+def trajMeasure (alg : Algorithm α R) (env : Environment α R) :
+    Measure (ℕ → α × R) :=
+  Kernel.trajMeasure (alg.p0 ⊗ₘ env.ν0) (stepKernel alg env)
+deriving IsProbabilityMeasure
+
+/-- Action and reward at step `n`. -/
+def step (n : ℕ) (h : ℕ → α × R) : α × R := h n
+
+/-- `action n` is the action pulled at time `n`. This is a random variable on the measurable space
+`ℕ → α × ℝ`. -/
+def action (n : ℕ) (h : ℕ → α × R) : α := (h n).1
+
+/-- `reward n` is the reward at time `n`. This is a random variable on the measurable space
+`ℕ → α × R`. -/
+def reward (n : ℕ) (h : ℕ → α × R) : R := (h n).2
+
+/-- `hist n` is the history up to time `n`. This is a random variable on the measurable space
+`ℕ → α × R`. -/
+def hist (n : ℕ) (h : ℕ → α × R) : Iic n → α × R := fun i ↦ h i
+
+lemma fst_comp_step (n : ℕ) : Prod.fst ∘ step (α := α) (R := R) n = action n := rfl
+
+@[fun_prop]
+lemma measurable_step (n : ℕ) : Measurable (step n (α := α) (R := R)) := by
+  unfold step; fun_prop
+
+@[fun_prop]
+lemma measurable_step_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ step p.1 p.2) := by
+  refine measurable_from_prod_countable_right fun n ↦ ?_
+  simp only
+  fun_prop
+
+@[fun_prop]
+lemma measurable_action (n : ℕ) : Measurable (action n (α := α) (R := R)) := by
+  unfold action; fun_prop
+
+@[fun_prop]
+lemma measurable_action_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ action p.1 p.2) := by
+  refine measurable_from_prod_countable_right fun n ↦ ?_
+  simp only
+  fun_prop
+
+@[fun_prop]
+lemma measurable_reward (n : ℕ) : Measurable (reward n (α := α) (R := R)) := by
+  unfold reward; fun_prop
+
+@[fun_prop]
+lemma measurable_reward_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ reward p.1 p.2) := by
+  refine measurable_from_prod_countable_right fun n ↦ ?_
+  simp only
+  fun_prop
+
+@[fun_prop]
+lemma measurable_hist (n : ℕ) : Measurable (hist n (α := α) (R := R)) := by unfold hist; fun_prop
+
+lemma hist_eq_frestrictLe :
+    hist = Preorder.frestrictLe («π» := fun _ ↦ α × R) := by
+  ext n h i : 3
+  simp [hist, Preorder.frestrictLe]
+
+/-- Filtration of the algorithm interaction. -/
+protected def filtration (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] :
+    Filtration ℕ (inferInstance : MeasurableSpace (ℕ → α × R)) :=
+  MeasureTheory.Filtration.piLE (X := fun _ ↦ α × R)
+
+lemma condDistrib_step [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
+    (alg : Algorithm α R) (env : Environment α R) (n : ℕ) :
+    condDistrib (step (n + 1)) (hist n) (trajMeasure alg env)
+      =ᵐ[(trajMeasure alg env).map (hist n)] stepKernel alg env n :=
+  Kernel.condDistrib_trajMeasure_ae_eq_kernel
+
+lemma condDistrib_action [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
+    (alg : Algorithm α R) (env : Environment α R) (n : ℕ) :
+    condDistrib (action (n + 1)) (hist n) (trajMeasure alg env)
+      =ᵐ[(trajMeasure alg env).map (hist n)] alg.policy n := by
+  rw [← fst_comp_step]
+  refine (condDistrib_comp' (by fun_prop) (by fun_prop) (by fun_prop)).trans ?_
+  filter_upwards [condDistrib_step alg env n] with h h_eq
+  rw [Kernel.map_apply _ (by fun_prop), h_eq, ← Kernel.map_apply _ (by fun_prop), ← Kernel.fst_eq,
+    fst_stepKernel]
+
+lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
+    (alg : Algorithm α R) (env : Environment α R) (n : ℕ) :
+    condDistrib (reward (n + 1)) (fun ω ↦ (hist n ω, action (n + 1) ω)) (trajMeasure alg env)
+      =ᵐ[(trajMeasure alg env).map (fun ω ↦ (hist n ω, action (n + 1) ω))] env.feedback n := by
+  have h_step := condDistrib_step alg env n
+  have h_action := condDistrib_action alg env n
+  rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)] at h_step h_action ⊢
+  rw [h_action, Measure.compProd_assoc, ← stepKernel, ← h_step,
+    Measure.map_map (by fun_prop) (by fun_prop)]
+  rfl
+
+lemma hasLaw_step_zero (alg : Algorithm α R) (env : Environment α R) :
+    HasLaw (step 0) (alg.p0 ⊗ₘ env.ν0) (trajMeasure alg env) where
+  aemeasurable := Measurable.aemeasurable (by fun_prop)
+  map_eq := by
+    unfold step
+    simp only [trajMeasure, Kernel.trajMeasure]
+    rw [← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc,
+      Kernel.deterministic_comp_eq_map, Kernel.traj_zero_map_eval_zero,
+      Measure.deterministic_comp_eq_map, Measure.map_map (by fun_prop) (by fun_prop)]
+    simp
+
+lemma hasLaw_action_zero (alg : Algorithm α R) (env : Environment α R) :
+    HasLaw (action 0) alg.p0 (trajMeasure alg env) where
+  map_eq := by
+    rw [← fst_comp_step, ← Measure.map_map (by fun_prop) (by fun_prop),
+      (hasLaw_step_zero alg env).map_eq, ← Measure.fst, Measure.fst_compProd]
+
+lemma condDistrib_reward_zero [StandardBorelSpace R] [Nonempty R]
+    (alg : Algorithm α R) (env : Environment α R) :
+    condDistrib (reward 0) (action 0) (trajMeasure alg env)
+      =ᵐ[(trajMeasure alg env).map (action 0)] env.ν0 := by
+  have h_step := (hasLaw_step_zero alg env).map_eq
+  have h_action := (hasLaw_action_zero alg env).map_eq
+  rwa [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop), h_action]
+
+section DetAlgorithm
+
+variable {nextaction : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextaction n)}
+  {action0 : α} {env : Environment α R}
+
+lemma HasLaw_action_zero_detAlgorithm :
+    HasLaw (action 0) (Measure.dirac action0)
+      (trajMeasure (detAlgorithm nextaction h_next action0) env) where
+  map_eq := (hasLaw_action_zero _ _).map_eq
+
+lemma action_zero_detAlgorithm [MeasurableSingletonClass α] :
+    action 0 =ᵐ[trajMeasure (detAlgorithm nextaction h_next action0) env] fun _ ↦ action0 := by
+  have h_eq : ∀ᵐ x ∂((trajMeasure (detAlgorithm nextaction h_next action0) env).map (action 0)), x
+      = action0 := by
+    rw [(hasLaw_action_zero _ _).map_eq]
+    simp [detAlgorithm]
+  exact ae_of_ae_map (by fun_prop) h_eq
+
+lemma action_detAlgorithm_ae_eq (n : ℕ) :
+    action (n + 1) =ᵐ[trajMeasure (detAlgorithm nextaction h_next action0) env]
+      fun h ↦ nextaction n (fun i ↦ h i) := by
+  sorry
+
+example [MeasurableSingletonClass α] :
+    ∀ᵐ h ∂(trajMeasure (detAlgorithm nextaction h_next action0) env),
+    action 0 h = action0 ∧ ∀ n, action (n + 1) h = nextaction n (fun i ↦ h i) := by
+  rw [eventually_and, ae_all_iff]
+  exact ⟨action_zero_detAlgorithm, action_detAlgorithm_ae_eq⟩
+
+end DetAlgorithm
+
+end Learning
diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean
index 517debd5..06be7c03 100644
--- a/LeanBandits/Bandit.lean
+++ b/LeanBandits/Bandit.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Paulo Rauber
 -/
 import Mathlib
+import LeanBandits.Algorithm
 import LeanBandits.ForMathlib.CondDistrib
 import LeanBandits.ForMathlib.KernelCompositionLemmas
 import LeanBandits.ForMathlib.Traj
@@ -12,7 +13,7 @@ import LeanBandits.ForMathlib.Traj
 # Bandit
 -/
 
-open MeasureTheory ProbabilityTheory Filter Real Finset
+open MeasureTheory ProbabilityTheory Filter Real Finset Learning
 
 open scoped ENNReal NNReal
 
@@ -22,54 +23,24 @@ variable {α R : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R}
 
 section MeasureSpace
 
-/-- A stochastic, sequential algorithm. -/
-structure Algorithm (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] where
-  /-- Policy or sampling rule: distribution of the next pull. -/
-  policy : (n : ℕ) → Kernel (Iic n → α × R) α
-  [h_policy : ∀ n, IsMarkovKernel (policy n)]
-  /-- Distribution of the first pull. -/
-  p0 : Measure α
-  [hp0 : IsProbabilityMeasure p0]
-
-instance (alg : Algorithm α R) (n : ℕ) : IsMarkovKernel (alg.policy n) := alg.h_policy n
-instance (alg : Algorithm α R) : IsProbabilityMeasure alg.p0 := alg.hp0
-
-/-- A deterministic algorithm. -/
-noncomputable
-def detAlgorithm (nextArm : (n : ℕ) → (Iic n → α × R) → α) (h_next : ∀ n, Measurable (nextArm n))
-    (arm0 : α) :
-    Algorithm α R where
-  policy n := Kernel.deterministic (nextArm n) (h_next n)
-  p0 := Measure.dirac arm0
-
 namespace Bandit
 
 /-- Kernel describing the distribution of the next arm-reward pair given the history up to `n`. -/
 noncomputable
-def stepKernel (alg : Algorithm α R) (ν : Kernel α R) (n : ℕ) : Kernel (Iic n → α × R) (α × R) :=
-  (alg.policy n) ⊗ₖ ν.prodMkLeft (Iic n → α × R)
-
-instance (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
-    IsMarkovKernel (stepKernel alg ν n) := by
-  rw [stepKernel]
-  infer_instance
+def stepKernel (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
+    Kernel (Iic n → α × R) (α × R) :=
+  Learning.stepKernel alg (stationaryEnv ν) n
+deriving IsMarkovKernel
 
 @[simp]
 lemma fst_stepKernel (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
     (stepKernel alg ν n).fst = alg.policy n := by
-  rw [stepKernel, Kernel.fst_compProd]
+  rw [stepKernel, Learning.fst_stepKernel]
 
 @[simp]
 lemma snd_stepKernel (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
     (stepKernel alg ν n).snd = ν ∘ₖ alg.policy n := by
-  rw [stepKernel, Kernel.snd_compProd_prodMkLeft]
-
-/-- Kernel sending a partial trajectory of the bandit interaction `Iic n → α × ℝ` to a measure
-on `ℕ → α × ℝ`, supported on full trajectories that start with the partial one. -/
-noncomputable def traj (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
-    Kernel (Iic n → α × R) (ℕ → α × R) :=
-  ProbabilityTheory.Kernel.traj (X := fun _ ↦ α × R) (stepKernel alg ν) n
-deriving IsMarkovKernel
+  rw [stepKernel, Learning.stepKernel, stationaryEnv_feedback, Kernel.snd_compProd_prodMkLeft]
 
 /-- Measure on the sequence of arms pulled and rewards observed generated by the bandit. -/
 noncomputable
@@ -116,26 +87,23 @@ def reward (n : ℕ) (h : ℕ → α × R) : R := (h n).2
 def hist (n : ℕ) (h : ℕ → α × R) : Iic n → α × R := fun i ↦ h i
 
 @[fun_prop]
-lemma measurable_arm (n : ℕ) : Measurable (arm n (α := α) (R := R)) := by unfold arm; fun_prop
+lemma measurable_arm (n : ℕ) : Measurable (arm n (α := α) (R := R)) := measurable_action n
 
 @[fun_prop]
-lemma measurable_arm_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ arm p.1 p.2) := by
-  refine measurable_from_prod_countable_right fun n ↦ ?_
-  simp only
-  fun_prop
+lemma measurable_arm_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ arm p.1 p.2) :=
+  measurable_action_prod
 
 @[fun_prop]
-lemma measurable_reward (n : ℕ) : Measurable (reward n (α := α) (R := R)) := by
-  unfold reward; fun_prop
+lemma measurable_reward (n : ℕ) : Measurable (reward n (α := α) (R := R)) :=
+  Learning.measurable_reward n
 
 @[fun_prop]
-lemma measurable_reward_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ reward p.1 p.2) := by
-  refine measurable_from_prod_countable_right fun n ↦ ?_
-  simp only
-  fun_prop
+lemma measurable_reward_prod : Measurable (fun p : ℕ × (ℕ → α × R) ↦ reward p.1 p.2) :=
+  Learning.measurable_reward_prod
 
 @[fun_prop]
-lemma measurable_hist (n : ℕ) : Measurable (hist n (α := α) (R := R)) := by unfold hist; fun_prop
+lemma measurable_hist (n : ℕ) : Measurable (hist n (α := α) (R := R)) :=
+  Learning.measurable_hist n
 
 lemma hist_eq_frestrictLe :
     hist = Preorder.frestrictLe («π» := fun _ ↦ α × R) := by
@@ -147,81 +115,64 @@ protected def filtration (α R : Type*) [MeasurableSpace α] [MeasurableSpace R]
     Filtration ℕ (inferInstance : MeasurableSpace (ℕ → α × R)) :=
   MeasureTheory.Filtration.piLE (X := fun _ ↦ α × R)
 
-section Traj
-
-open Kernel Preorder
+lemma hasLaw_step_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] :
+    HasLaw (fun h : ℕ → α × R ↦ h 0) (alg.p0 ⊗ₘ ν) (Bandit.trajMeasure alg ν) :=
+  Learning.hasLaw_step_zero alg (stationaryEnv ν)
 
-variable {X : ℕ → Type*} [∀ n, MeasurableSpace (X n)]
-    {κ : (n : ℕ) → Kernel ((i : { x // x ∈ Iic n }) → X i) (X (n + 1))} [∀ n, IsMarkovKernel (κ n)]
-
-lemma traj_zero_map_eval_zero :
-    (Kernel.traj κ 0).map (fun h ↦ h 0)
-      = Kernel.deterministic (MeasurableEquiv.piIicZero X)
-        (MeasurableEquiv.piIicZero X).measurable := by
-  suffices (Kernel.traj κ 0).map (fun h ↦ h 0) = (Kernel.partialTraj κ 0 0).map
-      (MeasurableEquiv.piIicZero X) by
-    rwa [Kernel.partialTraj_zero,
-      Kernel.deterministic_map _ (MeasurableEquiv.piIicZero X).measurable] at this
-  rw [← Kernel.traj_map_frestrictLe, ← Kernel.map_comp_right _ (by fun_prop) (by fun_prop)]
-  congr with h
-  sorry
-
-end Traj
+lemma hasLaw_arm_zero (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] :
+    HasLaw (arm 0) alg.p0 (Bandit.trajMeasure alg ν) :=
+  Learning.hasLaw_action_zero alg (stationaryEnv ν)
 
 lemma condDistrib_arm_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
     (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
     condDistrib (fun h ↦ (arm (n + 1) h, reward (n + 1) h)) (hist n) (Bandit.trajMeasure alg ν)
       =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] Bandit.stepKernel alg ν n :=
-  Kernel.condDistrib_trajMeasure_ae_eq_kernel
+  Learning.condDistrib_step alg (stationaryEnv ν) n
+
+lemma condDistrib_reward' [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
+    (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
+    condDistrib (reward (n + 1)) (fun ω ↦ (hist n ω, arm (n + 1) ω)) (Bandit.trajMeasure alg ν)
+      =ᵐ[(Bandit.trajMeasure alg ν).map (fun ω ↦ (hist n ω, arm (n + 1) ω))] ν.prodMkLeft _ :=
+  Learning.condDistrib_reward alg (stationaryEnv ν) n
 
 lemma condDistrib_reward [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
     (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
     condDistrib (reward n) (arm n) (Bandit.trajMeasure alg ν)
       =ᵐ[(Bandit.trajMeasure alg ν).map (arm n)] ν := by
   cases n with
-  | zero => sorry
+  | zero =>
+    rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)]
+    change (Bandit.trajMeasure alg ν).map (fun h ↦ h 0)
+      = (Bandit.trajMeasure alg ν).map (arm 0) ⊗ₘ ν
+    rw [(hasLaw_arm_zero alg ν).map_eq, (hasLaw_step_zero alg ν).map_eq]
   | succ n =>
-    have h_ar := condDistrib_arm_reward alg ν n
-    have h_prod := condDistrib_prod_left (X := arm (n + 1)) (Y := reward (n + 1))
-      (T := hist n) (μ := Bandit.trajMeasure alg ν) (by fun_prop) (by fun_prop) (by fun_prop)
-    sorry
+    have h_eq := condDistrib_reward' alg ν n
+    rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)] at h_eq ⊢
+    have : (Bandit.trajMeasure alg ν).map (arm (n + 1))
+        = ((Bandit.trajMeasure alg ν).map (fun x ↦ (hist n x, arm (n + 1) x))).snd := by
+      rw [Measure.snd_map_prodMk (by fun_prop)]
+    rw [this, ← Measure.snd_prodAssoc_compProd_prodMkLeft, ← h_eq,
+      Measure.snd_map_prodMk (by fun_prop), Measure.map_map (by fun_prop) (by fun_prop)]
+    congr
 
 lemma condDistrib_arm [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
     (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
     condDistrib (arm (n + 1)) (hist n) (Bandit.trajMeasure alg ν)
-      =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] alg.policy n := by
-  sorry
-
-lemma hasLaw_step_zero
-    (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] :
-    HasLaw (fun h : ℕ → α × R ↦ h 0) (alg.p0 ⊗ₘ ν) (Bandit.trajMeasure alg ν) where
-  aemeasurable := Measurable.aemeasurable (by fun_prop)
-  map_eq := by
-    simp only [Bandit.trajMeasure, Kernel.trajMeasure]
-    rw [← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc,
-      Kernel.deterministic_comp_eq_map, traj_zero_map_eval_zero,
-      Measure.deterministic_comp_eq_map, Measure.map_map (by fun_prop) (by fun_prop)]
-    simp
-
-lemma hasLaw_arm_zero [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
-    (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] :
-    HasLaw (arm 0) alg.p0 (Bandit.trajMeasure alg ν) where
-  map_eq := by
-    sorry
+      =ᵐ[(Bandit.trajMeasure alg ν).map (hist n)] alg.policy n :=
+  Learning.condDistrib_action alg (stationaryEnv ν) n
 
 /-- The reward at time `n+1` is independent of the history up to time `n` given the arm at `n+1`. -/
 lemma condIndepFun_reward_hist_arm [StandardBorelSpace α] [Nonempty α]
     [StandardBorelSpace R] [Nonempty R]
     {alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν] (n : ℕ) :
     CondIndepFun (MeasurableSpace.comap (arm (n + 1)) inferInstance)
-      (measurable_arm _).comap_le (reward (n + 1)) (hist n) (Bandit.trajMeasure alg ν) := by
-  rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft (by fun_prop) (by fun_prop) (by fun_prop)]
-  sorry
+      (measurable_arm _).comap_le (reward (n + 1)) (hist n) (Bandit.trajMeasure alg ν) :=
+  condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft
+    (by fun_prop) (by fun_prop) (by fun_prop) (condDistrib_reward' alg ν n)
 
 section DetAlgorithm
 
-variable [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
-  {nextArm : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextArm n)}
+variable {nextArm : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextArm n)}
   {arm0 : α} {ν : Kernel α R} [IsMarkovKernel ν]
 
 lemma HasLaw_arm_zero_detAlgorithm :
@@ -229,7 +180,7 @@ lemma HasLaw_arm_zero_detAlgorithm :
       (Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν) where
   map_eq := (hasLaw_arm_zero _ _).map_eq
 
-lemma arm_zero_detAlgorithm :
+lemma arm_zero_detAlgorithm [MeasurableSingletonClass α] :
     arm 0 =ᵐ[Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν] fun _ ↦ arm0 := by
   have h_eq : ∀ᵐ x ∂((Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν).map (arm 0)), x
       = arm0 := by
@@ -242,7 +193,8 @@ lemma arm_detAlgorithm_ae_eq (n : ℕ) :
       fun h ↦ nextArm n (fun i ↦ h i) := by
   sorry
 
-example : ∀ᵐ h ∂(Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν),
+example [MeasurableSingletonClass α] :
+    ∀ᵐ h ∂(Bandit.trajMeasure (detAlgorithm nextArm h_next arm0) ν),
     arm 0 h = arm0 ∧ ∀ n, arm (n + 1) h = nextArm n (fun i ↦ h i) := by
   rw [eventually_and, ae_all_iff]
   exact ⟨arm_zero_detAlgorithm, arm_detAlgorithm_ae_eq⟩
diff --git a/LeanBandits/ETC.lean b/LeanBandits/ETC.lean
index 85e3c12a..52d1c850 100644
--- a/LeanBandits/ETC.lean
+++ b/LeanBandits/ETC.lean
@@ -11,7 +11,7 @@ import LeanBandits.Regret
 
 -/
 
-open MeasureTheory ProbabilityTheory Finset
+open MeasureTheory ProbabilityTheory Finset Learning
 open scoped ENNReal NNReal
 
 namespace Bandits
diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanBandits/ForMathlib/CondDistrib.lean
index baf7bb06..26f7eef7 100644
--- a/LeanBandits/ForMathlib/CondDistrib.lean
+++ b/LeanBandits/ForMathlib/CondDistrib.lean
@@ -3,10 +3,13 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
+import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 import Mathlib.Probability.Independence.Basic
 import Mathlib.Probability.Independence.Conditional
 import Mathlib.Probability.Kernel.CompProdEqIff
 import Mathlib.Probability.Kernel.Composition.Lemmas
+import LeanBandits.ForMathlib.KernelCompositionParallelComp
+import LeanBandits.ForMathlib.KernelSub
 
 open MeasureTheory ProbabilityTheory Finset
 open scoped ENNReal NNReal
@@ -399,6 +402,25 @@ lemma condDistrib_ae_eq_iff_measure_eq_compProd₀
   refine ⟨fun h ↦ ?_, condDistrib_ae_eq_of_measure_eq_compProd₀ hX hY κ⟩
   rw [Measure.compProd_congr h.symm, compProd_map_condDistrib hY]
 
+lemma condDistrib_comp' (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
+    {f : Ω → Ω'} (hf : Measurable f) :
+    condDistrib (f ∘ Y) X μ =ᵐ[μ.map X] (condDistrib Y X μ).map f := by
+  refine condDistrib_ae_eq_of_measure_eq_compProd₀ hX (by fun_prop) _ ?_
+  calc μ.map (fun x ↦ (X x, (f ∘ Y) x))
+  _ = (μ.map (fun x ↦ (X x, Y x))).map (Prod.map id f) := by
+    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
+    rfl
+  _ = (μ.map X ⊗ₘ condDistrib Y X μ).map (Prod.map id f) := by
+    rw [compProd_map_condDistrib hY]
+  _ = μ.map X ⊗ₘ (condDistrib Y X μ).map f := by
+    rw [Measure.compProd_eq_comp_prod, ← Measure.deterministic_comp_eq_map (by fun_prop),
+      Measure.compProd_eq_comp_prod, Measure.comp_assoc]
+    congr
+    rw [← Kernel.deterministic_comp_eq_map hf, ← Kernel.parallelComp_comp_copy,
+      ← Kernel.parallelComp_comp_copy, ← Kernel.parallelComp_id_left_comp_parallelComp,
+      ← Kernel.deterministic_parallelComp_deterministic (by fun_prop), Kernel.comp_assoc,
+      ← Kernel.id]
+
 lemma condDistrib_comp (hX : AEMeasurable X μ) {f : β → Ω} (hf : Measurable f) :
     condDistrib (f ∘ X) X μ =ᵐ[μ.map X] Kernel.deterministic f hf := by
   refine condDistrib_ae_eq_of_measure_eq_compProd₀ hX (by fun_prop) _ ?_
@@ -731,6 +753,97 @@ lemma condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft
   rw [h1, h2]
   exact ⟨fun h ↦ by rw [h], fun h ↦ by rw [h1_symm, h1, h2_symm, h2, h]⟩
 
+lemma Measure.snd_compProd_prodMkLeft {α β γ : Type*}
+    {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+    {μ : Measure (α × β)} [SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] :
+    (μ ⊗ₘ (κ.prodMkLeft α)).snd = κ ∘ₘ μ.snd := by
+  ext s hs
+  rw [Measure.snd_apply hs, Measure.compProd_apply (hs.preimage (by fun_prop)),
+    Measure.bind_apply hs (by fun_prop), Measure.snd,
+    lintegral_map (κ.measurable_coe hs) (by fun_prop)]
+  simp only [Kernel.prodMkLeft_apply]
+  congr
+
+lemma Measure.snd_prodAssoc_compProd_prodMkLeft {α β γ : Type*}
+    {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+    {μ : Measure (α × β)} [SFinite μ] {κ : Kernel β γ} [IsSFiniteKernel κ] :
+    (((μ ⊗ₘ (κ.prodMkLeft α))).map MeasurableEquiv.prodAssoc).snd = μ.snd ⊗ₘ κ := by
+  ext s hs
+  rw [Measure.snd_apply hs, Measure.map_apply (by fun_prop) (hs.preimage (by fun_prop)),
+    Measure.compProd_apply, Measure.compProd_apply hs, Measure.snd, lintegral_map _ (by fun_prop)]
+  · simp only [Kernel.prodMkLeft_apply]
+    congr
+  · exact Kernel.measurable_kernel_prodMk_left hs
+  · exact hs.preimage (by fun_prop)
+
+lemma ProbabilityMeasure.ext_iff_coe {α : Type*} {mα : MeasurableSpace α}
+    {μ ν : ProbabilityMeasure α} :
+    μ = ν ↔ (μ : Measure α) = ν := Subtype.ext_iff
+
+lemma FiniteMeasure.ext_iff_coe {α : Type*} {mα : MeasurableSpace α} {μ ν : FiniteMeasure α} :
+    μ = ν ↔ (μ : Measure α) = ν := Subtype.ext_iff
+
+instance : PartialOrder (FiniteMeasure α) :=
+  PartialOrder.lift _ FiniteMeasure.toMeasure_injective
+
+lemma FiniteMeasure.le_iff_coe {μ ν : FiniteMeasure α} :
+    μ ≤ ν ↔ (μ : Measure α) ≤ (ν : Measure α) := Iff.rfl
+
+noncomputable
+instance : Sub (FiniteMeasure α) :=
+  ⟨fun μ ν ↦ ⟨μ.toMeasure - ν.toMeasure, inferInstance⟩⟩
+
+lemma FiniteMeasure.sub_def (μ ν : FiniteMeasure α) :
+    μ - ν = ⟨μ.toMeasure - ν.toMeasure, inferInstance⟩ :=
+  rfl
+
+@[simp, norm_cast]
+theorem FiniteMeasure.toMeasure_sub (μ ν : FiniteMeasure α) : ↑(μ - ν) = (↑μ - ↑ν : Measure α) :=
+  rfl
+
+instance : CanonicallyOrderedAdd (FiniteMeasure α) where
+  exists_add_of_le {μ ν} hμν := by
+    refine ⟨ν - μ, ?_⟩
+    rw [FiniteMeasure.ext_iff_coe]
+    simp only [FiniteMeasure.toMeasure_add, FiniteMeasure.toMeasure_sub]
+    rw [add_comm, Measure.sub_add_cancel_of_le hμν]
+  le_self_add μ ν := by
+    simp only [FiniteMeasure.le_iff_coe, FiniteMeasure.toMeasure_add]
+    exact Measure.le_add_right le_rfl
+
+instance : OrderedSub (FiniteMeasure α) where
+  tsub_le_iff_right μ ν ξ := by
+    simp only [FiniteMeasure.le_iff_coe, FiniteMeasure.toMeasure_sub, FiniteMeasure.toMeasure_add]
+    exact Measure.sub_le_iff_add
+
+lemma Kernel.prodMkLeft_ae_eq_iff [MeasurableSpace.CountableOrCountablyGenerated α β]
+    {κ η : Kernel α β} [IsFiniteKernel κ] [IsFiniteKernel η]
+    {μ : Measure (γ × α)} :
+    κ.prodMkLeft γ =ᵐ[μ] η.prodMkLeft γ ↔ κ =ᵐ[μ.snd] η := by
+  rw [Measure.snd, Filter.EventuallyEq, Filter.EventuallyEq, ae_map_iff (by fun_prop)]
+  · simp
+  · classical
+    exact Kernel.measurableSet_eq κ η
+
+omit [Nonempty Ω'] in
+lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft
+    [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty β]
+    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) {η : Kernel Ω' Ω}
+    [IsMarkovKernel η]
+    (h : condDistrib Y (fun ω ↦ (X ω, Z ω)) μ =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] η.prodMkLeft _) :
+    Y ⟂ᵢ[Z, hZ; μ] X := by
+  have hη_eq : condDistrib Y Z μ =ᵐ[μ.map Z] η := by
+    rw [condDistrib_ae_eq_iff_measure_eq_compProd₀ (by fun_prop) (by fun_prop)] at h ⊢
+    have h_snd : μ.map Z = (μ.map (fun ω ↦ (X ω, Z ω))).snd := by
+      rw [Measure.snd_map_prodMk hX]
+    rw [h_snd, ← Measure.snd_prodAssoc_compProd_prodMkLeft, ← h,
+      Measure.map_map (by fun_prop) (by fun_prop), Measure.snd_map_prodMk (by fun_prop)]
+    congr
+  rw [condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft hX hY hZ]
+  refine h.trans ?_
+  rw [Kernel.prodMkLeft_ae_eq_iff, Measure.snd_map_prodMk (by fun_prop)]
+  exact hη_eq.symm
+
 end CondDistrib
 
 section Cond
diff --git a/LeanBandits/ForMathlib/KernelSub.lean b/LeanBandits/ForMathlib/KernelSub.lean
new file mode 100644
index 00000000..16e5886d
--- /dev/null
+++ b/LeanBandits/ForMathlib/KernelSub.lean
@@ -0,0 +1,265 @@
+/-
+Copyright (c) 2025 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+import Mathlib.Probability.Kernel.RadonNikodym
+
+/-!
+# Kernels substraction
+
+-/
+
+open MeasureTheory MeasurableSpace
+open scoped ENNReal
+
+namespace MeasureTheory.Measure
+
+variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν ξ : Measure α}
+
+lemma sub_le_iff_add_of_le [IsFiniteMeasure ν] (h_le : ν ≤ μ) : μ - ν ≤ ξ ↔ μ ≤ ξ + ν := by
+  refine ⟨fun h ↦ ?_, Measure.sub_le_of_le_add⟩
+  rw [Measure.le_iff] at h ⊢
+  intro s hs
+  specialize h s hs
+  simp only [Measure.coe_add, Pi.add_apply]
+  rwa [Measure.sub_apply hs h_le, tsub_le_iff_right] at h
+
+lemma sub_le_iff_add [IsFiniteMeasure μ] [IsFiniteMeasure ν] : μ - ν ≤ ξ ↔ μ ≤ ξ + ν := by
+  refine ⟨fun h ↦ ?_, Measure.sub_le_of_le_add⟩
+  obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν
+  suffices μ.restrict s ≤ ξ.restrict s + ν.restrict s
+      ∧ μ.restrict sᶜ ≤ ξ.restrict sᶜ + ν.restrict sᶜ by
+    have h_eq_restrict (μ : Measure α) : μ = μ.restrict s + μ.restrict sᶜ := by
+      rw [Measure.restrict_add_restrict_compl hs.measurableSet]
+    rw [h_eq_restrict μ, h_eq_restrict ξ, h_eq_restrict ν]
+    suffices μ.restrict s + μ.restrict sᶜ
+        ≤ ξ.restrict s + ν.restrict s + (ξ.restrict sᶜ + ν.restrict sᶜ) by
+      refine this.trans_eq ?_
+      abel
+    gcongr
+    · exact this.1
+    · exact this.2
+  constructor
+  · have h_le := hs.le_on
+    refine h_le.trans ?_
+    exact Measure.le_add_left le_rfl
+  · have h_le := hs.ge_on_compl
+    have h' : μ.restrict sᶜ - ν.restrict sᶜ ≤ ξ.restrict sᶜ := by
+      rw [← Measure.restrict_sub_eq_restrict_sub_restrict hs.measurableSet.compl]
+      exact Measure.restrict_mono subset_rfl h
+    exact (Measure.sub_le_iff_add_of_le h_le).mp h'
+
+lemma add_sub_of_mutuallySingular (h : μ ⟂ₘ ξ) : μ + (ν - ξ) = μ + ν - ξ := by
+  let s := h.nullSet
+  have hs : MeasurableSet s := h.measurableSet_nullSet
+  suffices μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
+      ∧ μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ by
+    calc μ + (ν - ξ)
+    _ = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ := by
+      rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
+    _ = μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) := by abel
+    _ = (μ.restrict s + ν.restrict s - ξ.restrict s) +
+        (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) := by rw [this.1, this.2]
+    _ = (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ := by
+        simp [restrict_sub_eq_restrict_sub_restrict hs,
+          restrict_sub_eq_restrict_sub_restrict hs.compl]
+    _ = μ + ν - ξ := by rw [restrict_add_restrict_compl hs]
+  constructor
+  · rw [h.restrict_nullSet, restrict_sub_eq_restrict_sub_restrict hs]
+    simp
+  · rw [restrict_sub_eq_restrict_sub_restrict hs.compl, h.restrict_compl_nullSet]
+    simp
+
+lemma withDensity_sub_aux {f g : α → ℝ≥0∞} [IsFiniteMeasure (μ.withDensity g)]
+    (hg : Measurable g) (hgf : g ≤ᵐ[μ] f) :
+    (μ.withDensity f - μ.withDensity g) = μ.withDensity (f - g) := by
+  refine le_antisymm ?_ ?_
+  · refine sub_le_of_le_add ?_
+    rw [← withDensity_add_right _ hg]
+    refine withDensity_mono (ae_of_all _ fun x ↦ ?_)
+    simp only [Pi.add_apply, Pi.sub_apply]
+    exact le_tsub_add
+  · rw [sub_def, le_sInf_iff]
+    intro ξ hξ
+    simp only [Set.mem_setOf_eq] at hξ
+    rw [le_iff] at hξ ⊢
+    intro s hs
+    specialize hξ s hs
+    simp only [coe_add, Pi.add_apply] at hξ
+    simp_rw [withDensity_apply _ hs] at hξ ⊢
+    simp only [Pi.sub_apply]
+    rw [lintegral_sub hg]
+    · rwa [tsub_le_iff_right]
+    · rw [← withDensity_apply _ hs]
+      simp
+    · exact ae_restrict_of_ae hgf
+
+lemma withDensity_sub {f g : α → ℝ≥0∞} [IsFiniteMeasure (μ.withDensity g)]
+    (hf : Measurable f) (hg : Measurable g) :
+    (μ.withDensity f - μ.withDensity g) = μ.withDensity (f - g) := by
+  refine le_antisymm ?_ ?_
+  · refine sub_le_of_le_add ?_
+    rw [← withDensity_add_right _ hg]
+    refine withDensity_mono (ae_of_all _ fun x ↦ ?_)
+    simp only [Pi.add_apply, Pi.sub_apply]
+    exact le_tsub_add
+  · let t := {x | f x ≤ g x}
+    have ht : MeasurableSet t := measurableSet_le hf hg
+    rw [← restrict_add_restrict_compl (μ := μ.withDensity (f - g)) ht,
+      ← restrict_add_restrict_compl (μ := μ.withDensity f - μ.withDensity g) ht]
+    have h_zero : (μ.withDensity (f - g)).restrict t = 0 := by
+      simp only [restrict_eq_zero]
+      rw [withDensity_apply _ ht, lintegral_eq_zero_iff (by fun_prop)]
+      refine ae_restrict_of_forall_mem ht fun x hx ↦ ?_
+      simpa [tsub_eq_zero_iff_le]
+    rw [h_zero, zero_add]
+    suffices (μ.withDensity (f - g)).restrict tᶜ
+        ≤ (μ.withDensity f - μ.withDensity g).restrict tᶜ by
+      refine this.trans ?_
+      exact Measure.le_add_left le_rfl
+    rw [restrict_sub_eq_restrict_sub_restrict ht.compl]
+    simp_rw [restrict_withDensity ht.compl]
+    have : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g) := by
+      rw [← restrict_withDensity ht.compl]
+      infer_instance
+    rw [withDensity_sub_aux hg]
+    refine ae_restrict_of_forall_mem ht.compl fun x hx ↦ ?_
+    simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le, t] at hx
+    exact hx.le
+
+lemma sub_apply_eq_rnDeriv_add_singularPart [IsFiniteMeasure μ] [IsFiniteMeasure ν] (s : Set α) :
+    (μ - ν) s = ν.withDensity (fun a ↦ μ.rnDeriv ν a - 1) s + μ.singularPart ν s := by
+  have hμ : μ = ν.withDensity (fun a ↦ μ.rnDeriv ν a) + μ.singularPart ν := by
+    rw [rnDeriv_add_singularPart]
+  have hν : ν = ν.withDensity 1 := by rw [withDensity_one]
+  conv_lhs => rw [hν, hμ, add_comm _ (μ.singularPart ν)]
+  rw [← add_sub_of_mutuallySingular]
+  swap
+  · simp only [withDensity_one]
+    exact mutuallySingular_singularPart μ ν
+  simp only [coe_add, Pi.add_apply]
+  have : IsFiniteMeasure (ν.withDensity 1) := by simp only [withDensity_one]; infer_instance
+  rw [add_comm, withDensity_sub (by fun_prop) (by fun_prop)]
+  congr
+
+end MeasureTheory.Measure
+
+namespace ProbabilityTheory.Kernel
+
+variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
+  [CountableOrCountablyGenerated α β] {κ η : Kernel α β}
+
+noncomputable
+instance [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] :
+    Sub (Kernel α β) where
+  sub κ η := if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
+    then
+      have := h.1
+      have := h.2
+      η.withDensity (fun a ↦ κ.rnDeriv η a - 1) + κ.singularPart η
+    else 0
+
+lemma sub_def [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] :
+    κ - η = if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
+    then
+      have := h.1
+      have := h.2
+      η.withDensity (fun a ↦ κ.rnDeriv η a - 1) + κ.singularPart η
+    else 0 :=
+  rfl
+
+@[simp]
+lemma sub_of_not_isSFiniteKernel_left [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
+    (h : ¬IsSFiniteKernel κ) : κ - η = 0 := by simp [sub_def, h]
+
+@[simp]
+lemma sub_of_not_isSFiniteKernel_right [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
+    (h : ¬IsSFiniteKernel η) : κ - η = 0 := by simp [sub_def, h]
+
+lemma sub_of_isSFiniteKernel [IsSFiniteKernel κ] [IsSFiniteKernel η]
+    [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] :
+    κ - η = η.withDensity (fun a ↦ κ.rnDeriv η a - 1) + κ.singularPart η := by
+  rw [sub_def, dif_pos]
+  exact ⟨inferInstance, inferInstance⟩
+
+-- todo name
+lemma sub_apply_eq_rnDeriv_add_singularPart [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
+    [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) :
+    (κ - η) a = η.withDensity (fun a ↦ κ.rnDeriv η a - 1) a + κ.singularPart η a := by
+  rw [sub_of_isSFiniteKernel]
+  rfl
+
+lemma sub_apply [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ]
+    [IsFiniteKernel η] (a : α) :
+    (κ - η) a = κ a - η a := by
+  ext s hs
+  rw [sub_apply_eq_rnDeriv_add_singularPart, Kernel.withDensity_apply _ (by fun_prop),
+    Kernel.singularPart_eq_singularPart_measure, Measure.sub_apply_eq_rnDeriv_add_singularPart _]
+  simp only [Measure.coe_add, Pi.add_apply]
+  congr 2
+  refine MeasureTheory.withDensity_congr_ae ?_
+  filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb
+  simp [← hb]
+
+omit [CountableOrCountablyGenerated α β] in
+lemma le_iff (κ η : Kernel α β) : κ ≤ η ↔ ∀ a, κ a ≤ η a := Iff.rfl
+
+lemma sub_le_self [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ]
+    [IsFiniteKernel η] :
+    κ - η ≤ κ := by
+  rw [le_iff]
+  intro a
+  rw [sub_apply]
+  exact Measure.sub_le
+
+instance [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
+    [IsFiniteKernel κ] [IsFiniteKernel η] : IsFiniteKernel (κ - η) :=
+  isFiniteKernel_of_le sub_le_self
+
+lemma sub_apply_eq_zero_iff_le [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
+    [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) : (κ - η) a = 0 ↔ κ a ≤ η a := by
+  simp_rw [sub_apply_eq_rnDeriv_add_singularPart,
+    add_eq_zero_iff_of_nonneg (Measure.zero_le _) (Measure.zero_le _)]
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · rw [Kernel.withDensity_apply _ (by fun_prop), withDensity_eq_zero_iff (by fun_prop)] at h
+    rw [singularPart_eq_zero_iff_absolutelyContinuous κ η a] at h
+    rw [← Measure.rnDeriv_le_one_iff_le h.2]
+    filter_upwards [h.1, rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb1 hb2
+    rw [← hb2]
+    simp only [Pi.sub_apply, Pi.one_apply, Pi.zero_apply] at hb1
+    rwa [tsub_eq_zero_iff_le] at hb1
+  · rw [(singularPart_eq_zero_iff_absolutelyContinuous κ η a).mpr
+        (Measure.absolutelyContinuous_of_le h)]
+    rw [Kernel.withDensity_apply _ (by fun_prop), withDensity_eq_zero_iff (by fun_prop)]
+    simp only [and_true]
+    suffices κ.rnDeriv η a ≤ᵐ[η a] 1 by
+      filter_upwards [this] with b hb
+      simpa [tsub_eq_zero_iff_le] using hb
+    filter_upwards [Measure.rnDeriv_le_one_of_le h,
+      rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb1 hb2
+    rwa [hb2]
+
+lemma sub_eq_zero_iff_le [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
+    [IsFiniteKernel κ] [IsFiniteKernel η] : κ - η = 0 ↔ κ ≤ η := by
+  simp [Kernel.ext_iff, le_iff, sub_apply_eq_zero_iff_le]
+
+lemma measurableSet_eq_zero (κ : Kernel α β) [IsFiniteKernel κ] :
+    MeasurableSet {a | κ a = 0} := by
+  have h_sing : {a | κ a = 0} = {a | κ a ⟂ₘ κ a} := by ext; simp
+  rw [h_sing]
+  exact measurableSet_mutuallySingular κ κ
+
+lemma measurableSet_eq [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
+    (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
+    MeasurableSet {a | κ a = η a} := by
+  have h_sub : {a | κ a = η a} = {a | (κ - η) a = 0} ∩ {a | (η - κ) a = 0} := by
+    ext1 a
+    simp only [Set.mem_setOf_eq, Set.mem_inter_iff, sub_apply_eq_zero_iff_le]
+    exact ⟨fun h ↦ by simp [h], fun h ↦ le_antisymm h.1 h.2⟩
+  rw [h_sub]
+  refine MeasurableSet.inter ?_ ?_
+  · exact measurableSet_eq_zero _
+  · exact measurableSet_eq_zero _
+
+end ProbabilityTheory.Kernel
diff --git a/LeanBandits/ForMathlib/Traj.lean b/LeanBandits/ForMathlib/Traj.lean
index f8ee9d34..c50d7e81 100644
--- a/LeanBandits/ForMathlib/Traj.lean
+++ b/LeanBandits/ForMathlib/Traj.lean
@@ -84,4 +84,16 @@ lemma condDistrib_trajMeasure_ae_eq_kernel {a : ℕ}
   apply condDistrib_ae_eq_of_measure_eq_compProd₀ (by measurability) (by measurability)
   exact trajMeasure_map_frestrictLe_compProd_kernel_eq_trajMeasure_map.symm
 
+lemma traj_zero_map_eval_zero :
+    (Kernel.traj κ 0).map (fun h ↦ h 0)
+      = Kernel.deterministic (MeasurableEquiv.piIicZero X)
+        (MeasurableEquiv.piIicZero X).measurable := by
+  suffices (Kernel.traj κ 0).map (fun h ↦ h 0) = (Kernel.partialTraj κ 0 0).map
+      (MeasurableEquiv.piIicZero X) by
+    rwa [Kernel.partialTraj_zero,
+      Kernel.deterministic_map _ (MeasurableEquiv.piIicZero X).measurable] at this
+  rw [← Kernel.traj_map_frestrictLe, ← Kernel.map_comp_right _ (by fun_prop) (by fun_prop)]
+  congr with h
+  sorry
+
 end ProbabilityTheory.Kernel
diff --git a/LeanBandits/RewardByCountMeasure.lean b/LeanBandits/RewardByCountMeasure.lean
index cb581c7b..a03533cd 100644
--- a/LeanBandits/RewardByCountMeasure.lean
+++ b/LeanBandits/RewardByCountMeasure.lean
@@ -9,7 +9,7 @@ import LeanBandits.Regret
 /-! # Laws of `stepsUntil` and `rewardByCount`
 -/
 
-open MeasureTheory ProbabilityTheory Finset
+open MeasureTheory ProbabilityTheory Finset Learning
 open scoped ENNReal NNReal
 
 namespace Bandits
@@ -102,7 +102,7 @@ notation "𝓛[" Y " | " X " ← " x "; " μ "]" => Measure.map Y (μ[|X ⁻¹'
 notation "𝓛[" Y " | " X "; " μ "]" => condDistrib Y X μ
 
 omit [DecidableEq α] [MeasurableSingletonClass α] in
-lemma condDistrib_reward' [StandardBorelSpace α] [Nonempty α] (n : ℕ) :
+lemma condDistrib_reward'' [StandardBorelSpace α] [Nonempty α] (n : ℕ) :
     𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; Bandit.measure alg ν]
       =ᵐ[(Bandit.measure alg ν).map (fun ω ↦ arm n ω.1)] ν := by
   let μ := Bandit.measure alg ν
@@ -127,7 +127,7 @@ lemma reward_cond_arm [StandardBorelSpace α] [Nonempty α] [Countable α] (a :
     𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1 ← a; Bandit.measure alg ν] = ν a := by
   let μ := Bandit.measure alg ν
   have h_ra : 𝓛[fun ω ↦ reward n ω.1 | fun ω ↦ arm n ω.1; μ] =ᵐ[μ.map (fun ω ↦ arm n ω.1)] ν :=
-    condDistrib_reward' n
+    condDistrib_reward'' n
   have h_eq := condDistrib_ae_eq_cond (μ := μ)
     (X := fun ω ↦ arm n ω.1) (Y := fun ω ↦ reward n ω.1) (by fun_prop) (by fun_prop)
   rw [Filter.EventuallyEq, ae_iff_of_countable] at h_ra h_eq
diff --git a/LeanBandits/UCB.lean b/LeanBandits/UCB.lean
index 3ee285ef..b0db6429 100644
--- a/LeanBandits/UCB.lean
+++ b/LeanBandits/UCB.lean
@@ -11,7 +11,7 @@ import LeanBandits.Regret
 
 -/
 
-open MeasureTheory ProbabilityTheory Filter Real Finset
+open MeasureTheory ProbabilityTheory Filter Real Finset Learning
 
 open scoped ENNReal NNReal
 
diff --git a/blueprint/lean_decls b/blueprint/lean_decls
index 4f0cd71a..fa693245 100644
--- a/blueprint/lean_decls
+++ b/blueprint/lean_decls
@@ -1,4 +1,12 @@
-Bandits.Algorithm
+Learning.Algorithm
+Learning.Environment
+ProbabilityTheory.Kernel.traj
+ProbabilityTheory.Kernel.trajMeasure
+ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel
+Learning.condDistrib_action
+Learning.condDistrib_reward
+Learning.hasLaw_action_zero
+Learning.condDistrib_reward_zero
 Bandits.Bandit.measure
 Bandits.arm
 Bandits.reward
diff --git a/blueprint/src/biblio.bib b/blueprint/src/biblio.bib
new file mode 100644
index 00000000..82ef848f
--- /dev/null
+++ b/blueprint/src/biblio.bib
@@ -0,0 +1,271 @@
+@book{bogachev2007measure,
+  title     = {Measure theory},
+  author    = {V. I. Bogachev and M. A. S. Ruas},
+  volume    = {1},
+  year      = {2007},
+  publisher = {Springer}
+}
+
+@book{Billingsley1995,
+  author    = {Billingsley, P.},
+  title     = {{Probability and Measure. 3rd ed.}},
+  publisher = {{Wiley Series in
+               Probability and Statistics}},
+  year      = 1995,
+  keywords  = {{measure theory; probability theory; stochastic processes}}
+}
+
+@inproceedings{ying2023formalization,
+  title     = {A Formalization of {D}oob’s Martingale Convergence Theorems in mathlib},
+  author    = {K. Ying and R. Degenne},
+  booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+  pages     = {334--347},
+  year      = {2023}
+}
+
+@article{lean,
+  author     = {Ebner, Gabriel and Ullrich, Sebastian and Roesch, Jared and Avigad, Jeremy and de Moura, Leonardo},
+  title      = {A {M}etaprogramming {F}ramework for {F}ormal {V}erification},
+  year       = {2017},
+  issue_date = {September 2017},
+  publisher  = {Association for Computing Machinery},
+  address    = {New York, NY, USA},
+  volume     = {1},
+  number     = {ICFP},
+  url        = {https://doi.org/10.1145/3110278},
+  doi        = {10.1145/3110278},
+  abstract   = {We describe the metaprogramming framework currently used in Lean, an interactive theorem prover based on dependent type theory. This framework extends Lean's object language with an API to some of Lean's internal structures and procedures, and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our implementation is performant, and that it provides a convenient and flexible way of writing not only small-scale interactive tactics, but also more substantial kinds of automation.},
+  journal    = {Proc. ACM Program. Lang.},
+  month      = {aug},
+  articleno  = {34},
+  numpages   = {29},
+  keywords   = {tactic language, theorem proving, dependent type theory, metaprogramming}
+}
+
+@inproceedings{moura2021lean,
+  title={The lean 4 theorem prover and programming language},
+  author={Moura, Leonardo de and Ullrich, Sebastian},
+  booktitle={International Conference on Automated Deduction},
+  pages={625--635},
+  year={2021},
+  organization={Springer}
+}
+
+@inproceedings{mathlib,
+  author     = {{\ignorespaces The} {mathlib Community}},
+  booktitle  = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+  collection = {POPL '20},
+  doi        = {10.1145/3372885.3373824},
+  month      = jan,
+  year       = {2020},
+  title      = {The {L}ean {M}athematical {L}ibrary},
+  publisher  = {Association for Computing Machinery},
+  url        = {https://doi.org/10.1145/3372885.3373824},
+  doi        = {10.1145/3372885.3373824},
+  abstract   = {This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently typed foundations, focus on classical mathematics, extensive hierarchy of structures, use of large- and small-scale automation, and distributed organization. We explain the architecture and design decisions of the library and the social organization that has led to its development.},
+  booktitle  = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+  pages      = {367–381},
+  numpages   = {15},
+  keywords   = {formal library, Lean, formal proof, mathlib},
+  location   = {New Orleans, LA, USA},
+  series     = {CPP 2020}
+}
+
+@book{kallenberg2021,
+  author    = {Kallenberg, Olav},
+  title     = {Foundations of modern probability},
+  series    = {Probability Theory and Stochastic Modelling},
+  volume    = {99},
+  publisher = {Springer Nature Switzerland},
+  edition   = {Third Edition},
+  year      = {2021},
+  pages     = {193},
+  isbn      = {978-3-030-61870-4; 978-3-030-61871-1},
+  doi       = {10.1007/978-3-030-61871-1},
+  url       = {https://doi.org/10.1007/978-3-030-61871-1}
+}
+
+@article{Kolmogorov_Chentsov-AFP,
+  author  = {Christian Pardillo-Laursen and Simon Foster},
+  title   = {The Kolmogorov-Chentsov theorem},
+  journal = {Archive of Formal Proofs},
+  month   = {April},
+  year    = {2025},
+  note    = {\url{https://isa-afp.org/entries/Kolmogorov_Chentsov.html},
+             Formal proof development},
+  issn    = {2150-914x}
+}
+
+@misc{Immler2012,
+  author  = {Immler, F.},
+  title   = {Generic
+             Construction of Probability Spaces for Paths of Stochastic Processes in Isabelle/HOL},
+  journal = {Master’s Thesis in Informatik, TU Munich},
+  year    = {2012},
+  url     = {https://saloranta.de/immler/fabian/mastersthesis/thesis.pdf}
+}
+
+@misc{defaultValues,
+  author  = {Buzzard, Kevin},
+  title   = {Division by zero in type theory: A FAQ},
+  year    = {2020},
+  url     = {https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/},
+  note    = {Accessed: 2025-09-22}
+}
+
+@article{holzl2017markov,
+  title     = {Markov chains and Markov decision processes in Isabelle/HOL},
+  author    = {H{\"o}lzl, J.},
+  journal   = {Journal of Automated Reasoning},
+  volume    = {59},
+  number    = {3},
+  pages     = {345--387},
+  year      = {2017},
+  publisher = {Springer}
+}
+
+@software{Monticone_LeanProject_2025,
+  abstract    = {A template for blueprint-driven formalization projects in Lean.},
+  author      = {Monticone, Pietro},
+  institution = {University of Trento},
+  keywords    = {Lean4, Project Management, Formal Methods, Formal Verification, Theorem Proving, Interactive Theorem Proving, Proof Assistant, Mathematical Formalization, Formal Mathematics, Blueprint, Documentation, Template, Dependency Management, Continuous Integration, Automated Testing, Type Theory, Constructive Mathematics, Computer-Assisted Proof, Mathematical Software, Research Software Engineering},
+  license     = {Apache License 2.0},
+  title       = {LeanProject},
+  year        = {2025}
+}
+
+@software{Anderson_Formalization_of_the_2023,
+author = {Anderson, Aaron and Bakšys, Mantas and Bayer, Jonas and Collares, Mauricio and Degenne, Rémy and Dillies, Yaël and Eltschig, Ben and Gouëzel, Sébastien and Kytölä, Kalle and Lewis, Rob and Lez, Paul and Lorenzo, Luccioli and Macbeth, Heather and Massot, Patrick and Mellendijk, Arend and Miller, Kyle and Monticone, Pietro and Morrison, Kim and Nash, Oliver and Song, Utensil and Tao, Terence and van Doorn, Floris and Wilshaw, Sky and Wu, Lawrence},
+month = nov,
+title = {{Formalization of the Polynomial Freiman-Ruzsa Conjecture of Marton}},
+url = {https://github.com/teorth/pfr},
+version = {0.1.0},
+year = {2023}
+}
+
+@article{gowers2025conjecture,
+  title={On a conjecture of Marton},
+  author={Gowers, William Timothy and Green, Ben and Manners, Freddie and Tao, Terence},
+  journal={Annals of Mathematics},
+  volume={201},
+  number={2},
+  pages={515--549},
+  year={2025},
+}
+
+@article{faden1985existence,
+  title={The existence of regular conditional probabilities: necessary and sufficient conditions},
+  author={Faden, Arnold M},
+  journal={The Annals of Probability},
+  pages={288--298},
+  year={1985},
+  publisher={JSTOR}
+}
+
+@article{marion2025formalization,
+  title={A Formalization of the Ionescu-Tulcea Theorem in Mathlib},
+  author={Marion, Etienne},
+  journal={arXiv preprint arXiv:2506.18616},
+  year={2025}
+}
+
+@software{TestingLowerBounds,
+  author      = {Luccioli, Lorenzo and Degenne, Rémy},
+  title       = {TestingLowerBounds},
+  year        = {2024},
+  url         = {https://github.com/RemyDegenne/testing-lower-bounds}
+}
+
+@inproceedings{gouezel2022formalization,
+  title={A formalization of the change of variables formula for integrals in mathlib},
+  author={Gou{\"e}zel, S{\'e}bastien},
+  booktitle={International Conference on Intelligent Computer Mathematics},
+  pages={3--18},
+  year={2022},
+  organization={Springer}
+}
+
+@article{fritz2020synthetic,
+  title={A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics},
+  author={Fritz, Tobias},
+  journal={Advances in Mathematics},
+  volume={370},
+  pages={107239},
+  year={2020},
+  publisher={Elsevier}
+}
+
+@article{forre2021transitional,
+  title={Transitional conditional independence},
+  author={Forr{\'e}, Patrick},
+  journal={arXiv preprint arXiv:2104.11547},
+  year={2021}
+}
+
+@book{vershynin2018high,
+  title={High-dimensional probability: An introduction with applications in data science},
+  author={Vershynin, Roman},
+  volume={47},
+  year={2018},
+  publisher={Cambridge university press}
+}
+
+@article{hoeffding1963probability,
+  title={Probability inequalities for sums of bounded random variables},
+  author={Hoeffding, Wassily},
+  journal={Journal of the American statistical association},
+  volume={58},
+  number={301},
+  pages={13--30},
+  year={1963},
+  publisher={Taylor \& Francis}
+}
+
+@inproceedings{clerc2017pointless,
+  title={Pointless learning},
+  author={Clerc, Florence and Danos, Vincent and Dahlqvist, Fredrik and Garnier, Ilias},
+  booktitle={International conference on foundations of software science and computation structures},
+  pages={355--369},
+  year={2017},
+  organization={Springer}
+}
+
+@book{polyanskiy2025information,
+  title={Information theory: From coding to learning},
+  author={Polyanskiy, Yury and Wu, Yihong},
+  year={2025},
+  publisher={Cambridge university press}
+}
+
+@article{vakar2018s,
+  title={On s-finite measures and kernels},
+  author={V{\'a}k{\'a}r, Matthijs and Ong, Luke},
+  journal={arXiv preprint arXiv:1810.01837},
+  year={2018}
+}
+
+@article{affeldt2025semantics,
+  title={Semantics of Probabilistic Programs using s-Finite Kernels in Dependent Type Theory},
+  author={Affeldt, Reynald and Cohen, Cyril and Saito, Ayumu},
+  journal={ACM Transactions on Probabilistic Machine Learning},
+  year={2025},
+  publisher={ACM New York, NY}
+}
+
+@article{staton2020probabilistic,
+  title={Probabilistic programs as measures},
+  author={Staton, Sam},
+  journal={Foundations of Probabilistic Programming},
+  pages={43},
+  year={2020},
+  publisher={Cambridge University Press}
+}
+
+@inproceedings{hirata2023semantic,
+  title={Semantic foundations of higher-order probabilistic programs in Isabelle/HOL},
+  author={Hirata, Michikazu and Minamide, Yasuhiko and Sato, Tetsuya},
+  booktitle={14th International Conference on Interactive Theorem Proving (ITP 2023)},
+  pages={18--1},
+  year={2023},
+  organization={Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik}
+}
diff --git a/blueprint/src/chapters/algorithm.tex b/blueprint/src/chapters/algorithm.tex
new file mode 100644
index 00000000..000a5f16
--- /dev/null
+++ b/blueprint/src/chapters/algorithm.tex
@@ -0,0 +1,189 @@
+\chapter{Iterative stochastic algorithms}
+
+
+\begin{definition}[Algorithm]\label{def:algorithm}
+  \leanok
+  \lean{Learning.Algorithm}
+A sequential, stochastic algorithm with actions in a measurable space $\mathcal{A}$ and observations in a measurable space $\mathcal{R}$ is described by the following data:
+\begin{itemize}
+  \item for all $t \in \mathbb{N}$, a policy $\pi_t : (\mathcal{A} \times \mathcal{R})^{t+1} \rightsquigarrow \mathcal{A}$, a Markov kernel which gives the distribution of the action of the algorithm at time $t+1$ given the history of previous pulls and observations,
+  \item $P_0 \in \mathcal{P}(\mathcal{A})$, a probability measure that gives the distribution of the first action.
+\end{itemize}
+\end{definition}
+
+After the algorithm takes an action, the environment generates an observation according to a Markov kernel $\nu_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times \mathcal{A} \rightsquigarrow \mathcal{R}$.
+
+\begin{definition}[Environment]\label{def:environment}
+  \leanok
+  \lean{Learning.Environment}
+An environment with which an algorithm interacts is described by the following data:
+\begin{itemize}
+  \item for all $t \in \mathbb{N}$, a feedback $\nu_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times \mathcal{A} \rightsquigarrow \mathcal{R}$, a Markov kernel which gives the distribution of the observation at time $t+1$ given the history of previous pulls and observations, and the action of the algorithm at time $t+1$,
+  \item $\nu'_0 \in \mathcal{A} \rightsquigarrow \mathcal{R}$, a Markov kernel that gives the distribution of the first observation given the first action.
+\end{itemize}
+\end{definition}
+
+Let's detail four examples of interactions between an algorithm and an environment.
+\begin{enumerate}
+  \item \textbf{First order optimization}. The objective of the algorithm is to find the minimum of a function $f : \mathbb{R}^d \to \mathbb{R}$.
+  The action space is $\mathcal{A} = \mathbb{R}^d$ (a point on which the function will be queried) and the observation space is $\mathcal{R} = \mathbb{R} \times \mathbb{R}^d$.
+  The environment is described by a function $g : \mathbb{R}^d \to \mathbb{R} \times \mathbb{R}^d$ such that for all $x \in \mathbb{R}^d$, $g(x) = (f(x), \nabla f(x))$. That is, the kernel $\nu_t$ is deterministic and depends only on the action: it is given by $\nu_t(h_t, x) = \delta_{g(x)}$ (the Dirac measure at $g(x)$).
+  An example of algorithm is gradient descent with fixed step size $\eta > 0$: this is a deterministic algorithm defined by $P_0 = \delta_{x_0}$ for some initial point $x_0 \in \mathbb{R}^d$ and for all $t \in \mathbb{N}$, $\pi_t(h_t) = \delta_{x_{t+1}}$ where $x_{t+1} = x_t - \eta \nabla g_2(x_t)$.
+
+  \item \textbf{Stochastic bandits}. The action space is $\mathcal{A} = [K]$ for some $K \in \mathbb{N}$ (the set of arms) and the observation space is $\mathcal{R} = \mathbb{R}$ (the reward obtained after pulling an arm).
+  The kernel $\nu_t$ is stationary and depends only on the action: there are probability distributions $(P_a)_{a \in [K]}$ such that for all $t \in \mathbb{N}$, for all $h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$, for all $a \in \mathcal{A}$, $\nu_t(h_t, a) = P_a$.
+
+  \item \textbf{Adversarial bandits}. The action space is $\mathcal{A} = [K]$ for some $K \in \mathbb{N}$ (the set of arms) and the observation space is $\mathcal{R} = \mathbb{R}$ (the reward obtained after pulling an arm).
+  The reward kernels are usually taken to be deterministic and in an \emph{oblivious} adversarial bandit they depend only on the time step: there is a sequence of vectors $(r_t)_{t \in \mathbb{N}}$ in $[0,1]^K$ such that for all $t \in \mathbb{N}$, for all $h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$, for all $a \in \mathcal{A}$, $\nu_t(h_t, a) = \delta_{r_{t,a}}$ (the Dirac measure at $r_{t,a}$).
+
+  \item \textbf{Reinforcement learnings in Markov decision processes}.
+  TODO: main feature is that $\mathcal{R} = \mathcal{S} \times \mathbb{R}$ where $\mathcal{S}$ is the state space, and the kernel $\nu_t$ depends on the last state only.
+\end{enumerate}
+
+
+\section{Ionescu-Tulcea theorem}
+
+If we group together the policy of the algorithm and the kernel of the environment at each time step, we get a sequence of Markov kernels $(\kappa_t)_{t \in \mathbb{N}}$, with $\kappa_t : (\mathcal{A} \times \mathcal{R})^{t+1}  \rightsquigarrow (\mathcal{A} \times \mathcal{R})$.
+We will want to make global probabilistic statements about the whole sequence of actions and observations.
+For example, we may want to prove that an optimization algorithm converges to the minimum of a function almost surely.
+For such a statement to make sense, we need a probability space on which the whole sequence of actions and observations is defined as a random variable.
+
+We now abstract that situation and consider a sequence of measurable spaces $(\Omega_t)_{t \in \mathbb{N}}$, a probability measure $\mu$ on $\Omega_0$ and a sequence of Markov kernels $\kappa_t : \prod_{s=0}^t \Omega_s \rightsquigarrow \Omega_{t+1}$.
+The Ionescu-Tulcea theorem builds a probability space from the sequence of kernels and the initial measure.
+
+\begin{theorem}[Ionescu-Tulcea]\label{thm:ionescu-tulcea}
+  \mathlibok
+  \lean{ProbabilityTheory.Kernel.traj}
+Let $(\Omega_t)_{t \in \mathbb{N}}$ be a family of measurable spaces. Let $(\kappa_t)_{t \in \mathbb{N}}$ be a family of Markov kernels such that for any $t$, $\kappa_t$ is a kernel from $\prod_{i=0}^t \Omega_{i}$ to $\Omega_{t+1}$.
+Then there exists a unique Markov kernel $\xi : \Omega_0 \rightsquigarrow \prod_{i = 1}^{\infty} \Omega_{i}$ such that for any $n \ge 1$,
+$\pi_{[1,n]*} \xi = \kappa_0 \otimes \ldots \otimes \kappa_{n-1}$.
+Here $\pi_{[1,n]} : \prod_{i=1}^{\infty} \Omega_i \to \prod_{i=1}^n \Omega_i$ is the projection on the first $n$ coordinates.
+\end{theorem}
+
+\begin{proof}\leanok
+\end{proof}
+
+The Ionescu-Tulcea theorem in Mathlib \cite{marion2025formalization} actually generates kernels $\xi_t : \prod_{s=0}^t \Omega_s \rightsquigarrow \prod_{s=0}^{\infty} \Omega_s$ for any $t$, with the property that the kernels are the identity on the first $t+1$ coordinates.
+
+\begin{definition}\label{def:trajMeasure}
+  \uses{thm:ionescu-tulcea}
+  \leanok
+  \lean{ProbabilityTheory.Kernel.trajMeasure}
+For $\mu \in \mathcal{P}(\Omega_0)$, we call trajectory measure the probability measure $\xi_0 \circ \mu$ on $\Omega_{\mathcal{T}} := \prod_{i=0}^{\infty} \Omega_i$.
+We denote it by $P_{\mathcal{T}}$.
+The $\mathcal{T}$ subscript stands for ``trajectory''.
+\end{definition}
+
+
+\begin{definition}\label{def:history}
+  \mathlibok % no need for a Lean definition
+For $t \in \mathbb{N}$, we denote by $X_t \in \Omega_t$ the random variable describing the time step $t$, and by $H_t \in \prod_{s=0}^t \Omega_s$ the history up to time $t$.
+Formally, these are measurable functions on $\Omega_{\mathcal{T}}$, defined by $X_t(\omega) = \omega_t$ and $H_t(\omega) = (\omega_1, \ldots, \omega_t)$.
+\end{definition}
+
+Note: $(X_t)_{t \in \mathbb{N}}$ is the canonical process on $\Omega_{\mathcal{T}}$. $H_t$ is equal to $\pi_{[0,t]}$.
+
+We now list properties of those random variables that follow from the construction of the trajectory measure.
+
+We write $P[X \mid Y]$ for the conditional distribution of a random variable $X$ given another random variable $Y$ under a probability measure $P$.
+
+\begin{lemma}\label{lem:condDistrib_X_add_one}
+  \uses{def:history, def:trajMeasure}
+  \leanok
+  \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel}
+For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t$.
+\end{lemma}
+
+\begin{proof}\leanok
+This is proved through the defining property of the conditional distribution: it is the almost surely unique Markov kernel $\eta$ such that $((H_t)_* P_{\mathcal{T}}) \otimes \eta = (H_t, X_{t+1})_*P_{\mathcal{T}}$.
+
+TODO: complete proof.
+\end{proof}
+
+
+\begin{lemma}\label{lem:law_X_zero}
+  \uses{def:history, def:trajMeasure}
+The law of $X_0$ under $P_{\mathcal{T}}$ is $\mu$.
+\end{lemma}
+
+\begin{proof}
+
+\end{proof}
+
+
+\paragraph{Case of a composition-product}
+
+We suppose now that $\Omega_t = \mathcal{A}_t \times \mathcal{R}_t$ for some measurable spaces $\mathcal{A}_t$ and $\mathcal{R}_t$, and that for all $t \in \mathbb{N}$, $\kappa_t = \pi_t \otimes \nu_t$ for kernels $\pi_t : \prod_{s=0}^t(\mathcal{A}_s \times \mathcal{R}_s) \rightsquigarrow \mathcal{A}$ and $\nu_t : \prod_{s=0}^t(\mathcal{A}_s \times \mathcal{R}_s) \times \mathcal{A} \rightsquigarrow \mathcal{R}$.
+Likewise, $\mu = \alpha_0 \otimes \nu'_0$ for a probability measure $\alpha_0$ on $\mathcal{A}_0$ and a Markov kernel $\nu'_0 : \mathcal{A}_0 \rightsquigarrow \mathcal{R}_0$.
+That's the case of an algorithm interacting with an environment as described above.
+We write $A_t$ and $R_t$ for the projections of $X_t$ on $\mathcal{A}_t$ and $\mathcal{R}_t$ respectively.
+
+
+\begin{lemma}\label{lem:condDistrib_A_add_one}
+  \uses{def:history, def:trajMeasure, def:algorithm, def:environment}
+  \leanok
+  \lean{Learning.condDistrib_action}
+For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[A_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\pi_t$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:condDistrib_X_add_one}
+By Lemma~\ref{lem:condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t = \pi_t \otimes \nu_t$.
+Since $A_{t+1}$ is the projection of $X_{t+1}$ on $\mathcal{A}_{t+1}$, $P_{\mathcal{T}}\left[A_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to the projection of $\kappa_t$ on $\mathcal{A}_{t+1}$, which is $\pi_t$.
+\end{proof}
+
+
+\begin{lemma}\label{lem:condDistrib_R_add_one}
+  \uses{def:history, def:trajMeasure, def:algorithm, def:environment}
+  \leanok
+  \lean{Learning.condDistrib_reward}
+For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[R_{t+1} \mid H_t, A_{t+1}\right]$ is $((H_t, A_{t+1})_* P_{\mathcal{T}})$-almost surely equal to $\nu_t$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:condDistrib_X_add_one, lem:condDistrib_A_add_one}
+It suffices to show that $((H_t, A_{t+1})_* P_{\mathcal{T}}) \otimes \nu_t = (H_t, A_{t+1}, R_{t+1})_* P_{\mathcal{T}} = (H_t, X_{t+1})_* P_{\mathcal{T}}$.
+By Lemma~\ref{lem:condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t = \pi_t \otimes \nu_t$.
+Thus $((H_t)_* P_{\mathcal{T}}) \otimes (\pi_t \otimes \nu_t) = (H_t, X_{t+1})_* P_{\mathcal{T}}$.
+
+We thus have to prove that $((H_t)_* P_{\mathcal{T}}) \otimes (\pi_t \otimes \nu_t) = ((H_t, A_{t+1})_* P_{\mathcal{T}}) \otimes \nu_t$.
+
+By Lemma~\ref{lem:condDistrib_A_add_one}, $(H_t, A_{t+1})_* P_{\mathcal{T}} = (H_t)_* P_{\mathcal{T}} \otimes \pi_t$, and replacing this in the right-hand side gives the left-hand side (using associativity of the composition-product).
+\end{proof}
+
+
+\begin{lemma}\label{lem:law_A_zero}
+  \uses{def:history, def:trajMeasure, def:algorithm, def:environment}
+  \leanok
+  \lean{Learning.hasLaw_action_zero}
+The law of $A_0$ under $P_{\mathcal{T}}$ is $\alpha_0$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:law_X_zero}
+$X_0$ has law $\mu = \alpha_0 \otimes \nu'_0$. $A_0$ is the projection of $X_0$ on the first space $\mathcal{A}_0$ and $\nu_0'$ is Markov, so $A_0$ has law $\alpha_0$.
+\end{proof}
+
+
+\begin{lemma}\label{lem:condDistrib_R_zero}
+  \uses{def:history, def:trajMeasure, def:algorithm, def:environment}
+  \leanok
+  \lean{Learning.condDistrib_reward_zero}
+The conditional distribution $P_{\mathcal{T}}\left[R_0 \mid A_0\right]$ is $(A_{0*} P_{\mathcal{T}})$-almost surely equal to $\nu'_0$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:law_X_zero}
+To prove almost sure equality, it is enough to prove that $(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left[R_0 \mid A_0\right] = (A_{0*} P_{\mathcal{T}}) \otimes \nu'_0$.
+By definition of the conditional distribution, we have $(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left[R_0 \mid A_0\right] = (A_0, R_0)_* P_{\mathcal{T}} = X_{0*} P_{\mathcal{T}}$.
+By Lemma~\ref{lem:law_X_zero}, $X_{0*} P_{\mathcal{T}} = \mu = \alpha_0 \otimes \nu'_0$.
+By Lemma~\ref{lem:law_A_zero}, $A_{0*} P_{\mathcal{T}} = \alpha_0$.
+Thus the two sides are equal.
+\end{proof}
+
+
+
+
+\section{Independence and Markov property}
+
+The structure of the sequence of kernels $(\kappa_t)_{t \in \mathbb{N}}$ is reflected in independence properties of the sequence of random variables $(X_t)_{t \in \mathbb{N}}$.
diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex
index 41dab130..abb30068 100644
--- a/blueprint/src/chapters/bandit.tex
+++ b/blueprint/src/chapters/bandit.tex
@@ -2,28 +2,18 @@ \chapter{Stochastic multi-armed bandits}
 
 \section{Algorithm, bandit and probability space}
 
-\begin{definition}[Algorithm]\label{def:algorithm}
-  \leanok
-  \lean{Bandits.Algorithm}
-A sequential, stochastic algorithm with actions in a measurable space $\mathcal{A}$ and observations in a measurable space $\mathcal{R}$ is described by the following data:
-\begin{itemize}
-  \item for all $t \in \mathbb{N}$, a policy $\pi_t : (\mathcal{A} \times \mathcal{R})^{t+1} \rightsquigarrow \mathcal{A}$, a Markov kernel which gives the distribution of the arm to pull at time $t+1$ given the history of previous pulls and observations,
-  \item $P_0 \in \mathcal{P}(\mathcal{A})$, a probability measure that gives the distribution of the first arm to pull.
-\end{itemize}
-\end{definition}
-
+A bandit algorithm is an algorithm in the sense of Definition~\ref{def:algorithm}.
+We call the actions \emph{arms} and the observations \emph{rewards}.
 
 The first arm pulled by the algorithm is sampled from $P_0$, the arm pulled at time $1$ is sampled from $\pi_0(H_0)$, where $H_0 \in \mathcal{A} \times \mathcal{R}$ is the data of the first arm pulled and the first observation received, and so on.
 
 
 \begin{definition}[Bandit]\label{def:bandit}
-  \mathlibok
+  \uses{def:environment}
+  \leanok
 A stochastic bandit is simply a reward distribution for each arm: a Markov kernel $\nu : \mathcal{A} \rightsquigarrow \mathbb{R}$, conditional distribution of the rewards given the arm pulled.
 \end{definition}
 
-
-Note: we don't have a Lean definition for a bandit, since it is just a Markov kernel.
-
 An algorithm can interact with a bandit to produce a sequence of arms and rewards: after a time $t$, the history $H_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$ contains the arms pulled and rewards received up to that time,
 \begin{itemize}
   \item the algorithm chooses an arm $A_{t+1}$ sampled according to its policy $\pi_t(H_t)$,
@@ -47,6 +37,7 @@ \section{Algorithm, bandit and probability space}
 The reason for adding the extra stream of rewards is explained in Section~\ref{sec:alt_model}.
 
 \begin{definition}[Arms, rewards and history]\label{def:armAndReward}
+  \uses{def:history}
   \leanok
   \lean{Bandits.arm, Bandits.reward, Bandits.hist}
 For $t \in \mathbb{N}$, we denote by $A_t$ the arm pulled at time $t$ and by $X_t$ the reward received at time $t$.
@@ -112,7 +103,8 @@ \section{Algorithm, bandit and probability space}
 The conditional distribution of the reward $X_t$ given the arm $A_t$ in the bandit probability space $(\Omega, \mathbb{P})$ is $\nu(A_t)$.
 \end{lemma}
 
-\begin{proof}
+\begin{proof}\leanok
+  \uses{lem:condDistrib_R_add_one, lem:condDistrib_R_zero}
 
 \end{proof}
 
@@ -124,7 +116,8 @@ \section{Algorithm, bandit and probability space}
 The law of the arm $A_0$ in the bandit probability space $(\Omega, \mathbb{P})$ is $P_0$.
 \end{lemma}
 
-\begin{proof}
+\begin{proof}\leanok
+  \uses{lem:law_A_zero}
 
 \end{proof}
 
@@ -136,7 +129,8 @@ \section{Algorithm, bandit and probability space}
 The conditional distribution of the arm $A_{t+1}$ given the history $H_t$ in the bandit probability space $(\Omega, \mathbb{P})$ is $\pi_t(H_t)$.
 \end{lemma}
 
-\begin{proof}
+\begin{proof}\leanok
+  \uses{lem:condDistrib_A_add_one}
 
 \end{proof}
 
diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex
index e0c5f9a9..2c69b421 100644
--- a/blueprint/src/content.tex
+++ b/blueprint/src/content.tex
@@ -7,9 +7,13 @@
 % can start with a \section or \chapter for instance.
 
 \input{chapters/intro.tex}
+\input{chapters/algorithm.tex}
 \input{chapters/bandit.tex}
 \input{chapters/concentration.tex}
 \input{chapters/etc.tex}
 \input{chapters/ucb.tex}
 \input{chapters/practicalAlgorithms.tex}
 \input{chapters/sampling.tex}
+
+\bibliographystyle{amsalpha}
+\bibliography{biblio}