diff --git a/LMLTutorial/Pages/DefiningAlgorithm.lean b/LMLTutorial/Pages/DefiningAlgorithm.lean
index 86745598..5fb570ed 100644
--- a/LMLTutorial/Pages/DefiningAlgorithm.lean
+++ b/LMLTutorial/Pages/DefiningAlgorithm.lean
@@ -61,14 +61,14 @@ The `policy` field contains for each time `n` a kernel from that history togethe
 That is, it maps every possible history and current observation to a random action at time `n` (and that map is measurable).
 The `isMarkovKernel_policy` field records that the measure describing the action is a probability measure (and it is in square brackets to tell Lean to infer it automatically whenever possible).
 At time `0` the history is empty: `Hist 𝓞 𝓐 𝓨 0` has a unique element, and the distribution of the first action given the first observation is `policy 0` applied to that element.
-That kernel is called `Algorithm.p0`.
+That kernel is called `Algorithm.policyZero`.
 
 Many settings have no observations at all: the algorithm sees only the past rounds. Those are described by taking `𝓞 = Unit`, and we write `noObs Ω` for the corresponding (constant) observation process.
 
-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 action at each time, as a function of the history before that time and of the current observation.
+If the algorithms actions are not random, we can use the `Algorithm.deterministic` definition to build an algorithm from the data of a measurable function for the action at each time, as a function of the history before that time and of the current observation.
 The first action is the value of that function at time `0` on the empty history.
 
-{docstring detAlgorithm}
+{docstring Algorithm.deterministic}
 
 We can see here that we did not need to prove that the kernels are `IsMarkovKernel`.
 Lean knows that deterministic kernels are Markov.
@@ -79,19 +79,21 @@ The `Environment` structure is the mirror of the `Algorithm` structure, with a k
 
 `obs n` gives the distribution of the observation at time `n` given the history before `n`.
 `feedback n` gives the distribution of the feedback at time `n` given the history before `n`, the observation and the action at time `n`.
-The distribution of the first observation is `obs 0` applied to the empty history; it is called `Environment.obs0`.
-The distribution of the first feedback given the first observation and action is `feedback 0` applied to the empty history; it is called `Environment.ν0`.
+The distribution of the first observation is `obs 0` applied to the empty history; it is called `Environment.obsZero`.
+The distribution of the first feedback given the first observation and action is `feedback 0` applied to the empty history; it is called `Environment.feedbackZero`.
 
-In many applications there is no observation and the feedback depends only on the last action, not on the prior history.
-We provide an `obliviousEnv` definition that builds an environment for those cases.
+In many applications neither the observation nor the feedback depends on the prior history: the observation at time `n` has a fixed law, and the feedback depends only on the current observation and action.
+We provide an `Environment.oblivious` definition that builds an environment for those cases from a sequence of observation laws and a sequence of feedback kernels.
 
-{docstring obliviousEnv}
+{docstring Environment.oblivious}
 
-`(ν n).prodMkLeft _` is the kernel `ν n` seen as a `Kernel ((Hist Unit 𝓐 𝓨 n × Unit) × 𝓐) 𝓨` by ignoring the history and the observation.
+If furthermore those sequences do not change with time, we can use the `Environment.stationary` definition to build the environment.
 
-If furthermore the feedback kernel does not change with time, we can use the `stationaryEnv` definition to build the environment.
+{docstring Environment.stationary}
 
-{docstring stationaryEnv}
+When there is no observation (`𝓞 = Unit`), the feedback depends only on the last action. `Environment.banditSeq` builds such an environment from a sequence of kernels `ν : ℕ → Kernel 𝓐 𝓨`, and `Environment.bandit` from a single kernel `ν : Kernel 𝓐 𝓨` used at every time.
+
+{docstring Environment.bandit}
 
 
 # Sequences of actions and feedback, probability space
@@ -120,14 +122,14 @@ We now illustrate the use of `Algorithm`, `Environment`, and `IsAlgEnvSeq` by de
 
 In a stochastic bandit, an algorithm chooses at each time an action from a finite set (here `Fin K`, the type of natural numbers less than `K`) and receives a reward drawn from a distribution that depends only on the action, not on the prior history.
 
-The environment is thus simply `stationaryEnv ν` for some kernel `ν : Kernel (Fin K) ℝ`.
+The environment is thus simply `Environment.bandit ν` for some kernel `ν : Kernel (Fin K) ℝ`.
 
 ## Algorithm
 
 The UCB algorithm chooses at time `n` the action that maximizes the sum of the empirical mean reward and an exploration bonus.
 It starts by choosing each action once and then chooses $`\arg\max_a (\hat{\mu}_{n,a} + \sqrt{\frac{2c \log (n + 1)}{N_{n,a}}})`, in which $`\hat{\mu}_{n,a}` is the empirical mean reward of action `a` before time `n` (`empMean'` in the code), $`N_{n,a}` is the number of times action `a` has been chosen before time `n` (`pullCount'` in the code), and `c` is a parameter of the algorithm.
 
-To define the algorithm, we first define the exploration bonus and the next action function, and then we use `detAlgorithm` to build the algorithm.
+To define the algorithm, we first define the exploration bonus and the next action function, and then we use `Algorithm.deterministic` to build the algorithm.
 We also need to prove that the next action function is measurable, which is done by the `measurable_nextArm` lemma.
 Note that we are careful to use a measurable version of the argmax function, `argmax`.
 
@@ -139,7 +141,7 @@ Note that we are careful to use a measurable version of the argmax function, `ar
 
 {docstring Bandits.ucbAlgorithm}
 
-The last line builds the algorithm using `detAlgorithm` and the function `UCB.nextArm`.
+The last line builds the algorithm using `Algorithm.deterministic` and the function `UCB.nextArm`.
 Its measurability is proved by the `fun_prop` tactic, which proves measurability of functions by using lemmas tagged with `@[fun_prop]`.
 The first action of the algorithm is `UCB.nextArm K c 0` applied to the empty history, which is 0 as an element of `Fin K`.
 
diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean
index ef058a9c..992ca486 100644
--- a/LeanMachineLearning.lean
+++ b/LeanMachineLearning.lean
@@ -54,6 +54,7 @@ public import LeanMachineLearning.SequentialLearning.ActionIndicator
 public import LeanMachineLearning.SequentialLearning.Algorithm
 public import LeanMachineLearning.SequentialLearning.AlgorithmDensity
 public import LeanMachineLearning.SequentialLearning.AlgorithmDensityBayes
+public import LeanMachineLearning.SequentialLearning.Algorithms.Markov
 public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling.Basic
 public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling.Tendsto
 public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
index 12c60a34..6a28cc8f 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
@@ -48,7 +48,7 @@ variable (K) in
 to `ETC.nextArm`. -/
 noncomputable
 def etcAlgorithm [NeZero K] (m : ℕ) : Algorithm Unit (Fin K) ℝ :=
-  detAlgorithm (fun n p ↦ ETC.nextArm K m n p.1) (by fun_prop)
+  Algorithm.deterministic (fun n p ↦ ETC.nextArm K m n p.1) (by fun_prop)
 
 end AlgorithmDefinition
 
@@ -61,21 +61,22 @@ variable [NeZero K] {m : ℕ} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν]
 
 /-- Before round `K * m`, the ETC algorithm behaves like the Round-Robin algorithm. -/
 lemma isAlgEnvSeqUntil_roundRobinAlgorithm
-    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P) :
-    IsAlgEnvSeqUntil O A R (roundRobinAlgorithm K) (stationaryEnv ν) P (K * m) := by
+    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P) :
+    IsAlgEnvSeqUntil O A R (roundRobinAlgorithm K) (Environment.bandit ν) P (K * m) := by
   refine h.isAlgEnvSeqUntil_of_policy_eq fun n hn ↦ ?_
-  simp only [roundRobinAlgorithm, detAlgorithm_policy, etcAlgorithm]
+  simp only [roundRobinAlgorithm, Algorithm.deterministic_policy, etcAlgorithm]
   congr 1 with p
   simp [ETC.nextArm, hn]
 
 section AlgorithmBehavior
 
-lemma arm_ae_eq_nextArm (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P) (n : ℕ) :
+lemma arm_ae_eq_nextArm (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
+    (n : ℕ) :
     A n =ᵐ[P] fun ω ↦ nextArm K m n (history O A R n ω) :=
-  h.action_detAlgorithm_ae_eq n
+  h.action_deterministic_ae_eq n
 
 /-- For `n < K * m`, the arm pulled at time `n` is the arm `n % K`. -/
-lemma arm_of_lt (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma arm_of_lt (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     {n : ℕ} (hn : n < K * m) :
     A n =ᵐ[P] fun _ ↦ RoundRobin.nextAction K n :=
   RoundRobin.action_ae_eq n ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono hn)
@@ -83,13 +84,13 @@ lemma arm_of_lt (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
 /-- The arm pulled at time `K * m` is the arm with the highest empirical mean after the exploration
 phase. -/
 lemma arm_mul
-    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P) :
+    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P) :
     A (K * m) =ᵐ[P] fun ω ↦ argmax (empMean' (K * m) (history O A R (K * m) ω)) := by
   filter_upwards [arm_ae_eq_nextArm h (K * m)] with ω hn_eq
   rw [hn_eq, nextArm, dite_eq_right (by simp), dite_eq_left rfl]
 
 /-- For `n ≥ K * m`, the arm pulled at time `n + 1` is the same as the arm pulled at time `n`. -/
-lemma arm_add_one_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma arm_add_one_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     {n : ℕ} (hn : K * m ≤ n) :
     A (n + 1) =ᵐ[P] fun ω ↦ A n ω := by
   filter_upwards [arm_ae_eq_nextArm h (n + 1)] with ω hn_eq
@@ -97,7 +98,7 @@ lemma arm_add_one_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv
   rfl
 
 /-- For `n ≥ K * m`, the arm pulled at time `n` is the same as the arm pulled at time `K * m`. -/
-lemma arm_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma arm_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     {n : ℕ} (hn : K * m ≤ n) :
     A n =ᵐ[P] A (K * m) := by
   have h_ae n : K * m ≤ n → A (n + 1) =ᵐ[P] fun ω ↦ A n ω := arm_add_one_of_ge h
@@ -108,11 +109,12 @@ lemma arm_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
   | succ n hmn h_ind => rw [h_ae n hmn, h_ind]
 
 /-- At time `K * m`, the number of pulls of each arm is equal to `m`. -/
-lemma pullCount_mul (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P) (a : Fin K) :
+lemma pullCount_mul (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
+    (a : Fin K) :
     pullCount A a (K * m) =ᵐ[P] fun _ ↦ m :=
   RoundRobin.pullCount_mul m (isAlgEnvSeqUntil_roundRobinAlgorithm h) a
 
-lemma pullCount_add_one_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma pullCount_add_one_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     (a : Fin K) {n : ℕ} (hn : K * m ≤ n) :
     pullCount A a (n + 1)
       =ᵐ[P] fun ω ↦ pullCount A a n ω + {ω' | A (K * m) ω' = a}.indicator 1 ω := by
@@ -122,7 +124,7 @@ lemma pullCount_add_one_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (station
 
 /-- For `n ≥ K * m`, the number of pulls of each arm `a` at time `n` is equal to `m` plus
 `n - K * m` if arm `a` is the best arm after the exploration phase. -/
-lemma pullCount_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma pullCount_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     (a : Fin K) {n : ℕ} (hn : K * m ≤ n) :
     pullCount A a n
       =ᵐ[P] fun ω ↦ m + (n - K * m) * {ω' | A (K * m) ω' = a}.indicator 1 ω := by
@@ -142,7 +144,7 @@ lemma pullCount_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv 
 /-- If at time `K * m` the algorithm chooses arm `a`, then the total reward obtained by pulling
 arm `a` is at least the total reward obtained by pulling the best arm. -/
 lemma sumRewards_bestArm_le_of_arm_mul_eq
-    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P) (a : Fin K) (hm : m ≠ 0) :
+    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P) (a : Fin K) (hm : m ≠ 0) :
     ∀ᵐ ω ∂P, A (K * m) ω = a → sumRewards A R (bestArm ν) (K * m) ω ≤
       sumRewards A R a (K * m) ω := by
   filter_upwards [arm_mul h, pullCount_mul h a, pullCount_mul h (bestArm ν)]
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/ETC.lean
index cfc3f1ee..c5a40cfc 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/ETC.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/ETC.lean
@@ -26,7 +26,7 @@ variable {K : ℕ} [NeZero K] {m : ℕ} {ν : Kernel (Fin K) ℝ} [IsMarkovKerne
   {σ2 : ℝ≥0}
 
 lemma probReal_sumRewards_le_sumRewards_le
-    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (a : Fin K) :
     P.real {ω | sumRewards A R (bestArm ν) (K * m) ω ≤ sumRewards A R a (K * m) ω} ≤
       Real.exp (-↑m * gap ν a ^ 2 / (4 * σ2)) := by
@@ -42,7 +42,7 @@ lemma probReal_sumRewards_le_sumRewards_le
 
 /-- The probability that at time `K * m` the ETC algorithm chooses arm `a` is at most
 `exp(- m * Δ_a^2 / (4 * σ2))`. -/
-lemma prob_arm_mul_eq_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma prob_arm_mul_eq_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (a : Fin K)
     (hm : m ≠ 0) :
     P.real {ω | A (K * m) ω = a} ≤ Real.exp (- (m : ℝ) * gap ν a ^ 2 / (4 * σ2)) := by
@@ -57,7 +57,7 @@ lemma prob_arm_mul_eq_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEn
   exact h_le.trans (probReal_sumRewards_le_sumRewards_le h hν a)
 
 /-- Bound on the expectation of the number of pulls of each arm by the ETC algorithm. -/
-lemma expectation_pullCount_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma expectation_pullCount_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (a : Fin K) (hm : m ≠ 0) {n : ℕ} (hn : K * m ≤ n) :
     P[fun ω ↦ (pullCount A a n ω : ℝ)]
@@ -85,7 +85,7 @@ lemma expectation_pullCount_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (statio
   · exact (measurableSet_singleton _).preimage (by fun_prop)
 
 /-- Regret bound for the ETC algorithm. -/
-theorem regret_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+theorem regret_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hm : m ≠ 0)
     (n : ℕ) (hn : K * m ≤ n) :
     P[regret ν A n] ≤
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/UCB.lean
index 7d106788..275e3dba 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/UCB.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/UCB.lean
@@ -75,7 +75,7 @@ lemma pullCount_le_of_ucbIndex_le (hc : 0 ≤ c) {b : Fin K}
 /-- The probability that the UCB index of arm `a` is below its mean is at most
 `1 / (n + 1) ^ (c - 1)`. -/
 lemma prob_ucbIndex_le {alg : Algorithm Unit (Fin K) ℝ}
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (a : Fin K) (n : ℕ) :
     P {ω | 0 < pullCount A a n ω ∧ empMean A R a n ω + ucbWidth A (c * σ2) a n ω ≤ (ν a)[id]} ≤
@@ -102,7 +102,7 @@ lemma prob_ucbIndex_le {alg : Algorithm Unit (Fin K) ℝ}
 /-- The probability that the lower confidence bound of arm `a` is above its mean is at most
 `1 / (n + 1) ^ (c - 1)`. -/
 lemma prob_lcbIndex_ge {alg : Algorithm Unit (Fin K) ℝ}
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (a : Fin K) (n : ℕ) :
     P {ω | 0 < pullCount A a n ω ∧
@@ -170,7 +170,7 @@ lemma pullCount_le_add_three (a : Fin K) (n C : ℕ) (ω : Ω) :
       rw [Finset.sum_add_distrib, Finset.sum_add_distrib]
 
 lemma pullCount_le_add_three_ae
-    (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P)
     (a : Fin K) (n C : ℕ) (hC : C ≠ 0) :
     ∀ᵐ ω ∂P,
     pullCount A a n ω ≤ C + 1 +
@@ -195,7 +195,7 @@ lemma pullCount_le_add_three_ae
 at which it already has more than `C` pulls and the means of the best arm and of `a` lie in
 their confidence intervals. -/
 lemma sum_indicator_good_event_eq_zero
-    (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (Environment.bandit ν) P)
     (hc : 0 ≤ c) (a : Fin K) (h_gap : 0 < gap ν a) (n C : ℕ)
     (hC : C ≠ 0) (hC' : 8 * c * σ2 * log (n + 1) / gap ν a ^ 2 ≤ C) :
     ∀ᵐ ω ∂P,
@@ -228,7 +228,8 @@ lemma sum_indicator_good_event_eq_zero
     simp_rw [← mul_assoc]
     gcongr
 
-lemma pullCount_ae_le_add_two (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (stationaryEnv ν) P)
+lemma pullCount_ae_le_add_two
+    (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (Environment.bandit ν) P)
     (hc : 0 ≤ c) (a : Fin K) (h_gap : 0 < gap ν a)
     (n C : ℕ) (hC : C ≠ 0) (hC' : 8 * c * σ2 * log (n + 1) / gap ν a ^ 2 ≤ C) :
     ∀ᵐ ω ∂P,
@@ -296,7 +297,7 @@ lemma constSum_le {c : ℝ} (hc : 2 < c) (n : ℕ) : constSum c n ≤ 1 + 1 / (c
 
 /-- Bound on the expectation of the number of pulls of each arm by the UCB algorithm. -/
 lemma expectation_pullCount_le'
-    (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (hσ2 : σ2 ≠ 0) (hc : 0 < c) (a : Fin K) (h_gap : 0 < gap ν a) (n : ℕ) :
     ∫⁻ ω, pullCount A a n ω ∂P ≤
@@ -381,7 +382,8 @@ lemma expectation_pullCount_le'
     positivity
 
 /-- Bound on the expectation of the number of pulls of each arm by the UCB algorithm. -/
-lemma expectation_pullCount_le (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (stationaryEnv ν) P)
+lemma expectation_pullCount_le
+    (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (hσ2 : σ2 ≠ 0) (hc : 0 < c) (a : Fin K) (h_gap : 0 < gap ν a) (n : ℕ) :
     P[fun ω ↦ (pullCount A a n ω : ℝ)] ≤
@@ -403,7 +405,7 @@ lemma expectation_pullCount_le (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2))
   ring
 
 /-- Regret bound for the UCB algorithm. -/
-lemma regret_le (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (stationaryEnv ν) P)
+lemma regret_le (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (hσ2 : σ2 ≠ 0) (hc : 0 < c) (n : ℕ) :
     P[regret ν A n] ≤
@@ -417,7 +419,7 @@ lemma regret_le (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (stationaryEnv
   · field
 
 /-- Regret bound for the UCB algorithm with an explicit constant, for `c > 2`. -/
-lemma regret_le_of_gt_two (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (stationaryEnv ν) P)
+lemma regret_le_of_gt_two (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (hσ2 : σ2 ≠ 0) (hc : 2 < c) (n : ℕ) :
     P[regret ν A n] ≤
@@ -431,26 +433,26 @@ lemma regret_le_of_gt_two (h : IsAlgEnvSeq O A R (ucbAlgorithm K (c * σ2)) (sta
 
 /-- Regret bound for the UCB algorithm with exploration constant `c`,
 for `σ2`-subgaussian rewards. -/
-lemma regret_le' (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (stationaryEnv ν) P)
+lemma regret_le' (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (hσ2 : σ2 ≠ 0) (hc : 0 < c) (n : ℕ) :
     P[regret ν A n] ≤
       ∑ a, (8 * c * log (n + 1) / gap ν a + gap ν a * (2 + 2 * constSum (c / σ2) n)) := by
   have hσ2' : (0 : ℝ) < σ2 := NNReal.coe_pos.mpr (pos_iff_ne_zero.mpr hσ2)
-  have h' : IsAlgEnvSeq O A R (ucbAlgorithm K (c / σ2 * σ2)) (stationaryEnv ν) P := by
+  have h' : IsAlgEnvSeq O A R (ucbAlgorithm K (c / σ2 * σ2)) (Environment.bandit ν) P := by
     rwa [div_mul_cancel₀ _ hσ2'.ne']
   refine (regret_le h' hν hσ2 (div_pos hc hσ2') n).trans_eq ?_
   rw [show (8 : ℝ) * (c / σ2) * σ2 = 8 * c by rw [mul_assoc, div_mul_cancel₀ _ hσ2'.ne']]
 
 /-- Regret bound for the UCB algorithm with exploration constant `c > 2 * σ2`, for `σ2`-subgaussian
 rewards, with an explicit constant. -/
-theorem regret_le_of_gt_two' (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (stationaryEnv ν) P)
+theorem regret_le_of_gt_two' (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (hσ2 : σ2 ≠ 0) (hc : 2 * σ2 < c) (n : ℕ) :
     P[regret ν A n] ≤
       ∑ a, (8 * c * log (n + 1) / gap ν a + gap ν a * (4 + 2 * σ2 / (c - 2 * σ2))) := by
   have hσ2' : (0 : ℝ) < σ2 := NNReal.coe_pos.mpr (pos_iff_ne_zero.mpr hσ2)
-  have h' : IsAlgEnvSeq O A R (ucbAlgorithm K (c / σ2 * σ2)) (stationaryEnv ν) P := by
+  have h' : IsAlgEnvSeq O A R (ucbAlgorithm K (c / σ2 * σ2)) (Environment.bandit ν) P := by
     rwa [div_mul_cancel₀ _ hσ2'.ne']
   have hc' : 2 < c / σ2 := by rwa [lt_div_iff₀ hσ2']
   refine (regret_le_of_gt_two h' hν hσ2 hc' n).trans_eq ?_
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean b/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean
index aa380f73..12a46b0f 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/TS.lean
@@ -20,7 +20,7 @@ probability of being optimal under the posterior over environments given the his
 * `tsAlgorithm Q κ`: a Thompson sampling algorithm with actions in `Fin K` (for `K ≠ 0`), given
   a prior distribution over parameters `Q : Measure 𝓔` and a Markov kernel
   `κ : Kernel (𝓔 × Fin K) ℝ`. This kernel defines how a parameter `e : 𝓔` gives rise to
-  a stationary environment: `stationaryEnv (κ.sectR e) : Environment (Fin K) ℝ`.
+  a stationary environment: `Environment.bandit (κ.sectR e) : Environment (Fin K) ℝ`.
 
 ## Main results
 
@@ -60,7 +60,7 @@ instance [NeZero K] {Q : Measure 𝓔} [IsProbabilityMeasure Q] {κ : Kernel (
 
 /-- The Thompson sampling algorithm with actions in `Fin K`, where `Q : Measure 𝓔` is a prior
   distribution over parameters, and `κ : Kernel (𝓔 × Fin K) ℝ` is a Markov kernel that defines the
-  stationary environment `stationaryEnv (κ.sectR e)` that corresponds to a parameter `e : 𝓔`.
+  stationary environment `Environment.bandit (κ.sectR e)` that corresponds to a parameter `e : 𝓔`.
 
   At every time `n`, the Thompson sampling policy uses the posterior over the parameters given the
   history up to time `n` to derive the probability of each action being optimal. The action for time
@@ -81,9 +81,9 @@ variable {P : Measure Ω} [IsProbabilityMeasure P]
 
 /-- The first action of Thompson sampling is sampled according to its probability of being optimal
 under the prior over environments. -/
-lemma TS.p0_tsAlgorithm :
-    (tsAlgorithm Q κ).p0 () = Q.map (bestAction κ id) := by
-  rw [Algorithm.p0_apply]
+lemma TS.policyZero_tsAlgorithm :
+    (tsAlgorithm Q κ).policyZero () = Q.map (bestAction κ id) := by
+  rw [Algorithm.policyZero_apply]
   dsimp only [tsAlgorithm]
   rw [TS.policy, Kernel.prodMkRight_apply, Kernel.map_apply _ (by fun_prop),
     IT.bayesTrajMeasurePosterior_zero, Kernel.const_apply]
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
index 832b152f..38ca7461 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
@@ -54,7 +54,7 @@ variable (K) in
 /-- The UCB algorithm. -/
 noncomputable
 def ucbAlgorithm [NeZero K] (c : ℝ) : Algorithm Unit (Fin K) ℝ :=
-  detAlgorithm (fun n p ↦ UCB.nextArm K c n p.1) (by fun_prop)
+  Algorithm.deterministic (fun n p ↦ UCB.nextArm K c n p.1) (by fun_prop)
 end Algorithm
 
 namespace UCB
@@ -67,10 +67,10 @@ variable [NeZero K] {c : ℝ} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν]
 
 /-- Before round `K`, the UCB algorithm behaves like the Round-Robin algorithm. -/
 lemma isAlgEnvSeqUntil_roundRobinAlgorithm
-    (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (stationaryEnv ν) P) :
-    IsAlgEnvSeqUntil O A R (roundRobinAlgorithm K) (stationaryEnv ν) P K := by
+    (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P) :
+    IsAlgEnvSeqUntil O A R (roundRobinAlgorithm K) (Environment.bandit ν) P K := by
   refine h.isAlgEnvSeqUntil_of_policy_eq fun n hn ↦ ?_
-  simp only [roundRobinAlgorithm, detAlgorithm_policy, ucbAlgorithm]
+  simp only [roundRobinAlgorithm, Algorithm.deterministic_policy, ucbAlgorithm]
   congr 1 with p
   simp [UCB.nextArm, hn]
 
@@ -93,16 +93,17 @@ lemma ucbWidth_eq_ucbWidth' (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) :
     ucbWidth A c a n ω = ucbWidth' c n (history O A R n ω) a := by
   rw [ucbWidth, ucbWidth', pullCount_eq_pullCount' (O := O) (A := A) (R' := R)]
 
-lemma arm_zero (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (stationaryEnv ν) P) :
+lemma arm_zero (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P) :
     A 0 =ᵐ[P] fun _ ↦ 0 :=
   RoundRobin.action_zero ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono (Nat.pos_of_neZero K))
 
-lemma arm_ae_eq_nextArm (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (stationaryEnv ν) P) (n : ℕ) :
+lemma arm_ae_eq_nextArm (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P)
+    (n : ℕ) :
     A n =ᵐ[P] fun ω ↦ nextArm K c n (history O A R n ω) :=
-  h.action_detAlgorithm_ae_eq n
+  h.action_deterministic_ae_eq n
 
 lemma ucbIndex_le_ucbIndex_arm
-    (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (stationaryEnv ν) P) (a : Fin K) (hn : K ≤ n) :
+    (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P) (a : Fin K) (hn : K ≤ n) :
     ∀ᵐ ω ∂P, empMean A R a n ω + ucbWidth A c a n ω ≤
       empMean A R (A n ω) n ω + ucbWidth A c (A n ω) n ω := by
   filter_upwards [arm_ae_eq_nextArm h n] with ω h_arm
@@ -112,7 +113,7 @@ lemma ucbIndex_le_ucbIndex_arm
   exact isMaxOn_argmax (fun a ↦ empMean' n (history O A R n ω) a
     + ucbWidth' c n (history O A R n ω) a) _
 
-lemma forall_arm_eq_mod_of_lt (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (stationaryEnv ν) P) :
+lemma forall_arm_eq_mod_of_lt (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P) :
     ∀ᵐ ω ∂P, ∀ n < K, A n ω = RoundRobin.nextAction K n := by
   simp_rw [ae_all_iff]
   intro n hn
@@ -121,7 +122,7 @@ lemma forall_arm_eq_mod_of_lt (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (station
   simp only [nextArm, hn, ↓reduceIte]
 
 lemma forall_ucbIndex_le_ucbIndex_arm
-    (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (stationaryEnv ν) P) (a : Fin K) :
+    (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P) (a : Fin K) :
     ∀ᵐ ω ∂P, ∀ n, K ≤ n →
       empMean A R a n ω + ucbWidth A c a n ω ≤
         empMean A R (A n ω) n ω + ucbWidth A c (A n ω) n ω := by
@@ -129,12 +130,12 @@ lemma forall_ucbIndex_le_ucbIndex_arm
   exact fun _ ↦ ucbIndex_le_ucbIndex_arm h a
 
 lemma time_gt_of_pullCount_gt_one
-    (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (stationaryEnv ν) P) (a : Fin K) :
+    (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P) (a : Fin K) :
     ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → K < n :=
   RoundRobin.time_gt_of_pullCount_gt_one (isAlgEnvSeqUntil_roundRobinAlgorithm h) a
 
 lemma pullCount_pos_of_pullCount_gt_one
-    (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (stationaryEnv ν) P) (a : Fin K) :
+    (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P) (a : Fin K) :
     ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → ∀ b : Fin K, 0 < pullCount A b n ω :=
   RoundRobin.pullCount_pos_of_pullCount_gt_one (isAlgEnvSeqUntil_roundRobinAlgorithm h) a
 
diff --git a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
index 3bbfc3a6..55061bff 100644
--- a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
+++ b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
@@ -225,7 +225,7 @@ lemma algFunction_map (alg : Algorithm Unit 𝓐 𝓡) (n : ℕ) (h : Hist Unit
 
 /-- The initial action is the image of a uniform random variable by `algFunction alg 0 default`. -/
 lemma algFunction_zero_map (alg : Algorithm Unit 𝓐 𝓡) :
-    volume.map (algFunction alg 0 default) = alg.p0 () :=
+    volume.map (algFunction alg 0 default) = alg.policyZero () :=
   algFunction_map alg 0 default
 
 @[fun_prop]
@@ -755,7 +755,7 @@ lemma hasCondDistrib_reward (alg : Algorithm Unit 𝓐 𝓡) (ν : Kernel 𝓐 
     (n : ℕ) :
     HasCondDistrib (reward alg n)
       (fun ω ↦ ((history (noObs _) (action alg) (reward alg) n ω, noObs _ n ω), action alg n ω))
-      ((stationaryEnv ν).feedback n) (arrayMeasure ν) := by
+      ((Environment.bandit ν).feedback n) (arrayMeasure ν) := by
   let e : (Hist Unit 𝓐 𝓡 n × 𝓐) ≃ᵐ ((Hist Unit 𝓐 𝓡 n × Unit) × 𝓐) :=
     { toFun := fun p ↦ ((p.1, ()), p.2)
       invFun := fun p ↦ (p.1.1, p.2)
@@ -763,13 +763,14 @@ lemma hasCondDistrib_reward (alg : Algorithm Unit 𝓐 𝓡) (ν : Kernel 𝓐 
       right_inv := fun _ ↦ rfl
       measurable_toFun := by simp only [Equiv.coe_fn_mk]; fun_prop
       measurable_invFun := by simp only [Equiv.symm_mk, Equiv.coe_fn_mk]; fun_prop }
-  rw [feedback_stationaryEnv]
+  rw [feedback_bandit]
   have h := (hasCondDistrib_reward' alg ν n).measurableEquiv_comp_right e
   simp only [hist_eq_history] at h
   exact h
 
 lemma isAlgEnvSeq_arrayMeasure (alg : Algorithm Unit 𝓐 𝓡) (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] :
-    IsAlgEnvSeq (noObs _) (action alg) (reward alg) alg (stationaryEnv ν) (arrayMeasure ν) where
+    IsAlgEnvSeq (noObs _) (action alg) (reward alg) alg (Environment.bandit ν)
+      (arrayMeasure ν) where
   hasCondDistrib_obs n :=
     hasCondDistrib_unit (measurable_history (fun _ ↦ measurable_const)
       (measurable_action alg) (measurable_reward alg) n).aemeasurable _ _
@@ -777,8 +778,9 @@ lemma isAlgEnvSeq_arrayMeasure (alg : Algorithm Unit 𝓐 𝓡) (ν : Kernel 
   hasCondDistrib_feedback := hasCondDistrib_reward alg ν
 
 lemma hasLaw_action_zero (alg : Algorithm Unit 𝓐 𝓡) (ν : Kernel 𝓐 𝓡) [IsMarkovKernel ν] :
-    HasLaw (action alg 0) (alg.p0 ()) (arrayMeasure ν) := by
-  have h : HasCondDistrib (action alg 0) (fun _ : probSpace 𝓐 𝓡 ↦ ()) alg.p0 (arrayMeasure ν) :=
+    HasLaw (action alg 0) (alg.policyZero ()) (arrayMeasure ν) := by
+  have h : HasCondDistrib (action alg 0) (fun _ : probSpace 𝓐 𝓡 ↦ ()) alg.policyZero
+      (arrayMeasure ν) :=
     (isAlgEnvSeq_arrayMeasure alg ν).hasCondDistrib_action_zero
   exact h.hasLaw_of_const'
 
@@ -786,7 +788,7 @@ lemma hasCondDistrib_reward_zero (alg : Algorithm Unit 𝓐 𝓡) (ν : Kernel 
     [IsMarkovKernel ν] :
     HasCondDistrib (reward alg 0) (action alg 0) ν (arrayMeasure ν) := by
   have h := (isAlgEnvSeq_arrayMeasure alg ν).hasCondDistrib_feedback_zero
-  rw [ν0_stationaryEnv] at h
+  rw [feedbackZero_bandit] at h
   simpa using hasCondDistrib_prodMk_left_unique_iff.mp h
 
 end Laws
diff --git a/LeanMachineLearning/Online/Bandit/BayesRegret.lean b/LeanMachineLearning/Online/Bandit/BayesRegret.lean
index 00210b41..c1a95147 100644
--- a/LeanMachineLearning/Online/Bandit/BayesRegret.lean
+++ b/LeanMachineLearning/Online/Bandit/BayesRegret.lean
@@ -17,7 +17,7 @@ measurable space `Ω`. These definitions are useful when `IsBayesAlgEnvSeq Q κ
 Recall that `IsBayesAlgEnvSeq Q κ alg E A Y P` states that there is a measure `P : Measure Ω` such
 that the parameter `E : Ω → 𝓔` has law `Q` and that the sequences of actions `A : ℕ → Ω → 𝓐` and
 feedbacks `Y : ℕ → Ω → 𝓨` are generated by the algorithm `alg : Algorithm 𝓐 𝓨` interacting with an
-underlying environment that depends on `E` and `κ` (`stationaryEnv (κ.sectR (E ω))`)
+underlying environment that depends on `E` and `κ` (`Environment.bandit (κ.sectR (E ω))`)
 
 ## Main definitions
 
diff --git a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
index fe804ee9..29e24b5a 100644
--- a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
+++ b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
@@ -22,7 +22,7 @@ namespace Bandits
 variable {𝓐 Ω : Type*} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐]
   {O : ℕ → Ω → Unit} {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {P : Measure Ω} [IsProbabilityMeasure P]
   {alg : Algorithm Unit 𝓐 ℝ} {ν : Kernel 𝓐 ℝ} [IsMarkovKernel ν]
-  {h_inter : IsAlgEnvSeq O A R alg (stationaryEnv ν) P}
+  {h_inter : IsAlgEnvSeq O A R alg (Environment.bandit ν) P}
 
 local notation "𝔓" => P.prod (streamMeasure ν)
 
@@ -35,11 +35,11 @@ notation "𝓛[" Y " | " X " ← " x "; " μ "]" => Measure.map Y (μ[|X ⁻¹'
 
 omit [DecidableEq 𝓐] in
 lemma condDistrib_reward'' [Countable 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (n : ℕ) :
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (n : ℕ) :
     𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1; 𝔓] =ᵐ[(𝔓).map (fun ω ↦ A n ω.1)] ν := by
   have hA := h.measurable_action
   have hR := h.measurable_feedback
-  have h_ra' : 𝓛[R n | A n; P] =ᵐ[P.map (A n)] ν := h.condDistrib_feedback_stationaryEnv n
+  have h_ra' : 𝓛[R n | A n; P] =ᵐ[P.map (A n)] ν := h.condDistrib_feedback_bandit n
   have h_law : (𝔓).map (fun ω ↦ A n ω.1) = P.map (A n) := by
     change ((𝔓).map (A n ∘ Prod.fst)) = _
     rw [← Measure.map_map (by fun_prop) (by fun_prop), ← Measure.fst, Measure.fst_prod]
@@ -56,7 +56,7 @@ variable [StandardBorelSpace 𝓐]
 
 omit [DecidableEq 𝓐] in
 lemma reward_cond_action [Countable 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (a : 𝓐) (n : ℕ)
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (n : ℕ)
     (hμa : (𝔓).map (fun ω ↦ A n ω.1) {a} ≠ 0) :
     𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1 ← a; 𝔓] = ν a := by
   have hA := h.measurable_action
@@ -74,7 +74,7 @@ lemma reward_cond_action [Countable 𝓐]
 variable [Nonempty 𝓐]
 
 lemma condIndepFun_reward_stepsUntil_action' [StandardBorelSpace Ω]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (a : 𝓐) (m n : ℕ) :
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (m n : ℕ) :
     R n ⟂ᵢ[A n, h.measurable_action n; P] {ω | stepsUntil A a m ω = ↑n}.indicator (fun _ ↦ 1) := by
   -- the indicator of `stepsUntil ... = n` is a function of `hist (n-1)` and `action n`.
   -- It thus suffices to use the independence of `reward n` and `hist (n-1)` conditionally
@@ -83,12 +83,12 @@ lemma condIndepFun_reward_stepsUntil_action' [StandardBorelSpace Ω]
   have hR := h.measurable_feedback
   have h_indep : R n ⟂ᵢ[A n, hA n; P]
       fun ω ↦ ((history O A R n ω, O n ω), A n ω) :=
-    IsAlgEnvSeq.condIndepFun_feedback_history_action_action h n
+    IsAlgEnvSeq.condIndepFun_feedback_history_action_action_bandit h n
   refine h_indep.of_measurable_right (hX := hA n) ?_
   exact measurable_comap_indicator_stepsUntil_eq O R a m n
 
 lemma condIndepFun_reward_stepsUntil_action [StandardBorelSpace Ω] [Countable 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     (a : 𝓐) (m n : ℕ) :
     CondIndepFun (m𝓐.comap (fun ω ↦ A n ω.1)) ((h.measurable_action n).comp measurable_fst).comap_le
       (fun ω ↦ R n ω.1) ({ω | stepsUntil A a m ω.1 = ↑n}.indicator (fun _ ↦ 1)) 𝔓 := by
@@ -99,7 +99,7 @@ lemma condIndepFun_reward_stepsUntil_action [StandardBorelSpace Ω] [Countable 
     (condIndepFun_reward_stepsUntil_action' h a m n)
 
 lemma reward_cond_stepsUntil [StandardBorelSpace Ω] [Countable 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (a : 𝓐) (m n : ℕ)
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (m n : ℕ)
     (hm : m ≠ 0) (hμn : 𝔓 ((fun ω ↦ stepsUntil A a m ω.1) ⁻¹' {↑n}) ≠ 0) :
     𝓛[fun ω ↦ R n ω.1 | fun ω ↦ stepsUntil A a m ω.1 ← ↑n; 𝔓] = ν a := by
   have hA := h.measurable_action
@@ -145,7 +145,7 @@ lemma reward_cond_stepsUntil [StandardBorelSpace Ω] [Countable 𝓐]
 /-- The conditional distribution of the reward received at the `m`-th pull of action `a`
 given the time at which number of pulls is `m` is the constant kernel with value `ν a`. -/
 lemma condDistrib_rewardByCount_stepsUntil [StandardBorelSpace Ω] [Countable 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (a : 𝓐) (m : ℕ) (hm : m ≠ 0) :
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (m : ℕ) (hm : m ≠ 0) :
     condDistrib (rewardByCount A R a m) (fun ω ↦ stepsUntil A a m ω.1) 𝔓
       =ᵐ[(𝔓).map (fun ω ↦ stepsUntil A a m ω.1)] Kernel.const _ (ν a) := by
   have hA := h.measurable_action
@@ -178,7 +178,7 @@ lemma condDistrib_rewardByCount_stepsUntil [StandardBorelSpace Ω] [Countable 
 
 /-- The reward received at the `m`-th pull of action `a` has law `ν a`. -/
 lemma hasLaw_rewardByCount [StandardBorelSpace Ω] [Countable 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (a : 𝓐) (m : ℕ) (hm : m ≠ 0) :
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (m : ℕ) (hm : m ≠ 0) :
     HasLaw (rewardByCount A R a m) (ν a) 𝔓 where
   aemeasurable :=
     (measurable_rewardByCount h.measurable_action h.measurable_feedback a m).aemeasurable
@@ -198,7 +198,7 @@ lemma hasLaw_rewardByCount [StandardBorelSpace Ω] [Countable 𝓐]
     _ = ν a := by simp
 
 lemma identDistrib_rewardByCount [StandardBorelSpace Ω] [Countable 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (a : 𝓐) (n m : ℕ)
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (n m : ℕ)
     (hn : n ≠ 0) (hm : m ≠ 0) :
     IdentDistrib (rewardByCount A R a n) (rewardByCount A R a m) 𝔓 𝔓 where
   aemeasurable_fst :=
@@ -208,7 +208,7 @@ lemma identDistrib_rewardByCount [StandardBorelSpace Ω] [Countable 𝓐]
   map_eq := by rw [(hasLaw_rewardByCount h a n hn).map_eq, (hasLaw_rewardByCount h a m hm).map_eq]
 
 lemma identDistrib_rewardByCount_id [StandardBorelSpace Ω] [Countable 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (a : 𝓐) (n : ℕ) (hn : n ≠ 0) :
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (n : ℕ) (hn : n ≠ 0) :
     IdentDistrib (rewardByCount A R a n) id 𝔓 (ν a) where
   aemeasurable_fst :=
     (measurable_rewardByCount h.measurable_action h.measurable_feedback a n).aemeasurable
@@ -216,7 +216,7 @@ lemma identDistrib_rewardByCount_id [StandardBorelSpace Ω] [Countable 𝓐]
   map_eq := by rw [(hasLaw_rewardByCount h a n hn).map_eq, Measure.map_id]
 
 lemma identDistrib_rewardByCount_eval [StandardBorelSpace Ω] [Countable 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (a : 𝓐) (n m : ℕ) (hn : n ≠ 0) :
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (n m : ℕ) (hn : n ≠ 0) :
     IdentDistrib (rewardByCount A R a n) (fun ω ↦ ω m a) 𝔓 (streamMeasure ν) :=
   (identDistrib_rewardByCount_id h a n hn).trans
     (identDistrib_eval_eval_id_streamMeasure ν m a).symm
@@ -282,24 +282,25 @@ lemma indepFun_update_rewardByCountUntil_eval [Countable 𝓐] (hA : ∀ n, Meas
 /-- Conditionally on the event that the action at time `n` is `b` and that `b` was pulled `k`
 times before, the reward at time `n` is independent of the history before time `n` and of the
 action at time `n`. -/
-lemma indepFun_history_reward_cond (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+lemma indepFun_history_reward_cond (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     (n : ℕ) (b : 𝓐) (k : ℕ) :
     (fun x ↦ ((history O A R n x, O n x), A n x))
       ⟂ᵢ[P[|{x | A n x = b ∧ pullCount A b n x = k}]] R n := by
   rw [setOf_action_eq_and_pullCount_eq_eq_preimage (O := O) (R' := R)]
-  exact h.indepFun_history_action_feedback_cond_stationaryEnv n
+  exact h.indepFun_history_action_feedback_cond_bandit n
     (measurableSet_snd_eq_and_pullCount'_eq n b k) fun u hu ↦ hu.1
 
 /-- Conditionally on the event that the action at time `t` is `b` and that `b` was pulled `k`
 times before, the reward at time `t` has law `ν b`. -/
-lemma hasLaw_reward_cond (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (t : ℕ) (b : 𝓐) (k : ℕ)
+lemma hasLaw_reward_cond (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (t : ℕ) (b : 𝓐)
+    (k : ℕ)
     (hP : P {x | A t x = b ∧ pullCount A b t x = k} ≠ 0) :
     HasLaw (R t) (ν b) (P[|{x | A t x = b ∧ pullCount A b t x = k}]) := by
   rw [setOf_action_eq_and_pullCount_eq_eq_preimage (O := O) (R' := R)] at hP ⊢
-  exact h.hasLaw_feedback_cond_stationaryEnv t (measurableSet_snd_eq_and_pullCount'_eq t b k)
+  exact h.hasLaw_feedback_cond_bandit t (measurableSet_snd_eq_and_pullCount'_eq t b k)
     (fun u hu ↦ hu.1) hP
 
-lemma hasLaw_reward_cond_prod (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (t : ℕ) (b : 𝓐)
+lemma hasLaw_reward_cond_prod (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (t : ℕ) (b : 𝓐)
     (k : ℕ) (hP : P {x | A t x = b ∧ pullCount A b t x = k} ≠ 0) :
     HasLaw (fun ω ↦ R t ω.1) (ν b)
       ((P[|{x | A t x = b ∧ pullCount A b t x = k}]).prod (streamMeasure ν)) :=
@@ -310,7 +311,7 @@ variable [Countable 𝓐]
 /-- Conditionally on the event that the action at time `t` is `b` and that `b` was pulled `k`
 times before, the array `rewardByCountUntil A R t` with the entry `(b, k)` erased is independent of
 the reward at time `t`. -/
-lemma indepFun_update_rewardByCountUntil_reward (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+lemma indepFun_update_rewardByCountUntil_reward (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     (t : ℕ) (b : 𝓐) (k : ℕ) :
     (fun ω ↦ Function.update (rewardByCountUntil A R t ω) (b, k) 0)
       ⟂ᵢ[(P[|{x | A t x = b ∧ pullCount A b t x = k}]).prod (streamMeasure ν)]
@@ -343,7 +344,8 @@ lemma indepFun_update_rewardByCountUntil_reward (h : IsAlgEnvSeq O A R alg (stat
 times before, the arrays `rewardByCountUntil A R (t + 1)` and `rewardByCountUntil A R t` have the
 same law: they differ only in the entry `(b, k)`, which is `R t` in the first and an auxiliary
 reward in the second, and both are independent of the rest of the array with law `ν b`. -/
-lemma identDistrib_rewardByCountUntil_add_one_cond (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+lemma identDistrib_rewardByCountUntil_add_one_cond
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     (t : ℕ) (b : 𝓐) (k : ℕ) :
     IdentDistrib (rewardByCountUntil A R (t + 1)) (rewardByCountUntil A R t)
       ((P[|{x | A t x = b ∧ pullCount A b t x = k}]).prod (streamMeasure ν))
@@ -399,7 +401,7 @@ lemma identDistrib_rewardByCountUntil_add_one_cond (h : IsAlgEnvSeq O A R alg (s
     (IdentDistrib.of_ae_eq (measurable_rewardByCountUntil hA hR _).aemeasurable h2).symm
 
 /-- The law of `rewardByCountUntil A R t` under `𝔓` does not depend on `t`. -/
-lemma identDistrib_rewardByCountUntil_add_one (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+lemma identDistrib_rewardByCountUntil_add_one (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     (t : ℕ) :
     IdentDistrib (rewardByCountUntil A R (t + 1)) (rewardByCountUntil A R t) 𝔓 𝔓 := by
   have hA := h.measurable_action
@@ -424,7 +426,7 @@ lemma identDistrib_rewardByCountUntil_add_one (h : IsAlgEnvSeq O A R alg (statio
   exact identDistrib_rewardByCountUntil_add_one_cond h t p.1 p.2
 
 /-- The law of `rewardByCountUntil A R t` under `𝔓` is `⨂ (a, m), ν a`, for all `t`. -/
-lemma hasLaw_rewardByCountUntil (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (t : ℕ) :
+lemma hasLaw_rewardByCountUntil (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (t : ℕ) :
     HasLaw (rewardByCountUntil A R t) (Measure.infinitePi fun p : 𝓐 × ℕ ↦ ν p.1) 𝔓 := by
   induction t with
   | zero => exact hasLaw_rewardByCountUntil_zero P
@@ -432,7 +434,7 @@ lemma hasLaw_rewardByCountUntil (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
 
 /-- The array of rewards by count `(a, m) ↦ rewardByCount A R a (m + 1)` has law
 `⨂ (a, m), ν a`: its entries are independent, and the entry `(a, m)` has law `ν a`. -/
-lemma hasLaw_rewardByCount_infinitePi (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) :
+lemma hasLaw_rewardByCount_infinitePi (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) :
     HasLaw (fun ω (p : 𝓐 × ℕ) ↦ rewardByCount A R p.1 (p.2 + 1) ω)
       (Measure.infinitePi fun p : 𝓐 × ℕ ↦ ν p.1) 𝔓 := by
   have hY : Measurable fun ω (p : 𝓐 × ℕ) ↦ rewardByCount A R p.1 (p.2 + 1) ω :=
@@ -444,14 +446,14 @@ lemma hasLaw_rewardByCount_infinitePi (h : IsAlgEnvSeq O A R alg (stationaryEnv
     (hasLaw_rewardByCountUntil h) eventually_rewardByCountUntil_eq
 
 /-- The reward received at the `(m + 1)`-th pull of action `a` has law `ν a`. -/
-lemma hasLaw_rewardByCount_add_one (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+lemma hasLaw_rewardByCount_add_one (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     (a : 𝓐) (m : ℕ) :
     HasLaw (rewardByCount A R a (m + 1)) (ν a) 𝔓 :=
   (hasLaw_eval_infinitePi (fun p : 𝓐 × ℕ ↦ ν p.1) (a, m)).comp (hasLaw_rewardByCount_infinitePi h)
 
 /-- The rewards by count `rewardByCount A R a (m + 1)` are independent over all actions `a` and
 all counts `m`. -/
-lemma iIndepFun_rewardByCount_add_one (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) :
+lemma iIndepFun_rewardByCount_add_one (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) :
     iIndepFun (fun (p : 𝓐 × ℕ) ω ↦ rewardByCount A R p.1 (p.2 + 1) ω) 𝔓 :=
   (iIndepFun_iff_hasLaw_Pi_infinitePi
     (X := fun (p : 𝓐 × ℕ) ω ↦ rewardByCount A R p.1 (p.2 + 1) ω) (μ := fun p : 𝓐 × ℕ ↦ ν p.1)
@@ -460,7 +462,7 @@ lemma iIndepFun_rewardByCount_add_one (h : IsAlgEnvSeq O A R alg (stationaryEnv
 
 /-- The rewards by count `rewardByCount A R a m` for `m ≠ 0` are independent over all actions `a`
 and all counts `m`. -/
-lemma iIndepFun_rewardByCount (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) :
+lemma iIndepFun_rewardByCount (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) :
     iIndepFun (fun (p : {p : 𝓐 × ℕ // p.2 ≠ 0}) ω ↦ rewardByCount A R p.1.1 p.1.2 ω) 𝔓 := by
   have h_eq : (fun (p : {p : 𝓐 × ℕ // p.2 ≠ 0}) ω ↦ rewardByCount A R p.1.1 p.1.2 ω)
       = fun p ω ↦ rewardByCount A R p.1.1 (p.1.2 - 1 + 1) ω := by
@@ -474,14 +476,14 @@ lemma iIndepFun_rewardByCount (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) :
 
 /-- For each action `a`, the rewards by count `(rewardByCount A R a (m + 1))_m` are independent
 (and by `hasLaw_rewardByCount_add_one` identically distributed with law `ν a`). -/
-lemma iIndepFun_rewardByCount_add_one_action (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+lemma iIndepFun_rewardByCount_add_one_action (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     (a : 𝓐) :
     iIndepFun (fun m ω ↦ rewardByCount A R a (m + 1) ω) 𝔓 :=
   (iIndepFun_rewardByCount_add_one h).precomp (g := fun m ↦ (a, m))
     fun _ _ hmn ↦ (Prod.mk.inj hmn).2
 
 /-- Two distinct rewards by count are independent. -/
-lemma indepFun_rewardByCount (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+lemma indepFun_rewardByCount (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     {a b : 𝓐} {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) (hne : (a, m) ≠ (b, n)) :
     rewardByCount A R a m ⟂ᵢ[𝔓] rewardByCount A R b n :=
   (iIndepFun_rewardByCount h).indepFun (i := ⟨(a, m), hm⟩) (j := ⟨(b, n), hn⟩)
diff --git a/LeanMachineLearning/Online/Bandit/SumRewards.lean b/LeanMachineLearning/Online/Bandit/SumRewards.lean
index 0263c221..1e9221dd 100644
--- a/LeanMachineLearning/Online/Bandit/SumRewards.lean
+++ b/LeanMachineLearning/Online/Bandit/SumRewards.lean
@@ -157,8 +157,8 @@ lemma pullCount_eq_comp :
 
 -- todo: write those lemmas with IdentDistrib instead of equality of maps
 lemma _root_.Learning.IsAlgEnvSeq.law_sumRewards_unique [MeasurableSingletonClass 𝓐]
-    (h1 : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
-    (h2 : IsAlgEnvSeq O₂ A₂ R₂ alg (stationaryEnv ν) P') :
+    (h1 : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
+    (h2 : IsAlgEnvSeq O₂ A₂ R₂ alg (Environment.bandit ν) P') :
     P.map (sumRewards A R a n) = P'.map (sumRewards A₂ R₂ a n) := by
   have hA := h1.measurable_action
   have hR := h1.measurable_feedback
@@ -175,8 +175,8 @@ lemma _root_.Learning.IsAlgEnvSeq.law_sumRewards_unique [MeasurableSingletonClas
   · fun_prop
 
 lemma _root_.Learning.IsAlgEnvSeq.law_pullCount_sumRewards_unique' [MeasurableSingletonClass 𝓐]
-    (h1 : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
-    (h2 : IsAlgEnvSeq O₂ A₂ R₂ alg (stationaryEnv ν) P') :
+    (h1 : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
+    (h2 : IsAlgEnvSeq O₂ A₂ R₂ alg (Environment.bandit ν) P') :
     IdentDistrib (fun ω a ↦ (pullCount A a n ω, sumRewards A R a n ω))
       (fun ω a ↦ (pullCount A₂ a n ω, sumRewards A₂ R₂ a n ω)) P P' := by
   have hO := h1.measurable_obs
@@ -222,15 +222,15 @@ lemma _root_.Learning.IsAlgEnvSeq.law_pullCount_sumRewards_unique' [MeasurableSi
   · fun_prop
 
 lemma _root_.Learning.IsAlgEnvSeq.law_pullCount_sumRewards_unique [MeasurableSingletonClass 𝓐]
-    (h1 : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
-    (h2 : IsAlgEnvSeq O₂ A₂ R₂ alg (stationaryEnv ν) P') :
+    (h1 : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
+    (h2 : IsAlgEnvSeq O₂ A₂ R₂ alg (Environment.bandit ν) P') :
     P.map (fun ω ↦ (pullCount A a n ω, sumRewards A R a n ω)) =
       P'.map (fun ω ↦ (pullCount A₂ a n ω, sumRewards A₂ R₂ a n ω)) :=
   ((h1.law_pullCount_sumRewards_unique' h2 (n := n)).comp (u := fun f ↦ f a) (by fun_prop)).map_eq
 
 lemma _root_.Learning.IsAlgEnvSeq.identDistrib_pullCount_sumRewards [MeasurableSingletonClass 𝓐]
-    (h1 : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
-    (h2 : IsAlgEnvSeq O₂ A₂ R₂ alg (stationaryEnv ν) P') :
+    (h1 : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
+    (h2 : IsAlgEnvSeq O₂ A₂ R₂ alg (Environment.bandit ν) P') :
     IdentDistrib (fun ω n a ↦ (pullCount A a n ω, sumRewards A R a n ω))
       (fun ω' n a ↦ (pullCount A₂ a n ω', sumRewards A₂ R₂ a n ω')) P P' := by
   let f (τ : ℕ → Round Unit 𝓐 ℝ) (n : ℕ) (a : 𝓐) : ℕ × ℝ :=
@@ -263,7 +263,7 @@ variable [Nonempty 𝓐]
 
 -- this is what we will use for UCB
 lemma prob_pullCount_prod_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     {s : Set (ℕ × ℝ)} [DecidablePred (· ∈ Prod.fst '' s)] (hs : MeasurableSet s) :
     P {ω | (pullCount A a n ω, sumRewards A R a n ω) ∈ s} ≤
       ∑ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s),
@@ -289,7 +289,7 @@ property `p` holds for the number of pulls and the sum of rewards of action `a`
 least one pull, is at most `n` times a uniform bound on the probability of that property for the
 sums of `k ∈ [1, n]` i.i.d. rewards. -/
 lemma prob_pullCount_pos_and_le [Countable 𝓐] [MeasurableSingletonClass 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (a : 𝓐) (n : ℕ)
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (n : ℕ)
     {p : ℕ → ℝ → Prop} (hp : Measurable fun q : ℕ × ℝ ↦ p q.1 q.2) {B : ℝ≥0∞}
     (hB : ∀ k, k ≠ 0 → streamMeasure ν {ω | p k (∑ i ∈ range k, ω i a)} ≤ B) :
     P {ω | 0 < pullCount A a n ω ∧ p (pullCount A a n ω) (sumRewards A R a n ω)} ≤ n * B := by
@@ -313,7 +313,7 @@ lemma prob_pullCount_pos_and_le [Countable 𝓐] [MeasurableSingletonClass 𝓐]
   _ = n * B := by simp
 
 lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     {s : Set ℕ} [DecidablePred (· ∈ s)] (hs : MeasurableSet s) {B : Set ℝ} (hB : MeasurableSet B) :
     P {ω | pullCount A a n ω ∈ s ∧ sumRewards A R a n ω ∈ B} ≤
       ∑ k ∈ (range (n + 1)).filter (· ∈ s),
@@ -332,7 +332,7 @@ lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable 𝓐] [MeasurableSingl
     simp [hk.2.1]
 
 lemma prob_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     {B : Set ℝ} (hB : MeasurableSet B) :
     P (sumRewards A R a n ⁻¹' B) ≤
       ∑ k ∈ range (n + 1), streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by
@@ -343,7 +343,7 @@ lemma prob_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐]
   rfl
 
 lemma prob_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     {m : ℕ} (hm : m ≤ n) {B : Set ℝ} (hB : MeasurableSet B) :
     P {ω | pullCount A a n ω = m ∧ sumRewards A R a n ω ∈ B} ≤
       streamMeasure ν {ω | ∑ i ∈ range m, ω i a ∈ B} := by
@@ -352,7 +352,7 @@ lemma prob_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] [MeasurableSingle
   simpa [hm'] using h_le
 
 lemma prob_exists_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (a : 𝓐) (m : ℕ) {B : Set ℝ}
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (m : ℕ) {B : Set ℝ}
     (hB : MeasurableSet B) :
     P {ω | ∃ n, pullCount A a n ω = m ∧ sumRewards A R a n ω ∈ B} ≤
       streamMeasure ν {ω | ∑ i ∈ range m, ω i a ∈ B} :=
@@ -369,7 +369,7 @@ lemma prob_exists_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] [Measurabl
     _ ≤ _ := ArrayModel.prob_exists_pullCount_eq_and_sumRewards_mem_le a m hB
 
 lemma probReal_sumRewards_le_sumRewards_le [Fintype 𝓐] [MeasurableSingletonClass 𝓐]
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P)
     (a : 𝓐) (n m₁ m₂ : ℕ) :
     P.real {ω | pullCount A (bestArm ν) n ω = m₁ ∧ pullCount A a n ω = m₂ ∧
         sumRewards A R (bestArm ν) n ω ≤ sumRewards A R a n ω} ≤
@@ -468,7 +468,7 @@ end StreamMeasure
 
 lemma prob_sumRewards_sub_pullCount_mul_ge_le [Countable 𝓐] [MeasurableSingletonClass 𝓐]
     {σ2 : ℝ≥0} (hσ2 : 0 < σ2) (ha : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) {δ : ℝ} (hδ : 0 < δ) :
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) {δ : ℝ} (hδ : 0 < δ) :
     P {ω | ∃ t < n, pullCount A a t ω ≠ 0 ∧ √(2 * pullCount A a t ω * σ2 * Real.log (1 / δ)) ≤
       sumRewards A R a t ω - pullCount A a t ω * (ν a)[id]} ≤ ENNReal.ofReal ((n - 1) * δ) :=
   let B (m : ℕ) := {x : ℝ | √(2 * m * σ2 * Real.log (1 / δ)) ≤ x - m * (ν a)[id]}
@@ -502,7 +502,7 @@ lemma prob_sumRewards_sub_pullCount_mul_ge_le [Countable 𝓐] [MeasurableSingle
 
 lemma prob_sumRewards_sub_pullCount_mul_le_le [Countable 𝓐] [MeasurableSingletonClass 𝓐]
     {σ2 : ℝ≥0} (hσ2 : 0 < σ2) (ha : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) {δ : ℝ} (hδ : 0 < δ) :
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) {δ : ℝ} (hδ : 0 < δ) :
     P {ω | ∃ t < n, pullCount A a t ω ≠ 0 ∧
       sumRewards A R a t ω - pullCount A a t ω * (ν a)[id] ≤
         -√(2 * pullCount A a t ω * σ2 * Real.log (1 / δ))} ≤ ENNReal.ofReal ((n - 1) * δ) :=
@@ -537,7 +537,7 @@ lemma prob_sumRewards_sub_pullCount_mul_le_le [Countable 𝓐] [MeasurableSingle
 
 lemma prob_sumRewards_sub_pullCount_mul_ge_le_of_Fintype [Fintype 𝓐] [MeasurableSingletonClass 𝓐]
     {σ2 : ℝ≥0} (hσ2 : 0 < σ2) (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
-    (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) {δ : ℝ} (hδ : 0 < δ) :
+    (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) {δ : ℝ} (hδ : 0 < δ) :
     P {ω | ∃ a, ∃ t < n, pullCount A a t ω ≠ 0 ∧
         √(2 * pullCount A a t ω * σ2 * Real.log (1 / δ)) ≤
           sumRewards A R a t ω - pullCount A a t ω * (ν a)[id]} ≤
diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean
index 3185a206..20159435 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithm.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean
@@ -151,47 +151,48 @@ lemma measurable_environment_iff (f : Ω → Environment 𝓞 𝓐 𝓨) :
 
 /-- Distribution of the first observation: the observation kernel at time `0` applied to the empty
 history. -/
-def Environment.obs0 (env : Environment 𝓞 𝓐 𝓨) : Measure 𝓞 :=
+def Environment.obsZero (env : Environment 𝓞 𝓐 𝓨) : Measure 𝓞 :=
   env.obs 0 default
 deriving IsProbabilityMeasure
 
-lemma Environment.obs0_def (env : Environment 𝓞 𝓐 𝓨) : env.obs0 = env.obs 0 default := rfl
+lemma Environment.obsZero_def (env : Environment 𝓞 𝓐 𝓨) : env.obsZero = env.obs 0 default := rfl
 
 lemma Environment.obs_zero (env : Environment 𝓞 𝓐 𝓨) (h : Hist 𝓞 𝓐 𝓨 0) :
-    env.obs 0 h = env.obs0 := by
+    env.obs 0 h = env.obsZero := by
   rw [Unique.eq_default h]
   rfl
 
 /-- Distribution of the first action given the first observation: the policy at time `0` applied to
 the empty history. -/
-noncomputable def Algorithm.p0 (alg : Algorithm 𝓞 𝓐 𝓨) : Kernel 𝓞 𝓐 :=
+noncomputable def Algorithm.policyZero (alg : Algorithm 𝓞 𝓐 𝓨) : Kernel 𝓞 𝓐 :=
   (alg.policy 0).sectR default
 deriving IsMarkovKernel
 
-lemma Algorithm.p0_def (alg : Algorithm 𝓞 𝓐 𝓨) : alg.p0 = (alg.policy 0).sectR default := rfl
+lemma Algorithm.policyZero_def (alg : Algorithm 𝓞 𝓐 𝓨) :
+    alg.policyZero = (alg.policy 0).sectR default := rfl
 
-lemma Algorithm.p0_apply (alg : Algorithm 𝓞 𝓐 𝓨) (o : 𝓞) :
-    alg.p0 o = alg.policy 0 (default, o) := rfl
+lemma Algorithm.policyZero_apply (alg : Algorithm 𝓞 𝓐 𝓨) (o : 𝓞) :
+    alg.policyZero o = alg.policy 0 (default, o) := rfl
 
 lemma Algorithm.policy_zero (alg : Algorithm 𝓞 𝓐 𝓨) (h : Hist 𝓞 𝓐 𝓨 0) (o : 𝓞) :
-    alg.policy 0 (h, o) = alg.p0 o := by
+    alg.policy 0 (h, o) = alg.policyZero o := by
   rw [Unique.eq_default h]
   rfl
 
 /-- Distribution of the first feedback given the first observation and action: the feedback kernel
 at time `0` applied to the empty history. -/
-noncomputable def Environment.ν0 (env : Environment 𝓞 𝓐 𝓨) : Kernel (𝓞 × 𝓐) 𝓨 :=
+noncomputable def Environment.feedbackZero (env : Environment 𝓞 𝓐 𝓨) : Kernel (𝓞 × 𝓐) 𝓨 :=
   (env.feedback 0).comap (fun p ↦ ((default, p.1), p.2)) (by fun_prop)
 deriving IsMarkovKernel
 
-lemma Environment.ν0_def (env : Environment 𝓞 𝓐 𝓨) :
-    env.ν0 = (env.feedback 0).comap (fun p ↦ ((default, p.1), p.2)) (by fun_prop) := rfl
+lemma Environment.feedbackZero_def (env : Environment 𝓞 𝓐 𝓨) :
+    env.feedbackZero = (env.feedback 0).comap (fun p ↦ ((default, p.1), p.2)) (by fun_prop) := rfl
 
-lemma Environment.ν0_apply (env : Environment 𝓞 𝓐 𝓨) (o : 𝓞) (a : 𝓐) :
-    env.ν0 (o, a) = env.feedback 0 ((default, o), a) := rfl
+lemma Environment.feedbackZero_apply (env : Environment 𝓞 𝓐 𝓨) (o : 𝓞) (a : 𝓐) :
+    env.feedbackZero (o, a) = env.feedback 0 ((default, o), a) := rfl
 
 lemma Environment.feedback_zero (env : Environment 𝓞 𝓐 𝓨) (h : Hist 𝓞 𝓐 𝓨 0) (o : 𝓞) (a : 𝓐) :
-    env.feedback 0 ((h, o), a) = env.ν0 (o, a) := by
+    env.feedback 0 ((h, o), a) = env.feedbackZero (o, a) := by
   rw [Unique.eq_default h]
   rfl
 
@@ -211,7 +212,7 @@ lemma fst_stepKernel (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 
   rw [stepKernel, Kernel.fst_compProd]
 
 lemma stepKernel_zero (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (h : Hist 𝓞 𝓐 𝓨 0) :
-    stepKernel alg env 0 h = env.obs0 ⊗ₘ (alg.p0 ⊗ₖ env.ν0) := by
+    stepKernel alg env 0 h = env.obsZero ⊗ₘ (alg.policyZero ⊗ₖ env.feedbackZero) := by
   rw [Unique.eq_default h, stepKernel, Kernel.compProd_apply_eq_compProd_sectR]
   congr 1
   ext o s hs
@@ -475,30 +476,30 @@ lemma hasLaw_history_zero (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y
   map_eq := by rw [history_zero, Measure.map_const, measure_univ, one_smul]
 
 lemma IsAlgEnvSeqUntil.hasLaw_obs_zero (h : IsAlgEnvSeqUntil O A Y alg env P N) (hN : 0 < N) :
-    HasLaw (O 0) env.obs0 P := by
+    HasLaw (O 0) env.obsZero P := by
   have h0 := h.hasCondDistrib_obs 0 hN
   rw [history_zero] at h0
   exact h0.hasLaw_of_const'
 
 lemma IsAlgEnvSeq.hasLaw_obs_zero (h : IsAlgEnvSeq O A Y alg env P) :
-    HasLaw (O 0) env.obs0 P :=
+    HasLaw (O 0) env.obsZero P :=
   (h.isAlgEnvSeqUntil 1).hasLaw_obs_zero zero_lt_one
 
 omit [IsProbabilityMeasure P] in
 lemma IsAlgEnvSeqUntil.hasCondDistrib_action_zero (h : IsAlgEnvSeqUntil O A Y alg env P N)
     (hN : 0 < N) :
-    HasCondDistrib (A 0) (O 0) alg.p0 P :=
+    HasCondDistrib (A 0) (O 0) alg.policyZero P :=
   hasCondDistrib_prodMk_left_unique_iff.mp (h.hasCondDistrib_action 0 hN)
 
 omit [IsProbabilityMeasure P] in
 lemma IsAlgEnvSeq.hasCondDistrib_action_zero (h : IsAlgEnvSeq O A Y alg env P) :
-    HasCondDistrib (A 0) (O 0) alg.p0 P :=
+    HasCondDistrib (A 0) (O 0) alg.policyZero P :=
   (h.isAlgEnvSeqUntil 1).hasCondDistrib_action_zero zero_lt_one
 
 omit [IsProbabilityMeasure P] in
 lemma IsAlgEnvSeqUntil.hasCondDistrib_feedback_zero (h : IsAlgEnvSeqUntil O A Y alg env P N)
     (hN : 0 < N) :
-    HasCondDistrib (Y 0) (fun ω ↦ (O 0 ω, A 0 ω)) env.ν0 P := by
+    HasCondDistrib (Y 0) (fun ω ↦ (O 0 ω, A 0 ω)) env.feedbackZero P := by
   have h0 := h.hasCondDistrib_feedback 0 hN
   rw [history_zero] at h0
   exact h0.of_measurableEmbedding_comp_right
@@ -506,18 +507,18 @@ lemma IsAlgEnvSeqUntil.hasCondDistrib_feedback_zero (h : IsAlgEnvSeqUntil O A Y
 
 omit [IsProbabilityMeasure P] in
 lemma IsAlgEnvSeq.hasCondDistrib_feedback_zero (h : IsAlgEnvSeq O A Y alg env P) :
-    HasCondDistrib (Y 0) (fun ω ↦ (O 0 ω, A 0 ω)) env.ν0 P :=
+    HasCondDistrib (Y 0) (fun ω ↦ (O 0 ω, A 0 ω)) env.feedbackZero P :=
   (h.isAlgEnvSeqUntil 1).hasCondDistrib_feedback_zero zero_lt_one
 
 lemma IsAlgEnvSeqUntil.hasLaw_step_zero (h : IsAlgEnvSeqUntil O A Y alg env P N) (hN : 0 < N) :
-    HasLaw (step O A Y 0) (env.obs0 ⊗ₘ (alg.p0 ⊗ₖ env.ν0)) P := by
+    HasLaw (step O A Y 0) (env.obsZero ⊗ₘ (alg.policyZero ⊗ₖ env.feedbackZero)) P := by
   have h0 := h.hasCondDistrib_step 0 hN
   rw [history_zero] at h0
   rw [← stepKernel_zero alg env default]
   exact h0.hasLaw_of_const'
 
 lemma IsAlgEnvSeq.hasLaw_step_zero (h : IsAlgEnvSeq O A Y alg env P) :
-    HasLaw (step O A Y 0) (env.obs0 ⊗ₘ (alg.p0 ⊗ₖ env.ν0)) P :=
+    HasLaw (step O A Y 0) (env.obsZero ⊗ₘ (alg.policyZero ⊗ₖ env.feedbackZero)) P :=
   (h.isAlgEnvSeqUntil 1).hasLaw_step_zero zero_lt_one
 
 end Zero
@@ -539,11 +540,11 @@ lemma IsAlgEnvSeq.hasLaw_step_comp (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
     HasLaw (step O A Y n) (stepKernel alg env n ∘ₘ (P.map (history O A Y n))) P :=
   HasCondDistrib.hasLaw_comp (h.hasCondDistrib_step n)
 
-/-- Conditionally on the event `(O 0, A 0) = p`, the first feedback has law `env.ν0 p`. -/
+/-- Conditionally on the event `(O 0, A 0) = p`, the first feedback has law `env.feedbackZero p`. -/
 lemma IsAlgEnvSeq.hasLaw_feedback_zero_cond [MeasurableSingletonClass 𝓞]
     [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A Y alg env P) {p : 𝓞 × 𝓐}
     (hP : P ((fun ω ↦ (O 0 ω, A 0 ω)) ⁻¹' {p}) ≠ 0) :
-    HasLaw (Y 0) (env.ν0 p) P[|(fun ω ↦ (O 0 ω, A 0 ω)) ⁻¹' {p}] :=
+    HasLaw (Y 0) (env.feedbackZero p) P[|(fun ω ↦ (O 0 ω, A 0 ω)) ⁻¹' {p}] :=
   h.hasCondDistrib_feedback_zero.hasLaw_cond (h.measurable_feedback 0)
     (measurableSet_singleton p) (fun a ha ↦ by rw [Set.mem_singleton_iff.1 ha]) hP
 
@@ -747,16 +748,22 @@ the algorithm only sees the past rounds. Since `Unit` carries a unique probabili
 observation kernels of such an environment are all equal to `Kernel.const _ (Measure.dirac ())`,
 and the observation process of an algorithm-environment sequence is `noObs`. -/
 
+/-- Every probability measure on `Unit` is `Measure.dirac ()`. -/
+lemma Measure.eq_dirac_unit (μ : Measure Unit) [IsProbabilityMeasure μ] :
+    μ = Measure.dirac () := by
+  ext s hs
+  rcases Set.eq_empty_or_nonempty s with rfl | ⟨u, hu⟩
+  · simp
+  · have hs_univ : s = Set.univ := Set.eq_univ_of_forall fun x ↦ by rwa [Subsingleton.elim x u]
+    simp [hs_univ]
+
 /-- Every Markov kernel with codomain `Unit` is the constant kernel at `Measure.dirac ()`. -/
 lemma Kernel.eq_const_dirac_unit {α : Type*} {mα : MeasurableSpace α} (κ : Kernel α Unit)
     [IsMarkovKernel κ] :
     κ = Kernel.const α (Measure.dirac ()) := by
-  ext a s hs
+  ext a : 1
   rw [Kernel.const_apply]
-  rcases Set.eq_empty_or_nonempty s with rfl | ⟨u, hu⟩
-  · simp
-  · have hs_univ : s = Set.univ := Set.eq_univ_of_forall fun x ↦ by rwa [Subsingleton.elim x u]
-    simp [hs_univ]
+  exact Measure.eq_dirac_unit (κ a)
 
 /-- A random variable with values in `Unit` admits any Markov kernel as conditional
 distribution. -/
diff --git a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean
index 53dd65a8..0175947c 100644
--- a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean
+++ b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean
@@ -58,8 +58,8 @@ structure AbsolutelyContinuous (alg alg₀ : Algorithm 𝓞 𝓐 𝓨) : Prop wh
 @[inherit_doc AbsolutelyContinuous]
 scoped notation:50 alg " ≪ₐ " alg₀ => AbsolutelyContinuous alg alg₀
 
-lemma AbsolutelyContinuous.p0 {alg alg₀ : Algorithm 𝓞 𝓐 𝓨} (h : alg ≪ₐ alg₀) (o : 𝓞) :
-    alg.p0 o ≪ alg₀.p0 o :=
+lemma AbsolutelyContinuous.policyZero {alg alg₀ : Algorithm 𝓞 𝓐 𝓨} (h : alg ≪ₐ alg₀) (o : 𝓞) :
+    alg.policyZero o ≪ alg₀.policyZero o :=
   h.policy 0 (default, o)
 
 /-- If the algorithm `alg` is absolutely continuous with respect to the algorithm `alg₀` and they
diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/Markov.lean b/LeanMachineLearning/SequentialLearning/Algorithms/Markov.lean
new file mode 100644
index 00000000..3a612140
--- /dev/null
+++ b/LeanMachineLearning/SequentialLearning/Algorithms/Markov.lean
@@ -0,0 +1,270 @@
+/-
+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
+-/
+module
+
+public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MapComap
+public import LeanMachineLearning.SequentialLearning.Algorithm
+
+/-!
+# Algorithms that depend only on the time and the observation
+
+In general, an algorithm `alg : Algorithm 𝓞 𝓐 𝓨` has a policy
+`alg.policy n : Kernel (Hist 𝓞 𝓐 𝓨 n × 𝓞) 𝓐`, which depends on the history before time `n` and on
+the observation at time `n`. In some cases, the policy depends only on the time and on the
+observation. We say that `alg` is a *Markov algorithm* if there exists a sequence of Markov kernels
+`κ : ℕ → Kernel 𝓞 𝓐` such that `alg.policy n = (κ n).prodMkLeft (Hist 𝓞 𝓐 𝓨 n)` for all `n`.
+
+## Main definitions
+
+* `Algorithm.IsMarkov alg`: the policy of `alg` at time `n` depends only on `n` and on the current
+  observation, not on the history.
+* `Algorithm.policyCondObs alg n`: the kernel representing the conditional distribution of the
+  action at time `n` given the observation at time `n` in a Markov algorithm `alg`.
+* `Algorithm.markov κ`: the algorithm whose action at time `n` is drawn from the Markov kernel
+  `κ n` applied to the observation at time `n`.
+
+## Main statements
+
+* `Algorithm.IsMarkov.hasCondDistrib_action`: in a run of a Markov algorithm, the conditional
+  distribution of the action at time `n` given the observation at time `n` is
+  `alg.policyCondObs n`.
+* `Algorithm.IsMarkov.condIndepFun_action_history`: in a run of a Markov algorithm, the action at
+  time `n` is conditionally independent of the history before time `n` given the observation at
+  time `n`.
+
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory Filter Real Finset
+
+open scoped ENNReal NNReal
+
+namespace Learning
+
+variable {𝓞 𝓐 𝓨 : Type*} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐}
+  {m𝓨 : MeasurableSpace 𝓨}
+
+/-- The policy of the algorithm at time `n` depends only on `n` and on the current observation,
+not on the history. -/
+class Algorithm.IsMarkov (alg : Algorithm 𝓞 𝓐 𝓨) : Prop where
+  exists_policy_eq_prodMkLeft : ∃ κ : ℕ → Kernel 𝓞 𝓐, (∀ n, IsMarkovKernel (κ n)) ∧
+    ∀ n, alg.policy n = (κ n).prodMkLeft (Hist 𝓞 𝓐 𝓨 n)
+
+namespace Algorithm
+
+/-- The kernel representing the conditional distribution of the action at time `n` given the
+observation at time `n` in a Markov algorithm. -/
+noncomputable
+def policyCondObs (alg : Algorithm 𝓞 𝓐 𝓨) [h_markov : alg.IsMarkov] (n : ℕ) : Kernel 𝓞 𝓐 :=
+  h_markov.exists_policy_eq_prodMkLeft.choose n
+
+instance (alg : Algorithm 𝓞 𝓐 𝓨) [alg.IsMarkov] (n : ℕ) : IsMarkovKernel (alg.policyCondObs n) :=
+  IsMarkov.exists_policy_eq_prodMkLeft.choose_spec.1 n
+
+lemma policy_eq_prodMkLeft_policyCondObs (alg : Algorithm 𝓞 𝓐 𝓨) [alg.IsMarkov] (n : ℕ) :
+    alg.policy n = (alg.policyCondObs n).prodMkLeft (Hist 𝓞 𝓐 𝓨 n) :=
+  IsMarkov.exists_policy_eq_prodMkLeft.choose_spec.2 n
+
+lemma policy_apply_eq_policyCondObs (alg : Algorithm 𝓞 𝓐 𝓨) [alg.IsMarkov] (n : ℕ)
+    (h : Hist 𝓞 𝓐 𝓨 n) (o : 𝓞) :
+    alg.policy n (h, o) = alg.policyCondObs n o := by
+  rw [policy_eq_prodMkLeft_policyCondObs, Kernel.prodMkLeft_apply]
+
+lemma policyZero_eq_policyCondObs (alg : Algorithm 𝓞 𝓐 𝓨) [alg.IsMarkov] :
+    alg.policyZero = alg.policyCondObs 0 := by
+  ext o : 1
+  rw [policyZero_apply, policy_apply_eq_policyCondObs]
+
+/-- The kernel `alg.policyCondObs n` is determined by the policy at time `n`. The assumption
+`Nonempty 𝓨` ensures that there are histories of every length. -/
+lemma policyCondObs_eq_of_policy_eq [Nonempty 𝓨] (alg : Algorithm 𝓞 𝓐 𝓨) [alg.IsMarkov] {n : ℕ}
+    {κ : Kernel 𝓞 𝓐} (h : alg.policy n = κ.prodMkLeft (Hist 𝓞 𝓐 𝓨 n)) :
+    alg.policyCondObs n = κ := by
+  rcases isEmpty_or_nonempty 𝓞 with h𝓞 | h𝓞
+  · ext o : 1
+    exact h𝓞.elim o
+  have : Nonempty 𝓐 := Measure.nonempty_of_neZero (alg.policyCondObs n (Classical.arbitrary 𝓞))
+  rw [policy_eq_prodMkLeft_policyCondObs, Kernel.prodMkLeft_inj] at h
+  exact h
+
+namespace IsMarkov
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
+  {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : Measure Ω} [IsFiniteMeasure P]
+  {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {n N : ℕ}
+
+lemma hasCondDistrib_action_history_obs [alg.IsMarkov] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    HasCondDistrib (A n) (fun ω ↦ (history O A Y n ω, O n ω))
+      ((alg.policyCondObs n).prodMkLeft (Hist 𝓞 𝓐 𝓨 n)) P := by
+  rw [← alg.policy_eq_prodMkLeft_policyCondObs]
+  exact h.hasCondDistrib_action n
+
+lemma hasCondDistrib_action_history_obs_of_isAlgEnvSeqUntil [alg.IsMarkov]
+    (h : IsAlgEnvSeqUntil O A Y alg env P N) (hn : n < N) :
+    HasCondDistrib (A n) (fun ω ↦ (history O A Y n ω, O n ω))
+      ((alg.policyCondObs n).prodMkLeft (Hist 𝓞 𝓐 𝓨 n)) P := by
+  rw [← alg.policy_eq_prodMkLeft_policyCondObs]
+  exact h.hasCondDistrib_action n hn
+
+/-- The conditional distribution of the action at time `n` given the observation at time `n` is
+`alg.policyCondObs n`. -/
+lemma hasCondDistrib_action [alg.IsMarkov] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    HasCondDistrib (A n) (O n) (alg.policyCondObs n) P :=
+  (hasCondDistrib_action_history_obs h n).comp_right
+
+/-- The conditional distribution of the action at time `n < N` given the observation at time `n`
+is `alg.policyCondObs n`. -/
+lemma hasCondDistrib_action_of_isAlgEnvSeqUntil [alg.IsMarkov]
+    (h : IsAlgEnvSeqUntil O A Y alg env P N) (hn : n < N) :
+    HasCondDistrib (A n) (O n) (alg.policyCondObs n) P :=
+  (hasCondDistrib_action_history_obs_of_isAlgEnvSeqUntil h hn).comp_right
+
+/-- The law of the action at time `n` is the law of the observation at time `n` composed with
+`alg.policyCondObs n`. -/
+lemma hasLaw_action_comp [alg.IsMarkov] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    HasLaw (A n) (alg.policyCondObs n ∘ₘ (P.map (O n))) P :=
+  (hasCondDistrib_action h n).hasLaw_comp
+
+/-- Conditionally on an event determined by the history before time `n` and the observation at
+time `n`, on which that observation is equal to `b`, the action at time `n` has law
+`alg.policyCondObs n b`. -/
+lemma hasLaw_action_cond [alg.IsMarkov] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ)
+    {s : Set (Hist 𝓞 𝓐 𝓨 n × 𝓞)} (hs : MeasurableSet s) {b : 𝓞} (hsb : ∀ u ∈ s, u.2 = b)
+    (hP : P ((fun ω ↦ (history O A Y n ω, O n ω)) ⁻¹' s) ≠ 0) :
+    HasLaw (A n) (alg.policyCondObs n b) P[|(fun ω ↦ (history O A Y n ω, O n ω)) ⁻¹' s] := by
+  refine (hasCondDistrib_action_history_obs h n).hasLaw_cond (h.measurable_action _) hs
+    (fun u hu ↦ ?_) hP
+  rw [Kernel.prodMkLeft_apply, hsb u hu]
+
+/-- Conditionally on an event determined by the history before time `n` and the observation at
+time `n`, on which that observation is constant, the action at time `n` is independent of the
+history before time `n` and of the observation at time `n`. -/
+lemma indepFun_history_obs_action_cond [alg.IsMarkov] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ)
+    {s : Set (Hist 𝓞 𝓐 𝓨 n × 𝓞)} (hs : MeasurableSet s) {b : 𝓞} (hsb : ∀ u ∈ s, u.2 = b) :
+    (fun ω ↦ (history O A Y n ω, O n ω))
+      ⟂ᵢ[P[|(fun ω ↦ (history O A Y n ω, O n ω)) ⁻¹' s]] A n := by
+  have hO := h.measurable_obs
+  have hA := h.measurable_action
+  have hY := h.measurable_feedback
+  refine (hasCondDistrib_action_history_obs h n).indepFun_cond (by fun_prop) hs
+    (η := alg.policyCondObs n b) fun u hu ↦ ?_
+  rw [Kernel.prodMkLeft_apply, hsb u hu]
+
+variable [StandardBorelSpace 𝓞] [Nonempty 𝓞] [StandardBorelSpace 𝓐] [Nonempty 𝓐]
+  [StandardBorelSpace 𝓨] [Nonempty 𝓨]
+
+/-- The action at time `n` is conditionally independent of the history before time `n`, given the
+observation at time `n`. -/
+lemma condIndepFun_action_history [StandardBorelSpace Ω] [alg.IsMarkov]
+    (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    A n ⟂ᵢ[O n, h.measurable_obs n; P] history O A Y n := by
+  have hO := h.measurable_obs
+  have hA := h.measurable_action
+  have hY := h.measurable_feedback
+  refine condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft (η := alg.policyCondObs n)
+    (by fun_prop) (by fun_prop) (by fun_prop) ?_
+  exact HasCondDistrib.condDistrib_eq (hasCondDistrib_action_history_obs h n)
+
+/-- The action at time `n` is conditionally independent of the history before time `n` and the
+observation at time `n`, given the observation at time `n`. -/
+lemma condIndepFun_action_history_obs [StandardBorelSpace Ω] [alg.IsMarkov]
+    (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    A n ⟂ᵢ[O n, h.measurable_obs n; P] (fun ω ↦ (history O A Y n ω, O n ω)) := by
+  have hO := h.measurable_obs
+  have hA := h.measurable_action
+  have hY := h.measurable_feedback
+  exact (condIndepFun_action_history h n).prod_right (by fun_prop) (by fun_prop) (by fun_prop)
+
+end IsMarkov
+
+section Markov
+
+variable {κ : ℕ → Kernel 𝓞 𝓐} [∀ n, IsMarkovKernel (κ n)]
+
+/-- The algorithm whose action at time `n` is drawn from `κ n` applied to the observation at
+time `n`, whatever the history. -/
+def markov (κ : ℕ → Kernel 𝓞 𝓐) [∀ n, IsMarkovKernel (κ n)] : Algorithm 𝓞 𝓐 𝓨 where
+  policy n := (κ n).prodMkLeft (Hist 𝓞 𝓐 𝓨 n)
+
+@[simp]
+lemma policy_markov (n : ℕ) :
+    (markov κ : Algorithm 𝓞 𝓐 𝓨).policy n = (κ n).prodMkLeft (Hist 𝓞 𝓐 𝓨 n) := rfl
+
+@[simp]
+lemma policyZero_markov : (markov κ : Algorithm 𝓞 𝓐 𝓨).policyZero = κ 0 := by
+  ext o : 1
+  rw [policyZero_apply, policy_markov, Kernel.prodMkLeft_apply]
+
+instance : (markov κ : Algorithm 𝓞 𝓐 𝓨).IsMarkov where
+  exists_policy_eq_prodMkLeft := ⟨κ, inferInstance, fun _ ↦ rfl⟩
+
+@[simp]
+lemma policyCondObs_markov [Nonempty 𝓨] (n : ℕ) :
+    (markov κ : Algorithm 𝓞 𝓐 𝓨).policyCondObs n = κ n :=
+  policyCondObs_eq_of_policy_eq _ rfl
+
+end Markov
+
+end Algorithm
+
+namespace IsAlgEnvSeq
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
+  {κ : ℕ → Kernel 𝓞 𝓐} [∀ n, IsMarkovKernel (κ n)] {env : Environment 𝓞 𝓐 𝓨}
+  {P : Measure Ω} [IsFiniteMeasure P]
+  {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
+
+lemma hasCondDistrib_action_history_obs_markov
+    (h : IsAlgEnvSeq O A Y (Algorithm.markov κ) env P) (n : ℕ) :
+    HasCondDistrib (A n) (fun ω ↦ (history O A Y n ω, O n ω)) ((κ n).prodMkLeft (Hist 𝓞 𝓐 𝓨 n)) P :=
+  h.hasCondDistrib_action n
+
+/-- The conditional distribution of the action at time `n` given the observation at time `n`
+is `κ n`. -/
+lemma hasCondDistrib_action_markov (h : IsAlgEnvSeq O A Y (Algorithm.markov κ) env P) (n : ℕ) :
+    HasCondDistrib (A n) (O n) (κ n) P :=
+  (hasCondDistrib_action_history_obs_markov h n).comp_right
+
+/-- The conditional distribution of the action at time `n` given the observation at time `n`
+is `κ n`. -/
+lemma condDistrib_action_markov [StandardBorelSpace 𝓐] [Nonempty 𝓐]
+    (h : IsAlgEnvSeq O A Y (Algorithm.markov κ) env P) (n : ℕ) :
+    condDistrib (A n) (O n) P =ᵐ[P.map (O n)] κ n :=
+  (hasCondDistrib_action_markov h n).condDistrib_eq
+
+/-- Conditionally on an event determined by the history before time `n` and the observation at
+time `n`, on which that observation is equal to `b`, the action at time `n` has law `κ n b`. -/
+lemma hasLaw_action_cond_markov (h : IsAlgEnvSeq O A Y (Algorithm.markov κ) env P) (n : ℕ)
+    {s : Set (Hist 𝓞 𝓐 𝓨 n × 𝓞)} (hs : MeasurableSet s) {b : 𝓞} (hsb : ∀ u ∈ s, u.2 = b)
+    (hP : P ((fun ω ↦ (history O A Y n ω, O n ω)) ⁻¹' s) ≠ 0) :
+    HasLaw (A n) (κ n b) P[|(fun ω ↦ (history O A Y n ω, O n ω)) ⁻¹' s] := by
+  refine (hasCondDistrib_action_history_obs_markov h n).hasLaw_cond (h.measurable_action _) hs
+    (fun u hu ↦ ?_) hP
+  rw [Kernel.prodMkLeft_apply, hsb u hu]
+
+/-- Conditionally on an event determined by the history before time `n` and the observation at
+time `n`, on which that observation is constant, the action at time `n` is independent of the
+history before time `n` and of the observation at time `n`. -/
+lemma indepFun_history_obs_action_cond_markov
+    (h : IsAlgEnvSeq O A Y (Algorithm.markov κ) env P) (n : ℕ)
+    {s : Set (Hist 𝓞 𝓐 𝓨 n × 𝓞)} (hs : MeasurableSet s) {b : 𝓞} (hsb : ∀ u ∈ s, u.2 = b) :
+    (fun ω ↦ (history O A Y n ω, O n ω))
+      ⟂ᵢ[P[|(fun ω ↦ (history O A Y n ω, O n ω)) ⁻¹' s]] A n :=
+  Algorithm.IsMarkov.indepFun_history_obs_action_cond h n hs hsb
+
+/-- The action at time `n` is conditionally independent of the history before time `n`, given the
+observation at time `n`. -/
+lemma condIndepFun_action_history_markov [StandardBorelSpace Ω]
+    [StandardBorelSpace 𝓞] [Nonempty 𝓞] [StandardBorelSpace 𝓐] [Nonempty 𝓐]
+    [StandardBorelSpace 𝓨] [Nonempty 𝓨]
+    (h : IsAlgEnvSeq O A Y (Algorithm.markov κ) env P) (n : ℕ) :
+    A n ⟂ᵢ[O n, h.measurable_obs n; P] history O A Y n :=
+  Algorithm.IsMarkov.condIndepFun_action_history h n
+
+end IsAlgEnvSeq
+
+end Learning
diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Basic.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Basic.lean
index 7ade0abe..26b287bf 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Basic.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Basic.lean
@@ -5,7 +5,7 @@ Authors: Gaëtan Serré
 -/
 module
 
-public import LeanMachineLearning.SequentialLearning.Algorithm
+public import LeanMachineLearning.SequentialLearning.Algorithms.Markov
 
 import LeanMachineLearning.ForMathlib.Probability.Independence.IndepFun
 
@@ -17,7 +17,7 @@ measure at each iteration.
 
 ## Main definitions
 
-* `randomSampling`: The random sampling algorithm that samples from a fixed distribution at
+* `Algorithm.const`: The random sampling algorithm that samples from a fixed distribution at
 each iteration.
 
 ## Main statements
@@ -43,28 +43,41 @@ open Set in
 /-- The _Random Sampling_ algorithm, which samples from a fixed probability
 measure at each iteration. -/
 @[simps]
-noncomputable def randomSampling (μ : Measure 𝓐) [IsProbabilityMeasure μ] :
+noncomputable def Algorithm.const (μ : Measure 𝓐) [IsProbabilityMeasure μ] :
     Algorithm 𝓞 𝓐 𝓨 where
   policy _ := Kernel.const _ μ
 
-namespace randomSampling
+/-- The random sampling algorithm is the Markov algorithm with the constant kernel `μ` at every
+time. -/
+lemma Algorithm.const_eq_markov :
+    (Algorithm.const μ : Algorithm 𝓞 𝓐 𝓨) = Algorithm.markov (fun _ ↦ Kernel.const 𝓞 μ) := rfl
+
+instance : (Algorithm.const μ : Algorithm 𝓞 𝓐 𝓨).IsMarkov :=
+  inferInstanceAs (Algorithm.markov (fun _ ↦ Kernel.const 𝓞 μ) : Algorithm 𝓞 𝓐 𝓨).IsMarkov
+
+@[simp]
+lemma policyCondObs_const [Nonempty 𝓨] (n : ℕ) :
+    (Algorithm.const μ : Algorithm 𝓞 𝓐 𝓨).policyCondObs n = Kernel.const 𝓞 μ :=
+  Algorithm.policyCondObs_eq_of_policy_eq _ rfl
+
+namespace Algorithm.const
 
 variable {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {env : Environment 𝓞 𝓐 𝓨}
 
-/-- Each action follows the distribution μ. -/
-lemma hasLaw_action (h : IsAlgEnvSeq O A Y (randomSampling μ) env P) (n : ℕ) :
+/-- Each action of the random sampling algorithm follows the distribution μ. -/
+lemma hasLaw_action (h : IsAlgEnvSeq O A Y (Algorithm.const μ) env P) (n : ℕ) :
     HasLaw (A n) μ P :=
   (h.hasCondDistrib_action n).hasLaw_of_const
 
-/-- Actions are mutually independent. -/
-lemma iIndep_action (h : IsAlgEnvSeq O A Y (randomSampling μ) env P) :
+/-- Actions of the random sampling algorithm are mutually independent. -/
+lemma iIndep_action (h : IsAlgEnvSeq O A Y (Algorithm.const μ) env P) :
     iIndepFun A P := by
   have hO := h.measurable_obs
   have hA := h.measurable_action
   rw [iIndepFun_nat_iff_forall_indepFun (by fun_prop)]
   intro n
   have map_eq := (h.hasCondDistrib_action (n + 1)).map_eq
-  simp only [randomSampling_policy, Measure.compProd_const] at map_eq
+  simp only [Algorithm.const_policy, Measure.compProd_const] at map_eq
   have law_eq : P.map (A (n + 1)) = μ := (hasLaw_action h (n + 1)).map_eq
   rw [← law_eq, ← indepFun_iff_map_prod_eq_prod_map_map] at map_eq
   · change A (n + 1) ⟂ᵢ[P] (fun (p : Hist 𝓞 𝓐 𝓨 (n + 1) × 𝓞) (i : Iic n) ↦
@@ -74,6 +87,6 @@ lemma iIndep_action (h : IsAlgEnvSeq O A Y (randomSampling μ) env P) :
   · exact ((h.measurable_history (n + 1)).prodMk (h.measurable_obs (n + 1))).aemeasurable
   · exact (h.measurable_action (n + 1)).aemeasurable
 
-end randomSampling
+end Algorithm.const
 
 end Learning
diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean
index 91829c5e..b82d306c 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean
@@ -17,8 +17,8 @@ import LeanMachineLearning.ForMathlib.Topology.Instances.ENNReal.Lemmas
 /-!
 # Random Sampling convergence lemmas
 
-This file contains several convergence lemmas for the `randomSampling` algorithm along with an
-`evalEnv` environment, that evaluates the actions using a measurable function.
+This file contains several convergence lemmas for the `Algorithm.const` algorithm along with an
+`Environment.eval` environment, that evaluates the actions using a measurable function.
 
 ## Main statements
 
@@ -38,7 +38,7 @@ open Learning MeasureTheory ProbabilityTheory Filter Finset ENNReal
 
 open scoped Topology
 
-namespace Learning.randomSampling
+namespace Learning.Algorithm.const
 
 variable {𝓐 𝓨 Ω : Type*} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
   {mΩ : MeasurableSpace Ω} {μ : Measure 𝓐} [IsProbabilityMeasure μ] {P : Measure Ω}
@@ -51,18 +51,18 @@ section rewards
 variable [StandardBorelSpace 𝓨] [Nonempty 𝓨]
 
 /-- Each reward follows the distribution μ.map f. -/
-lemma hasLaw_feeback (h : IsAlgEnvSeq O A Y (randomSampling μ) (evalEnv f hf) P) (n : ℕ) :
+lemma hasLaw_feeback (h : IsAlgEnvSeq O A Y (Algorithm.const μ) (Environment.eval f hf) P) (n : ℕ) :
     HasLaw (Y n) (μ.map f) P := by
-  refine HasLaw.congr ?_ (feedback_evalEnv_ae_eq_eval_action h n)
+  refine HasLaw.congr ?_ (feedback_eval_ae_eq_eval_action h n)
   have hA := h.measurable_action n
   refine ⟨by fun_prop, ?_⟩
   rw [← Measure.map_map hf hA, (hasLaw_action h n).map_eq]
 
 /-- Rewards are mutually independent. -/
-lemma iIndep_feedback (h : IsAlgEnvSeq O A Y (randomSampling μ) (evalEnv f hf) P) :
+lemma iIndep_feedback (h : IsAlgEnvSeq O A Y (Algorithm.const μ) (Environment.eval f hf) P) :
     iIndepFun Y P :=
   have (n : ℕ) : f ∘ A n =ᵐ[P] Y n :=
-    (feedback_evalEnv_ae_eq_eval_action h n).symm
+    (feedback_eval_ae_eq_eval_action h n).symm
   iIndepFun.congr this <| (iIndep_action h).comp _ (fun _ ↦ hf)
 
 end rewards
@@ -71,17 +71,17 @@ variable [PseudoMetricSpace 𝓐] [SecondCountableTopology 𝓐] [OpensMeasurabl
   [μ.IsOpenPosMeasure]
 
 /-- The minimum distance from sampled actions to any point tends to zero. -/
-theorem action_tendsto_any (h : IsAlgEnvSeq O A Y (randomSampling μ) (evalEnv f hf) P) (a : 𝓐)
-    {ε : ℝ} (hε : 0 < ε) :
+theorem action_tendsto_any (h : IsAlgEnvSeq O A Y (Algorithm.const μ) (Environment.eval f hf) P)
+    (a : 𝓐) {ε : ℝ} (hε : 0 < ε) :
     Tendsto (fun i => P {x | ε ≤ (fun (j : Iic i) ↦ dist (A j.1 x) a).min}) atTop (𝓝 0) := by
-  set randomSampling_alg := randomSampling (𝓞 := Unit) (𝓨 := 𝓨) μ
+  set const_alg := Algorithm.const (𝓞 := Unit) (𝓨 := 𝓨) μ
   refine tendsto_zero_of_le (g := fun n ↦ P (⋂ i ∈ Iic n, {x | ε ≤ dist (A i x) a})) ?_ ?_
   · have inter_prod (n : ℕ) : P (⋂ j ∈ Iic n, {x | ε ≤ dist (A j x) a}) =
         ∏ j ∈ Iic n, P {x | ε ≤ dist (A j x) a} := by
       refine iIndepSet.meas_biInter ?_ _
       rw [iIndepSet_iff_meas_biInter fun i ↦ ?_]
       · intro s
-        have iIndep_actions := randomSampling.iIndep_action h
+        have iIndep_actions := Algorithm.const.iIndep_action h
         rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at iIndep_actions
         have meas_dist : ∀ i ∈ s, MeasurableSet {x | ε ≤ dist x a} := by
           intro i hs
@@ -94,7 +94,7 @@ theorem action_tendsto_any (h : IsAlgEnvSeq O A Y (randomSampling μ) (evalEnv f
     have prod_law (n : ℕ) : ∏ j ∈ Iic n, P {x | ε ≤ dist (A j x) a} =
         ∏ j ∈ Iic n, μ {x | ε ≤ dist x a} := by
       refine prod_congr rfl fun j hj ↦ ?_
-      have hlaw (n : ℕ) : HasLaw (A n) μ P := randomSampling.hasLaw_action h n
+      have hlaw (n : ℕ) : HasLaw (A n) μ P := Algorithm.const.hasLaw_action h n
       rw [← (hlaw j).map_eq, P.map_apply]
       · simp
       · exact h.measurable_action j
@@ -118,7 +118,7 @@ variable [PseudoMetricSpace 𝓨] [BorelSpace 𝓨] (hfc : Continuous f)
 
 /-- The minimum distance from image of actions to any function value tends to zero. -/
 lemma image_action_tendsto_any
-    (h : IsAlgEnvSeq O A Y (randomSampling μ) (evalEnv f hfc.measurable) P)
+    (h : IsAlgEnvSeq O A Y (Algorithm.const μ) (Environment.eval f hfc.measurable) P)
     (a : 𝓐) {ε : ℝ} (hε : 0 < ε) :
     Tendsto (fun i => P {x | ε ≤ (fun (j : Iic i) ↦
       dist (f (A j.1 x)) (f a)).min}) atTop (𝓝 0) := by
@@ -140,20 +140,21 @@ lemma image_action_tendsto_any
 variable [StandardBorelSpace 𝓨] [Nonempty 𝓨]
 
 /-- The minimum distance from rewards to any function value tends to zero. -/
-lemma feedback_tendsto_any (h : IsAlgEnvSeq O A Y (randomSampling μ) (evalEnv f hfc.measurable) P)
+lemma feedback_tendsto_any
+    (h : IsAlgEnvSeq O A Y (Algorithm.const μ) (Environment.eval f hfc.measurable) P)
     (a : 𝓐) {ε : ℝ} (hε : 0 < ε) :
     Tendsto (fun i => P {x | ε ≤ (fun (j : Iic i) ↦ dist (Y j.1 x) (f a)).min}) atTop (𝓝 0) := by
   convert image_action_tendsto_any hfc h a hε using 2 with n
   refine measure_congr ?_
   let g : ((Iic n) → 𝓨) → ℝ := fun r ↦ (fun i ↦ dist (r i) (f a)).min
-  filter_upwards [feedback_evalEnv_ae_eq_eval_action_comp h g] with ω hω
+  filter_upwards [feedback_eval_ae_eq_eval_action_comp h g] with ω hω
   simp only [eq_iff_iff]
   simp [g, hω]
 
 variable {R : ℕ → Ω → ℝ} {f : 𝓐 → ℝ} (hfc : Continuous f) {a : 𝓐}
 
 /-- The minimum image action converges to the function's global minimum. -/
-lemma tendsto_min₀ (h : IsAlgEnvSeq O A R (randomSampling μ) (evalEnv f hfc.measurable) P)
+lemma tendsto_min₀ (h : IsAlgEnvSeq O A R (Algorithm.const μ) (Environment.eval f hfc.measurable) P)
     (hf_min : ∀ x, f a ≤ f x) :
     TendstoInMeasure P (fun n ω ↦ (fun (i : Iic n) ↦ f (A i.1 ω)).min) atTop (fun _ ↦ f a) := by
   rw [tendstoInMeasure_iff_dist]
@@ -174,15 +175,15 @@ lemma tendsto_min₀ (h : IsAlgEnvSeq O A R (randomSampling μ) (evalEnv f hfc.m
   grind
 
 /-- The minimum reward converges to the function's global minimum. -/
-lemma tendsto_min (h : IsAlgEnvSeq O A R (randomSampling μ) (evalEnv f hfc.measurable) P)
+lemma tendsto_min (h : IsAlgEnvSeq O A R (Algorithm.const μ) (Environment.eval f hfc.measurable) P)
     (hf_min : ∀ x, f a ≤ f x) :
     TendstoInMeasure P (fun n ω ↦ (fun (i : Iic n) ↦ R i.1 ω).min) atTop (fun _ ↦ f a) := by
   refine TendstoInMeasure.congr_left (fun n ↦ ?_) <| tendsto_min₀ hfc h hf_min
-  filter_upwards [feedback_evalEnv_ae_eq_eval_action_comp h Function.min] with ω hω
+  filter_upwards [feedback_eval_ae_eq_eval_action_comp h Function.min] with ω hω
   rw [← hω]
 
 /-- The maximum image action converges to the function's global maximum. -/
-lemma tendsto_max₀ (h : IsAlgEnvSeq O A R (randomSampling μ) (evalEnv f hfc.measurable) P)
+lemma tendsto_max₀ (h : IsAlgEnvSeq O A R (Algorithm.const μ) (Environment.eval f hfc.measurable) P)
     (hf_max : ∀ x, f x ≤ f a) :
     TendstoInMeasure P (fun n ω ↦ (fun (i : Iic n) ↦ f (A i.1 ω)).max) atTop (fun _ ↦ f a) := by
   rw [tendstoInMeasure_iff_dist]
@@ -204,11 +205,11 @@ lemma tendsto_max₀ (h : IsAlgEnvSeq O A R (randomSampling μ) (evalEnv f hfc.m
   grind
 
 /-- The maximum reward converges to the function's global maximum. -/
-lemma tendsto_max (h : IsAlgEnvSeq O A R (randomSampling μ) (evalEnv f hfc.measurable) P)
+lemma tendsto_max (h : IsAlgEnvSeq O A R (Algorithm.const μ) (Environment.eval f hfc.measurable) P)
     (hf_max : ∀ x, f x ≤ f a) :
     TendstoInMeasure P (fun n ω ↦ (fun (i : Iic n) ↦ R i.1 ω).max) atTop (fun _ ↦ f a) := by
   refine TendstoInMeasure.congr_left (fun n ↦ ?_) <| tendsto_max₀ hfc h hf_max
-  filter_upwards [feedback_evalEnv_ae_eq_eval_action_comp h Function.max] with ω hω
+  filter_upwards [feedback_eval_ae_eq_eval_action_comp h Function.max] with ω hω
   rw [← hω]
 
-end Learning.randomSampling
+end Learning.Algorithm.const
diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean
index 3f377515..f73d6dde 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean
@@ -84,7 +84,7 @@ variable (K) in
 /-- The Round-Robin algorithm: deterministic algorithm that chooses action `n % K` at time `n`. -/
 noncomputable
 def roundRobinAlgorithm [NeZero K] : Algorithm 𝓞 (Fin K) 𝓨 :=
-  detAlgorithm (fun n _ ↦ RoundRobin.nextAction K n) (by fun_prop)
+  Algorithm.deterministic (fun n _ ↦ RoundRobin.nextAction K n) (by fun_prop)
 
 end AlgorithmDefinition
 
@@ -97,12 +97,12 @@ variable [NeZero K] {ν : Kernel (Fin K) 𝓨} [IsMarkovKernel ν]
 
 /-- The action chosen at time `n` is the action `n % K`. -/
 lemma action_ae_eq (n : ℕ)
-    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P (n + 1)) :
+    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (Environment.bandit ν) P (n + 1)) :
     A n =ᵐ[P] fun _ ↦ nextAction K n :=
-  h.action_detAlgorithm_ae_eq n.lt_succ_self
+  h.action_deterministic_ae_eq n.lt_succ_self
 
 lemma action_zero
-    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P 1) :
+    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (Environment.bandit ν) P 1) :
     A 0 =ᵐ[P] fun _ ↦ 0 := by
   filter_upwards [action_ae_eq 0 h] with ω hω
   rw [hω]
@@ -110,7 +110,7 @@ lemma action_zero
 
 /-- At time `K * m`, the number of times each action is chosen is equal to `m`. -/
 lemma pullCount_mul (m : ℕ)
-    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P (K * m))
+    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (Environment.bandit ν) P (K * m))
     (a : Fin K) :
     pullCount A a (K * m) =ᵐ[P] fun _ ↦ m := by
   rw [Filter.EventuallyEq]
@@ -126,14 +126,14 @@ lemma pullCount_mul (m : ℕ)
   _ = m := sum_mod_range_mul (Nat.pos_of_neZero K) m a
 
 lemma pullCount_eq_one
-    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P K) (a : Fin K) :
+    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (Environment.bandit ν) P K) (a : Fin K) :
     pullCount A a K =ᵐ[P] fun _ ↦ 1 := by
   suffices pullCount A a (K * 1) =ᵐ[P] fun _ ↦ 1 by simpa using this
   refine pullCount_mul 1 (P := P) (ν := ν) (O := O) (Y := Y) ?_ a
   simpa
 
 lemma time_gt_of_pullCount_gt_one
-    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P K) (a : Fin K) :
+    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (Environment.bandit ν) P K) (a : Fin K) :
     ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → K < n := by
   filter_upwards [pullCount_eq_one h a] with h h_eq n hn
   rw [← h_eq] at hn
@@ -141,7 +141,7 @@ lemma time_gt_of_pullCount_gt_one
   exact hn.not_ge (pullCount_mono _ h_lt _)
 
 lemma pullCount_pos_of_time_ge
-    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P K) :
+    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (Environment.bandit ν) P K) :
     ∀ᵐ ω ∂P, ∀ n, K ≤ n → ∀ b : Fin K, 0 < pullCount A b n ω := by
   have h_ae a := pullCount_eq_one h a
   simp_rw [Filter.EventuallyEq, ← ae_all_iff] at h_ae
@@ -151,7 +151,7 @@ lemma pullCount_pos_of_time_ge
   exact pullCount_mono _ hn _
 
 lemma pullCount_pos_of_pullCount_gt_one
-    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (stationaryEnv ν) P K) (a : Fin K) :
+    (h : IsAlgEnvSeqUntil O A Y (roundRobinAlgorithm K) (Environment.bandit ν) P K) (a : Fin K) :
     ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → ∀ b : Fin K, 0 < pullCount A b n ω := by
   filter_upwards [time_gt_of_pullCount_gt_one h a, pullCount_pos_of_time_ge h] with ω h1 h2 n h_gt a
   exact h2 n (h1 n h_gt).le a
diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/Uniform.lean b/LeanMachineLearning/SequentialLearning/Algorithms/Uniform.lean
index 7c6f3c4d..b636cf58 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithms/Uniform.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithms/Uniform.lean
@@ -38,7 +38,10 @@ variable {𝓞 𝓐 𝓨 : Type*} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : Measur
 /-- The Uniform algorithm: actions are chosen uniformly at random. -/
 noncomputable
 def uniformAlgorithm [Finite 𝓐] [Nonempty 𝓐] : Algorithm 𝓞 𝓐 𝓨 :=
-  randomSampling (uniformOn Set.univ)
+  Algorithm.const (uniformOn Set.univ)
+
+instance [Finite 𝓐] [Nonempty 𝓐] : (uniformAlgorithm : Algorithm 𝓞 𝓐 𝓨).IsMarkov :=
+  inferInstanceAs (Algorithm.const (uniformOn Set.univ) : Algorithm 𝓞 𝓐 𝓨).IsMarkov
 
 lemma absolutelyContinuous_uniformAlgorithm [Finite 𝓐] [Nonempty 𝓐] {alg : Algorithm 𝓞 𝓐 𝓨} :
     alg ≪ₐ uniformAlgorithm where
diff --git a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean
index dd29a648..e177abbd 100644
--- a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean
+++ b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean
@@ -14,7 +14,7 @@ public import LeanMachineLearning.SequentialLearning.StationaryEnv
 
 A Bayesian stationary environment is an environment that draws a parameter `e : 𝓔` from a prior
 `Q` before the first round and then behaves like the stationary environment
-`stationaryEnv (κ.sectR e)`. Concretely, `bayesStationaryEnv Q κ : Environment 𝓔 𝓐 𝓨` announces
+`Environment.bandit (κ.sectR e)`. Concretely, `bayesStationaryEnv Q κ : Environment 𝓔 𝓐 𝓨` announces
 an observation `e` at every round and runs against `alg.comapObs (fun _ ↦ ())`, for
 an `alg : Algorithm Unit 𝓐 𝓨`, an algorithm that does not use the observation.
 
@@ -27,7 +27,7 @@ an `alg : Algorithm Unit 𝓐 𝓨`, an algorithm that does not use the observat
   the sequences of actions `A : ℕ → Ω → 𝓐` and feedbacks `Y : ℕ → Ω → 𝓨` are generated by the
   algorithm `alg : Algorithm Unit 𝓐 𝓨` interacting with `bayesStationaryEnv Q κ`, which it sees
   through `Algorithm.comapObs (fun _ ↦ ())`. Equivalently, `A` and `Y` are generated by `alg`
-  interacting with the stationary environment `stationaryEnv (κ.sectR (E ω))`.
+  interacting with the stationary environment `Environment.bandit (κ.sectR (E ω))`.
 * `bayesTrajMeasure Q κ alg`: for any choice of probability measure `Q : Measure 𝓔`, Markov kernel
   `κ : Kernel (𝓔 × 𝓐) 𝓨`, and algorithm `alg : Algorithm Unit 𝓐 𝓨`, provides a probability measure
   `P : Measure (ℕ → Round 𝓔 𝓐 𝓨)` on a space that carries `E`, `A`, and `Y` such that
@@ -43,12 +43,13 @@ an `alg : Algorithm Unit 𝓐 𝓨`, an algorithm that does not use the observat
 * `IsAlgEnvSeq.isBayesAlgEnvSeq`: a run of `alg.comapObs (fun _ ↦ ())` against
   `bayesStationaryEnv Q κ` is a Bayesian algorithm-environment sequence for the announced parameter.
 * `ae_IsAlgEnvSeq h`: if `h : IsBayesAlgEnvSeq Q κ alg E A Y P`, for `Q`-almost every `e : 𝓔`,
-  `IsAlgEnvSeq O' A' Y' alg (stationaryEnv (κ.sectR e)) (condDistrib (trajectory _ A Y) E P e)` for
-  some sequence of actions `A' : ℕ → (ℕ → Round Unit 𝓐 𝓨) → 𝓐` and sequence of feedbacks
+  `IsAlgEnvSeq O' A' Y' alg (Environment.bandit (κ.sectR e)) (condDistrib (trajectory _ A Y) E P e)`
+  for some sequence of actions `A' : ℕ → (ℕ → Round Unit 𝓐 𝓨) → 𝓐` and sequence of feedbacks
   `Y' : ℕ → (ℕ → Round Unit 𝓐 𝓨) → 𝓨`. Intuitively, if the observable trajectory is generated by an
   underlying parameter `e : 𝓔`, the measure that carries the `IsBayesAlgEnvSeq` structure reveals a
-  measure that carries an `IsAlgEnvSeq` structure under the environment `stationaryEnv (κ.sectR e)`
-  and the same algorithm. This allows transferring results from the `IsAlgEnvSeq` structure to the
+  measure that carries an `IsAlgEnvSeq` structure under the environment
+  `Environment.bandit (κ.sectR e)` and the same algorithm. This allows transferring results from
+  the `IsAlgEnvSeq` structure to the
   `IsBayesAlgEnvSeq` structure.
 
 -/
@@ -93,10 +94,10 @@ lemma feedback_bayesStationaryEnv (n : ℕ) :
     (bayesStationaryEnv Q κ).feedback n = κ.comap (fun p ↦ (p.1.2, p.2)) (by fun_prop) := rfl
 
 @[simp]
-lemma obs0_bayesStationaryEnv : (bayesStationaryEnv Q κ).obs0 = Q := rfl
+lemma obsZero_bayesStationaryEnv : (bayesStationaryEnv Q κ).obsZero = Q := rfl
 
 @[simp]
-lemma ν0_bayesStationaryEnv : (bayesStationaryEnv Q κ).ν0 = κ := rfl
+lemma feedbackZero_bayesStationaryEnv : (bayesStationaryEnv Q κ).feedbackZero = κ := rfl
 
 end BayesEnv
 
@@ -114,7 +115,7 @@ lemma measurable_announceHist (n : ℕ) :
 that the parameter `E : Ω → 𝓔` has law `Q` and that the sequences of actions `A : ℕ → Ω → 𝓐`
 and feedbacks `Y : ℕ → Ω → 𝓨` are generated by the algorithm `alg : Algorithm Unit 𝓐 𝓨`
 interacting with an underlying environment that depends on `E` and `κ`
-(`stationaryEnv (κ.sectR (E ω))`).
+(`Environment.bandit (κ.sectR (E ω))`).
 
 This is `IsAlgEnvSeq` for the announcing environment `bayesStationaryEnv Q κ` and the algorithm
 `alg.comapObs (fun _ ↦ ())` that ignores the announced parameter: the observation at every round
@@ -183,16 +184,16 @@ lemma hasCondDistrib_feedback' (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ)
   (h.hasCondDistrib_feedback n).comp_right
 
 lemma hasLaw_action_zero (h : IsBayesAlgEnvSeq Q κ alg E A Y P) :
-    HasLaw (A 0) (alg.p0 ()) P := by
+    HasLaw (A 0) (alg.policyZero ()) P := by
   have h0 : HasCondDistrib (A 0)
       (fun _ : Ω ↦ ((default : Hist Unit 𝓐 𝓨 0), ())) (alg.policy 0) P := by
     have h1 := h.hasCondDistrib_action' 0
     rwa [history_zero] at h1
   exact h0.hasLaw_of_const'
 
-/-- The first action is independent of the parameter `E`, and has law `alg.p0 ()`. -/
+/-- The first action is independent of the parameter `E`, and has law `alg.policyZero ()`. -/
 lemma hasCondDistrib_action_zero (h : IsBayesAlgEnvSeq Q κ alg E A Y P) :
-    HasCondDistrib (A 0) E (Kernel.const _ (alg.p0 ())) P :=
+    HasCondDistrib (A 0) E (Kernel.const _ (alg.policyZero ())) P :=
   hasCondDistrib_prodMk_right_unique_iff.mp (h.hasCondDistrib_action 0)
 
 /-- The posterior over the parameter given the empty history is the prior. -/
@@ -254,7 +255,7 @@ lemma hasLaw_IT_hist (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) :
     rw [← Kernel.map_apply _ (IT.measurable_hist n), he]⟩
 
 lemma ae_IsAlgEnvSeq (h : IsBayesAlgEnvSeq Q κ alg E A Y P) :
-    ∀ᵐ e ∂Q, IsAlgEnvSeq IT.obs IT.action IT.feedback alg (stationaryEnv (κ.sectR e))
+    ∀ᵐ e ∂Q, IsAlgEnvSeq IT.obs IT.action IT.feedback alg (Environment.bandit (κ.sectR e))
       (condDistrib (trajectory (noObs Ω) A Y) E P e) := by
   filter_upwards [ae_all_iff.2 (hasCondDistrib_IT_obs h),
     ae_all_iff.2 (hasCondDistrib_IT_action h),
diff --git a/LeanMachineLearning/SequentialLearning/Comap.lean b/LeanMachineLearning/SequentialLearning/Comap.lean
index 78392f5a..bda9378f 100644
--- a/LeanMachineLearning/SequentialLearning/Comap.lean
+++ b/LeanMachineLearning/SequentialLearning/Comap.lean
@@ -136,12 +136,13 @@ lemma Algorithm.policy_comap (alg : Algorithm 𝓞 𝓐 𝓨)
     (alg.comap F hF).policy n = (alg.policy n).comap (F n) (hF n) := rfl
 
 @[simp]
-lemma Algorithm.p0_comap (alg : Algorithm 𝓞 𝓐 𝓨)
+lemma Algorithm.policyZero_comap (alg : Algorithm 𝓞 𝓐 𝓨)
     {F : (n : ℕ) → Hist 𝓞' 𝓐 𝓨' n × 𝓞' → Hist 𝓞 𝓐 𝓨 n × 𝓞} (hF : ∀ n, Measurable (F n)) :
-    (alg.comap F hF).p0
-      = alg.p0.comap (fun o ↦ (F 0 (default, o)).2) (((hF 0).comp measurable_prodMk_left).snd) := by
+    (alg.comap F hF).policyZero
+      = alg.policyZero.comap (fun o ↦ (F 0 (default, o)).2)
+          (((hF 0).comp measurable_prodMk_left).snd) := by
   ext o : 1
-  rw [p0_apply, policy_comap, Kernel.comap_apply, alg.policy_zero, Kernel.comap_apply]
+  rw [policyZero_apply, policy_comap, Kernel.comap_apply, alg.policy_zero, Kernel.comap_apply]
 
 @[simp]
 lemma Algorithm.comap_id (alg : Algorithm 𝓞 𝓐 𝓨) :
@@ -172,10 +173,10 @@ lemma Algorithm.policy_comapObs (alg : Algorithm 𝓞 𝓐 𝓨) (hf : Measurabl
       = (alg.policy n).comap (fun p ↦ (Hist.mapObs f p.1, f p.2)) (by fun_prop) := rfl
 
 @[simp]
-lemma Algorithm.p0_comapObs (alg : Algorithm 𝓞 𝓐 𝓨) (hf : Measurable f) :
-    (alg.comapObs f hf).p0 = alg.p0.comap f hf := by
+lemma Algorithm.policyZero_comapObs (alg : Algorithm 𝓞 𝓐 𝓨) (hf : Measurable f) :
+    (alg.comapObs f hf).policyZero = alg.policyZero.comap f hf := by
   ext o : 1
-  rw [p0_apply, policy_comapObs, Kernel.comap_apply, alg.policy_zero, Kernel.comap_apply]
+  rw [policyZero_apply, policy_comapObs, Kernel.comap_apply, alg.policy_zero, Kernel.comap_apply]
 
 @[simp]
 lemma Algorithm.comapObs_id (alg : Algorithm 𝓞 𝓐 𝓨) : alg.comapObs id measurable_id = alg := rfl
@@ -205,10 +206,10 @@ lemma Algorithm.policy_comapFeedback (alg : Algorithm 𝓞 𝓐 𝓨) (hg : Meas
       = (alg.policy n).comap (fun p ↦ (Hist.mapFeedback g p.1, p.2)) (by fun_prop) := rfl
 
 @[simp]
-lemma Algorithm.p0_comapFeedback (alg : Algorithm 𝓞 𝓐 𝓨) (hg : Measurable g) :
-    (alg.comapFeedback g hg).p0 = alg.p0 := by
+lemma Algorithm.policyZero_comapFeedback (alg : Algorithm 𝓞 𝓐 𝓨) (hg : Measurable g) :
+    (alg.comapFeedback g hg).policyZero = alg.policyZero := by
   ext o : 1
-  rw [p0_apply, policy_comapFeedback, Kernel.comap_apply, alg.policy_zero, p0_apply]
+  rw [policyZero_apply, policy_comapFeedback, Kernel.comap_apply, alg.policy_zero, policyZero_apply]
 
 @[simp]
 lemma Algorithm.comapFeedback_id (alg : Algorithm 𝓞 𝓐 𝓨) :
@@ -255,17 +256,18 @@ lemma Environment.feedback_comap (env : Environment 𝓞 𝓐 𝓨) (hF : ∀ n,
       = (env.feedback n).comap (fun p ↦ ((F n p.1.1, p.1.2), f p.2)) (by fun_prop) := rfl
 
 @[simp]
-lemma Environment.obs0_comap (env : Environment 𝓞 𝓐 𝓨) (hF : ∀ n, Measurable (F n))
+lemma Environment.obsZero_comap (env : Environment 𝓞 𝓐 𝓨) (hF : ∀ n, Measurable (F n))
     (hf : Measurable f) :
-    (env.comap F hF f hf).obs0 = env.obs0 := by
-  rw [Environment.obs0_def, obs_comap, Kernel.comap_apply, env.obs_zero]
+    (env.comap F hF f hf).obsZero = env.obsZero := by
+  rw [Environment.obsZero_def, obs_comap, Kernel.comap_apply, env.obs_zero]
 
 @[simp]
-lemma Environment.ν0_comap (env : Environment 𝓞 𝓐 𝓨) (hF : ∀ n, Measurable (F n))
+lemma Environment.feedbackZero_comap (env : Environment 𝓞 𝓐 𝓨) (hF : ∀ n, Measurable (F n))
     (hf : Measurable f) :
-    (env.comap F hF f hf).ν0 = env.ν0.comap (fun p ↦ (p.1, f p.2)) (by fun_prop) := by
+    (env.comap F hF f hf).feedbackZero
+      = env.feedbackZero.comap (fun p ↦ (p.1, f p.2)) (by fun_prop) := by
   ext p : 1
-  rw [Environment.ν0_apply, feedback_comap, Kernel.comap_apply, env.feedback_zero,
+  rw [Environment.feedbackZero_apply, feedback_comap, Kernel.comap_apply, env.feedback_zero,
     Kernel.comap_apply]
 
 @[simp]
@@ -299,15 +301,16 @@ lemma Environment.feedback_comapAction (env : Environment 𝓞 𝓐 𝓨) (hf :
       (fun p ↦ ((Hist.mapAction f p.1.1, p.1.2), f p.2)) (by fun_prop) := rfl
 
 @[simp]
-lemma Environment.obs0_comapAction (env : Environment 𝓞 𝓐 𝓨) (hf : Measurable f) :
-    (env.comapAction f hf).obs0 = env.obs0 := by
-  rw [Environment.obs0_def, obs_comapAction, Kernel.comap_apply, env.obs_zero]
+lemma Environment.obsZero_comapAction (env : Environment 𝓞 𝓐 𝓨) (hf : Measurable f) :
+    (env.comapAction f hf).obsZero = env.obsZero := by
+  rw [Environment.obsZero_def, obs_comapAction, Kernel.comap_apply, env.obs_zero]
 
 @[simp]
-lemma Environment.ν0_comapAction (env : Environment 𝓞 𝓐 𝓨) (hf : Measurable f) :
-    (env.comapAction f hf).ν0 = env.ν0.comap (fun p ↦ (p.1, f p.2)) (by fun_prop) := by
+lemma Environment.feedbackZero_comapAction (env : Environment 𝓞 𝓐 𝓨) (hf : Measurable f) :
+    (env.comapAction f hf).feedbackZero
+      = env.feedbackZero.comap (fun p ↦ (p.1, f p.2)) (by fun_prop) := by
   ext p : 1
-  rw [Environment.ν0_apply, feedback_comapAction, Kernel.comap_apply, env.feedback_zero,
+  rw [Environment.feedbackZero_apply, feedback_comapAction, Kernel.comap_apply, env.feedback_zero,
     Kernel.comap_apply]
 
 @[simp]
@@ -341,11 +344,11 @@ lemma Algorithm.policy_congr (alg : Algorithm 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃
       (fun p ↦ (Hist.map e𝓞.symm e𝓐.symm e𝓨.symm p.1, e𝓞.symm p.2)) (by fun_prop) := rfl
 
 @[simp]
-lemma Algorithm.p0_congr (alg : Algorithm 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐')
+lemma Algorithm.policyZero_congr (alg : Algorithm 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐')
     (e𝓨 : 𝓨 ≃ᵐ 𝓨') :
-    (alg.congr e𝓞 e𝓐 e𝓨).p0 = (alg.p0.map e𝓐).comap e𝓞.symm e𝓞.symm.measurable := by
+    (alg.congr e𝓞 e𝓐 e𝓨).policyZero = (alg.policyZero.map e𝓐).comap e𝓞.symm e𝓞.symm.measurable := by
   ext o : 1
-  rw [p0_apply, policy_congr, Kernel.comap_apply, Kernel.map_apply _ e𝓐.measurable,
+  rw [policyZero_apply, policy_congr, Kernel.comap_apply, Kernel.map_apply _ e𝓐.measurable,
     alg.policy_zero, Kernel.comap_apply, Kernel.map_apply _ e𝓐.measurable]
 
 @[simp]
@@ -402,19 +405,19 @@ lemma Environment.feedback_congr (env : Environment 𝓞 𝓐 𝓨) (e𝓞 : 
       (by fun_prop) := rfl
 
 @[simp]
-lemma Environment.obs0_congr (env : Environment 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐')
+lemma Environment.obsZero_congr (env : Environment 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐')
     (e𝓨 : 𝓨 ≃ᵐ 𝓨') :
-    (env.congr e𝓞 e𝓐 e𝓨).obs0 = env.obs0.map e𝓞 := by
-  rw [Environment.obs0_def, obs_congr, Kernel.comap_apply, Kernel.map_apply _ e𝓞.measurable,
+    (env.congr e𝓞 e𝓐 e𝓨).obsZero = env.obsZero.map e𝓞 := by
+  rw [Environment.obsZero_def, obs_congr, Kernel.comap_apply, Kernel.map_apply _ e𝓞.measurable,
     env.obs_zero]
 
 @[simp]
-lemma Environment.ν0_congr (env : Environment 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐')
+lemma Environment.feedbackZero_congr (env : Environment 𝓞 𝓐 𝓨) (e𝓞 : 𝓞 ≃ᵐ 𝓞') (e𝓐 : 𝓐 ≃ᵐ 𝓐')
     (e𝓨 : 𝓨 ≃ᵐ 𝓨') :
-    (env.congr e𝓞 e𝓐 e𝓨).ν0
-      = (env.ν0.map e𝓨).comap (fun p ↦ (e𝓞.symm p.1, e𝓐.symm p.2)) (by fun_prop) := by
+    (env.congr e𝓞 e𝓐 e𝓨).feedbackZero
+      = (env.feedbackZero.map e𝓨).comap (fun p ↦ (e𝓞.symm p.1, e𝓐.symm p.2)) (by fun_prop) := by
   ext p : 1
-  rw [Environment.ν0_apply, feedback_congr, Kernel.comap_apply,
+  rw [Environment.feedbackZero_apply, feedback_congr, Kernel.comap_apply,
     Kernel.map_apply _ e𝓨.measurable, env.feedback_zero, Kernel.comap_apply,
     Kernel.map_apply _ e𝓨.measurable]
 
diff --git a/LeanMachineLearning/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean
index 66784d36..ab7824b0 100644
--- a/LeanMachineLearning/SequentialLearning/Deterministic.lean
+++ b/LeanMachineLearning/SequentialLearning/Deterministic.lean
@@ -17,28 +17,33 @@ kernel. Similarly, a deterministic environment gives feedback in a deterministic
 
 ## Main definitions
 
-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
+We introduce two typeclasses `Algorithm.IsDeterministic` and
+`Environment.HasDeterministicFeedback` to express that an algorithm is deterministic or that an
+environment gives deterministic feedback. 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.
-* `nextAction alg n`: the function that gives the action of a deterministic algorithm `alg`
-  at step `n`, as a function of the history before `n` and of the observation at step `n`.
-* `actionZero alg`: the initial action of a deterministic algorithm `alg`, as a function of the
-  first observation. This is `nextAction alg 0` applied to the empty history.
-* `feedbackFun env n`: the function that gives the feedback of a deterministic environment `env`
-  at step `n`, as a function of the history, the current observation and the current action.
-* `feedbackFunZero env`: the function that gives the initial feedback of a deterministic
-  environment `env`. This is `feedbackFun env 0` applied to the empty history.
-
-* `detAlgorithm nextA h_next`: a deterministic algorithm that chooses its action
+* `Algorithm.IsDeterministic alg`: a typeclass expressing that the algorithm `alg` is
+  deterministic.
+* `Environment.HasDeterministicFeedback env`: a typeclass expressing that the feedback of the
+  environment `env` is deterministic.
+* `Algorithm.nextAction alg n`: the function that gives the action of a deterministic algorithm
+  `alg` at step `n`, as a function of the history before `n` and of the observation at step `n`.
+* `Algorithm.actionZero alg`: the initial action of a deterministic algorithm `alg`, as a function
+  of the first observation. This is `alg.nextAction 0` applied to the empty history.
+* `Environment.feedbackFun env n`: the function that gives the feedback of a deterministic
+  environment `env` at step `n`, as a function of the history, the current observation and the
+  current action.
+* `Environment.feedbackFunZero env`: the function that gives the initial feedback of a
+  deterministic environment `env`. This is `env.feedbackFun 0` applied to the empty history.
+
+* `Algorithm.deterministic nextA h_next`: a deterministic algorithm that chooses its action
   according to the measurable function `nextA` (with proof of measurability `h_next`).
   The initial action is `fun o ↦ nextA 0 (default, o)`.
-* `detEnvironment obs f hf`: a deterministic environment with observation kernels `obs`, that gives
-  feedback according to the measurable function `f` (with proof of measurability `hf`).
+* `Environment.detFeedback obs f hf`: an environment with observation kernels `obs`, that gives
+  deterministic feedback according to the measurable function `f` (with proof of measurability
+  `hf`).
 
 -/
 
@@ -55,178 +60,186 @@ variable {𝓞 𝓐 𝓨 : Type*} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : Measur
 
 /-- An algorithm is deterministic if its actions are determined by measurable functions of the
 history and of the current observation (and not possibly random kernels). -/
-class IsDeterministicAlg (alg : Algorithm 𝓞 𝓐 𝓨) : Prop where
+class Algorithm.IsDeterministic (alg : Algorithm 𝓞 𝓐 𝓨) : Prop where
   exists_nextAction n : ∃ (nextAction : (Hist 𝓞 𝓐 𝓨 n × 𝓞) → 𝓐) (h_meas : Measurable nextAction),
     alg.policy n = Kernel.deterministic nextAction h_meas
 
+namespace Algorithm
+
 /-- The action of a deterministic algorithm at step `n`, as a function of the history before `n`
 and of the observation at step `n`. -/
 noncomputable
-def nextAction (alg : Algorithm 𝓞 𝓐 𝓨) [h_det : IsDeterministicAlg alg] (n : ℕ) :
+def nextAction (alg : Algorithm 𝓞 𝓐 𝓨) [h_det : alg.IsDeterministic] (n : ℕ) :
     (Hist 𝓞 𝓐 𝓨 n × 𝓞) → 𝓐 :=
   (h_det.exists_nextAction n).choose
 
 /-- The initial action of a deterministic algorithm, as a function of the first observation. -/
 noncomputable
-def actionZero (alg : Algorithm 𝓞 𝓐 𝓨) [IsDeterministicAlg alg] : 𝓞 → 𝓐 :=
-  fun o ↦ nextAction alg 0 (default, o)
+def actionZero (alg : Algorithm 𝓞 𝓐 𝓨) [alg.IsDeterministic] : 𝓞 → 𝓐 :=
+  fun o ↦ alg.nextAction 0 (default, o)
 
 @[fun_prop]
-lemma measurable_nextAction (alg : Algorithm 𝓞 𝓐 𝓨) [IsDeterministicAlg alg] (n : ℕ) :
-    Measurable (nextAction alg n) :=
-  (IsDeterministicAlg.exists_nextAction n).choose_spec.choose
+lemma measurable_nextAction (alg : Algorithm 𝓞 𝓐 𝓨) [alg.IsDeterministic] (n : ℕ) :
+    Measurable (alg.nextAction n) :=
+  (IsDeterministic.exists_nextAction n).choose_spec.choose
 
 @[fun_prop]
-lemma measurable_actionZero (alg : Algorithm 𝓞 𝓐 𝓨) [IsDeterministicAlg alg] :
-    Measurable (actionZero alg) :=
-  (measurable_nextAction alg 0).comp (measurable_const.prodMk measurable_id)
+lemma measurable_actionZero (alg : Algorithm 𝓞 𝓐 𝓨) [alg.IsDeterministic] :
+    Measurable alg.actionZero :=
+  (alg.measurable_nextAction 0).comp (measurable_const.prodMk measurable_id)
 
-lemma policy_eq_deterministic (alg : Algorithm 𝓞 𝓐 𝓨) [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
+lemma policy_eq_deterministic (alg : Algorithm 𝓞 𝓐 𝓨) [h_det : alg.IsDeterministic] (n : ℕ) :
+    alg.policy n = Kernel.deterministic (alg.nextAction n) (alg.measurable_nextAction n) :=
+  (IsDeterministic.exists_nextAction n).choose_spec.choose_spec
 
-lemma nextAction_zero (alg : Algorithm 𝓞 𝓐 𝓨) [IsDeterministicAlg alg] (h : Hist 𝓞 𝓐 𝓨 0)
+lemma nextAction_zero (alg : Algorithm 𝓞 𝓐 𝓨) [alg.IsDeterministic] (h : Hist 𝓞 𝓐 𝓨 0)
     (o : 𝓞) :
-    nextAction alg 0 (h, o) = actionZero alg o := by
+    alg.nextAction 0 (h, o) = alg.actionZero o := by
   rw [Unique.eq_default h]
   rfl
 
-lemma p0_eq_deterministic (alg : Algorithm 𝓞 𝓐 𝓨) [IsDeterministicAlg alg] :
-    alg.p0 = Kernel.deterministic (actionZero alg) (measurable_actionZero alg) := by
+lemma policyZero_eq_deterministic (alg : Algorithm 𝓞 𝓐 𝓨) [alg.IsDeterministic] :
+    alg.policyZero = Kernel.deterministic alg.actionZero alg.measurable_actionZero := by
   ext o : 1
-  rw [Algorithm.p0_apply, policy_eq_deterministic, Kernel.deterministic_apply,
+  rw [policyZero_apply, policy_eq_deterministic, Kernel.deterministic_apply,
     Kernel.deterministic_apply]
   rfl
 
-namespace IsDeterministicAlg
+end Algorithm
+
+namespace Algorithm.IsDeterministic
 
 variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
   {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : Measure Ω} [IsFiniteMeasure P]
   {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {n N : ℕ}
 
 lemma action_ae_eq_of_IsAlgEnvSeqUntil [MeasurableEq 𝓐]
-    [h_det : IsDeterministicAlg alg] (h : IsAlgEnvSeqUntil O A Y alg env P N) (hn : n < N) :
-    A n =ᵐ[P] fun ω ↦ nextAction alg n (history O A Y n ω, O n ω) := by
+    [h_det : alg.IsDeterministic] (h : IsAlgEnvSeqUntil O A Y alg env P N) (hn : n < N) :
+    A n =ᵐ[P] fun ω ↦ alg.nextAction n (history O A Y n ω, O n ω) := by
   have h_eq := (h.hasCondDistrib_action n hn)
-  rw [policy_eq_deterministic alg n] at h_eq
+  rw [alg.policy_eq_deterministic n] at h_eq
   have hO := h.measurable_obs
   have hA := h.measurable_action
   have hY := h.measurable_feedback
   exact ae_eq_of_hasCondDistrib_deterministic (measurable_nextAction _ _) (by fun_prop)
     (by fun_prop) h_eq
 
-lemma action_zero_of_IsAlgEnvSeqUntil [MeasurableEq 𝓐] [h_det : IsDeterministicAlg alg]
+lemma action_zero_of_IsAlgEnvSeqUntil [MeasurableEq 𝓐] [h_det : alg.IsDeterministic]
     (h : IsAlgEnvSeqUntil O A Y alg env P N) (hN : 0 < N) :
-    A 0 =ᵐ[P] fun ω ↦ actionZero alg (O 0 ω) := by
+    A 0 =ᵐ[P] fun ω ↦ alg.actionZero (O 0 ω) := by
   filter_upwards [action_ae_eq_of_IsAlgEnvSeqUntil h hN] with ω hω
   rw [hω, nextAction_zero]
 
-lemma hasCondDistrib_action_zero_of_IsAlgEnvSeqUntil [h_det : IsDeterministicAlg alg]
+lemma hasCondDistrib_action_zero_of_IsAlgEnvSeqUntil [h_det : alg.IsDeterministic]
     (h : IsAlgEnvSeqUntil O A Y alg env P N) (hN : 0 < N) :
     HasCondDistrib (A 0) (O 0)
-      (Kernel.deterministic (actionZero alg) (measurable_actionZero alg)) P := by
-  rw [← p0_eq_deterministic]
+      (Kernel.deterministic alg.actionZero alg.measurable_actionZero) P := by
+  rw [← policyZero_eq_deterministic]
   exact h.hasCondDistrib_action_zero hN
 
-lemma hasCondDistrib_action_zero [h_det : IsDeterministicAlg alg]
+lemma hasCondDistrib_action_zero [h_det : alg.IsDeterministic]
     (h : IsAlgEnvSeq O A Y alg env P) :
     HasCondDistrib (A 0) (O 0)
-      (Kernel.deterministic (actionZero alg) (measurable_actionZero alg)) P :=
+      (Kernel.deterministic alg.actionZero alg.measurable_actionZero) P :=
   hasCondDistrib_action_zero_of_IsAlgEnvSeqUntil (h.isAlgEnvSeqUntil 1) zero_lt_one
 
-lemma action_ae_eq [MeasurableEq 𝓐] [h_det : IsDeterministicAlg alg]
+lemma action_ae_eq [MeasurableEq 𝓐] [h_det : alg.IsDeterministic]
     (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
-    A n =ᵐ[P] fun ω ↦ nextAction alg n (history O A Y n ω, O n ω) :=
+    A n =ᵐ[P] fun ω ↦ alg.nextAction n (history O A Y n ω, O n ω) :=
   action_ae_eq_of_IsAlgEnvSeqUntil (h.isAlgEnvSeqUntil (n + 1)) n.lt_succ_self
 
-lemma action_zero_ae_eq [MeasurableEq 𝓐] [h_det : IsDeterministicAlg alg]
+lemma action_zero_ae_eq [MeasurableEq 𝓐] [h_det : alg.IsDeterministic]
     (h : IsAlgEnvSeq O A Y alg env P) :
-    A 0 =ᵐ[P] fun ω ↦ actionZero alg (O 0 ω) :=
+    A 0 =ᵐ[P] fun ω ↦ alg.actionZero (O 0 ω) :=
   action_zero_of_IsAlgEnvSeqUntil (h.isAlgEnvSeqUntil 1) zero_lt_one
 
-lemma action_ae_all_eq [MeasurableEq 𝓐] [h_det : IsDeterministicAlg alg]
+lemma action_ae_all_eq [MeasurableEq 𝓐] [h_det : alg.IsDeterministic]
     (h : IsAlgEnvSeq O A Y alg env P) :
-    ∀ᵐ ω ∂P, ∀ n, A n ω = nextAction alg n (history O A Y n ω, O n ω) :=
+    ∀ᵐ ω ∂P, ∀ n, A n ω = alg.nextAction n (history O A Y n ω, O n ω) :=
   ae_all_iff.mpr (action_ae_eq h)
 
-end IsDeterministicAlg
+end Algorithm.IsDeterministic
 
-/-- An environment is deterministic if its feedbacks are determined by measurable functions of
-the history, the observation and the action (and not possibly random kernels). -/
-class IsDeterministicEnv (env : Environment 𝓞 𝓐 𝓨) : Prop where
+/-- An environment has deterministic feedback if its feedbacks are determined by measurable
+functions of the history, the observation and the action (and not possibly random kernels). -/
+class Environment.HasDeterministicFeedback (env : Environment 𝓞 𝓐 𝓨) : Prop where
   exists_f : ∀ n, ∃ (f : ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐) → 𝓨) (hf : Measurable f),
     env.feedback n = Kernel.deterministic f hf
 
+namespace Environment
+
 /-- The feedback function of a deterministic environment at step `n`. -/
 noncomputable
-def feedbackFun (env : Environment 𝓞 𝓐 𝓨) [h_det : IsDeterministicEnv env] (n : ℕ) :
+def feedbackFun (env : Environment 𝓞 𝓐 𝓨) [h_det : env.HasDeterministicFeedback] (n : ℕ) :
     ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐) → 𝓨 :=
   (h_det.exists_f n).choose
 
 @[fun_prop]
-lemma measurable_feedbackFun (env : Environment 𝓞 𝓐 𝓨) [IsDeterministicEnv env] (n : ℕ) :
-    Measurable (feedbackFun env n) :=
-  (IsDeterministicEnv.exists_f n).choose_spec.choose
+lemma measurable_feedbackFun (env : Environment 𝓞 𝓐 𝓨) [env.HasDeterministicFeedback] (n : ℕ) :
+    Measurable (env.feedbackFun n) :=
+  (HasDeterministicFeedback.exists_f n).choose_spec.choose
 
-lemma feedback_eq_deterministic (env : Environment 𝓞 𝓐 𝓨) [IsDeterministicEnv env] (n : ℕ) :
-    env.feedback n = Kernel.deterministic (feedbackFun env n) (measurable_feedbackFun env n) :=
-  (IsDeterministicEnv.exists_f n).choose_spec.choose_spec
+lemma feedback_eq_deterministic (env : Environment 𝓞 𝓐 𝓨) [env.HasDeterministicFeedback] (n : ℕ) :
+    env.feedback n = Kernel.deterministic (env.feedbackFun n) (env.measurable_feedbackFun n) :=
+  (HasDeterministicFeedback.exists_f n).choose_spec.choose_spec
 
 /-- The initial feedback function of a deterministic environment, as a function of the first
 observation and the first action. -/
 noncomputable
-def feedbackFunZero (env : Environment 𝓞 𝓐 𝓨) [IsDeterministicEnv env] : 𝓞 × 𝓐 → 𝓨 :=
-  fun p ↦ feedbackFun env 0 ((default, p.1), p.2)
+def feedbackFunZero (env : Environment 𝓞 𝓐 𝓨) [env.HasDeterministicFeedback] : 𝓞 × 𝓐 → 𝓨 :=
+  fun p ↦ env.feedbackFun 0 ((default, p.1), p.2)
 
 @[fun_prop]
-lemma measurable_feedbackFunZero (env : Environment 𝓞 𝓐 𝓨) [IsDeterministicEnv env] :
-    Measurable (feedbackFunZero env) :=
-  (measurable_feedbackFun env 0).comp
+lemma measurable_feedbackFunZero (env : Environment 𝓞 𝓐 𝓨) [env.HasDeterministicFeedback] :
+    Measurable env.feedbackFunZero :=
+  (env.measurable_feedbackFun 0).comp
     ((measurable_const.prodMk measurable_fst).prodMk measurable_snd)
 
-lemma feedbackFun_zero (env : Environment 𝓞 𝓐 𝓨) [IsDeterministicEnv env] (h : Hist 𝓞 𝓐 𝓨 0)
+lemma feedbackFun_zero (env : Environment 𝓞 𝓐 𝓨) [env.HasDeterministicFeedback] (h : Hist 𝓞 𝓐 𝓨 0)
     (o : 𝓞) (a : 𝓐) :
-    feedbackFun env 0 ((h, o), a) = feedbackFunZero env (o, a) := by
+    env.feedbackFun 0 ((h, o), a) = env.feedbackFunZero (o, a) := by
   rw [Unique.eq_default h]
   rfl
 
-lemma ν0_eq_deterministic (env : Environment 𝓞 𝓐 𝓨) [IsDeterministicEnv env] :
-    env.ν0 = Kernel.deterministic (feedbackFunZero env) (measurable_feedbackFunZero env) := by
+lemma feedbackZero_eq_deterministic (env : Environment 𝓞 𝓐 𝓨) [env.HasDeterministicFeedback] :
+    env.feedbackZero = Kernel.deterministic env.feedbackFunZero env.measurable_feedbackFunZero := by
   ext p : 1
-  rw [Environment.ν0_def, Kernel.comap_apply, feedback_eq_deterministic, Kernel.deterministic_apply,
+  rw [feedbackZero_def, Kernel.comap_apply, feedback_eq_deterministic, Kernel.deterministic_apply,
     Kernel.deterministic_apply]
   rfl
 
-namespace IsDeterministicEnv
+end Environment
+
+namespace Environment.HasDeterministicFeedback
 
 variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
   {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : Measure Ω} [IsFiniteMeasure P]
   {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
 
-lemma hasCondDistrib_feedback [h_det : IsDeterministicEnv env]
+lemma hasCondDistrib_feedback [h_det : env.HasDeterministicFeedback]
     (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
     HasCondDistrib (Y n) (fun ω ↦ ((history O A Y n ω, O n ω), A n ω))
-      (Kernel.deterministic (feedbackFun env n) (measurable_feedbackFun env n)) P := by
+      (Kernel.deterministic (env.feedbackFun n) (env.measurable_feedbackFun n)) P := by
   rw [← feedback_eq_deterministic]
   exact h.hasCondDistrib_feedback n
 
-lemma hasCondDistrib_feedback_zero [h_det : IsDeterministicEnv env]
+lemma hasCondDistrib_feedback_zero [h_det : env.HasDeterministicFeedback]
     (h : IsAlgEnvSeq O A Y alg env P) :
     HasCondDistrib (Y 0) (fun ω ↦ (O 0 ω, A 0 ω))
-      (Kernel.deterministic (feedbackFunZero env) (measurable_feedbackFunZero env)) P := by
-  rw [← ν0_eq_deterministic]
+      (Kernel.deterministic env.feedbackFunZero env.measurable_feedbackFunZero) P := by
+  rw [← feedbackZero_eq_deterministic]
   exact h.hasCondDistrib_feedback_zero
 
-lemma feedback_ae_eq [MeasurableEq 𝓨] [h_det : IsDeterministicEnv env]
+lemma feedback_ae_eq [MeasurableEq 𝓨] [h_det : env.HasDeterministicFeedback]
     (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
-    Y n =ᵐ[P] fun ω ↦ feedbackFun env n ((history O A Y n ω, O n ω), A n ω) := by
+    Y n =ᵐ[P] fun ω ↦ env.feedbackFun n ((history O A Y n ω, O n ω), A n ω) := by
   have hO := h.measurable_obs
   have hA := h.measurable_action
   have hY := h.measurable_feedback
   exact ae_eq_of_hasCondDistrib_deterministic (measurable_feedbackFun _ _) (by fun_prop)
     (by fun_prop) (hasCondDistrib_feedback h n)
 
-end IsDeterministicEnv
+end Environment.HasDeterministicFeedback
 
 variable {nextA : (n : ℕ) → (Hist 𝓞 𝓐 𝓨 n × 𝓞) → 𝓐} {h_next : ∀ n, Measurable (nextA n)}
   {env : Environment 𝓞 𝓐 𝓨}
@@ -237,38 +250,38 @@ variable {nextA : (n : ℕ) → (Hist 𝓞 𝓐 𝓨 n × 𝓞) → 𝓐} {h_nex
 The initial action is `fun o ↦ nextA 0 (default, o)`. -/
 @[simps]
 noncomputable
-def detAlgorithm (nextA : (n : ℕ) → (Hist 𝓞 𝓐 𝓨 n × 𝓞) → 𝓐)
+def Algorithm.deterministic (nextA : (n : ℕ) → (Hist 𝓞 𝓐 𝓨 n × 𝓞) → 𝓐)
     (h_next : ∀ n, Measurable (nextA n)) :
     Algorithm 𝓞 𝓐 𝓨 where
   policy n := Kernel.deterministic (nextA n) (h_next n)
 
-instance : IsDeterministicAlg (detAlgorithm nextA h_next) where
+instance : (Algorithm.deterministic nextA h_next).IsDeterministic where
   exists_nextAction n := ⟨nextA n, h_next n, rfl⟩
 
 @[simp]
-lemma p0_detAlgorithm :
-    (detAlgorithm nextA h_next).p0
+lemma policyZero_deterministic :
+    (Algorithm.deterministic nextA h_next).policyZero
       = Kernel.deterministic (fun o ↦ nextA 0 (default, o))
         ((h_next 0).comp (measurable_const.prodMk measurable_id)) := by
   ext o : 1
-  rw [Algorithm.p0_apply, detAlgorithm_policy, Kernel.deterministic_apply,
+  rw [Algorithm.policyZero_apply, Algorithm.deterministic_policy, Kernel.deterministic_apply,
     Kernel.deterministic_apply]
 
 @[simp]
-lemma nextAction_detAlgorithm [MeasurableSpace.SeparatesPoints 𝓐] (n : ℕ) :
-    nextAction (detAlgorithm nextA h_next) n = nextA n := by
-  have h_eq := policy_eq_deterministic (detAlgorithm nextA h_next) n
-  simpa [detAlgorithm] using h_eq.symm
+lemma nextAction_deterministic [MeasurableSpace.SeparatesPoints 𝓐] (n : ℕ) :
+    (Algorithm.deterministic nextA h_next).nextAction n = nextA n := by
+  have h_eq := (Algorithm.deterministic nextA h_next).policy_eq_deterministic n
+  simpa [Algorithm.deterministic] using h_eq.symm
 
 @[simp]
-lemma actionZero_detAlgorithm [MeasurableSpace.SeparatesPoints 𝓐] :
-    actionZero (detAlgorithm nextA h_next) = fun o ↦ nextA 0 (default, o) := by
-  unfold actionZero
-  rw [nextAction_detAlgorithm]
+lemma actionZero_deterministic [MeasurableSpace.SeparatesPoints 𝓐] :
+    (Algorithm.deterministic nextA h_next).actionZero = fun o ↦ nextA 0 (default, o) := by
+  unfold Algorithm.actionZero
+  rw [nextAction_deterministic]
 
 /-- A deterministic environment, where the feedback is given by evaluating
 fixed measurable functions. -/
-noncomputable def detEnvironment (obs : (n : ℕ) → Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞)
+noncomputable def Environment.detFeedback (obs : (n : ℕ) → Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞)
     [∀ n, IsMarkovKernel (obs n)]
     (f : (n : ℕ) → ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐) → 𝓨) (hf : ∀ n, Measurable (f n)) :
     Environment 𝓞 𝓐 𝓨 where
@@ -276,25 +289,26 @@ noncomputable def detEnvironment (obs : (n : ℕ) → Kernel (Hist 𝓞 𝓐 
   feedback n := (Kernel.deterministic (f n) (hf n))
 
 @[simp]
-lemma obs_detEnvironment (n : ℕ) : (detEnvironment obs f hf).obs n = obs n := rfl
+lemma obs_detFeedback (n : ℕ) : (Environment.detFeedback obs f hf).obs n = obs n := rfl
 
 @[simp]
-lemma feedback_detEnvironment (n : ℕ) :
-    (detEnvironment obs f hf).feedback n = Kernel.deterministic (f n) (hf n) := rfl
+lemma feedback_detFeedback (n : ℕ) :
+    (Environment.detFeedback obs f hf).feedback n = Kernel.deterministic (f n) (hf n) := rfl
 
-instance : IsDeterministicEnv (detEnvironment obs f hf) where
+instance : (Environment.detFeedback obs f hf).HasDeterministicFeedback where
   exists_f n := ⟨f n, hf n, rfl⟩
 
 @[simp]
-lemma feedbackFun_detEnvironment [MeasurableSpace.SeparatesPoints 𝓨] (n : ℕ) :
-    feedbackFun (detEnvironment obs f hf) n = f n := by
-  simpa [detEnvironment] using (feedback_eq_deterministic (detEnvironment obs f hf) n).symm
+lemma feedbackFun_detFeedback [MeasurableSpace.SeparatesPoints 𝓨] (n : ℕ) :
+    (Environment.detFeedback obs f hf).feedbackFun n = f n := by
+  simpa [Environment.detFeedback] using
+    ((Environment.detFeedback obs f hf).feedback_eq_deterministic n).symm
 
 @[simp]
-lemma feedbackFunZero_detEnvironment [MeasurableSpace.SeparatesPoints 𝓨] :
-    feedbackFunZero (detEnvironment obs f hf) = fun p ↦ f 0 ((default, p.1), p.2) := by
-  unfold feedbackFunZero
-  rw [feedbackFun_detEnvironment]
+lemma feedbackFunZero_detFeedback [MeasurableSpace.SeparatesPoints 𝓨] :
+    (Environment.detFeedback obs f hf).feedbackFunZero = fun p ↦ f 0 ((default, p.1), p.2) := by
+  unfold Environment.feedbackFunZero
+  rw [feedbackFun_detFeedback]
 
 namespace IsAlgEnvSeq
 
@@ -303,28 +317,28 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
   {P : Measure Ω} [IsProbabilityMeasure P]
   {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
 
-lemma hasCondDistrib_action_zero_detAlgorithm
-    (h : IsAlgEnvSeq O A Y (detAlgorithm nextA h_next) env P) :
+lemma hasCondDistrib_action_zero_deterministic
+    (h : IsAlgEnvSeq O A Y (Algorithm.deterministic nextA h_next) env P) :
     HasCondDistrib (A 0) (O 0)
       (Kernel.deterministic (fun o ↦ nextA 0 (default, o))
         ((h_next 0).comp (measurable_const.prodMk measurable_id))) P := by
-  rw [← p0_detAlgorithm]
+  rw [← policyZero_deterministic]
   exact h.hasCondDistrib_action_zero
 
-lemma action_detAlgorithm_ae_eq [MeasurableEq 𝓐]
-    (h : IsAlgEnvSeq O A Y (detAlgorithm nextA h_next) env P) (n : ℕ) :
+lemma action_deterministic_ae_eq [MeasurableEq 𝓐]
+    (h : IsAlgEnvSeq O A Y (Algorithm.deterministic nextA h_next) env P) (n : ℕ) :
     A n =ᵐ[P] fun ω ↦ nextA n (history O A Y n ω, O n ω) :=
-  (IsDeterministicAlg.action_ae_eq h n).trans (by simp)
+  (Algorithm.IsDeterministic.action_ae_eq h n).trans (by simp)
 
-lemma action_zero_detAlgorithm [MeasurableEq 𝓐]
-    (h : IsAlgEnvSeq O A Y (detAlgorithm nextA h_next) env P) :
+lemma action_zero_deterministic [MeasurableEq 𝓐]
+    (h : IsAlgEnvSeq O A Y (Algorithm.deterministic nextA h_next) env P) :
     A 0 =ᵐ[P] fun ω ↦ nextA 0 (default, O 0 ω) :=
-  (IsDeterministicAlg.action_zero_ae_eq h).trans (by simp)
+  (Algorithm.IsDeterministic.action_zero_ae_eq h).trans (by simp)
 
-lemma action_detAlgorithm_ae_all_eq [MeasurableEq 𝓐]
-    (h : IsAlgEnvSeq O A Y (detAlgorithm nextA h_next) env P) :
+lemma action_deterministic_ae_all_eq [MeasurableEq 𝓐]
+    (h : IsAlgEnvSeq O A Y (Algorithm.deterministic nextA h_next) env P) :
     ∀ᵐ ω ∂P, ∀ n, A n ω = nextA n (history O A Y n ω, O n ω) :=
-  ae_all_iff.mpr (action_detAlgorithm_ae_eq h)
+  ae_all_iff.mpr (action_deterministic_ae_eq h)
 
 end IsAlgEnvSeq
 
@@ -335,23 +349,23 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
   {P : Measure Ω} [IsProbabilityMeasure P]
   {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {N n : ℕ}
 
-lemma hasCondDistrib_action_zero_detAlgorithm
-    (h : IsAlgEnvSeqUntil O A Y (detAlgorithm nextA h_next) env P N) (hN : 0 < N) :
+lemma hasCondDistrib_action_zero_deterministic
+    (h : IsAlgEnvSeqUntil O A Y (Algorithm.deterministic nextA h_next) env P N) (hN : 0 < N) :
     HasCondDistrib (A 0) (O 0)
       (Kernel.deterministic (fun o ↦ nextA 0 (default, o))
         ((h_next 0).comp (measurable_const.prodMk measurable_id))) P := by
-  rw [← p0_detAlgorithm]
+  rw [← policyZero_deterministic]
   exact h.hasCondDistrib_action_zero hN
 
-lemma action_detAlgorithm_ae_eq [MeasurableEq 𝓐]
-    (h : IsAlgEnvSeqUntil O A Y (detAlgorithm nextA h_next) env P N) (hn : n < N) :
+lemma action_deterministic_ae_eq [MeasurableEq 𝓐]
+    (h : IsAlgEnvSeqUntil O A Y (Algorithm.deterministic nextA h_next) env P N) (hn : n < N) :
     A n =ᵐ[P] fun ω ↦ nextA n (history O A Y n ω, O n ω) :=
-  (IsDeterministicAlg.action_ae_eq_of_IsAlgEnvSeqUntil h hn).trans (by simp)
+  (Algorithm.IsDeterministic.action_ae_eq_of_IsAlgEnvSeqUntil h hn).trans (by simp)
 
-lemma action_zero_detAlgorithm [MeasurableEq 𝓐]
-    (h : IsAlgEnvSeqUntil O A Y (detAlgorithm nextA h_next) env P N) (hN : 0 < N) :
+lemma action_zero_deterministic [MeasurableEq 𝓐]
+    (h : IsAlgEnvSeqUntil O A Y (Algorithm.deterministic nextA h_next) env P N) (hN : 0 < N) :
     A 0 =ᵐ[P] fun ω ↦ nextA 0 (default, O 0 ω) :=
-  (IsDeterministicAlg.action_zero_of_IsAlgEnvSeqUntil h hN).trans (by simp)
+  (Algorithm.IsDeterministic.action_zero_of_IsAlgEnvSeqUntil h hN).trans (by simp)
 
 end IsAlgEnvSeqUntil
 
diff --git a/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean b/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean
index 3cad44da..d80f6b19 100644
--- a/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean
+++ b/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean
@@ -158,22 +158,22 @@ variable {O : ℕ → Ω → Unit} {O' : ℕ → Ω' → Unit} {alg : Algorithm
   {κ κ' : Kernel 𝓐 𝓨} [IsMarkovKernel κ] [IsMarkovKernel κ']
 
 /-- Chain rule for histories of a single algorithm versus two stationary environments. -/
-lemma IsAlgEnvSeq.klDiv_map_history_compProd (h : IsAlgEnvSeq O A Y alg (stationaryEnv κ) P)
-    (h' : IsAlgEnvSeq O' A' Y' alg (stationaryEnv κ') P') (M : ℕ) :
+lemma IsAlgEnvSeq.klDiv_map_history_compProd (h : IsAlgEnvSeq O A Y alg (Environment.bandit κ) P)
+    (h' : IsAlgEnvSeq O' A' Y' alg (Environment.bandit κ') P') (M : ℕ) :
     klDiv (P.map (history O A Y M)) (P'.map (history O' A' Y' M)) =
       ∑ t ∈ range M, klDiv (P.map (A t) ⊗ₘ κ) (P.map (A t) ⊗ₘ κ') := by
   rw [h.klDiv_map_history_stepKernel h']
   refine sum_congr rfl fun t _ ↦ ?_
   have h_obs := (h.hasCondDistrib_obs t).map_eq
-  rw [obs_stationaryEnv] at h_obs
-  rw [stepKernel_stationaryEnv, stepKernel_stationaryEnv,
+  rw [obs_bandit] at h_obs
+  rw [stepKernel_bandit, stepKernel_bandit,
     klDiv_compProd_compProd_compProd_prodMkLeft_eq_klDiv_comp_compProd, ← h_obs,
     ← (h.hasCondDistrib_action t).hasLaw_comp.map_eq]
 
 /-- Chain rule for histories of a single algorithm versus two stationary environments. -/
 lemma IsAlgEnvSeq.klDiv_map_history [MeasurableSpace.CountablyGenerated 𝓨]
-    (h : IsAlgEnvSeq O A Y alg (stationaryEnv κ) P)
-    (h' : IsAlgEnvSeq O' A' Y' alg (stationaryEnv κ') P') (M : ℕ) :
+    (h : IsAlgEnvSeq O A Y alg (Environment.bandit κ) P)
+    (h' : IsAlgEnvSeq O' A' Y' alg (Environment.bandit κ') P') (M : ℕ) :
     klDiv (P.map (history O A Y M)) (P'.map (history O' A' Y' M)) =
       ∑ t ∈ range M, ∫⁻ ω, klDiv (κ (A t ω)) (κ' (A t ω)) ∂P := by
   rw [h.klDiv_map_history_compProd h']
@@ -182,8 +182,8 @@ lemma IsAlgEnvSeq.klDiv_map_history [MeasurableSpace.CountablyGenerated 𝓨]
     lintegral_map (measurable_klDiv_kernel κ κ') (h.measurable_action t)]
 
 /-- Chain rule for trajectories of a single algorithm versus two stationary environments. -/
-lemma IsAlgEnvSeq.klDiv_map_trajectory_compProd (h : IsAlgEnvSeq O A Y alg (stationaryEnv κ) P)
-    (h' : IsAlgEnvSeq O' A' Y' alg (stationaryEnv κ') P') :
+lemma IsAlgEnvSeq.klDiv_map_trajectory_compProd (h : IsAlgEnvSeq O A Y alg (Environment.bandit κ) P)
+    (h' : IsAlgEnvSeq O' A' Y' alg (Environment.bandit κ') P') :
     klDiv (P.map (trajectory O A Y)) (P'.map (trajectory O' A' Y')) =
       ∑' t : ℕ, klDiv (P.map (A t) ⊗ₘ κ) (P.map (A t) ⊗ₘ κ') := by
   rw [klDiv_map_trajectory_eq_iSup h.measurable_obs h.measurable_action h.measurable_feedback
@@ -192,8 +192,8 @@ lemma IsAlgEnvSeq.klDiv_map_trajectory_compProd (h : IsAlgEnvSeq O A Y alg (stat
 
 /-- Chain rule for trajectories of a single algorithm versus two stationary environments. -/
 lemma IsAlgEnvSeq.klDiv_map_trajectory [MeasurableSpace.CountablyGenerated 𝓨]
-    (h : IsAlgEnvSeq O A Y alg (stationaryEnv κ) P)
-    (h' : IsAlgEnvSeq O' A' Y' alg (stationaryEnv κ') P') :
+    (h : IsAlgEnvSeq O A Y alg (Environment.bandit κ) P)
+    (h' : IsAlgEnvSeq O' A' Y' alg (Environment.bandit κ') P') :
     klDiv (P.map (trajectory O A Y)) (P'.map (trajectory O' A' Y')) =
       ∑' t : ℕ, ∫⁻ ω, klDiv (κ (A t ω)) (κ' (A t ω)) ∂P := by
   rw [h.klDiv_map_trajectory_compProd h']
diff --git a/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean b/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean
index fdae6c06..d60e522a 100644
--- a/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean
+++ b/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean
@@ -12,24 +12,26 @@ public import LeanMachineLearning.ForMathlib.Probability.Independence.CondDistri
 /-!
 # Function evaluation environments
 
-We define two environments, `onlineEvalEnv` and `evalEnv`, where the feedback 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.
+We define two environments, `Environment.evalSeq` and `Environment.eval`, where the feedback 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 feedback at time `n` is given by a
+* `Environment.evalSeq g hg`: A stationary environment where the feedback 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 feedback is given by a deterministic kernel
-  that evaluates a fixed measurable function `f` at the chosen action.
+* `Environment.eval f hf`: A stationary environment where the feedback 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`.
+They both satisfy the typeclasses `Environment.IsOblivious` and
+`Environment.HasDeterministicFeedback`, and `Environment.eval f hf` is also
+`Environment.IsStationary`.
 
 ## Main statements
 
-* `forall_feedback_onlineEvalEnv_ae_eq_eval_action`: For almost all `ω`, the feedback at time `n` is
+* `forall_feedback_evalSeq_ae_eq_eval_action`: For almost all `ω`, the feedback at time `n` is
   equal to `g n` evaluated at the action taken at time `n`.
-* `forall_feedback_evalEnv_ae_eq_eval_action`: For almost all `ω`, the feedback at time `n` is equal
+* `forall_feedback_eval_ae_eq_eval_action`: For almost all `ω`, the feedback at time `n` is equal
   to `f` evaluated at the action taken at time `n`.
 
 -/
@@ -46,32 +48,33 @@ variable {𝓐 𝓨 : Type*} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableS
 
 /-- The evaluation environment where the feedback is given by evaluating a fixed measurable function
 `f` at the chosen action. -/
-noncomputable def onlineEvalEnv (g : ℕ → 𝓐 → 𝓨) (hg : ∀ n, Measurable (g n)) :=
-  obliviousEnv (fun n ↦ Kernel.deterministic (g n) (hg n))
+noncomputable def Environment.evalSeq (g : ℕ → 𝓐 → 𝓨) (hg : ∀ n, Measurable (g n)) :=
+  Environment.banditSeq (fun n ↦ Kernel.deterministic (g n) (hg n))
 
-instance : IsObliviousEnv (onlineEvalEnv g hg) :=
-  ⟨⟨fun n ↦ Kernel.deterministic (g n) (hg n), fun _ ↦ inferInstance, fun _ ↦ rfl⟩⟩
+instance : (Environment.evalSeq g hg).IsOblivious :=
+  inferInstanceAs (Environment.banditSeq fun n ↦ Kernel.deterministic (g n) (hg n)).IsOblivious
 
-instance : IsDeterministicEnv (onlineEvalEnv g hg) where
+instance : (Environment.evalSeq g hg).HasDeterministicFeedback where
   exists_f n := ⟨fun p ↦ g n 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]
+lemma feedbackCondObsAction_evalSeq (n : ℕ) :
+    (Environment.evalSeq g hg).feedbackCondObsAction n
+      = Kernel.deterministic (fun p ↦ g n p.2) (by fun_prop) := by
+  simp [Environment.evalSeq]
 
 @[simp]
-lemma feedbackFun_onlineEvalEnv [MeasurableSpace.SeparatesPoints 𝓨] (n : ℕ) :
-    feedbackFun (onlineEvalEnv g hg) n = fun p ↦ g n p.2 := by
-  have h_eq := feedback_eq_deterministic (onlineEvalEnv g hg) n
-  simpa only [onlineEvalEnv, feedback_obliviousEnv, Kernel.prodMkLeft_deterministic,
+lemma feedbackFun_evalSeq [MeasurableSpace.SeparatesPoints 𝓨] (n : ℕ) :
+    (Environment.evalSeq g hg).feedbackFun n = fun p ↦ g n p.2 := by
+  have h_eq := (Environment.evalSeq g hg).feedback_eq_deterministic n
+  simpa only [Environment.evalSeq, feedback_banditSeq, Kernel.prodMkLeft_deterministic,
     Kernel.deterministic_inj] using h_eq.symm
 
 @[simp]
-lemma feedbackFunZero_onlineEvalEnv [MeasurableSpace.SeparatesPoints 𝓨] :
-    feedbackFunZero (onlineEvalEnv g hg) = fun p ↦ g 0 p.2 := by
-  unfold feedbackFunZero
-  rw [feedbackFun_onlineEvalEnv]
+lemma feedbackFunZero_evalSeq [MeasurableSpace.SeparatesPoints 𝓨] :
+    (Environment.evalSeq g hg).feedbackFunZero = fun p ↦ g 0 p.2 := by
+  unfold Environment.feedbackFunZero
+  rw [feedbackFun_evalSeq]
 
 section OnlineEvalEnv
 
@@ -80,46 +83,55 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {alg : Algorithm Unit 𝓐 𝓨
   {P : Measure Ω} [IsProbabilityMeasure P]
   {O : ℕ → Ω → Unit} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
 
-lemma hascondDistrib_feedback_onlineEvalEnv
-    (h : IsAlgEnvSeq O A Y alg (onlineEvalEnv g hg) P) (n : ℕ) :
-    HasCondDistrib (Y n) (A n) (Kernel.deterministic (g n) (hg n)) P := by
-  simpa using IsObliviousEnv.hasCondDistrib_feedback h n
+lemma hasCondDistrib_feedback_evalSeq
+    (h : IsAlgEnvSeq O A Y alg (Environment.evalSeq g hg) P) (n : ℕ) :
+    HasCondDistrib (Y n) (A n) (Kernel.deterministic (g n) (hg n)) P :=
+  h.hasCondDistrib_feedback_banditSeq n
 
-lemma feedback_onlineEvalEnv_ae_eq_eval_action [StandardBorelSpace 𝓨] [Nonempty 𝓨]
-    (h : IsAlgEnvSeq O A Y alg (onlineEvalEnv g hg) P) (n : ℕ) :
+lemma feedback_evalSeq_ae_eq_eval_action [StandardBorelSpace 𝓨] [Nonempty 𝓨]
+    (h : IsAlgEnvSeq O A Y alg (Environment.evalSeq g hg) P) (n : ℕ) :
     Y n =ᵐ[P] g n ∘ A n :=
   ae_eq_of_condDistrib_eq_deterministic (hg n) (h.measurable_action n).aemeasurable
     (h.measurable_feedback n).aemeasurable
-    (hascondDistrib_feedback_onlineEvalEnv h n).condDistrib_eq
+    (hasCondDistrib_feedback_evalSeq h n).condDistrib_eq
 
-lemma forall_feedback_onlineEvalEnv_ae_eq_eval_action [StandardBorelSpace 𝓨] [Nonempty 𝓨]
-    (h : IsAlgEnvSeq O A Y alg (onlineEvalEnv g hg) P) :
+lemma forall_feedback_evalSeq_ae_eq_eval_action [StandardBorelSpace 𝓨] [Nonempty 𝓨]
+    (h : IsAlgEnvSeq O A Y alg (Environment.evalSeq g hg) P) :
     ∀ᵐ ω ∂P, ∀ n, Y n ω = g n (A n ω) := by
   rw [ae_all_iff]
   intro n
-  exact feedback_onlineEvalEnv_ae_eq_eval_action h n
+  exact feedback_evalSeq_ae_eq_eval_action h n
 
 end OnlineEvalEnv
 
 /-- The evaluation environment where the feedback is given by evaluating a fixed measurable function
 `f` at the chosen action. -/
-noncomputable def evalEnv (f : 𝓐 → 𝓨) (hf : Measurable f) := onlineEvalEnv (fun _ ↦ f) (fun _ ↦ hf)
+noncomputable def Environment.eval (f : 𝓐 → 𝓨) (hf : Measurable f) :=
+  Environment.evalSeq (fun _ ↦ f) (fun _ ↦ hf)
 
-instance : IsObliviousEnv (evalEnv f hf) := by unfold evalEnv; infer_instance
+instance : (Environment.eval f hf).IsStationary where
+  exists_obs_eq_const := ⟨Measure.dirac (), inferInstance, fun _ ↦ rfl⟩
+  exists_feedback_eq_comap :=
+    ⟨(Kernel.deterministic f hf).prodMkLeft Unit, inferInstance, fun _ ↦ rfl⟩
 
-instance : IsDeterministicEnv (evalEnv f hf) := by unfold evalEnv; infer_instance
+instance : (Environment.eval f hf).IsOblivious := by unfold Environment.eval; infer_instance
+
+instance : (Environment.eval f hf).HasDeterministicFeedback := by
+  unfold Environment.eval; infer_instance
 
 @[simp]
-lemma feedbackCondAction_evalEnv (n : ℕ) :
-    feedbackCondAction (evalEnv f hf) n = Kernel.deterministic f hf := by simp [evalEnv]
+lemma feedbackCondObsAction_eval (n : ℕ) :
+    (Environment.eval f hf).feedbackCondObsAction n
+      = Kernel.deterministic (fun p ↦ f p.2) (by fun_prop) := by
+  simp [Environment.eval]
 
 @[simp]
-lemma feedbackFunZero_evalEnv [MeasurableSpace.SeparatesPoints 𝓨] :
-    feedbackFunZero (evalEnv f hf) = fun p ↦ f p.2 := by simp [evalEnv]
+lemma feedbackFunZero_eval [MeasurableSpace.SeparatesPoints 𝓨] :
+    (Environment.eval f hf).feedbackFunZero = fun p ↦ f p.2 := by simp [Environment.eval]
 
 @[simp]
-lemma feedbackFun_evalEnv [MeasurableSpace.SeparatesPoints 𝓨] (n : ℕ) :
-    feedbackFun (evalEnv f hf) n = fun p ↦ f p.2 := by simp [evalEnv]
+lemma feedbackFun_eval [MeasurableSpace.SeparatesPoints 𝓨] (n : ℕ) :
+    (Environment.eval f hf).feedbackFun n = fun p ↦ f p.2 := by simp [Environment.eval]
 
 section EvalEnv
 
@@ -128,23 +140,23 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {alg : Algorithm Unit 𝓐 𝓨
   {P : Measure Ω} [IsProbabilityMeasure P]
   {O : ℕ → Ω → Unit} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
 
-lemma hascondDistrib_feedback_evalEnv (h : IsAlgEnvSeq O A Y alg (evalEnv f hf) P) (n : ℕ) :
-    HasCondDistrib (Y n) (A n) (Kernel.deterministic f hf) P := by
-  simpa using IsObliviousEnv.hasCondDistrib_feedback h n
+lemma hasCondDistrib_feedback_eval (h : IsAlgEnvSeq O A Y alg (Environment.eval f hf) P) (n : ℕ) :
+    HasCondDistrib (Y n) (A n) (Kernel.deterministic f hf) P :=
+  h.hasCondDistrib_feedback_banditSeq n
 
-lemma feedback_evalEnv_ae_eq_eval_action [StandardBorelSpace 𝓨] [Nonempty 𝓨]
-  (h : IsAlgEnvSeq O A Y alg (evalEnv f hf) P) (n : ℕ) :
-    Y n =ᵐ[P] f ∘ A n := feedback_onlineEvalEnv_ae_eq_eval_action h n
+lemma feedback_eval_ae_eq_eval_action [StandardBorelSpace 𝓨] [Nonempty 𝓨]
+  (h : IsAlgEnvSeq O A Y alg (Environment.eval f hf) P) (n : ℕ) :
+    Y n =ᵐ[P] f ∘ A n := feedback_evalSeq_ae_eq_eval_action h n
 
-lemma forall_feedback_evalEnv_ae_eq_eval_action [StandardBorelSpace 𝓨] [Nonempty 𝓨]
-    (h : IsAlgEnvSeq O A Y alg (evalEnv f hf) P) :
-    ∀ᵐ ω ∂P, ∀ n, Y n ω = f (A n ω) := forall_feedback_onlineEvalEnv_ae_eq_eval_action h
+lemma forall_feedback_eval_ae_eq_eval_action [StandardBorelSpace 𝓨] [Nonempty 𝓨]
+    (h : IsAlgEnvSeq O A Y alg (Environment.eval f hf) P) :
+    ∀ᵐ ω ∂P, ∀ n, Y n ω = f (A n ω) := forall_feedback_evalSeq_ae_eq_eval_action h
 
 open Finset in
-lemma feedback_evalEnv_ae_eq_eval_action_comp {β : Type*} [StandardBorelSpace 𝓨] [Nonempty 𝓨]
-    (h : IsAlgEnvSeq O A Y alg (evalEnv f hf) P) {n : ℕ} (g : (Iic n → 𝓨) → β) :
+lemma feedback_eval_ae_eq_eval_action_comp {β : Type*} [StandardBorelSpace 𝓨] [Nonempty 𝓨]
+    (h : IsAlgEnvSeq O A Y alg (Environment.eval f hf) P) {n : ℕ} (g : (Iic n → 𝓨) → β) :
     ∀ᵐ ω ∂P, g (fun i ↦ Y i ω) = g (fun i ↦ f (A i ω)) := by
-  filter_upwards [forall_feedback_evalEnv_ae_eq_eval_action h] with ω hω
+  filter_upwards [forall_feedback_eval_ae_eq_eval_action h] with ω hω
   simp_rw [hω]
 
 end EvalEnv
diff --git a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
index 515c6874..9601a064 100644
--- a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
+++ b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
@@ -345,19 +345,20 @@ lemma isAlgEnvSeq_trajMeasure (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environmen
   hasCondDistrib_feedback n := hasCondDistrib_feedback alg env n
 
 lemma hasLaw_step_zero (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) :
-    HasLaw (step 0) (env.obs0 ⊗ₘ (alg.p0 ⊗ₖ env.ν0)) (trajMeasure alg env) :=
+    HasLaw (step 0) (env.obsZero ⊗ₘ (alg.policyZero ⊗ₖ env.feedbackZero)) (trajMeasure alg env) :=
   (isAlgEnvSeq_trajMeasure alg env).hasLaw_step_zero
 
 lemma hasLaw_obs_zero (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) :
-    HasLaw (obs 0) env.obs0 (trajMeasure alg env) :=
+    HasLaw (obs 0) env.obsZero (trajMeasure alg env) :=
   (isAlgEnvSeq_trajMeasure alg env).hasLaw_obs_zero
 
 lemma hasCondDistrib_action_zero (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) :
-    HasCondDistrib (action 0) (obs 0) alg.p0 (trajMeasure alg env) :=
+    HasCondDistrib (action 0) (obs 0) alg.policyZero (trajMeasure alg env) :=
   (isAlgEnvSeq_trajMeasure alg env).hasCondDistrib_action_zero
 
 lemma hasCondDistrib_feedback_zero (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) :
-    HasCondDistrib (feedback 0) (fun ω ↦ (obs 0 ω, action 0 ω)) env.ν0 (trajMeasure alg env) :=
+    HasCondDistrib (feedback 0) (fun ω ↦ (obs 0 ω, action 0 ω)) env.feedbackZero
+      (trajMeasure alg env) :=
   (isAlgEnvSeq_trajMeasure alg env).hasCondDistrib_feedback_zero
 
 end Laws
diff --git a/LeanMachineLearning/SequentialLearning/Means.lean b/LeanMachineLearning/SequentialLearning/Means.lean
index 6207a34f..62460fcb 100644
--- a/LeanMachineLearning/SequentialLearning/Means.lean
+++ b/LeanMachineLearning/SequentialLearning/Means.lean
@@ -65,22 +65,36 @@ noncomputable def Environment.means (env : Environment 𝓞 𝓐 𝓨) (O : ℕ
 @[simp]
 lemma means_zero (env : Environment 𝓞 𝓐 𝓨) (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨)
     (k : 𝓐) (ω : Ω) :
-    env.means O A Y k 0 ω = (env.ν0 (O 0 ω, k))[id] := by
+    env.means O A Y k 0 ω = (env.feedbackZero (O 0 ω, k))[id] := by
   simp [Environment.means, Environment.measure, Environment.feedback_zero]
 
 @[simp]
-lemma means_of_isObliviousEnv [IsObliviousEnv env] (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐)
+lemma means_of_isOblivious [env.IsOblivious] (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐)
     (Y : ℕ → Ω → 𝓨) (k : 𝓐) (n : ℕ) (ω : Ω) :
-    env.means O A Y k n ω = (feedbackCondAction env n k)[id] := by
-  simp [Environment.means, Environment.measure, feedback_eq_feedbackCondAction]
+    env.means O A Y k n ω = (env.feedbackCondObsAction n (O n ω, k))[id] := by
+  simp [Environment.means, Environment.measure, env.feedback_eq_comap_feedbackCondObsAction,
+    Kernel.comap_apply]
 
-lemma means_obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)]
+lemma means_of_isStationary [env.IsStationary] (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐)
+    (Y : ℕ → Ω → 𝓨) (k : 𝓐) (n : ℕ) (ω : Ω) :
+    env.means O A Y k n ω = (env.feedbackZero (O n ω, k))[id] := by
+  rw [means_of_isOblivious, env.feedbackCondObsAction_eq_feedbackZero]
+
+lemma means_oblivious (μ : ℕ → Measure 𝓞) [∀ n, IsProbabilityMeasure (μ n)]
+    (ν : ℕ → Kernel (𝓞 × 𝓐) 𝓨) [∀ n, IsMarkovKernel (ν n)] (k : 𝓐) (n : ℕ) (ω : Ω) :
+    (Environment.oblivious μ ν).means O A Y k n ω = (ν n (O n ω, k))[id] := by simp
+
+lemma means_stationary (μ : Measure 𝓞) [IsProbabilityMeasure μ] (ν : Kernel (𝓞 × 𝓐) 𝓨)
+    [IsMarkovKernel ν] (k : 𝓐) (n : ℕ) (ω : Ω) :
+    (Environment.stationary μ ν).means O A Y k n ω = (ν (O n ω, k))[id] := by simp
+
+lemma means_banditSeq (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)]
     {O : ℕ → Ω → Unit} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (k : 𝓐) (n : ℕ) (ω : Ω) :
-    (obliviousEnv ν).means O A Y k n ω = (ν n k)[id] := by simp
+    (Environment.banditSeq ν).means O A Y k n ω = (ν n k)[id] := by simp
 
-lemma means_stationaryEnv (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν]
+lemma means_bandit (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν]
     {O : ℕ → Ω → Unit} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (k : 𝓐) (n : ℕ) (ω : Ω) :
-    (stationaryEnv ν).means O A Y k n ω = (ν k)[id] := by simp
+    (Environment.bandit ν).means O A Y k n ω = (ν k)[id] := by simp
 
 @[fun_prop]
 lemma IsAlgEnvSeq.stronglyMeasurable_means [SecondCountableTopology 𝓨] [OpensMeasurableSpace 𝓨]
diff --git a/LeanMachineLearning/SequentialLearning/README.md b/LeanMachineLearning/SequentialLearning/README.md
new file mode 100644
index 00000000..eb0cecbf
--- /dev/null
+++ b/LeanMachineLearning/SequentialLearning/README.md
@@ -0,0 +1,94 @@
+# Naming of algorithms and environments
+
+The file `Algorithm.lean` defines the `Algorithm` and `Environment` structures.
+An algorithm has a sequence of Markov kernels (the policy) which reads a history and an observation and returns an action.
+```lean
+structure Algorithm (𝓞 𝓐 𝓨 : Type*) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
+    where
+  /-- Law of the action of round `n` given the past rounds and the current observation. -/
+  policy : (n : ℕ) → Kernel (Hist 𝓞 𝓐 𝓨 n × 𝓞) 𝓐
+  /-- The policy is a Markov kernel. -/
+  [isMarkovKernel_policy : ∀ n, IsMarkovKernel (policy n)]
+```
+An environment has two sequences of kernels: one for observations, which reads the history, and one for feedback, which reads the history, the current observation and the current action.
+```lean
+structure Environment (𝓞 𝓐 𝓨 : Type*) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
+    where
+  /-- Law of the observation of round `n` given the past rounds. -/
+  obs : (n : ℕ) → Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞
+  /-- Law of the feedback of round `n` given the past rounds, the observation and the action. -/
+  feedback : (n : ℕ) → Kernel ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐) 𝓨
+  /-- The observation kernel is a Markov kernel. -/
+  [isMarkovKernel_obs : ∀ n, IsMarkovKernel (obs n)]
+  /-- The feedback kernel is a Markov kernel. -/
+  [isMarkovKernel_feedback : ∀ n, IsMarkovKernel (feedback n)]
+```
+
+In many applications, some of those kernels are deterministic, or do not depend on some of their inputs.
+We detail here the naming conventions for the various constructors, predicates and accessors that are used in the library.
+
+NOTE: some names described below are marked as MISSING because they are not yet implemented in the library.
+They may never be implemented if we don't need them.
+If you need one of them, treat the name here as a recommendation that you may want to use.
+
+Generic constructions live in the `Algorithm` and `Environment` namespaces.
+Predicates live in the `Algorithm` and `Environment` namespaces: they are classes when they carry an accessor, and `Prop` definitions otherwise.
+Accessors are namespaced so that dot notation works.
+
+All time zero accessors are `…Zero` definitions. Example: `Algorithm.policyZero`.
+
+## Algorithms
+
+The policy at round `n` can depend on `n`, on the history at `n` and the current observation. It can be deterministic or stochastic.
+
+Not stochastic: `Algorithm.IsDeterministic`, `Algorithm.deterministic`
+
+No observation: `Algorithm.IgnoresObs` (MISSING), `Algorithm.comapObs fun _ ↦ ()`
+
+No history: `Algorithm.IsMarkov`, `Algorithm.markov`
+
+No history, no observation: `Algorithm.IsOpenLoop` (MISSING), `Algorithm.openLoop` (MISSING), `Algorithm.ofSeq` (MISSING) (det version)
+
+Not time-dependent, no history: `Algorithm.IsStationary` (MISSING), `Algorithm.stationary` (MISSING)
+
+No time, no history, no observation: `Algorithm.const`
+
+## Environments
+
+The observation at round `n` can depend on `n` and on the history at `n`, and can be deterministic or stochastic.
+
+The feedback at round `n` can depend on `n`, on the history at `n`, on the current observation and on the current action.
+It can be deterministic or stochastic.
+
+In general, the dependence on history is the same for both kernels.
+
+All for obs, no action for feedback: `Environment.FeedbackIgnoresAction` (MISSING), `Environment.adversary` (MISSING).
+
+No history for obs and feedback: `Environment.IsOblivious`, `Environment.oblivious`.
+
+No time, no history for obs and feedback: `Environment.IsStationary`, `Environment.stationary`.
+
+No time, last round of history for obs, not history for feedback: `Environment.IsMarkov` (MISSING), `Environment.markov` (MISSING).
+
+Determinism: `Environment.HasDeterministicObs` (MISSING), `Environment.HasDeterministicFeedback`, `Environment.detFeedback` (any observation kernels, deterministic feedback).
+
+### Obs = Unit
+
+Only the feedback matters, so the constructors are named by the feedback's shape.
+It can depend on time, history and action and be stochastic or deterministic.
+
+general: use `Environment` with Obs = Unit.
+
+No history: `Environment.banditSeq` and `Environment.bandit` (no time).
+
+No history, deterministic: `Environment.evalSeq` and `Environment.eval` (no time).
+
+No history, no action (only time): `Environment.indep` (MISSING) and `Environment.ofSeq` (MISSING) (deterministic).
+
+Nothing: `Environment.const` (MISSING) (stochastic). The deterministic version is probably not useful.
+
+## Examples
+
+Oblivious adversarial bandit environment: Obs = Unit, feedback depends on time and action, deterministic. Use `Environment.evalSeq`.
+
+Stochastic optimization: Obs = Unit, feedback depends on time and action, stochastic. Use `Environment.banditSeq`.
diff --git a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
index b652c7e5..dcd5571d 100644
--- a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
+++ b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
@@ -11,29 +11,41 @@ public import LeanMachineLearning.SequentialLearning.Algorithm
 /-!
 # Oblivious and stationary environments
 
-An oblivious environment is an environment in which the distribution of the next feedback depends
-only on the last action (and not on the past history nor on the current observation).
-If the kernel that gives the distribution of the next feedback given the last action is the same at
-every time step, then we say that the environment is stationary.
+An oblivious environment is an environment in which the distributions of the observation and of
+the feedback do not depend on the past history: at time `n`, the observation has law
+`env.obsLaw n`, and the feedback depends only on the current observation and action, through the
+Markov kernel `env.feedbackCondObsAction n`.
+A stationary environment is an oblivious environment in which these laws do not depend on time
+either: every observation has law `env.obsZero`, and the feedback is drawn from the Markov kernel
+`env.feedbackZero` applied to the current observation and action.
 
 ## Main definitions
 
-We define a `Prop`-valued typeclass `IsObliviousEnv` to express that an environment is oblivious,
-and we define two constructors for oblivious environments. Those constructors build environments
-without observations, that is with observation type `Unit`.
-
-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`.
+We define `Prop`-valued typeclasses `Environment.IsOblivious` and `Environment.IsStationary` to
+express that an environment is oblivious or stationary, and we define constructors for oblivious
+and stationary environments, with and without observations.
+
+Typeclasses and related definitions:
+* `Environment.IsOblivious env`: the environment `env` is oblivious.
+* `Environment.obsLaw env n`: the law of the observation at time `n` in an oblivious
+  environment `env`.
+* `Environment.feedbackCondObsAction env n`: the kernel representing the conditional distribution
+  of the feedback given the observation and the action at time `n` in an oblivious
+  environment `env`.
+* `Environment.IsStationary env`: the environment `env` is stationary. A stationary environment is
+  oblivious, and its laws are described by the time zero accessors `env.obsZero` and
+  `env.feedbackZero` (see `Environment.obs_eq_const_obsZero` and
+  `Environment.feedback_eq_comap_feedbackZero`).
 
 Constructors for oblivious environments:
-* `obliviousEnv ν`: an oblivious environment without observations, in which the distribution of the
-  next feedback depends only on the last action, but in a possibly time-dependent manner, and is
-  given by a sequence of Markov kernels `ν : ℕ → Kernel 𝓐 𝓨`.
-* `stationaryEnv ν`: a stationary environment without observations, in which the distribution of
-  the next feedback depends only on the last action (and not on the past history), and is given by
-  a Markov kernel `ν : Kernel 𝓐 𝓨`.
+* `Environment.oblivious μ ν`: the oblivious environment in which the observation at time `n` has
+  law `μ n` and the feedback at time `n` is drawn from the Markov kernel `ν n : Kernel (𝓞 × 𝓐) 𝓨`
+  applied to the observation and the action at time `n`.
+* `Environment.stationary μ ν`: the oblivious environment with constant sequences: the observations
+  have law `μ` and the feedback is drawn from `ν` applied to the observation and the action.
+* `Environment.banditSeq ν`, `Environment.bandit ν`: the versions without observations
+  (`𝓞 = Unit`), in which the feedback at time `n` is drawn from `ν n : Kernel 𝓐 𝓨`
+  (respectively from `ν : Kernel 𝓐 𝓨`) applied to the action at time `n`.
 
 -/
 
@@ -48,246 +60,593 @@ namespace Learning
 variable {𝓞 𝓐 𝓨 : Type*} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐}
   {m𝓨 : MeasurableSpace 𝓨}
 
-/-- An environment is oblivious if the distribution of the next feedback depends only on
-the last action and not on the past history nor on the current observation. -/
-class IsObliviousEnv (env : Environment 𝓞 𝓐 𝓨) : Prop where
-  exists_eq_prodMkLeft : ∃ ν : ℕ → Kernel 𝓐 𝓨, (∀ n, IsMarkovKernel (ν n)) ∧
-    (∀ n, env.feedback n = (ν n).prodMkLeft _)
+/-- An environment is oblivious if the distributions of the next observation and feedback
+don't depend on the past history: the observation at time `n` has a fixed law, and the feedback
+at time `n` depends only on the observation and the action at time `n`. -/
+class Environment.IsOblivious (env : Environment 𝓞 𝓐 𝓨) : Prop where
+  exists_obs_eq_const : ∃ μ : ℕ → Measure 𝓞, (∀ n, IsProbabilityMeasure (μ n)) ∧
+    ∀ n, env.obs n = Kernel.const _ (μ n)
+  exists_feedback_eq_comap : ∃ ν : ℕ → Kernel (𝓞 × 𝓐) 𝓨, (∀ n, IsMarkovKernel (ν n)) ∧
+    ∀ n, env.feedback n = (ν n).comap (fun p ↦ (p.1.2, p.2)) (by fun_prop)
+
+namespace Environment
+
+/-- The law of the observation at time `n` in an oblivious environment. -/
+noncomputable
+def obsLaw (env : Environment 𝓞 𝓐 𝓨) [h_obl : env.IsOblivious] (n : ℕ) : Measure 𝓞 :=
+  h_obl.exists_obs_eq_const.choose n
+
+instance (env : Environment 𝓞 𝓐 𝓨) [env.IsOblivious] (n : ℕ) :
+    IsProbabilityMeasure (env.obsLaw n) :=
+  IsOblivious.exists_obs_eq_const.choose_spec.1 n
+
+lemma obs_eq_const_obsLaw (env : Environment 𝓞 𝓐 𝓨) [env.IsOblivious] (n : ℕ) :
+    env.obs n = Kernel.const _ (env.obsLaw n) :=
+  IsOblivious.exists_obs_eq_const.choose_spec.2 n
 
-/-- The kernel representing the conditional distribution of the feedback given the action
-at time `n` in an oblivious environment. -/
+lemma obsZero_eq_obsLaw (env : Environment 𝓞 𝓐 𝓨) [env.IsOblivious] :
+    env.obsZero = env.obsLaw 0 := by
+  rw [Environment.obsZero_def, obs_eq_const_obsLaw, Kernel.const_apply]
+
+/-- The kernel representing the conditional distribution of the feedback given the observation and
+the action at time `n` in an oblivious environment. -/
 noncomputable
-def feedbackCondAction (env : Environment 𝓞 𝓐 𝓨) [h_obl : IsObliviousEnv env] (n : ℕ) :
-    Kernel 𝓐 𝓨 :=
-  h_obl.exists_eq_prodMkLeft.choose n
+def feedbackCondObsAction (env : Environment 𝓞 𝓐 𝓨) [h_obl : env.IsOblivious] (n : ℕ) :
+    Kernel (𝓞 × 𝓐) 𝓨 :=
+  h_obl.exists_feedback_eq_comap.choose n
 
-instance (env : Environment 𝓞 𝓐 𝓨) [IsObliviousEnv env] (n : ℕ) :
-    IsMarkovKernel (feedbackCondAction env n) :=
-  IsObliviousEnv.exists_eq_prodMkLeft.choose_spec.1 n
+instance (env : Environment 𝓞 𝓐 𝓨) [env.IsOblivious] (n : ℕ) :
+    IsMarkovKernel (env.feedbackCondObsAction n) :=
+  IsOblivious.exists_feedback_eq_comap.choose_spec.1 n
 
-lemma feedback_eq_feedbackCondAction (env : Environment 𝓞 𝓐 𝓨) [IsObliviousEnv env] (n : ℕ) :
-    env.feedback n = (feedbackCondAction env n).prodMkLeft _ :=
-  IsObliviousEnv.exists_eq_prodMkLeft.choose_spec.2 n
+lemma feedback_eq_comap_feedbackCondObsAction (env : Environment 𝓞 𝓐 𝓨) [env.IsOblivious]
+    (n : ℕ) :
+    env.feedback n = (env.feedbackCondObsAction n).comap (fun p ↦ (p.1.2, p.2)) (by fun_prop) :=
+  IsOblivious.exists_feedback_eq_comap.choose_spec.2 n
 
-lemma ν0_eq_feedbackCondAction (env : Environment 𝓞 𝓐 𝓨) [IsObliviousEnv env] :
-    env.ν0 = (feedbackCondAction env 0).prodMkLeft 𝓞 := by
+lemma feedbackZero_eq_feedbackCondObsAction (env : Environment 𝓞 𝓐 𝓨) [env.IsOblivious] :
+    env.feedbackZero = env.feedbackCondObsAction 0 := by
   ext p : 1
-  rw [Environment.ν0_def, Kernel.comap_apply, feedback_eq_feedbackCondAction,
-    Kernel.prodMkLeft_apply, Kernel.prodMkLeft_apply]
+  rw [Environment.feedbackZero_def, Kernel.comap_apply, feedback_eq_comap_feedbackCondObsAction,
+    Kernel.comap_apply]
+
+lemma obsLaw_eq_of_obs_eq_const [Nonempty 𝓐] [Nonempty 𝓨]
+    (env : Environment 𝓞 𝓐 𝓨) [env.IsOblivious] {n : ℕ} {μ : Measure 𝓞} [IsProbabilityMeasure μ]
+    (h : env.obs n = Kernel.const _ μ) :
+    env.obsLaw n = μ := by
+  have : Nonempty 𝓞 := Measure.nonempty_of_neZero μ
+  have h_eq := env.obs_eq_const_obsLaw n
+  rw [h, Kernel.ext_iff] at h_eq
+  simpa using (h_eq (Classical.arbitrary _)).symm
+
+lemma feedbackCondObsAction_eq_of_feedback_eq (env : Environment 𝓞 𝓐 𝓨) [env.IsOblivious]
+    {n : ℕ} {ν : Kernel (𝓞 × 𝓐) 𝓨} [hν : IsMarkovKernel ν]
+    (h : env.feedback n = ν.comap (fun p ↦ (p.1.2, p.2)) (by fun_prop)) :
+    env.feedbackCondObsAction n = ν := by
+  rcases isEmpty_or_nonempty 𝓞 with h𝓞 | h𝓞
+  · ext p : 1
+    exact h𝓞.elim p.1
+  rcases isEmpty_or_nonempty 𝓐 with h𝓐 | h𝓐
+  · ext p : 1
+    exact h𝓐.elim p.2
+  rcases isEmpty_or_nonempty 𝓨 with h𝓨 | h𝓨
+  · refine absurd hν ?_
+    rw [Subsingleton.eq_zero ν]
+    exact Kernel.not_isMarkovKernel_zero
+  have h_eq := env.feedback_eq_comap_feedbackCondObsAction n
+  rw [h, Kernel.ext_iff] at h_eq
+  ext p : 1
+  obtain ⟨o, a⟩ := p
+  exact (h_eq ((Classical.arbitrary _, o), a)).symm
+
+end Environment
 
-namespace IsObliviousEnv
+namespace Environment.IsOblivious
 
 variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
-  {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : Measure Ω} [IsFiniteMeasure P]
+  {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : Measure Ω}
   {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {n N : ℕ}
-  {ν : ℕ → Kernel 𝓐 𝓨} [∀ n, IsMarkovKernel (ν n)]
 
-lemma hasCondDistrib_feedback_history_action [IsObliviousEnv env]
+/-- The observation at time `n` has law `env.obsLaw n`. -/
+lemma hasLaw_obs [IsProbabilityMeasure P] [env.IsOblivious]
+    (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    HasLaw (O n) (env.obsLaw n) P := by
+  have h' := h.hasCondDistrib_obs n
+  rw [env.obs_eq_const_obsLaw] at h'
+  exact h'.hasLaw_of_const
+
+variable [IsFiniteMeasure P]
+
+lemma hasCondDistrib_feedback_history_action [env.IsOblivious]
     (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
     HasCondDistrib (Y n) (fun ω ↦ ((history O A Y n ω, O n ω), A n ω))
-      ((feedbackCondAction env n).prodMkLeft _) P := by
-  rw [← feedback_eq_feedbackCondAction]
+      ((env.feedbackCondObsAction n).comap (fun p ↦ (p.1.2, p.2)) (by fun_prop)
+        : Kernel ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐) 𝓨) P := by
+  rw [← env.feedback_eq_comap_feedbackCondObsAction]
   exact h.hasCondDistrib_feedback n
 
-lemma hasCondDistrib_feedback [IsObliviousEnv env] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
-    HasCondDistrib (Y n) (A n) (feedbackCondAction env n) P :=
+/-- The conditional distribution of the feedback at time `n` given the observation and the action
+at time `n` is `env.feedbackCondObsAction n`. -/
+lemma hasCondDistrib_feedback [env.IsOblivious] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    HasCondDistrib (Y n) (fun ω ↦ (O n ω, A n ω)) (env.feedbackCondObsAction n) P :=
   (hasCondDistrib_feedback_history_action h n).comp_right
 
-/-- Conditionally on an event determined by the history before time `n` and the action at time
-`n`, on which that action is equal to `b`, the feedback at time `n` has law
-`feedbackCondAction env n b`. -/
-lemma hasLaw_feedback_cond [IsObliviousEnv env] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ)
-    {s : Set ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐)} (hs : MeasurableSet s) {b : 𝓐} (hsb : ∀ u ∈ s, u.2 = b)
+/-- Conditionally on an event determined by the history before time `n`, the observation and the
+action at time `n`, on which the observation-action pair is equal to `b`, the feedback at time `n`
+has law `env.feedbackCondObsAction n b`. -/
+lemma hasLaw_feedback_cond [env.IsOblivious] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ)
+    {s : Set ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐)} (hs : MeasurableSet s) {b : 𝓞 × 𝓐}
+    (hsb : ∀ u ∈ s, (u.1.2, u.2) = b)
     (hP : P ((fun ω ↦ ((history O A Y n ω, O n ω), A n ω)) ⁻¹' s) ≠ 0) :
-    HasLaw (Y n) (feedbackCondAction env n b)
+    HasLaw (Y n) (env.feedbackCondObsAction n b)
       P[|(fun ω ↦ ((history O A Y n ω, O n ω), A n ω)) ⁻¹' s] := by
   refine (hasCondDistrib_feedback_history_action h n).hasLaw_cond (h.measurable_feedback _) hs
     (fun u hu ↦ ?_) hP
-  rw [Kernel.prodMkLeft_apply, hsb u hu]
+  rw [Kernel.comap_apply, hsb u hu]
 
-/-- Conditionally on an event determined by the history before time `n` and the action at time
-`n`, on which that action is constant, the feedback at time `n` is independent of the
-history before time `n` and of the action at time `n`. -/
-lemma indepFun_history_action_feedback_cond [IsObliviousEnv env]
+/-- Conditionally on an event determined by the history before time `n`, the observation and the
+action at time `n`, on which the observation-action pair is constant, the feedback at time `n` is
+independent of the history before time `n`, the observation and the action at time `n`. -/
+lemma indepFun_history_action_feedback_cond [env.IsOblivious]
     (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ)
-    {s : Set ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐)} (hs : MeasurableSet s) {b : 𝓐} (hsb : ∀ u ∈ s, u.2 = b) :
+    {s : Set ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐)} (hs : MeasurableSet s) {b : 𝓞 × 𝓐}
+    (hsb : ∀ u ∈ s, (u.1.2, u.2) = b) :
     (fun ω ↦ ((history O A Y n ω, O n ω), A n ω))
       ⟂ᵢ[P[|(fun ω ↦ ((history O A Y n ω, O n ω), A n ω)) ⁻¹' s]] Y n := by
   have hO := h.measurable_obs
   have hA := h.measurable_action
   have hY := h.measurable_feedback
   refine (hasCondDistrib_feedback_history_action h n).indepFun_cond (by fun_prop) hs
-    (η := feedbackCondAction env n b) fun u hu ↦ ?_
-  rw [Kernel.prodMkLeft_apply, hsb u hu]
+    (η := env.feedbackCondObsAction n b) fun u hu ↦ ?_
+  rw [Kernel.comap_apply, hsb u hu]
 
 variable [StandardBorelSpace 𝓞] [Nonempty 𝓞] [StandardBorelSpace 𝓐] [Nonempty 𝓐]
   [StandardBorelSpace 𝓨] [Nonempty 𝓨]
 
-/-- The feedback at time `n` is conditionally independent of the history before time `n` and of
-the observation at time `n`, given the action at time `n`. -/
-lemma condIndepFun_feedback_history_action [StandardBorelSpace Ω]
-        [IsObliviousEnv env] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
-    Y n ⟂ᵢ[A n, h.measurable_action _ ; P] (fun ω ↦ (history O A Y n ω, O n ω)) := by
+/-- The feedback at time `n` is conditionally independent of the history before time `n`, given
+the observation and the action at time `n`. -/
+lemma condIndepFun_feedback_history [StandardBorelSpace Ω]
+    [env.IsOblivious] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    Y n ⟂ᵢ[fun ω ↦ (O n ω, A n ω), (h.measurable_obs n).prodMk (h.measurable_action n); P]
+      history O A Y n := by
   have hO := h.measurable_obs
   have hA := h.measurable_action
   have hY := h.measurable_feedback
   refine condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft
-    (η := feedbackCondAction env n)
-    (by fun_prop) (by fun_prop) (by fun_prop) ?_
+    (η := env.feedbackCondObsAction n) (by fun_prop) (by fun_prop) (by fun_prop) ?_
   refine HasCondDistrib.condDistrib_eq ?_
-  rw [← feedback_eq_feedbackCondAction]
-  exact h.hasCondDistrib_feedback n
-
-lemma condIndepFun_feedback_history_action_action [StandardBorelSpace Ω]
-    [IsObliviousEnv env] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
-    Y n ⟂ᵢ[A n, h.measurable_action n; P] (fun ω ↦ ((history O A Y n ω, O n ω), A n ω)) := by
-  have h_indep : Y n ⟂ᵢ[A n, h.measurable_action n; P]
-      (fun ω ↦ (history O A Y n ω, O n ω)) := condIndepFun_feedback_history_action h n
+  have h' := hasCondDistrib_feedback_history_action h n
+  have hκ : ((env.feedbackCondObsAction n).comap (fun p ↦ (p.1.2, p.2)) (by fun_prop)
+        : Kernel ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐) 𝓨)
+      = ((env.feedbackCondObsAction n).prodMkLeft (Hist 𝓞 𝓐 𝓨 n)).comap
+          (fun p ↦ (p.1.1, (p.1.2, p.2))) (by fun_prop) := rfl
+  rw [hκ] at h'
+  exact h'.comp_right
+
+/-- The feedback at time `n` is conditionally independent of the history before time `n`, the
+observation and the action at time `n`, given the observation and the action at time `n`. -/
+lemma condIndepFun_feedback_history_obs_action [StandardBorelSpace Ω]
+    [env.IsOblivious] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    Y n ⟂ᵢ[fun ω ↦ (O n ω, A n ω), (h.measurable_obs n).prodMk (h.measurable_action n); P]
+      (fun ω ↦ (history O A Y n ω, (O n ω, A n ω))) := by
   have hO := h.measurable_obs
   have hA := h.measurable_action
   have hY := h.measurable_feedback
-  exact h_indep.prod_right (by fun_prop) (by fun_prop) (by fun_prop)
+  exact (condIndepFun_feedback_history h n).prod_right (by fun_prop) (by fun_prop) (by fun_prop)
+
+end Environment.IsOblivious
+
+/-- An environment is stationary if it is oblivious and its laws do not depend on time: the
+observations have a fixed law, and the feedback depends only on the current observation and action,
+through a fixed Markov kernel. -/
+class Environment.IsStationary (env : Environment 𝓞 𝓐 𝓨) : Prop where
+  exists_obs_eq_const : ∃ μ : Measure 𝓞, IsProbabilityMeasure μ ∧ ∀ n, env.obs n = Kernel.const _ μ
+  exists_feedback_eq_comap : ∃ ν : Kernel (𝓞 × 𝓐) 𝓨, IsMarkovKernel ν ∧
+    ∀ n, env.feedback n = ν.comap (fun p ↦ (p.1.2, p.2)) (by fun_prop)
+
+namespace Environment
+
+/-- In a stationary environment, the observation at every time has law `env.obsZero`. -/
+lemma obs_eq_const_obsZero (env : Environment 𝓞 𝓐 𝓨) [h : env.IsStationary] (n : ℕ) :
+    env.obs n = Kernel.const _ env.obsZero := by
+  obtain ⟨μ, -, hμ⟩ := h.exists_obs_eq_const
+  rw [hμ n, obsZero_def, hμ 0, Kernel.const_apply]
+
+/-- In a stationary environment, the feedback at every time is drawn from `env.feedbackZero` applied
+to the current observation and action. -/
+lemma feedback_eq_comap_feedbackZero (env : Environment 𝓞 𝓐 𝓨) [h : env.IsStationary] (n : ℕ) :
+    env.feedback n = env.feedbackZero.comap (fun p ↦ (p.1.2, p.2)) (by fun_prop) := by
+  obtain ⟨ν, -, hν⟩ := h.exists_feedback_eq_comap
+  have hν0 : env.feedbackZero = ν := by
+    ext p : 1
+    rw [feedbackZero_def, Kernel.comap_apply, hν 0, Kernel.comap_apply]
+  rw [hν n, hν0]
+
+instance (env : Environment 𝓞 𝓐 𝓨) [env.IsStationary] : env.IsOblivious where
+  exists_obs_eq_const := ⟨fun _ ↦ env.obsZero, fun _ ↦ inferInstance, env.obs_eq_const_obsZero⟩
+  exists_feedback_eq_comap :=
+    ⟨fun _ ↦ env.feedbackZero, fun _ ↦ inferInstance, env.feedback_eq_comap_feedbackZero⟩
+
+/-- In a stationary environment, the law of the observation at time `n` is `env.obsZero`. -/
+lemma obsLaw_eq_obsZero (env : Environment 𝓞 𝓐 𝓨) [env.IsStationary] [Nonempty 𝓐] [Nonempty 𝓨]
+    (n : ℕ) :
+    env.obsLaw n = env.obsZero :=
+  env.obsLaw_eq_of_obs_eq_const (env.obs_eq_const_obsZero n)
+
+/-- In a stationary environment, the conditional distribution of the feedback given the observation
+and the action at time `n` is `env.feedbackZero`. -/
+lemma feedbackCondObsAction_eq_feedbackZero (env : Environment 𝓞 𝓐 𝓨) [env.IsStationary]
+    (n : ℕ) :
+    env.feedbackCondObsAction n = env.feedbackZero :=
+  env.feedbackCondObsAction_eq_of_feedback_eq (env.feedback_eq_comap_feedbackZero n)
+
+end Environment
+
+namespace Environment.IsStationary
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
+  {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : Measure Ω}
+  {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
 
-end IsObliviousEnv
+/-- The observation at time `n` has law `env.obsZero`. -/
+lemma hasLaw_obs [IsProbabilityMeasure P] [env.IsStationary]
+    (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    HasLaw (O n) env.obsZero P := by
+  have h' := h.hasCondDistrib_obs n
+  rw [env.obs_eq_const_obsZero] at h'
+  exact h'.hasLaw_of_const
+
+variable [IsFiniteMeasure P]
+
+lemma hasCondDistrib_feedback_history_action [env.IsStationary]
+    (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    HasCondDistrib (Y n) (fun ω ↦ ((history O A Y n ω, O n ω), A n ω))
+      (env.feedbackZero.comap (fun p ↦ (p.1.2, p.2)) (by fun_prop)
+        : Kernel ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐) 𝓨) P := by
+  rw [← env.feedback_eq_comap_feedbackZero]
+  exact h.hasCondDistrib_feedback n
+
+/-- The conditional distribution of the feedback at time `n` given the observation and the action
+at time `n` is `env.feedbackZero`. -/
+lemma hasCondDistrib_feedback [env.IsStationary] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) :
+    HasCondDistrib (Y n) (fun ω ↦ (O n ω, A n ω)) env.feedbackZero P :=
+  (hasCondDistrib_feedback_history_action h n).comp_right
 
-/-- An oblivious environment without observations, in which the distribution of the next feedback
-depends only on the last action, but in a possibly time-dependent manner. -/
-@[simps]
+/-- Conditionally on an event determined by the history before time `n`, the observation and the
+action at time `n`, on which the observation-action pair is equal to `b`, the feedback at time `n`
+has law `env.feedbackZero b`. -/
+lemma hasLaw_feedback_cond [env.IsStationary] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ)
+    {s : Set ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐)} (hs : MeasurableSet s) {b : 𝓞 × 𝓐}
+    (hsb : ∀ u ∈ s, (u.1.2, u.2) = b)
+    (hP : P ((fun ω ↦ ((history O A Y n ω, O n ω), A n ω)) ⁻¹' s) ≠ 0) :
+    HasLaw (Y n) (env.feedbackZero b)
+      P[|(fun ω ↦ ((history O A Y n ω, O n ω), A n ω)) ⁻¹' s] := by
+  rw [← env.feedbackCondObsAction_eq_feedbackZero n]
+  exact IsOblivious.hasLaw_feedback_cond h n hs hsb hP
+
+end Environment.IsStationary
+
+section Oblivious
+
+variable {μ : ℕ → Measure 𝓞} [∀ n, IsProbabilityMeasure (μ n)]
+  {ν : ℕ → Kernel (𝓞 × 𝓐) 𝓨} [∀ n, IsMarkovKernel (ν n)]
+
+/-- The oblivious environment in which the observation at time `n` has law `μ n` and the feedback
+at time `n` is drawn from `ν n` applied to the observation and the action at time `n`, whatever the
+past history. -/
 noncomputable
-def obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)] : Environment Unit 𝓐 𝓨 where
-  obs _ := Kernel.const _ (Measure.dirac ())
-  feedback n := (ν n).prodMkLeft _
+def Environment.oblivious (μ : ℕ → Measure 𝓞) [∀ n, IsProbabilityMeasure (μ n)]
+    (ν : ℕ → Kernel (𝓞 × 𝓐) 𝓨) [∀ n, IsMarkovKernel (ν n)] : Environment 𝓞 𝓐 𝓨 where
+  obs n := Kernel.const _ (μ n)
+  feedback n := (ν n).comap (fun p ↦ (p.1.2, p.2)) (by fun_prop)
+
+@[simp]
+lemma obs_oblivious (n : ℕ) : (Environment.oblivious μ ν).obs n = Kernel.const _ (μ n) := rfl
 
-lemma feedback_obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)] (n : ℕ) :
-    (obliviousEnv ν).feedback n = (ν n).prodMkLeft _ := rfl
+@[simp]
+lemma feedback_oblivious (n : ℕ) :
+    (Environment.oblivious μ ν).feedback n = (ν n).comap (fun p ↦ (p.1.2, p.2)) (by fun_prop) := rfl
 
 @[simp]
-lemma obs0_obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)] :
-    (obliviousEnv ν).obs0 = Measure.dirac () := rfl
+lemma obsZero_oblivious : (Environment.oblivious μ ν).obsZero = μ 0 := rfl
 
 @[simp]
-lemma ν0_obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)] :
-    (obliviousEnv ν).ν0 = (ν 0).prodMkLeft Unit := by
+lemma feedbackZero_oblivious : (Environment.oblivious μ ν).feedbackZero = ν 0 := by
   ext p : 1
-  rw [Environment.ν0_def, Kernel.comap_apply, feedback_obliviousEnv, Kernel.prodMkLeft_apply,
-    Kernel.prodMkLeft_apply]
+  rw [Environment.feedbackZero_def, Kernel.comap_apply, feedback_oblivious, Kernel.comap_apply]
 
-instance (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)] :
-    IsObliviousEnv (obliviousEnv ν) where
-  exists_eq_prodMkLeft := ⟨ν, inferInstance, fun _ ↦ rfl⟩
+lemma stepKernel_oblivious (alg : Algorithm 𝓞 𝓐 𝓨) (n : ℕ) :
+    stepKernel alg (Environment.oblivious μ ν) n
+      = Kernel.const _ (μ n)
+        ⊗ₖ (alg.policy n ⊗ₖ (ν n).comap (fun p ↦ (p.1.2, p.2)) (by fun_prop)) :=
+  rfl
 
+instance : (Environment.oblivious μ ν).IsOblivious where
+  exists_obs_eq_const := ⟨μ, inferInstance, fun _ ↦ rfl⟩
+  exists_feedback_eq_comap := ⟨ν, inferInstance, fun _ ↦ rfl⟩
+
+/-- The law of the observations of `Environment.oblivious μ ν` is `μ`. The nonemptiness assumptions
+ensure that there are histories of every length, so that the observation kernels determine `μ`. -/
 @[simp]
-lemma feedbackCondAction_obliviousEnv (ν : ℕ → Kernel 𝓐 𝓨) [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 𝓨 with hR | hR
-  · refine absurd (hν 0) ?_
-    simp only [Subsingleton.eq_zero ν, Pi.zero_apply]
-    exact Kernel.not_isMarkovKernel_zero
-  have : Nonempty (Hist Unit 𝓐 𝓨 n × Unit) := ⟨(fun _ ↦ ((), h𝓐.some, hR.some), ())⟩
-  have h_eq := feedback_eq_feedbackCondAction (obliviousEnv ν) n
-  rw [feedback_obliviousEnv, Kernel.prodMkLeft_inj] at h_eq
-  exact h_eq.symm
+lemma obsLaw_oblivious [Nonempty 𝓐] [Nonempty 𝓨] (n : ℕ) :
+    (Environment.oblivious μ ν).obsLaw n = μ n :=
+  Environment.obsLaw_eq_of_obs_eq_const _ rfl
+
+@[simp]
+lemma feedbackCondObsAction_oblivious (n : ℕ) :
+    (Environment.oblivious μ ν).feedbackCondObsAction n = ν n :=
+  Environment.feedbackCondObsAction_eq_of_feedback_eq _ rfl
 
-/-- A stationary environment without observations, in which the distribution of the next feedback
-depends only on the last action. -/
+end Oblivious
+
+section Stationary
+
+variable {μ : Measure 𝓞} [IsProbabilityMeasure μ] {ν : Kernel (𝓞 × 𝓐) 𝓨} [IsMarkovKernel ν]
+
+/-- The stationary environment in which the observations have law `μ` and the feedback is drawn
+from `ν` applied to the observation and the action, whatever the past history. -/
 noncomputable
-def stationaryEnv (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν] : Environment Unit 𝓐 𝓨 :=
-  obliviousEnv fun _ ↦ ν
+def Environment.stationary (μ : Measure 𝓞) [IsProbabilityMeasure μ] (ν : Kernel (𝓞 × 𝓐) 𝓨)
+    [IsMarkovKernel ν] : Environment 𝓞 𝓐 𝓨 :=
+  Environment.oblivious (fun _ ↦ μ) (fun _ ↦ ν)
+
+lemma Environment.stationary_def :
+    Environment.stationary μ ν = Environment.oblivious (fun _ ↦ μ) (fun _ ↦ ν) := rfl
 
 @[simp]
-lemma obs_stationaryEnv (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν] (n : ℕ) :
-    (stationaryEnv ν).obs n = Kernel.const _ (Measure.dirac ()) := rfl
+lemma obs_stationary (n : ℕ) : (Environment.stationary μ ν).obs n = Kernel.const _ μ := rfl
 
 @[simp]
-lemma feedback_stationaryEnv (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν] (n : ℕ) :
-    (stationaryEnv ν).feedback n = ν.prodMkLeft _ := rfl
+lemma feedback_stationary (n : ℕ) :
+    (Environment.stationary μ ν).feedback n = ν.comap (fun p ↦ (p.1.2, p.2)) (by fun_prop) := rfl
 
-lemma stepKernel_stationaryEnv (alg : Algorithm Unit 𝓐 𝓨) (η : Kernel 𝓐 𝓨) [IsMarkovKernel η]
-    (n : ℕ) :
-    stepKernel alg (stationaryEnv η) n
-      = Kernel.const _ (Measure.dirac ()) ⊗ₖ (alg.policy n ⊗ₖ η.prodMkLeft _) := by
-  rw [stepKernel_def, obs_stationaryEnv, feedback_stationaryEnv]
+@[simp]
+lemma obsZero_stationary : (Environment.stationary μ ν).obsZero = μ := rfl
+
+@[simp]
+lemma feedbackZero_stationary : (Environment.stationary μ ν).feedbackZero = ν :=
+  feedbackZero_oblivious
+
+lemma stepKernel_stationary (alg : Algorithm 𝓞 𝓐 𝓨) (n : ℕ) :
+    stepKernel alg (Environment.stationary μ ν) n
+      = Kernel.const _ μ ⊗ₖ (alg.policy n ⊗ₖ ν.comap (fun p ↦ (p.1.2, p.2)) (by fun_prop)) :=
+  rfl
+
+instance : (Environment.stationary μ ν).IsStationary where
+  exists_obs_eq_const := ⟨μ, inferInstance, fun _ ↦ rfl⟩
+  exists_feedback_eq_comap := ⟨ν, inferInstance, fun _ ↦ rfl⟩
+
+instance : (Environment.stationary μ ν).IsOblivious :=
+  inferInstanceAs (Environment.oblivious _ _).IsOblivious
+
+@[simp]
+lemma obsLaw_stationary [Nonempty 𝓐] [Nonempty 𝓨] (n : ℕ) :
+    (Environment.stationary μ ν).obsLaw n = μ :=
+  obsLaw_oblivious n
+
+@[simp]
+lemma feedbackCondObsAction_stationary (n : ℕ) :
+    (Environment.stationary μ ν).feedbackCondObsAction n = ν :=
+  feedbackCondObsAction_oblivious n
+
+end Stationary
+
+section BanditSeq
+
+variable {ν : ℕ → Kernel 𝓐 𝓨} [∀ n, IsMarkovKernel (ν n)]
+
+/-- The oblivious environment without observations in which the feedback at time `n` is drawn from
+`ν n` applied to the action at time `n`, whatever the past history. -/
+noncomputable
+def Environment.banditSeq (ν : ℕ → Kernel 𝓐 𝓨) [∀ n, IsMarkovKernel (ν n)] :
+    Environment Unit 𝓐 𝓨 :=
+  Environment.oblivious (fun _ ↦ Measure.dirac ()) (fun n ↦ (ν n).prodMkLeft Unit)
+
+lemma Environment.banditSeq_def :
+    Environment.banditSeq ν
+      = Environment.oblivious (fun _ ↦ Measure.dirac ()) (fun n ↦ (ν n).prodMkLeft Unit) :=
+  rfl
+
+@[simp]
+lemma obs_banditSeq (n : ℕ) :
+    (Environment.banditSeq ν).obs n = Kernel.const _ (Measure.dirac ()) := rfl
+
+@[simp]
+lemma feedback_banditSeq (n : ℕ) : (Environment.banditSeq ν).feedback n = (ν n).prodMkLeft _ := rfl
+
+@[simp]
+lemma obsZero_banditSeq : (Environment.banditSeq ν).obsZero = Measure.dirac () := rfl
+
+@[simp]
+lemma feedbackZero_banditSeq : (Environment.banditSeq ν).feedbackZero = (ν 0).prodMkLeft Unit :=
+  feedbackZero_oblivious
+
+instance : (Environment.banditSeq ν).IsOblivious :=
+  inferInstanceAs (Environment.oblivious _ _).IsOblivious
+
+@[simp]
+lemma obsLaw_banditSeq (n : ℕ) : (Environment.banditSeq ν).obsLaw n = Measure.dirac () :=
+  Measure.eq_dirac_unit _
+
+@[simp]
+lemma feedbackCondObsAction_banditSeq (n : ℕ) :
+    (Environment.banditSeq ν).feedbackCondObsAction n = (ν n).prodMkLeft Unit :=
+  feedbackCondObsAction_oblivious n
+
+end BanditSeq
+
+section Bandit
+
+variable {ν : Kernel 𝓐 𝓨} [IsMarkovKernel ν]
+
+/-- The stationary environment without observations in which the feedback is drawn from `ν`
+applied to the action, whatever the past history: a stochastic bandit. -/
+noncomputable
+def Environment.bandit (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν] : Environment Unit 𝓐 𝓨 :=
+  Environment.stationary (Measure.dirac ()) (ν.prodMkLeft Unit)
+
+lemma Environment.bandit_def :
+    Environment.bandit ν = Environment.stationary (Measure.dirac ()) (ν.prodMkLeft Unit) := rfl
+
+lemma Environment.bandit_eq_banditSeq : Environment.bandit ν = Environment.banditSeq fun _ ↦ ν :=
+  rfl
 
 @[simp]
-lemma obs0_stationaryEnv (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν] :
-    (stationaryEnv ν).obs0 = Measure.dirac () := rfl
+lemma obs_bandit (n : ℕ) : (Environment.bandit ν).obs n = Kernel.const _ (Measure.dirac ()) := rfl
 
 @[simp]
-lemma ν0_stationaryEnv (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν] :
-    (stationaryEnv ν).ν0 = ν.prodMkLeft Unit :=
-  ν0_obliviousEnv _
+lemma feedback_bandit (n : ℕ) : (Environment.bandit ν).feedback n = ν.prodMkLeft _ := rfl
 
-instance (ν : Kernel 𝓐 𝓨) [IsMarkovKernel ν] : IsObliviousEnv (stationaryEnv ν) where
-  exists_eq_prodMkLeft := ⟨fun _ ↦ ν, inferInstance, fun _ ↦ rfl⟩
+lemma stepKernel_bandit (alg : Algorithm Unit 𝓐 𝓨) (n : ℕ) :
+    stepKernel alg (Environment.bandit ν) n
+      = Kernel.const _ (Measure.dirac ()) ⊗ₖ (alg.policy n ⊗ₖ ν.prodMkLeft _) := by
+  rw [stepKernel_def, obs_bandit, feedback_bandit]
 
 @[simp]
-lemma feedbackCondAction_stationaryEnv (ν : Kernel 𝓐 𝓨) [hν : IsMarkovKernel ν] (n : ℕ) :
-    feedbackCondAction (stationaryEnv ν) n = ν := feedbackCondAction_obliviousEnv _ _
+lemma obsZero_bandit : (Environment.bandit ν).obsZero = Measure.dirac () := rfl
+
+@[simp]
+lemma feedbackZero_bandit : (Environment.bandit ν).feedbackZero = ν.prodMkLeft Unit :=
+  feedbackZero_oblivious
+
+instance : (Environment.bandit ν).IsStationary :=
+  inferInstanceAs (Environment.stationary _ _).IsStationary
+
+instance : (Environment.bandit ν).IsOblivious :=
+  inferInstanceAs (Environment.oblivious _ _).IsOblivious
+
+@[simp]
+lemma obsLaw_bandit (n : ℕ) : (Environment.bandit ν).obsLaw n = Measure.dirac () :=
+  Measure.eq_dirac_unit _
+
+@[simp]
+lemma feedbackCondObsAction_bandit (n : ℕ) :
+    (Environment.bandit ν).feedbackCondObsAction n = ν.prodMkLeft Unit :=
+  feedbackCondObsAction_oblivious n
+
+end Bandit
+
+namespace IsAlgEnvSeq
+
+section General
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓞 𝓐 𝓨}
+  {P : Measure Ω} [IsProbabilityMeasure P]
+  {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
+
+/-- The observation at time `n` has law `μ n`. -/
+lemma hasLaw_obs_oblivious {μ : ℕ → Measure 𝓞} [∀ n, IsProbabilityMeasure (μ n)]
+    {ν : ℕ → Kernel (𝓞 × 𝓐) 𝓨} [∀ n, IsMarkovKernel (ν n)]
+    (h : IsAlgEnvSeq O A Y alg (Environment.oblivious μ ν) P) (n : ℕ) :
+    HasLaw (O n) (μ n) P := by
+  have h' := h.hasCondDistrib_obs n
+  rw [obs_oblivious] at h'
+  exact h'.hasLaw_of_const
+
+/-- The conditional distribution of the feedback at time `n` given the observation and the action
+at time `n` is `ν n`. -/
+lemma hasCondDistrib_feedback_oblivious {μ : ℕ → Measure 𝓞} [∀ n, IsProbabilityMeasure (μ n)]
+    {ν : ℕ → Kernel (𝓞 × 𝓐) 𝓨} [∀ n, IsMarkovKernel (ν n)]
+    (h : IsAlgEnvSeq O A Y alg (Environment.oblivious μ ν) P) (n : ℕ) :
+    HasCondDistrib (Y n) (fun ω ↦ (O n ω, A n ω)) (ν n) P := by
+  have h' := h.hasCondDistrib_feedback n
+  rw [feedback_oblivious] at h'
+  exact h'.comp_right
+
+/-- The observation at time `n` has law `μ`. -/
+lemma hasLaw_obs_stationary {μ : Measure 𝓞} [IsProbabilityMeasure μ]
+    {ν : Kernel (𝓞 × 𝓐) 𝓨} [IsMarkovKernel ν]
+    (h : IsAlgEnvSeq O A Y alg (Environment.stationary μ ν) P) (n : ℕ) :
+    HasLaw (O n) μ P :=
+  hasLaw_obs_oblivious h n
+
+/-- The conditional distribution of the feedback at time `n` given the observation and the action
+at time `n` is `ν`. -/
+lemma hasCondDistrib_feedback_stationary {μ : Measure 𝓞} [IsProbabilityMeasure μ]
+    {ν : Kernel (𝓞 × 𝓐) 𝓨} [IsMarkovKernel ν]
+    (h : IsAlgEnvSeq O A Y alg (Environment.stationary μ ν) P) (n : ℕ) :
+    HasCondDistrib (Y n) (fun ω ↦ (O n ω, A n ω)) ν P :=
+  hasCondDistrib_feedback_oblivious h n
+
+end General
+
+section Bandit
 
 variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
   {alg : Algorithm Unit 𝓐 𝓨} {ν : Kernel 𝓐 𝓨} [IsMarkovKernel ν]
   {P : Measure Ω} [IsProbabilityMeasure P]
   {O : ℕ → Ω → Unit} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
 
-namespace IsAlgEnvSeq
-
 /-- The conditional distribution of the feedback at time `n` given the action at time `n`
 is `ν n`. -/
-lemma hasCondDistrib_feedback_obliviousEnv {ν : ℕ → Kernel 𝓐 𝓨} [∀ n, IsMarkovKernel (ν n)]
-    (h : IsAlgEnvSeq O A Y alg (obliviousEnv ν) P) (n : ℕ) :
+lemma hasCondDistrib_feedback_banditSeq {ν : ℕ → Kernel 𝓐 𝓨} [∀ n, IsMarkovKernel (ν n)]
+    (h : IsAlgEnvSeq O A Y alg (Environment.banditSeq ν) P) (n : ℕ) :
     HasCondDistrib (Y n) (A n) (ν n) P := by
-  simpa using IsObliviousEnv.hasCondDistrib_feedback h n
+  have h' : HasCondDistrib (Y n) (fun ω ↦ (O n ω, A n ω)) ((ν n).prodMkLeft Unit) P :=
+    hasCondDistrib_feedback_oblivious h n
+  exact h'.comp_right
 
 /-- The conditional distribution of the feedback at time `n` given the action at time `n` is `ν`. -/
-lemma hasCondDistrib_feedback_stationaryEnv
-    (h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P) (n : ℕ) :
+lemma hasCondDistrib_feedback_bandit
+    (h : IsAlgEnvSeq O A Y alg (Environment.bandit ν) P) (n : ℕ) :
     HasCondDistrib (Y n) (A n) ν P :=
-  hasCondDistrib_feedback_obliviousEnv h n
+  hasCondDistrib_feedback_banditSeq h n
 
 /-- The conditional distribution of the feedback at time `n` given the action at time `n` is `ν`. -/
-lemma condDistrib_feedback_stationaryEnv [StandardBorelSpace 𝓨] [Nonempty 𝓨]
-    (h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P) (n : ℕ) :
+lemma condDistrib_feedback_bandit [StandardBorelSpace 𝓨] [Nonempty 𝓨]
+    (h : IsAlgEnvSeq O A Y alg (Environment.bandit ν) P) (n : ℕ) :
     condDistrib (Y n) (A n) P =ᵐ[P.map (A n)] ν :=
-  (hasCondDistrib_feedback_stationaryEnv h n).condDistrib_eq
+  (hasCondDistrib_feedback_bandit h n).condDistrib_eq
 
 /-- Conditionally on an event determined by the history before time `n` and the action at time
 `n`, on which that action is equal to `b`, the feedback at time `n` has law `ν b`. -/
-lemma hasLaw_feedback_cond_stationaryEnv (h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P) (n : ℕ)
+lemma hasLaw_feedback_cond_bandit (h : IsAlgEnvSeq O A Y alg (Environment.bandit ν) P) (n : ℕ)
     {s : Set ((Hist Unit 𝓐 𝓨 n × Unit) × 𝓐)} (hs : MeasurableSet s) {b : 𝓐}
     (hsb : ∀ u ∈ s, u.2 = b)
     (hP : P ((fun ω ↦ ((history O A Y n ω, O n ω), A n ω)) ⁻¹' s) ≠ 0) :
     HasLaw (Y n) (ν b) P[|(fun ω ↦ ((history O A Y n ω, O n ω), A n ω)) ⁻¹' s] := by
-  simpa using IsObliviousEnv.hasLaw_feedback_cond h n hs hsb hP
+  simpa using Environment.IsOblivious.hasLaw_feedback_cond h n hs (b := ((), b))
+    (fun u hu ↦ by simp [hsb u hu]) hP
 
 /-- Conditionally on an event determined by the history before time `n` and the action at time
 `n`, on which that action is constant, the feedback at time `n` is independent of the
 history before time `n` and of the action at time `n`. -/
-lemma indepFun_history_action_feedback_cond_stationaryEnv
-    (h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P) (n : ℕ)
+lemma indepFun_history_action_feedback_cond_bandit
+    (h : IsAlgEnvSeq O A Y alg (Environment.bandit ν) P) (n : ℕ)
     {s : Set ((Hist Unit 𝓐 𝓨 n × Unit) × 𝓐)} (hs : MeasurableSet s) {b : 𝓐}
     (hsb : ∀ u ∈ s, u.2 = b) :
     (fun ω ↦ ((history O A Y n ω, O n ω), A n ω))
       ⟂ᵢ[P[|(fun ω ↦ ((history O A Y n ω, O n ω), A n ω)) ⁻¹' s]] Y n :=
-  IsObliviousEnv.indepFun_history_action_feedback_cond h n hs hsb
+  Environment.IsOblivious.indepFun_history_action_feedback_cond h n hs (b := ((), b))
+    fun u hu ↦ by simp [hsb u hu]
 
 /-- The feedback at time `n` is conditionally independent of the history before time `n`
 given the action at time `n`. -/
-lemma condIndepFun_feedback_history_action [StandardBorelSpace Ω]
+lemma condIndepFun_feedback_history_action_bandit [StandardBorelSpace Ω]
     [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨]
-    (h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P) (n : ℕ) :
-    Y n ⟂ᵢ[A n, h.measurable_action _ ; P] (fun ω ↦ (history O A Y n ω, O n ω)) :=
-  IsObliviousEnv.condIndepFun_feedback_history_action h n
+    (h : IsAlgEnvSeq O A Y alg (Environment.bandit ν) P) (n : ℕ) :
+    Y n ⟂ᵢ[A n, h.measurable_action _ ; P] (fun ω ↦ (history O A Y n ω, O n ω)) := by
+  have hO := h.measurable_obs
+  have hA := h.measurable_action
+  have hY := h.measurable_feedback
+  refine condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft (η := ν)
+    (by fun_prop) (by fun_prop) (by fun_prop) ?_
+  refine HasCondDistrib.condDistrib_eq ?_
+  have h' := h.hasCondDistrib_feedback n
+  rwa [feedback_bandit] at h'
 
-lemma condIndepFun_feedback_history_action_action [StandardBorelSpace Ω]
+lemma condIndepFun_feedback_history_action_action_bandit [StandardBorelSpace Ω]
     [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨]
-    (h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P) (n : ℕ) :
+    (h : IsAlgEnvSeq O A Y alg (Environment.bandit ν) P) (n : ℕ) :
     Y n ⟂ᵢ[A n, h.measurable_action n; P]
-      (fun ω ↦ ((history O A Y n ω, O n ω), A n ω)) :=
-  IsObliviousEnv.condIndepFun_feedback_history_action_action h n
+      (fun ω ↦ ((history O A Y n ω, O n ω), A n ω)) := by
+  have hO := h.measurable_obs
+  have hA := h.measurable_action
+  have hY := h.measurable_feedback
+  exact (condIndepFun_feedback_history_action_bandit h n).prod_right (by fun_prop) (by fun_prop)
+    (by fun_prop)
+
+end Bandit
 
 end IsAlgEnvSeq