From 18ba6ad391a4f219699ded3649d4fcf1f6be040b Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Sun, 12 Apr 2026 19:44:10 +0200
Subject: [PATCH] docstrings

---
 .../SequentialLearning/Algorithm.lean         | 20 ++++++++++++++++---
 .../SequentialLearning/Deterministic.lean     |  9 ++++++++-
 .../IonescuTulceaSpace.lean                   | 10 +++++++++-
 .../SequentialLearning/StationaryEnv.lean     | 10 ++++++++++
 4 files changed, 44 insertions(+), 5 deletions(-)

diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean
index ca9717a9..db2172f3 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithm.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean
@@ -9,19 +9,33 @@ public import LeanMachineLearning.ForMathlib.Measurable
 public import LeanMachineLearning.ForMathlib.Traj
 
 /-!
-# Algorithms
+# Algorithms and environments
+
+We define structures for stochastic, sequential algorithms and environments, and the notion of an
+algorithm-environment sequence, which is a sequence of actions and rewards generated by an algorithm
+interacting with an environment.
 
 ## Main definitions
 
 * `Algorithm α R`: a stochastic, sequential algorithm.
 * `Environment α R`: a stochastic environment.
-* `IsAlgEnvSeq A R' alg env P`: an algorithm-environment sequence. TODO
-* `IsAlgEnvSeqUntil A R' alg env P N`: an algorithm-environment sequence until time `N`. TODO
+* `IsAlgEnvSeq A R' alg env P`: an algorithm-environment sequence. That is, a sequence of
+  actions `A` and feedback `R'` that have the correct conditional distributions to be generated by
+  an algorithm `alg` interacting with an environment `env`, defined on a probability space `(Ω, P)`.
+* `IsAlgEnvSeqUntil A R' alg env P N`: `A` and `R'` form an algorithm-environment sequence until
+  time `N`.
 
 ## Main statements
 
 * `isAlgEnvSeq_unique`: the law of the sequence of actions and observations generated by an
   algorithm-environment pair is unique: it does not depend on the probability space used.
+  If `A₁`, `R₁` and `A₂`, `R₂` are two algorithm-environment sequences generated by the same
+  algorithm-environment pair on probability spaces `(Ω, P)` and `(Ω', P')`, then
+  `P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω))`.
+
+## Notes
+
+The `ANCHOR` comments are used to mark code that appears in the tutorials.
 
 -/
 
diff --git a/LeanMachineLearning/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean
index 5ca311c0..3f84fda8 100644
--- a/LeanMachineLearning/SequentialLearning/Deterministic.lean
+++ b/LeanMachineLearning/SequentialLearning/Deterministic.lean
@@ -11,7 +11,10 @@ public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
 # Deterministic algorithms
 
 A deterministic algorithm chooses its action in a deterministic way. That is, that action is given
-by a measurable function of the history and not by a Markov kernel.
+by a measurable function of the history instead of a general Markov kernel.
+
+We introduce a definition for those algorithms and prove results about the conditional distribution
+of the actions they generate when interacting with an environment.
 
 ## Main definitions
 
@@ -19,6 +22,10 @@ by a measurable function of the history and not by a Markov kernel.
   according to the measurable function `nextAction` (with proof of measurability `h_next`),
   with initial action `action0`.
 
+## Notes
+
+The `ANCHOR` comments are used to mark code that appears in the tutorials.
+
 -/
 
 @[expose] public section
diff --git a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
index e0aab116..5b2cc49f 100644
--- a/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
+++ b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
@@ -8,7 +8,15 @@ module
 public import LeanMachineLearning.SequentialLearning.Algorithm
 
 /-!
-# Algorithms
+# Probability space for algorithm-environment interactions
+
+For any algorithm and environment, we construct a probability space on which we can define
+a sequence of random variables representing the actions and feedback generated by the interaction
+of the algorithm and the environment.
+The main ingredient of the construction is the Ionescu-Tulcea theorem.
+
+TODO: actually, the probability measure is already defined in the Algorithm file. Reorganize?
+
 -/
 
 @[expose] public section
diff --git a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
index 874cd9a0..88e841cb 100644
--- a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
+++ b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
@@ -9,6 +9,16 @@ public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
 
 /-!
 # Stationary environments
+
+A stationary environment is an environment in which the distribution of the next reward depends only
+on the last action (and not on the past history).
+
+## Main definitions
+
+* `stationaryEnv ν`: a stationary environment, in which the distribution of the next reward depends
+  only on the last action (and not on the past history), and is given by a Markov kernel
+  `ν : Kernel α R`.
+
 -/
 
 @[expose] public section