Docstrings

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.
 
 -/
 

LeanMachineLearning/SequentialLearning/Deterministic.lean

@@ -11,14 +11,21 @@ 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
 
 * `detAlgorithm nextAction h_next action0`: a deterministic algorithm that chooses its action
   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

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

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