diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean
index 64e000e2..7d539fc3 100644
--- a/LeanMachineLearning.lean
+++ b/LeanMachineLearning.lean
@@ -15,6 +15,8 @@ public import LeanMachineLearning.Probability.Independence.CondIndepFun
 public import LeanMachineLearning.Probability.Independence.IndepFun
 public import LeanMachineLearning.Probability.Independence.IndepInfinitePi
 public import LeanMachineLearning.Probability.Integrable
+public import LeanMachineLearning.Probability.Kernel.Basic
+public import LeanMachineLearning.Probability.Kernel.Composition.MapComap
 public import LeanMachineLearning.Probability.Kernel.IonescuTulcea.Traj
 public import LeanMachineLearning.Probability.Kernel.KernelSub
 public import LeanMachineLearning.Probability.Moments.SubGaussian
@@ -22,6 +24,7 @@ public import LeanMachineLearning.SequentialLearning.Algorithm
 public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling
 public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
 public import LeanMachineLearning.SequentialLearning.Deterministic
+public import LeanMachineLearning.SequentialLearning.EvaluationEnv
 public import LeanMachineLearning.SequentialLearning.FiniteActions
 public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
 public import LeanMachineLearning.SequentialLearning.StationaryEnv
diff --git a/LeanMachineLearning/Probability/Kernel/Basic.lean b/LeanMachineLearning/Probability/Kernel/Basic.lean
new file mode 100644
index 00000000..723691fc
--- /dev/null
+++ b/LeanMachineLearning/Probability/Kernel/Basic.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.Probability.Kernel.Basic
+
+@[expose] public section
+
+open MeasureTheory
+
+namespace ProbabilityTheory.Kernel
+
+variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
+
+/-- Two deterministic kernels are equal if and only if their underlying functions are equal. -/
+@[simp]
+lemma deterministic_inj [MeasurableSpace.SeparatesPoints β]
+    {f g : α → β} {hf : Measurable f} {hg : Measurable g} :
+    Kernel.deterministic f hf = Kernel.deterministic g hg ↔ f = g := by
+  simp [Kernel.ext_iff, Kernel.deterministic_apply, dirac_eq_dirac_iff, funext_iff]
+
+end ProbabilityTheory.Kernel
diff --git a/LeanMachineLearning/Probability/Kernel/Composition/MapComap.lean b/LeanMachineLearning/Probability/Kernel/Composition/MapComap.lean
new file mode 100644
index 00000000..093e04dc
--- /dev/null
+++ b/LeanMachineLearning/Probability/Kernel/Composition/MapComap.lean
@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.Probability.Kernel.Composition.MapComap
+
+@[expose] public section
+
+namespace ProbabilityTheory.Kernel
+
+variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+
+@[simp]
+lemma prodMkLeft_inj [h_nonempty : Nonempty γ]
+    (κ ν : Kernel α β) :
+    κ.prodMkLeft γ = ν.prodMkLeft γ ↔ κ = ν := by
+  simp only [Kernel.ext_iff, Kernel.prodMkLeft_apply, Prod.forall]
+  exact ⟨fun h b ↦ h h_nonempty.some b, fun h _ b ↦ h b⟩
+
+@[simp]
+lemma prodMkRight_inj [h_nonempty : Nonempty γ]
+    (κ ν : Kernel α β) :
+    κ.prodMkRight γ = ν.prodMkRight γ ↔ κ = ν := by
+  simp only [Kernel.ext_iff, Kernel.prodMkRight_apply, Prod.forall]
+  exact ⟨fun h a ↦ h a h_nonempty.some, fun h a _ ↦ h a⟩
+
+@[simp]
+lemma prodMkLeft_deterministic {f : α → β} (hf : Measurable f) :
+    (Kernel.deterministic f hf).prodMkLeft γ =
+      Kernel.deterministic (fun p ↦ f p.2) (by fun_prop) := by
+  ext
+  simp [Kernel.deterministic_apply]
+
+@[simp]
+lemma prodMkRight_deterministic {f : α → β} (hf : Measurable f) :
+    (Kernel.deterministic f hf).prodMkRight γ =
+      Kernel.deterministic (fun p ↦ f p.1) (by fun_prop) := by
+  ext
+  simp [Kernel.deterministic_apply]
+
+end ProbabilityTheory.Kernel
diff --git a/LeanMachineLearning/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean
index 3f84fda8..d152e58b 100644
--- a/LeanMachineLearning/SequentialLearning/Deterministic.lean
+++ b/LeanMachineLearning/SequentialLearning/Deterministic.lean
@@ -5,21 +5,36 @@ Authors: Rémy Degenne
 -/
 module
 
+public import LeanMachineLearning.Probability.Kernel.Basic
 public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
 
 /-!
-# Deterministic algorithms
+# Deterministic algorithms and environments
 
 A deterministic algorithm chooses its action in a deterministic way. That is, that action is given
 by a measurable function of the history instead of a general Markov kernel.
-
-We introduce a definition for those algorithms and prove results about the conditional distribution
-of the actions they generate when interacting with an environment.
+Similarly, a deterministic environment gives feedback in a deterministic way.
 
 ## Main definitions
 
-* `detAlgorithm nextAction h_next action0`: a deterministic algorithm that chooses its action
-  according to the measurable function `nextAction` (with proof of measurability `h_next`),
+We introduce two typeclasses `IsDeterministicAlg` and `IsDeterministicEnv` to express that
+an algorithm or an environment is deterministic. We also give definitions for the initial action
+and the next action of a deterministic algorithm, and for the feedback functions of a deterministic
+environment. Finally, we give a construction of a deterministic algorithm and environment from
+measurable functions.
+
+* `IsDeterministicAlg alg`: a typeclass expressing that the algorithm `alg` is deterministic.
+* `IsDeterministicEnv env`: a typeclass expressing that the environment `env` is deterministic.
+* `actionZero alg`: the initial action of a deterministic algorithm `alg`.
+* `nextAction alg n`: the function that gives the next action of a deterministic algorithm `alg`
+  at step `n`, as a function of the history.
+* `feedbackFunZero env`: the function that gives the initial feedback of a deterministic
+  environment `env`.
+* `feedbackFun env n`: the function that gives the feedback of a deterministic environment `env`
+  at step `n`, as a function of the history and the current action.
+
+* `detAlgorithm nextA h_next action0`: a deterministic algorithm that chooses its action
+  according to the measurable function `nextA` (with proof of measurability `h_next`),
   with initial action `action0`.
 
 ## Notes
@@ -38,19 +53,206 @@ namespace Learning
 
 variable {α R : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R}
 
+/-- An algorithm is deterministic if its initial action and subsequent actions are determined by
+measurable functions (and not possibly random kernels). -/
+class IsDeterministicAlg (alg : Algorithm α R) : Prop where
+  exists_action0 : ∃ action0, alg.p0 = Measure.dirac action0
+  exists_nextAction n : ∃ (nextAction : (Iic n → α × R) → α) (h_meas : Measurable nextAction),
+    alg.policy n = Kernel.deterministic nextAction h_meas
+
+/-- The initial action of a deterministic algorithm. -/
+noncomputable
+def actionZero (alg : Algorithm α R) [h_det : IsDeterministicAlg alg] : α :=
+  h_det.exists_action0.choose
+
+/-- The next action of a deterministic algorithm after step `n`. -/
+noncomputable
+def nextAction (alg : Algorithm α R) [h_det : IsDeterministicAlg alg] (n : ℕ) :
+    (Iic n → α × R) → α :=
+  (h_det.exists_nextAction n).choose
+
+@[fun_prop]
+lemma measurable_nextAction (alg : Algorithm α R) [IsDeterministicAlg alg] (n : ℕ) :
+    Measurable (nextAction alg n) :=
+  (IsDeterministicAlg.exists_nextAction n).choose_spec.choose
+
+lemma p0_eq_dirac (alg : Algorithm α R) [h_det : IsDeterministicAlg alg] :
+    alg.p0 = Measure.dirac (actionZero alg) :=
+  h_det.exists_action0.choose_spec
+
+lemma policy_eq_deterministic (alg : Algorithm α R) [h_det : IsDeterministicAlg alg] (n : ℕ) :
+    alg.policy n = Kernel.deterministic (nextAction alg n) (measurable_nextAction alg n) :=
+  (IsDeterministicAlg.exists_nextAction n).choose_spec.choose_spec
+
+namespace IsDeterministicAlg
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
+  [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
+  {alg : Algorithm α R} {env : Environment α R} {P : Measure Ω} [IsFiniteMeasure P]
+  {A : ℕ → Ω → α} {R' : ℕ → Ω → R} {n N : ℕ}
+
+lemma hasLaw_action_zero_of_IsAlgEnvSeqUntil [h_det : IsDeterministicAlg alg]
+    (h : IsAlgEnvSeqUntil A R' alg env P N) :
+    HasLaw (A 0) (Measure.dirac (actionZero alg)) P where
+  aemeasurable := have hA := h.measurable_A; by fun_prop
+  map_eq := (h.hasLaw_action_zero).map_eq.trans (p0_eq_dirac alg)
+
+lemma action_zero_of_IsAlgEnvSeqUntil [h_det : IsDeterministicAlg alg]
+    (h : IsAlgEnvSeqUntil A R' alg env P N) :
+    A 0 =ᵐ[P] fun _ ↦ actionZero alg := by
+  have h_eq : ∀ᵐ x ∂(P.map (A 0)), x = actionZero alg := by
+    simp [(hasLaw_action_zero_of_IsAlgEnvSeqUntil h).map_eq]
+  have hA := h.measurable_A
+  exact ae_of_ae_map (by fun_prop) h_eq
+
+lemma action_ae_eq_of_IsAlgEnvSeqUntil [h_det : IsDeterministicAlg alg]
+    (h : IsAlgEnvSeqUntil A R' alg env P N) (hn : n < N) :
+    A (n + 1) =ᵐ[P] fun ω ↦ nextAction alg n (IsAlgEnvSeq.hist A R' n ω) := by
+  have hA := h.measurable_A
+  have hR' := h.measurable_R
+  have h_eq := (h.hasCondDistrib_action n hn).condDistrib_eq
+  rw [policy_eq_deterministic alg n] at h_eq
+  refine ae_eq_of_condDistrib_eq_deterministic (by fun_prop : Measurable (nextAction alg n))
+    (by fun_prop) (by fun_prop) h_eq
+
+lemma hasLaw_action_zero [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A R' alg env P) :
+    HasLaw (A 0) (Measure.dirac (actionZero alg)) P where
+  aemeasurable := have hA := h.measurable_A; by fun_prop
+  map_eq := (h.hasLaw_action_zero).map_eq.trans (p0_eq_dirac alg)
+
+lemma action_zero_ae_eq [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A R' alg env P) :
+    A 0 =ᵐ[P] fun _ ↦ actionZero alg :=
+  action_zero_of_IsAlgEnvSeqUntil (h.isAlgEnvSeqUntil 0)
+
+lemma action_ae_eq [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A R' alg env P) (n : ℕ) :
+    A (n + 1) =ᵐ[P] fun ω ↦ nextAction alg n (IsAlgEnvSeq.hist A R' n ω) :=
+  action_ae_eq_of_IsAlgEnvSeqUntil (h.isAlgEnvSeqUntil (n + 1)) (by simp)
+
+lemma action_ae_all_eq [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeq A R' alg env P) :
+    ∀ᵐ ω ∂P, A 0 ω = actionZero alg ∧
+      ∀ n, A (n + 1) ω = nextAction alg n (IsAlgEnvSeq.hist A R' n ω) := by
+  rw [eventually_and, ae_all_iff]
+  exact ⟨action_zero_ae_eq h, action_ae_eq h⟩
+
+end IsDeterministicAlg
+
+/-- An environment is deterministic if its initial feedbacks are determined by
+measurable functions (and not possibly random kernels). -/
+class IsDeterministicEnv (env : Environment α R) : Prop where
+  exists_f0 : ∃ (f0 : α → R) (hf0 : Measurable f0), env.ν0 = Kernel.deterministic f0 hf0
+  exists_f : ∀ n, ∃ (f : ((Iic n → α × R) × α) → R) (hf : Measurable f),
+    env.feedback n = Kernel.deterministic f hf
+
+/-- The initial feedback function of a deterministic environment. -/
+noncomputable
+def feedbackFunZero (env : Environment α R) [h_det : IsDeterministicEnv env] : α → R :=
+  h_det.exists_f0.choose
+
+@[fun_prop]
+lemma measurable_feedbackFunZero (env : Environment α R) [IsDeterministicEnv env] :
+    Measurable (feedbackFunZero env) :=
+  (IsDeterministicEnv.exists_f0).choose_spec.choose
+
+lemma ν0_eq_deterministic (env : Environment α R) [IsDeterministicEnv env] :
+    env.ν0 = Kernel.deterministic (feedbackFunZero env) (measurable_feedbackFunZero env) :=
+  (IsDeterministicEnv.exists_f0).choose_spec.choose_spec
+
+/-- The feedback function of a deterministic environment at step `n`. -/
+noncomputable
+def feedbackFun (env : Environment α R) [h_det : IsDeterministicEnv env] (n : ℕ) :
+    ((Iic n → α × R) × α) → R :=
+  (h_det.exists_f n).choose
+
+@[fun_prop]
+lemma measurable_feedbackFun (env : Environment α R) [IsDeterministicEnv env] (n : ℕ) :
+    Measurable (feedbackFun env n) :=
+  (IsDeterministicEnv.exists_f n).choose_spec.choose
+
+lemma feedback_eq_deterministic (env : Environment α R) [IsDeterministicEnv env] (n : ℕ) :
+    env.feedback n = Kernel.deterministic (feedbackFun env n) (measurable_feedbackFun env n) :=
+  (IsDeterministicEnv.exists_f n).choose_spec.choose_spec
+
+namespace IsDeterministicEnv
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
+  [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
+  {alg : Algorithm α R} {env : Environment α R} {P : Measure Ω} [IsFiniteMeasure P]
+  {A : ℕ → Ω → α} {R' : ℕ → Ω → R}
+  {f : (n : ℕ) → ((Iic n → α × R) × α) → R} {hf : ∀ n, Measurable (f n)}
+  {f0 : α → R} {hf0 : Measurable f0}
+
+lemma hasCondDistrib_reward_zero [h_det : IsDeterministicEnv env]
+    (h : IsAlgEnvSeq A R' alg env P) :
+    HasCondDistrib (R' 0) (A 0)
+      (Kernel.deterministic (feedbackFunZero env) (measurable_feedbackFunZero env)) P := by
+  rw [← ν0_eq_deterministic]
+  exact h.hasCondDistrib_reward_zero
+
+lemma hasCondDistrib_reward [h_det : IsDeterministicEnv env]
+    (h : IsAlgEnvSeq A R' alg env P) (n : ℕ) :
+    HasCondDistrib (R' (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A R' n ω, A (n + 1) ω))
+      (Kernel.deterministic (feedbackFun env n) (measurable_feedbackFun env n)) P := by
+  rw [← feedback_eq_deterministic]
+  exact h.hasCondDistrib_reward n
+
+end IsDeterministicEnv
+
+variable {nextA : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextA n)}
+  {action0 : α} {env : Environment α R}
+  {f0 : α → R} {hf0 : Measurable f0}
+  {f : (n : ℕ) → ((Iic n → α × R) × α) → R} {hf : ∀ n, Measurable (f n)}
+
 /-- A deterministic algorithm, which chooses the action given by the function `nextAction`. -/
 @[simps]
 noncomputable
 -- ANCHOR: detAlgorithm
-def detAlgorithm (nextAction : (n : ℕ) → (Iic n → α × R) → α)
-    (h_next : ∀ n, Measurable (nextAction n)) (action0 : α) :
+def detAlgorithm (nextA : (n : ℕ) → (Iic n → α × R) → α)
+    (h_next : ∀ n, Measurable (nextA n)) (action0 : α) :
     Algorithm α R where
-  policy n := Kernel.deterministic (nextAction n) (h_next n)
+  policy n := Kernel.deterministic (nextA n) (h_next n)
   p0 := Measure.dirac action0
 -- ANCHOR_END: detAlgorithm
 
-variable {nextAction : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextAction n)}
-  {action0 : α} {env : Environment α R}
+instance : IsDeterministicAlg (detAlgorithm nextA h_next action0) where
+  exists_action0 := ⟨action0, rfl⟩
+  exists_nextAction n := ⟨nextA n, h_next n, rfl⟩
+
+@[simp]
+lemma actionZero_detAlgorithm [MeasurableSpace.SeparatesPoints α] :
+    actionZero (detAlgorithm nextA h_next action0) = action0 := by
+  have h_eq := p0_eq_dirac (detAlgorithm nextA h_next action0)
+  simp only [detAlgorithm] at h_eq
+  rw [dirac_eq_dirac_iff] at h_eq
+  exact h_eq.symm
+
+@[simp]
+lemma nextAction_detAlgorithm [MeasurableSpace.SeparatesPoints α] (n : ℕ) :
+    nextAction (detAlgorithm nextA h_next action0) n = nextA n := by
+  have h_eq := policy_eq_deterministic (detAlgorithm nextA h_next action0) n
+  simpa [detAlgorithm] using h_eq.symm
+
+/-- A deterministic environment, where the feedback is given by evaluating
+fixed measurable functions. -/
+noncomputable def detEnvironment
+    (f0 : α → R) (hf0 : Measurable f0)
+    (f : (n : ℕ) → ((Iic n → α × R) × α) → R) (hf : ∀ n, Measurable (f n)) :
+    Environment α R where
+  feedback n := (Kernel.deterministic (f n) (hf n))
+  ν0 := Kernel.deterministic f0 hf0
+
+instance : IsDeterministicEnv (detEnvironment f0 hf0 f hf) where
+  exists_f0 := ⟨f0, hf0, rfl⟩
+  exists_f n := ⟨f n, hf n, rfl⟩
+
+@[simp]
+lemma feedbackFunZero_detEnvironment [MeasurableSpace.SeparatesPoints R] :
+    feedbackFunZero (detEnvironment f0 hf0 f hf) = f0 := by
+  simpa [detEnvironment] using (ν0_eq_deterministic (detEnvironment f0 hf0 f hf)).symm
+
+@[simp]
+lemma feedbackFun_detEnvironment [MeasurableSpace.SeparatesPoints R] (n : ℕ) :
+    feedbackFun (detEnvironment f0 hf0 f hf) n = f n := by
+  simpa [detEnvironment] using (feedback_eq_deterministic (detEnvironment f0 hf0 f hf) n).symm
 
 namespace IsAlgEnvSeq
 
@@ -59,34 +261,26 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
   {alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν]
   {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → α} {R' : ℕ → Ω → R}
 
-lemma HasLaw_action_zero_detAlgorithm
-    (h : IsAlgEnvSeq A R' (detAlgorithm nextAction h_next action0) env P) :
-    HasLaw (A 0) (Measure.dirac action0) P where
-  aemeasurable := have hA := h.measurable_A; by fun_prop
-  map_eq := (hasLaw_action_zero h).map_eq
+lemma hasLaw_action_zero_detAlgorithm
+    (h : IsAlgEnvSeq A R' (detAlgorithm nextA h_next action0) env P) :
+    HasLaw (A 0) (Measure.dirac action0) P := by
+  simpa using IsDeterministicAlg.hasLaw_action_zero h
 
 lemma action_zero_detAlgorithm
-    (h : IsAlgEnvSeq A R' (detAlgorithm nextAction h_next action0) env P) :
-    A 0 =ᵐ[P] fun _ ↦ action0 := by
-  have h_eq : ∀ᵐ x ∂(P.map (A 0)), x = action0 := by
-    rw [(hasLaw_action_zero h).map_eq]
-    simp [detAlgorithm]
-  have hA := h.measurable_A
-  exact ae_of_ae_map (by fun_prop) h_eq
+    (h : IsAlgEnvSeq A R' (detAlgorithm nextA h_next action0) env P) :
+    A 0 =ᵐ[P] fun _ ↦ action0 :=
+  (IsDeterministicAlg.action_zero_ae_eq h).trans (by simp)
 
 lemma action_detAlgorithm_ae_eq
-    (h : IsAlgEnvSeq A R' (detAlgorithm nextAction h_next action0) env P) (n : ℕ) :
-    A (n + 1) =ᵐ[P] fun ω ↦ nextAction n (hist A R' n ω) := by
-  have hA := h.measurable_A
-  have hR' := h.measurable_R
-  exact ae_eq_of_condDistrib_eq_deterministic (by fun_prop) (by fun_prop) (by fun_prop)
-    (h.hasCondDistrib_action n).condDistrib_eq
+    (h : IsAlgEnvSeq A R' (detAlgorithm nextA h_next action0) env P) (n : ℕ) :
+    A (n + 1) =ᵐ[P] fun ω ↦ nextA n (hist A R' n ω) :=
+  (IsDeterministicAlg.action_ae_eq h n).trans (by simp)
 
 lemma action_detAlgorithm_ae_all_eq
-    (h : IsAlgEnvSeq A R' (detAlgorithm nextAction h_next action0) env P) :
-    ∀ᵐ ω ∂P, A 0 ω = action0 ∧ ∀ n, A (n + 1) ω = nextAction n (hist A R' n ω) := by
-  rw [eventually_and, ae_all_iff]
-  exact ⟨action_zero_detAlgorithm h, action_detAlgorithm_ae_eq h⟩
+    (h : IsAlgEnvSeq A R' (detAlgorithm nextA h_next action0) env P) :
+    ∀ᵐ ω ∂P, A 0 ω = action0 ∧ ∀ n, A (n + 1) ω = nextA n (hist A R' n ω) := by
+  filter_upwards [IsDeterministicAlg.action_ae_all_eq h] with ω hω using by simp [hω]
+
 
 end IsAlgEnvSeq
 
@@ -97,34 +291,26 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
   {alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν]
   {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → α} {R' : ℕ → Ω → R} {N n : ℕ}
 
-lemma HasLaw_action_zero_detAlgorithm
-    (h : IsAlgEnvSeqUntil A R' (detAlgorithm nextAction h_next action0) env P N) :
-    HasLaw (A 0) (Measure.dirac action0) P where
-  aemeasurable := have hA := h.measurable_A; by fun_prop
-  map_eq := (hasLaw_action_zero h).map_eq
+lemma hasLaw_action_zero_detAlgorithm
+    (h : IsAlgEnvSeqUntil A R' (detAlgorithm nextA h_next action0) env P N) :
+    HasLaw (A 0) (Measure.dirac action0) P := by
+  simpa using IsDeterministicAlg.hasLaw_action_zero_of_IsAlgEnvSeqUntil h
 
 lemma action_zero_detAlgorithm
-    (h : IsAlgEnvSeqUntil A R' (detAlgorithm nextAction h_next action0) env P N) :
-    A 0 =ᵐ[P] fun _ ↦ action0 := by
-  have h_eq : ∀ᵐ x ∂(P.map (A 0)), x = action0 := by
-    rw [(hasLaw_action_zero h).map_eq]
-    simp [detAlgorithm]
-  have hA := h.measurable_A
-  exact ae_of_ae_map (by fun_prop) h_eq
+    (h : IsAlgEnvSeqUntil A R' (detAlgorithm nextA h_next action0) env P N) :
+    A 0 =ᵐ[P] fun _ ↦ action0 :=
+  (IsDeterministicAlg.action_zero_of_IsAlgEnvSeqUntil h).trans (by simp)
 
 lemma action_detAlgorithm_ae_eq
-    (h : IsAlgEnvSeqUntil A R' (detAlgorithm nextAction h_next action0) env P N) (hn : n < N) :
-    A (n + 1) =ᵐ[P] fun ω ↦ nextAction n (IsAlgEnvSeq.hist A R' n ω) := by
-  have hA := h.measurable_A
-  have hR' := h.measurable_R
-  exact ae_eq_of_condDistrib_eq_deterministic (by fun_prop) (by fun_prop) (by fun_prop)
-    (h.hasCondDistrib_action n hn).condDistrib_eq
+    (h : IsAlgEnvSeqUntil A R' (detAlgorithm nextA h_next action0) env P N) (hn : n < N) :
+    A (n + 1) =ᵐ[P] fun ω ↦ nextA n (IsAlgEnvSeq.hist A R' n ω) :=
+  (IsDeterministicAlg.action_ae_eq_of_IsAlgEnvSeqUntil h hn).trans (by simp)
 
 end IsAlgEnvSeqUntil
 
 namespace IT
 
-local notation "𝔓" => trajMeasure (detAlgorithm nextAction h_next action0) env
+local notation "𝔓" => trajMeasure (detAlgorithm nextA h_next action0) env
 
 lemma HasLaw_action_zero_detAlgorithm : HasLaw (IT.action 0) (Measure.dirac action0) 𝔓 where
   map_eq := (IT.hasLaw_action_zero _ _).map_eq
@@ -137,13 +323,13 @@ lemma action_zero_detAlgorithm [MeasurableSingletonClass α] :
   exact ae_of_ae_map (by fun_prop) h_eq
 
 lemma action_detAlgorithm_ae_eq [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R]
-    [Nonempty R] (n : ℕ) : IT.action (n + 1) =ᵐ[𝔓] fun h ↦ nextAction n (IT.hist n h) :=
+    [Nonempty R] (n : ℕ) : IT.action (n + 1) =ᵐ[𝔓] fun h ↦ nextA n (IT.hist n h) :=
   ae_eq_of_condDistrib_eq_deterministic (by fun_prop) (by fun_prop) (by fun_prop)
-    (IT.condDistrib_action (detAlgorithm nextAction h_next action0) env n)
+    (IT.condDistrib_action (detAlgorithm nextA h_next action0) env n)
 
 lemma action_detAlgorithm_ae_all_eq
     [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] :
-    ∀ᵐ h ∂𝔓, IT.action 0 h = action0 ∧ ∀ n, IT.action (n + 1) h = nextAction n (IT.hist n h) := by
+    ∀ᵐ h ∂𝔓, IT.action 0 h = action0 ∧ ∀ n, IT.action (n + 1) h = nextA n (IT.hist n h) := by
   rw [eventually_and, ae_all_iff]
   exact ⟨action_zero_detAlgorithm, action_detAlgorithm_ae_eq⟩
 
diff --git a/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean b/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean
new file mode 100644
index 00000000..684633a6
--- /dev/null
+++ b/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean
@@ -0,0 +1,150 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré, Rémy Degenne
+-/
+module
+
+public import LeanMachineLearning.SequentialLearning.Deterministic
+public import LeanMachineLearning.SequentialLearning.StationaryEnv
+public import LeanMachineLearning.Probability.Independence.CondDistrib
+
+/-!
+# Function evaluation environments
+
+We define two environments, `onlineEvalEnv` and `evalEnv`, where the reward is given by evaluating
+a measurable function at the chosen action. The first one allows the function to change at every
+time step, while the second one uses a fixed function at every time step.
+
+## Main definitions
+
+* `onlineEvalEnv g hg`: A stationary environment where the reward at time `n` is given by a
+  deterministic kernel that evaluates the measurable function `g n` at the chosen action.
+* `evalEnv f hf`: A stationary environment where the reward is given by a deterministic kernel that
+  evaluates a fixed measurable function `f` at the chosen action.
+
+They both satisfy the typeclasses `IsObliviousEnv` and `IsDeterministicEnv`.
+
+## Main statements
+
+* `forall_reward_onlineEvalEnv_ae_eq_eval_action`: For almost all `ω`, the reward at time `n` is
+  equal to `g n` evaluated at the action taken at time `n`.
+* `forall_reward_evalEnv_ae_eq_eval_action`: For almost all `ω`, the reward at time `n` is equal to
+  `f` evaluated at the action taken at time `n`.
+
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory
+
+namespace Learning
+
+variable {α R : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R}
+  {g : ℕ → α → R} {hg : ∀ n, Measurable (g n)}
+  {f : α → R} {hf : Measurable f}
+
+/-- The evaluation environment where the reward is given by evaluating a fixed measurable function
+`f` at the chosen action. -/
+noncomputable def onlineEvalEnv (g : ℕ → α → R) (hg : ∀ n, Measurable (g n)) :=
+  obliviousEnv (fun n ↦ Kernel.deterministic (g n) (hg n))
+
+instance : IsObliviousEnv (onlineEvalEnv g hg) :=
+  ⟨⟨fun n ↦ Kernel.deterministic (g n) (hg n), fun _ ↦ inferInstance, rfl, fun _ ↦ rfl⟩⟩
+
+instance : IsDeterministicEnv (onlineEvalEnv g hg) where
+  exists_f0 := ⟨g 0, hg 0, rfl⟩
+  exists_f n := ⟨fun p ↦ g (n + 1) p.2, by fun_prop, rfl⟩
+
+@[simp]
+lemma feedbackCondAction_onlineEvalEnv (n : ℕ) :
+    feedbackCondAction (onlineEvalEnv g hg) n = Kernel.deterministic (g n) (hg n) := by
+  simp [onlineEvalEnv]
+
+@[simp]
+lemma feedbackFunZero_onlineEvalEnv [MeasurableSpace.SeparatesPoints R] :
+    feedbackFunZero (onlineEvalEnv g hg) = g 0 := by
+  have h_eq := ν0_eq_deterministic (onlineEvalEnv g hg)
+  simpa only [onlineEvalEnv, ν0_obliviousEnv, Kernel.prodMkLeft_deterministic,
+    Kernel.deterministic_inj] using h_eq.symm
+
+@[simp]
+lemma feedbackFun_onlineEvalEnv [MeasurableSpace.SeparatesPoints R] (n : ℕ) :
+    feedbackFun (onlineEvalEnv g hg) n = fun p ↦ g (n + 1) p.2 := by
+  have h_eq := feedback_eq_deterministic (onlineEvalEnv g hg) n
+  simpa only [onlineEvalEnv, feedback_obliviousEnv, Kernel.prodMkLeft_deterministic,
+    Kernel.deterministic_inj] using h_eq.symm
+
+section OnlineEvalEnv
+
+variable [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
+  {Ω : Type*} {mΩ : MeasurableSpace Ω} {alg : Algorithm α R}
+  {g : ℕ → α → R} {hg : ∀ n, Measurable (g n)}
+  {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → α} {R' : ℕ → Ω → R}
+
+lemma hascondDistrib_reward_onlineEvalEnv
+    (h : IsAlgEnvSeq A R' alg (onlineEvalEnv g hg) P) (n : ℕ) :
+    HasCondDistrib (R' n) (A n) (Kernel.deterministic (g n) (hg n)) P := by
+  simpa using IsObliviousEnv.hasCondDistrib_reward h n
+
+lemma reward_onlineEvalEnv_ae_eq_eval_action
+    (h : IsAlgEnvSeq A R' alg (onlineEvalEnv g hg) P) (n : ℕ) :
+    R' n =ᵐ[P] g n ∘ A n :=
+  ae_eq_of_condDistrib_eq_deterministic (hg n) (h.measurable_A n).aemeasurable
+    (h.measurable_R n).aemeasurable (hascondDistrib_reward_onlineEvalEnv h n).condDistrib_eq
+
+lemma forall_reward_onlineEvalEnv_ae_eq_eval_action
+    (h : IsAlgEnvSeq A R' alg (onlineEvalEnv g hg) P) :
+    ∀ᵐ ω ∂P, ∀ n, R' n ω = g n (A n ω) := by
+  rw [ae_all_iff]
+  intro n
+  exact reward_onlineEvalEnv_ae_eq_eval_action h n
+
+end OnlineEvalEnv
+
+/-- The evaluation environment where the reward is given by evaluating a fixed measurable function
+`f` at the chosen action. -/
+noncomputable def evalEnv (f : α → R) (hf : Measurable f) := onlineEvalEnv (fun _ ↦ f) (fun _ ↦ hf)
+
+instance : IsObliviousEnv (evalEnv f hf) := by unfold evalEnv; infer_instance
+
+instance : IsDeterministicEnv (evalEnv f hf) := by unfold evalEnv; infer_instance
+
+@[simp]
+lemma feedbackCondAction_evalEnv (n : ℕ) :
+    feedbackCondAction (evalEnv f hf) n = Kernel.deterministic f hf := by simp [evalEnv]
+
+@[simp]
+lemma feedbackFunZero_evalEnv [MeasurableSpace.SeparatesPoints R] :
+    feedbackFunZero (evalEnv f hf) = f := by simp [evalEnv]
+
+@[simp]
+lemma feedbackFun_evalEnv [MeasurableSpace.SeparatesPoints R] (n : ℕ) :
+    feedbackFun (evalEnv f hf) n = fun p ↦ f p.2 := by simp [evalEnv]
+
+section EvalEnv
+
+variable [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
+  {Ω : Type*} {mΩ : MeasurableSpace Ω} {alg : Algorithm α R} {f : α → R} {hf : Measurable f}
+  {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → α} {R' : ℕ → Ω → R}
+
+lemma hascondDistrib_reward_evalEnv (h : IsAlgEnvSeq A R' alg (evalEnv f hf) P) (n : ℕ) :
+    HasCondDistrib (R' n) (A n) (Kernel.deterministic f hf) P := by
+  simpa using IsObliviousEnv.hasCondDistrib_reward h n
+
+lemma reward_evalEnv_ae_eq_eval_action (h : IsAlgEnvSeq A R' alg (evalEnv f hf) P) (n : ℕ) :
+    R' n =ᵐ[P] f ∘ A n := reward_onlineEvalEnv_ae_eq_eval_action h n
+
+lemma forall_reward_evalEnv_ae_eq_eval_action (h : IsAlgEnvSeq A R' alg (evalEnv f hf) P) :
+    ∀ᵐ ω ∂P, ∀ n, R' n ω = f (A n ω) := forall_reward_onlineEvalEnv_ae_eq_eval_action h
+
+open Finset in
+lemma reward_evalEnv_ae_eq_eval_action_comp {β : Type*}
+    (h : IsAlgEnvSeq A R' alg (evalEnv f hf) P) {n : ℕ} (g : (Iic n → R) → β) :
+    ∀ᵐ ω ∂P, g (fun i ↦ R' i ω) = g (fun i ↦ f (A i ω)) := by
+  filter_upwards [forall_reward_evalEnv_ae_eq_eval_action h] with ω hω
+  simp_rw [hω]
+
+end EvalEnv
+
+end Learning
diff --git a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
index 88e841cb..72405acd 100644
--- a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
+++ b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
@@ -5,16 +5,31 @@ Authors: Rémy Degenne, Paulo Rauber
 -/
 module
 
+public import LeanMachineLearning.Probability.Kernel.Composition.MapComap
 public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
 
 /-!
-# Stationary environments
+# Oblivious and stationary environments
 
-A stationary environment is an environment in which the distribution of the next reward depends only
+An oblivious environment is an environment in which the distribution of the next reward depends only
 on the last action (and not on the past history).
+If the kernel that gives the distribution of the next reward given the last action is the same at
+every time step, then we say that the environment is stationary.
 
 ## Main definitions
 
+We define a `Prop`-valued typeclass `IsObliviousEnv` to express that an environment is oblivious,
+and we define two constructors for oblivious environments.
+
+Typeclass and related definitions:
+* `IsObliviousEnv env`: the environment `env` is oblivious.
+* `feedbackCondAction env n`: the kernel representing the conditional distribution of the feedback
+  given the action at time `n` in an oblivious environment `env`.
+
+Constructors for oblivious environments:
+* `obliviousEnv ν`: an oblivious environment, in which the distribution of the next reward depends
+  only on the last action, but in a possibly time-dependent manner, and is given by a sequence of
+  Markov kernels `ν : ℕ → Kernel α R`.
 * `stationaryEnv ν`: a stationary environment, in which the distribution of the next reward depends
   only on the last action (and not on the past history), and is given by a Markov kernel
   `ν : Kernel α R`.
@@ -31,40 +46,52 @@ namespace Learning
 
 variable {α R : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R}
 
-/-- A stationary environment, in which the distribution of the next reward depends only on the last
-action. -/
-@[simps]
--- ANCHOR: stationaryEnv
-def stationaryEnv (ν : Kernel α R) [IsMarkovKernel ν] : Environment α R where
-  feedback _ := ν.prodMkLeft _
-  ν0 := ν
--- ANCHOR_END: stationaryEnv
+/-- An environment is oblivious if the distribution of the next feedback depends only on
+the last action and not on the past history. -/
+class IsObliviousEnv (env : Environment α R) : Prop where
+  exists_eq_prodMkLeft : ∃ ν : ℕ → Kernel α R, (∀ n, IsMarkovKernel (ν n)) ∧
+    (env.ν0 = ν 0) ∧ (∀ n, env.feedback n = (ν (n + 1)).prodMkLeft _)
+
+/-- The kernel representing the conditional distribution of the feedback given the action
+at time `n` in an oblivious environment. -/
+noncomputable
+def feedbackCondAction (env : Environment α R) [h_obl : IsObliviousEnv env] (n : ℕ) : Kernel α R :=
+  h_obl.exists_eq_prodMkLeft.choose n
+
+instance (env : Environment α R) [IsObliviousEnv env] (n : ℕ) :
+    IsMarkovKernel (feedbackCondAction env n) :=
+  IsObliviousEnv.exists_eq_prodMkLeft.choose_spec.1 n
+
+lemma ν0_eq_feedbackCondAction (env : Environment α R) [IsObliviousEnv env] :
+    env.ν0 = feedbackCondAction env 0 :=
+  IsObliviousEnv.exists_eq_prodMkLeft.choose_spec.2.1
+
+lemma feedback_eq_feedbackCondAction (env : Environment α R) [IsObliviousEnv env] (n : ℕ) :
+    env.feedback n = (feedbackCondAction env (n + 1)).prodMkLeft _ :=
+  IsObliviousEnv.exists_eq_prodMkLeft.choose_spec.2.2 n
+
+namespace IsObliviousEnv
 
 variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
   [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
-  {alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν]
-  {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → α} {R' : ℕ → Ω → R}
-
-namespace IsAlgEnvSeq
+  {alg : Algorithm α R} {env : Environment α R} {P : Measure Ω} [IsFiniteMeasure P]
+  {A : ℕ → Ω → α} {R' : ℕ → Ω → R} {n N : ℕ}
+  {ν : ℕ → Kernel α R} [∀ n, IsMarkovKernel (ν n)]
 
-/-- The conditional distribution of the reward at time `n` given the action at time `n` is `ν`. -/
-lemma condDistrib_reward_stationaryEnv
-    (h : IsAlgEnvSeq A R' alg (stationaryEnv ν) P) (n : ℕ) :
-    condDistrib (R' n) (A n) P =ᵐ[P.map (A n)] ν := by
+lemma hasCondDistrib_reward [IsObliviousEnv env] (h : IsAlgEnvSeq A R' alg env P) (n : ℕ) :
+    HasCondDistrib (R' n) (A n) (feedbackCondAction env n) P := by
   have hA := h.measurable_A
   have hR' := h.measurable_R
   cases n with
-  | zero =>
-    rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)]
-    change P.map (step A R' 0) = P.map (A 0) ⊗ₘ ν
-    rw [(hasLaw_action_zero h).map_eq, (hasLaw_step_zero h).map_eq, stationaryEnv_ν0]
+  | zero => rw [← ν0_eq_feedbackCondAction]; exact h.hasCondDistrib_reward_zero
   | succ n =>
+    refine ⟨by fun_prop, by fun_prop, ?_⟩
     have h_eq := (h.hasCondDistrib_reward n).condDistrib_eq
     rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h_eq ⊢
     have : P.map (A (n + 1)) =
-        (P.map (fun x ↦ (hist A R' n x, A (n + 1) x))).snd := by
+        (P.map (fun x ↦ (IsAlgEnvSeq.hist A R' n x, A (n + 1) x))).snd := by
       rw [Measure.snd_map_prodMk (by fun_prop)]
-    simp only [stationaryEnv_feedback] at h_eq
+    simp only [feedback_eq_feedbackCondAction] at h_eq
     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
@@ -72,29 +99,135 @@ lemma condDistrib_reward_stationaryEnv
 /-- The reward at time `n + 1` is conditionally independent of the history up to time `n`
 given the action at time `n + 1`. -/
 lemma condIndepFun_reward_hist_action [StandardBorelSpace Ω]
-    (h : IsAlgEnvSeq A R' alg (stationaryEnv ν) P) (n : ℕ) :
-    R' (n + 1) ⟂ᵢ[A (n + 1), h.measurable_A _ ; P] hist A R' n := by
+        [IsObliviousEnv env] (h : IsAlgEnvSeq A R' alg env P) (n : ℕ) :
+    R' (n + 1) ⟂ᵢ[A (n + 1), h.measurable_A _ ; P] IsAlgEnvSeq.hist A R' n := by
   have hA := h.measurable_A
   have hR' := h.measurable_R
-  exact condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft
-    (by fun_prop) (by fun_prop) (by fun_prop) (h.hasCondDistrib_reward n).condDistrib_eq
+  refine condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft
+    (η := feedbackCondAction env (n + 1))
+    (by fun_prop) (by fun_prop) (by fun_prop) ?_
+  refine HasCondDistrib.condDistrib_eq ?_
+  rw [← feedback_eq_feedbackCondAction]
+  exact h.hasCondDistrib_reward n
 
 lemma condIndepFun_reward_hist_action_action [StandardBorelSpace Ω]
-    (h : IsAlgEnvSeq A R' alg (stationaryEnv ν) P) (n : ℕ) :
+    [IsObliviousEnv env] (h : IsAlgEnvSeq A R' alg env P) (n : ℕ) :
     R' (n + 1) ⟂ᵢ[A (n + 1), h.measurable_A (n + 1); P]
-      (fun ω ↦ (hist A R' n ω, A (n + 1) ω)) := by
-  have h_indep : R' (n + 1) ⟂ᵢ[A (n + 1), h.measurable_A (n + 1); P] hist A R' n := by
-    convert h.condIndepFun_reward_hist_action n
+      (fun ω ↦ (IsAlgEnvSeq.hist A R' n ω, A (n + 1) ω)) := by
+  have h_indep : R' (n + 1) ⟂ᵢ[A (n + 1), h.measurable_A (n + 1); P] IsAlgEnvSeq.hist A R' n :=
+    condIndepFun_reward_hist_action h n
   have hA := h.measurable_A
   have hR' := h.measurable_R
   exact h_indep.prod_right (by fun_prop) (by fun_prop) (by fun_prop)
 
 lemma condIndepFun_reward_hist_action_action' [StandardBorelSpace Ω]
-    (h : IsAlgEnvSeq A R' alg (stationaryEnv ν) P) (n : ℕ) (hn : n ≠ 0) :
-    R' n ⟂ᵢ[A n, h.measurable_A n; P] (fun ω ↦ (hist A R' (n - 1) ω, A n ω)) := by
-  have := h.condIndepFun_reward_hist_action_action (n - 1)
+        [IsObliviousEnv env] (h : IsAlgEnvSeq A R' alg env P) (n : ℕ) (hn : n ≠ 0) :
+    R' n ⟂ᵢ[A n, h.measurable_A n; P] (fun ω ↦ (IsAlgEnvSeq.hist A R' (n - 1) ω, A n ω)) := by
+  have := condIndepFun_reward_hist_action_action h (n - 1)
   grind
 
+end IsObliviousEnv
+
+/-- An oblivious environment, in which the distribution of the next reward depends only on the last
+action, but in a possibly time-dependent manner. -/
+@[simps]
+-- ANCHOR: obliviousEnv
+def obliviousEnv (ν : ℕ → Kernel α R) [∀ n, IsMarkovKernel (ν n)] : Environment α R where
+  feedback n := (ν (n + 1)).prodMkLeft _
+  ν0 := ν 0
+-- ANCHOR_END: obliviousEnv
+
+@[simp]
+lemma feedback_obliviousEnv (ν : ℕ → Kernel α R) [∀ n, IsMarkovKernel (ν n)] (n : ℕ) :
+    (obliviousEnv ν).feedback n = (ν (n + 1)).prodMkLeft _ := by simp [obliviousEnv]
+
+@[simp]
+lemma ν0_obliviousEnv (ν : ℕ → Kernel α R) [∀ n, IsMarkovKernel (ν n)] :
+    (obliviousEnv ν).ν0 = ν 0 := by simp [obliviousEnv]
+
+instance (ν : ℕ → Kernel α R) [∀ n, IsMarkovKernel (ν n)] :
+    IsObliviousEnv (obliviousEnv ν) where
+  exists_eq_prodMkLeft := ⟨fun n ↦ ν n, inferInstance,rfl, fun _ ↦ rfl⟩
+
+@[simp]
+lemma feedbackCondAction_obliviousEnv (ν : ℕ → Kernel α R) [hν : ∀ n, IsMarkovKernel (ν n)]
+    (n : ℕ) :
+    feedbackCondAction (obliviousEnv ν) n = ν n := by
+  rcases isEmpty_or_nonempty α with hα | hα
+  · ext a : 1
+    exact hα.elim a
+  rcases isEmpty_or_nonempty R with hR | hR
+  · refine absurd (hν 0) ?_
+    simp only [Subsingleton.eq_zero ν, Pi.zero_apply]
+    exact Kernel.not_isMarkovKernel_zero
+  have : Nonempty (Iic n → α × R) := ⟨fun _ ↦ (hα.some, hR.some)⟩
+  have h_eq_zero := ν0_eq_feedbackCondAction (obliviousEnv ν)
+  have h_eq := feedback_eq_feedbackCondAction (obliviousEnv ν) (n - 1)
+  cases n with
+  | zero => exact h_eq_zero.symm
+  | succ n =>
+    simp only [Nat.add_one_sub_one, obliviousEnv_feedback, add_tsub_cancel_right] at h_eq
+    rw [← Kernel.prodMkLeft_inj (γ := Iic n → α × R)]
+    exact h_eq.symm
+
+/-- A stationary environment, in which the distribution of the next reward depends only on the last
+action. -/
+-- ANCHOR: stationaryEnv
+def stationaryEnv (ν : Kernel α R) [IsMarkovKernel ν] : Environment α R := obliviousEnv fun _ ↦ ν
+-- ANCHOR_END: stationaryEnv
+
+@[simp]
+lemma feedback_stationaryEnv (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) :
+    (stationaryEnv ν).feedback n = ν.prodMkLeft _ := by simp [stationaryEnv]
+
+@[simp]
+lemma ν0_stationaryEnv (ν : Kernel α R) [IsMarkovKernel ν] : (stationaryEnv ν).ν0 = ν := by
+  simp [stationaryEnv]
+
+instance (ν : Kernel α R) [IsMarkovKernel ν] : IsObliviousEnv (stationaryEnv ν) where
+  exists_eq_prodMkLeft := ⟨fun _ ↦ ν, inferInstance, rfl, fun _ ↦ rfl⟩
+
+@[simp]
+lemma feedbackCondAction_stationaryEnv (ν : Kernel α R) [hν : IsMarkovKernel ν] (n : ℕ) :
+    feedbackCondAction (stationaryEnv ν) n = ν := feedbackCondAction_obliviousEnv _ _
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
+  [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
+  {alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν]
+  {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → α} {R' : ℕ → Ω → R}
+
+namespace IsAlgEnvSeq
+
+/-- The conditional distribution of the reward at time `n` given the action at time `n` is `ν`. -/
+lemma hasCondDistrib_reward_stationaryEnv
+    (h : IsAlgEnvSeq A R' alg (stationaryEnv ν) P) (n : ℕ) :
+    HasCondDistrib (R' n) (A n) ν P := by
+  simpa using IsObliviousEnv.hasCondDistrib_reward h n
+
+/-- The conditional distribution of the reward at time `n` given the action at time `n` is `ν`. -/
+lemma condDistrib_reward_stationaryEnv
+    (h : IsAlgEnvSeq A R' alg (stationaryEnv ν) P) (n : ℕ) :
+    condDistrib (R' n) (A n) P =ᵐ[P.map (A n)] ν :=
+  (hasCondDistrib_reward_stationaryEnv h n).condDistrib_eq
+
+/-- The reward at time `n + 1` is conditionally independent of the history up to time `n`
+given the action at time `n + 1`. -/
+lemma condIndepFun_reward_hist_action [StandardBorelSpace Ω]
+    (h : IsAlgEnvSeq A R' alg (stationaryEnv ν) P) (n : ℕ) :
+    R' (n + 1) ⟂ᵢ[A (n + 1), h.measurable_A _ ; P] hist A R' n :=
+  IsObliviousEnv.condIndepFun_reward_hist_action h n
+
+lemma condIndepFun_reward_hist_action_action [StandardBorelSpace Ω]
+    (h : IsAlgEnvSeq A R' alg (stationaryEnv ν) P) (n : ℕ) :
+    R' (n + 1) ⟂ᵢ[A (n + 1), h.measurable_A (n + 1); P]
+      (fun ω ↦ (hist A R' n ω, A (n + 1) ω)) :=
+  IsObliviousEnv.condIndepFun_reward_hist_action_action h n
+
+lemma condIndepFun_reward_hist_action_action' [StandardBorelSpace Ω]
+    (h : IsAlgEnvSeq A R' alg (stationaryEnv ν) P) (n : ℕ) (hn : n ≠ 0) :
+    R' n ⟂ᵢ[A n, h.measurable_A n; P] (fun ω ↦ (hist A R' (n - 1) ω, A n ω)) :=
+  IsObliviousEnv.condIndepFun_reward_hist_action_action' h n hn
+
 end IsAlgEnvSeq
 
 namespace IT
diff --git a/tutorial/Manual/Pages/DefiningAlgorithm.lean b/tutorial/Manual/Pages/DefiningAlgorithm.lean
index 916b6c5a..bf381c01 100644
--- a/tutorial/Manual/Pages/DefiningAlgorithm.lean
+++ b/tutorial/Manual/Pages/DefiningAlgorithm.lean
@@ -46,10 +46,10 @@ The `h_policy` field records that the measure describing the next action is a pr
 If the algorithms actions are not random, we can use the `detAlgorithm` definition to build an algorithm from the data of a measurable function for the next action and a choice for the first action.
 
 ```anchor detAlgorithm (module := LeanMachineLearning.SequentialLearning.Deterministic)
-def detAlgorithm (nextAction : (n : ℕ) → (Iic n → α × R) → α)
-    (h_next : ∀ n, Measurable (nextAction n)) (action0 : α) :
+def detAlgorithm (nextA : (n : ℕ) → (Iic n → α × R) → α)
+    (h_next : ∀ n, Measurable (nextA n)) (action0 : α) :
     Algorithm α R where
-  policy n := Kernel.deterministic (nextAction n) (h_next n)
+  policy n := Kernel.deterministic (nextA n) (h_next n)
   p0 := Measure.dirac action0
 ```
 We can see here that we did not need to prove that the kernels are `IsMarkovKernel` and that the distribution of the first action is a probability measure.
@@ -70,15 +70,19 @@ structure Environment (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] wh
 `ν0` gives the distribution of the first feedback given the first action, and `feedback` gives the distribution of the next feedback given the history and the next action.
 
 In many applications the feedback depends only on the last action and not on the prior history.
-We provide a `stationaryEnv` definition that builds an environment for those cases.
+We provide an `obliviousEnv` definition that builds an environment for those cases.
 
-```anchor stationaryEnv (module := LeanMachineLearning.SequentialLearning.StationaryEnv)
-def stationaryEnv (ν : Kernel α R) [IsMarkovKernel ν] : Environment α R where
-  feedback _ := ν.prodMkLeft _
-  ν0 := ν
+```anchor obliviousEnv (module := LeanMachineLearning.SequentialLearning.StationaryEnv)
+def obliviousEnv (ν : ℕ → Kernel α R) [∀ n, IsMarkovKernel (ν n)] : Environment α R where
+  feedback n := (ν (n + 1)).prodMkLeft _
+  ν0 := ν 0
 ```
-`ν.prodMkLeft _` is the kernel `ν` seen as a `Kernel ((Iic n → α × R) × α) R` by ignoring the history.
+`(ν (n + 1)).prodMkLeft _` is the kernel `ν (n + 1)` seen as a `Kernel ((Iic n → α × R) × α) R` by ignoring the history.
 
+If furthermore the feedback kernel does not change with time, we can use the `stationaryEnv` definition to build the environment.
+```anchor stationaryEnv (module := LeanMachineLearning.SequentialLearning.StationaryEnv)
+def stationaryEnv (ν : Kernel α R) [IsMarkovKernel ν] : Environment α R := obliviousEnv fun _ ↦ ν
+```
 
 
 # Sequences of actions and feedback, probability space