diff --git a/.gitignore b/.gitignore
index 95ba36df..ad3d495a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -37,7 +37,15 @@ blueprint/src/web.pdf
 *.synctex.gz
 *.synctex.gz(busy)
 *.pdfsync
-## Verso
-/tutorial/.lake/
-/tutorial/html/
+
+## Website
 /home_page/
+
+## Tutorial
+/tutorial/.lake/
+/tutorial/_out/
+
+## Verso Blueprint
+/verso_blueprint/.lake/
+/verso_blueprint/.build/
+/verso_blueprint/_out/
diff --git a/build_all.sh b/build_all.sh
index 153cc9e5..c0875e81 100755
--- a/build_all.sh
+++ b/build_all.sh
@@ -3,15 +3,21 @@ set -x -e
 # Build tutorial
 cd tutorial
 lake build
-rm -rf html _out
-lake exe manual
-mkdir html
-mv _out/html-multi/* html/
-rm -rf _out
-mkdir -p html/static
-cp static_files/* html/static
+lake exe manual --output _out/site
+mkdir -p _out/site/html-multi/static
+cp static_files/* _out/site/html-multi/static
+cd ..
+
+cd verso_blueprint
+lake exe cache get
+lake build
+lake exe blueprint-gen --output _out/site
+mkdir -p _out/site/html-multi/static
+cp static_files/* _out/site/html-multi/static
 cd ..
 
 # Copy outputs to home_page
 mkdir -p home_page/tutorial
-cp -r tutorial/html/* home_page/tutorial
+cp -r tutorial/_out/site/html-multi/* home_page/tutorial
+mkdir -p home_page/verso_blueprint
+cp -r verso_blueprint/_out/site/html-multi/* home_page/verso_blueprint
diff --git a/verso_blueprint/LMLBlueprint.lean b/verso_blueprint/LMLBlueprint.lean
new file mode 100644
index 00000000..df46b6c8
--- /dev/null
+++ b/verso_blueprint/LMLBlueprint.lean
@@ -0,0 +1 @@
+import LMLBlueprint.Blueprint
diff --git a/verso_blueprint/LMLBlueprint/Blueprint.lean b/verso_blueprint/LMLBlueprint/Blueprint.lean
new file mode 100644
index 00000000..abbf1fc1
--- /dev/null
+++ b/verso_blueprint/LMLBlueprint/Blueprint.lean
@@ -0,0 +1,31 @@
+import Verso
+import VersoManual
+import VersoBlueprint
+import VersoBlueprint.Commands.Graph
+import VersoBlueprint.Commands.Summary
+import LMLBlueprint.Chapters.Algorithm
+import LMLBlueprint.Chapters.Bandit
+import LMLBlueprint.Chapters.BanditAlgs
+import LMLBlueprint.Chapters.Concentration
+import LMLBlueprint.Chapters.Intro
+
+open Verso.Genre
+open Verso.Genre.Manual
+open Informal
+
+set_option verso.blueprint.foldProofs true
+set_option verso.blueprint.summary.debugDiagnostics false
+
+#doc (Manual) "Lean Machine Learning" =>
+
+A Lean package for machine learning algorithms
+
+{include 0 LMLBlueprint.Chapters.Intro}
+{include 0 LMLBlueprint.Chapters.Algorithm}
+{include 0 LMLBlueprint.Chapters.Bandit}
+{include 0 LMLBlueprint.Chapters.Concentration}
+{include 0 LMLBlueprint.Chapters.BanditAlgs}
+
+{blueprint_graph}
+{blueprint_summary}
+{blueprint_bibliography}
diff --git a/verso_blueprint/LMLBlueprint/Chapters/Algorithm.lean b/verso_blueprint/LMLBlueprint/Chapters/Algorithm.lean
new file mode 100644
index 00000000..5f185aa6
--- /dev/null
+++ b/verso_blueprint/LMLBlueprint/Chapters/Algorithm.lean
@@ -0,0 +1,492 @@
+import Verso
+import VersoManual
+import VersoBlueprint
+import LeanMachineLearning.SequentialLearning.Deterministic
+import LeanMachineLearning.SequentialLearning.FiniteActions
+import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
+import LeanMachineLearning.SequentialLearning.StationaryEnv
+import LMLBlueprint.References
+import LMLBlueprint.TeXPrelude
+
+open Verso.Genre
+open Verso.Genre.Manual
+open Informal
+
+#doc (Manual) "Iterative stochastic algorithms" =>
+
+:::group "algorithm_environment"
+Stochastic algorithms and environments
+:::
+
+Warning: all times start at zero.
+
+TODO: notations
+
+All measurable spaces are assumed to be standard Borel.
+
+:::definition "algorithm" (parent := "algorithm_environment") (lean := "Learning.Algorithm")
+A sequential, stochastic algorithm with actions in a measurable space $`\mathcal{A}` and observations in a measurable space $`\mathcal{R}` is described by the following data:
+- for all $`t \in \mathbb{N}`, a policy $`\pi_t : (\mathcal{A} \times \mathcal{R})^{t+1} \rightsquigarrow \mathcal{A}`, a Markov kernel which gives the distribution of the action of the algorithm at time $`t+1` given the history of previous actions and observations,
+- $`P_0 \in \mathcal{P}(\mathcal{A})`, a probability measure that gives the distribution of the first action.
+:::
+
+After the algorithm takes an action, the environment generates an observation according to a Markov kernel $`\nu_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times \mathcal{A} \rightsquigarrow \mathcal{R}`.
+
+:::definition "environment" (parent := "algorithm_environment") (lean := "Learning.Environment")
+An environment with which an algorithm interacts is described by the following data:
+- for all $`t \in \mathbb{N}`, a feedback $`\nu_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times \mathcal{A} \rightsquigarrow \mathcal{R}`, a Markov kernel which gives the distribution of the observation at time $`t+1` given the history of previous pulls and observations, and the action of the algorithm at time $`t+1`,
+- $`\nu'_0 \in \mathcal{A} \rightsquigarrow \mathcal{R}`, a Markov kernel that gives the distribution of the first observation given the first action.
+:::
+
+
+:::definition "detAlgorithm" (parent := "algorithm_environment") (lean := "Learning.detAlgorithm")
+An algorithm ({uses "algorithm"}[]) is deterministic if its initial probability measure $`P_0` is a Dirac measure and if all its policies $`\pi_t` are deterministic kernels.
+:::
+
+
+:::definition "stationaryEnv" (parent := "algorithm_environment") (lean := "Learning.stationaryEnv")
+An environment ({uses "environment"}[]) is stationary if there exists a Markov kernel $`\nu : \mathcal{A} \rightsquigarrow \mathcal{R}` such that $`\nu'_0 = \nu` and for all $`t \in \mathbb{N}`, for all $`h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}`, for all $`a \in \mathcal{A}`, $`\nu_t(h_t, a) = \nu(a)`.
+:::
+
+TODO: possibly change the _stationary_ name.
+
+
+Let's detail four examples of interactions between an algorithm and an environment.
+- *First order optimization*. The objective of the algorithm is to find the minimum of a function $`f : \mathbb{R}^d \to \mathbb{R}`.
+  The action space is $`\mathcal{A} = \mathbb{R}^d` (a point on which the function will be queried) and the observation space is $`\mathcal{R} = \mathbb{R} \times \mathbb{R}^d`.
+  The environment is described by a function $`g : \mathbb{R}^d \to \mathbb{R} \times \mathbb{R}^d` such that for all $`x \in \mathbb{R}^d`, $`g(x) = (f(x), \nabla f(x))`. That is, the kernel $`\nu_t` is deterministic and depends only on the action: it is given by $`\nu_t(h_t, x) = \delta_{g(x)}` (the Dirac measure at $`g(x)`).
+  An example of algorithm is gradient descent with fixed step size $`\eta > 0`: this is a deterministic algorithm defined by $`P_0 = \delta_{x_0}` for some initial point $`x_0 \in \mathbb{R}^d` and for all $`t \in \mathbb{N}`, $`\pi_t(h_t) = \delta_{x_{t+1}}` where $`x_{t+1} = x_t - \eta \nabla g_2(x_t)`.
+- *Stochastic bandits*. The action space is $`\mathcal{A} = [K]` for some $`K \in \mathbb{N}` (the set of arms) and the observation space is $`\mathcal{R} = \mathbb{R}` (the reward obtained after pulling an arm).
+  The kernel $`\nu_t` is stationary and depends only on the action: there are probability distributions $`(P_a)_{a \in [K]}` such that for all $`t \in \mathbb{N}`, for all $`h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}`, for all $`a \in \mathcal{A}`, $`\nu_t(h_t, a) = P_a`.
+- *Adversarial bandits*. The action space is $`\mathcal{A} = [K]` for some $`K \in \mathbb{N}` (the set of arms) and the observation space is $`\mathcal{R} = \mathbb{R}` (the reward obtained after pulling an arm).
+  The reward kernels are usually taken to be deterministic and in an _oblivious_ adversarial bandit they depend only on the time step: there is a sequence of vectors $`(r_t)_{t \in \mathbb{N}}` in $`[0,1]^K` such that for all $`t \in \mathbb{N}`, for all $`h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}`, for all $`a \in \mathcal{A}`, $`\nu_t(h_t, a) = \delta_{r_{t,a}}` (the Dirac measure at $`r_{t,a}`).
+- *Reinforcement learning in Markov decision processes*.
+  TODO: main feature is that $`\mathcal{R} = \mathcal{S} \times \mathbb{R}` where $`\mathcal{S}` is the state space, and the kernel $`\nu_t` depends on the last state only.
+
+
+We will want to make global probabilistic statements about the whole sequence of actions and observations.
+For example, we may want to prove that an optimization algorithm converges to the minimum of a function almost surely.
+For such a statement to make sense, we need a probability space on which the whole sequence of actions and observations is defined as a random variable.
+
+We denote by $`P(X \mid Y)` the conditional distribution of a random variable $`X` given another random variable $`Y` under a probability measure $`P`.
+When we write that $`P(X \mid Y) = \kappa`, or that $`X` has conditional distribution $`\kappa` given $`Y`, the equality should be understood as holding $`Y_* P`-almost surely.
+
+*Lean remark*: `HasCondDistrib`
+
+In the Lean implementation, we define a predicate to state those almost sure equalities of conditional distributions: `HasCondDistrib X Y k P` states that under the probability measure $`P`, the random variable $`X` has conditional distribution $`k` given the random variable $`Y` (almost surely with respect to the law of $`X`).
+For convenience, the predicate also records that both random variables are almost everywhere measurable.
+
+
+:::definition "history" (parent := "algorithm_environment") (lean := "Learning.IsAlgEnvSeq.hist, Learning.IsAlgEnvSeq.step")
+For two sequences of random variables $`A : \mathbb{N} \to \Omega \to \mathcal{A}` and $`R : \mathbb{N} \to \Omega \to \mathcal{R}` (actions and observations), we call step of the interaction at time $`t` the random variable $`X_t : \Omega \to \mathcal{A} \times \mathcal{R}` defined by $`X_t(\omega) = (A_t(\omega), R_t(\omega))`.
+We call history up to time $`t` the random variable $`H_t : \Omega \to (\mathcal{A} \times \mathcal{R})^{t+1}` defined by $`H_t(\omega) = (X_0(\omega), \ldots, X_t(\omega))`.
+:::
+
+
+:::definition "IsAlgEnvSeq" (parent := "algorithm_environment") (lean := "Learning.IsAlgEnvSeq")
+Let $`\mathfrak{A}` be an algorithm ({uses "algorithm"}[]) and $`\mathfrak{E}` be an environment ({uses "environment"}[]).
+A probability space $`(\Omega, P)` and two sequences of random variables $`A : \mathbb{N} \to \Omega \to \mathcal{A}` and $`R : \mathbb{N} \to \Omega \to \mathcal{R}` form an algorithm-environment interaction for $`\mathfrak{A}` and $`\mathfrak{E}` if the following conditions hold:
+1. The law of $`A_0` is $`P_0`.
+2. $`P \left( R_0 \mid A_0 \right) = \nu'_0`.
+3. For all $`t \in \mathbb{N}`, $`P\left(A_{t+1} \mid A_0, R_0, \ldots, A_t, R_t \right) = \pi_t`.
+4. For all $`t \in \mathbb{N}`, $`P\left(R_{t+1} \mid A_0, R_0, \ldots, A_t, R_t, A_{t+1}\right) = \nu_t`.
+
+Uses: {uses "history"}[]
+:::
+
+
+:::lemma_ "law_step" (parent := "algorithm_environment") (lean := "Learning.IsAlgEnvSeq.hasLaw_step_zero, Learning.IsAlgEnvSeq.hasCondDistrib_step")
+In an algorithm-environment interaction $`(A, R, P)` as in {uses "IsAlgEnvSeq"}[],
+- the law of the initial step $`X_0` is $`P_0 \otimes \nu'_0`,
+- for all $`t \in \mathbb{N}`, $`P \left( X_{t+1} \mid H_t \right) = \pi_t \otimes \nu_t`.
+:::
+
+:::proof "law_step"
+Immediate from the properties of an algorithm-environment interaction.
+:::
+
+
+:::definition "IsAlgEnvSeq.filtration" (parent := "algorithm_environment") (lean := "Learning.IsAlgEnvSeq.filtration, Learning.IsAlgEnvSeq.filtrationAction")
+For an algorithm-environment interaction $`(A, R, P)` as in {uses "IsAlgEnvSeq"}[], we denote by $`\mathcal{F}_t` the sigma-algebra generated by the history up to time $`t`: $`\mathcal{F}_t = \sigma(H_t)`.
+We denote by $`\mathcal{F}^A_t` the sigma-algebra generated by the history up to time $`t-1` and the action at time $`t`: $`\mathcal{F}^A_t = \sigma(H_{t-1}, A_t)`.
+:::
+
+
+:::lemma_ "IsAlgEnvSeq.adapted" (parent := "algorithm_environment") (lean := "Learning.IsAlgEnvSeq.adapted_step, Learning.IsAlgEnvSeq.adapted_hist, Learning.IsAlgEnvSeq.adapted_action, Learning.IsAlgEnvSeq.adapted_reward")
+The history, step, action and observation processes ({uses "history"}[]) are adapted to the filtration $`(\mathcal{F}_t)_{t \in \mathbb{N}}` ({uses "IsAlgEnvSeq.filtration"}[]).
+:::
+
+:::proof "IsAlgEnvSeq.adapted"
+By definition of the filtration.
+:::
+
+
+:::theorem "isAlgEnvSeq_unique" (parent := "algorithm_environment") (lean := "Learning.isAlgEnvSeq_unique")
+If $`(A, R, P)` and $`(A', R', P')` are two {uses "IsAlgEnvSeq"}[algorithm-environment interactions] for the same {uses "algorithm"}[algorithm] $`\mathfrak{A}` and {uses "environment"}[environment] $`\mathfrak{E}`, then the joint distributions of the sequences of actions and observations are equal: the law of $`(A_i, R_i)_{i \in \mathbb{N}}` under $`P` is equal to the law of $`(A'_i, R'_i)_{i \in \mathbb{N}}` under $`P'`.
+
+This is Proposition 4.8 in {Informal.citep lattimore2020bandit}[].
+:::
+
+:::proof "isAlgEnvSeq_unique"
+Uses: {uses "ionescu-tulcea"}[], {uses "law_step"}[], {uses "trajMeasure"}[]
+:::
+
+
+
+
+# Stationary environment
+
+:::group "stationary_environment"
+Stationary environments
+:::
+
+Recall that in a stationary environment, there exists a Markov kernel $`\nu : \mathcal{A} \rightsquigarrow \mathcal{R}` such that $`\nu'_0 = \nu` and for all $`t \in \mathbb{N}`, for all $`h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}`, for all $`a \in \mathcal{A}`, $`\nu_t(h_t, a) = \nu(a)`.
+
+Let $`(A, R, P)` be an algorithm-environment interaction in a stationary environment with kernel $`\nu`.
+
+:::lemma_ "condDistrib_reward_stationaryEnv" (parent := "stationary_environment") (lean := "Learning.IsAlgEnvSeq.condDistrib_reward_stationaryEnv")
+In a {uses "stationaryEnv"}[stationary environment], an {uses "IsAlgEnvSeq"}[algorithm-environment interaction] satisfies for any $`t \in \mathbb{N}`, $`P\left(R_t \mid A_t\right) = \nu`.
+:::
+
+:::proof "condDistrib_reward_stationaryEnv"
+Uses: {uses "law_step"}[]
+:::
+
+
+::: lemma_ "condIndepFun_reward_hist_action" (parent := "stationary_environment") (lean := "Learning.IsAlgEnvSeq.condIndepFun_reward_hist_action")
+For an {uses "IsAlgEnvSeq"}[algorithm-environment interaction] in a {uses "stationaryEnv"}[stationary environment], for any $`t \in \mathbb{N}`, the reward $`R_{t+1}` is conditionally independent of the history $`H_t` given the action $`A_{t+1}` (more succinctly, $`R_{t+1} \ind H_t \mid A_{t+1}`).
+:::
+
+:::proof "condIndepFun_reward_hist_action"
+:::
+
+
+
+# Probability space: Ionescu-Tulcea theorem
+
+We saw that the distribution of the sequence of actions and observations in a suitable probability space is uniquely determined by the algorithm and the environment.
+We now show that such a probability space actually exists: for any algorithm and environment, we build an algorithm-environment interaction.
+
+:::group "ionescu_tulcea"
+Ionescu-Tulcea theorem
+:::
+
+## Ionescu-Tulcea theorem
+
+If we group together the policy of the algorithm and the kernel of the environment at each time step, we get a sequence of Markov kernels $`(\kappa_t)_{t \in \mathbb{N}}`, with $`\kappa_t : (\mathcal{A} \times \mathcal{R})^{t+1}  \rightsquigarrow (\mathcal{A} \times \mathcal{R})`.
+
+
+We now abstract that situation and consider a sequence of measurable spaces $`(\Omega_t)_{t \in \mathbb{N}}`, a probability measure $`\mu` on $`\Omega_0` and a sequence of Markov kernels $`\kappa_t : \prod_{s=0}^t \Omega_s \rightsquigarrow \Omega_{t+1}`.
+The Ionescu-Tulcea theorem builds a probability space from the sequence of kernels and the initial measure.
+
+
+:::theorem "ionescu-tulcea" (parent := "ionescu_tulcea") (lean := "ProbabilityTheory.Kernel.traj")
+Let $`(\Omega_t)_{t \in \mathbb{N}}` be a family of measurable spaces. Let $`(\kappa_t)_{t \in \mathbb{N}}` be a family of Markov kernels such that for any $`t`, $`\kappa_t` is a kernel from $`\prod_{i=0}^t \Omega_{i}` to $`\Omega_{t+1}`.
+Then there exists a unique Markov kernel $`\xi : \Omega_0 \rightsquigarrow \prod_{i = 1}^{\infty} \Omega_{i}` such that for any $n \ge 1$,
+$`\pi_{[1,n]*} \xi = \kappa_0 \otimes \ldots \otimes \kappa_{n-1}`.
+Here $`\pi_{[1,n]} : \prod_{i=1}^{\infty} \Omega_i \to \prod_{i=1}^n \Omega_i` is the projection on the first $`n` coordinates.
+:::
+
+The Ionescu-Tulcea theorem in Mathlib {Informal.citep marion2025formalization}[] actually generates kernels $`\xi_t : \prod_{s=0}^t \Omega_s \rightsquigarrow \prod_{s=0}^{\infty} \Omega_s` for any $`t`, with the property that the kernels are the identity on the first $`t+1` coordinates.
+
+:::definition "trajMeasure" (parent := "ionescu_tulcea") (lean := "ProbabilityTheory.Kernel.trajMeasure")
+For $`\mu \in \mathcal{P}(\Omega_0)`, we call trajectory measure the probability measure $`\xi_0 \circ \mu` on $`\Omega_{\mathcal{T}} := \prod_{i=0}^{\infty} \Omega_i`.
+We denote it by $`P_{\mathcal{T}}`.
+The $`\mathcal{T}` subscript stands for _trajectory_.
+:::
+
+
+:::definition "IT.history" (parent := "ionescu_tulcea") (lean := "Learning.IT.hist, Learning.IT.step")
+For $`t \in \mathbb{N}`, we denote by $`X_t \in \Omega_t` the random variable describing the time step $`t`, and by $`H_t \in \prod_{s=0}^t \Omega_s` the history up to time $`t`.
+Formally, these are measurable functions on $`\Omega_{\mathcal{T}}`, defined by $`X_t(\omega) = \omega_t` and $`H_t(\omega) = (\omega_1, \ldots, \omega_t)`.
+:::
+
+Note: $`(X_t)_{t \in \mathbb{N}}` is the canonical process on $`\Omega_{\mathcal{T}}`. $`H_t` is equal to $`\pi_{[0,t]}`.
+
+
+:::definition "IT.filtration" (parent := "ionescu_tulcea") (lean := "Learning.IT.filtration")
+For $`t \in \mathbb{N}`, we denote by $`\mathcal{F}_t` the sigma-algebra generated by the {uses "IT.history"}[history] up to time $`t`: $`\mathcal{F}_t = \sigma(H_t)`.
+The family $`(\mathcal{F}_t)_{t \in \mathbb{N}}` is a filtration on $`\Omega_{\mathcal{T}}`.
+:::
+
+$`(\mathcal{F}_t)_{t \in \mathbb{N}}` is the canonical filtration on $`\Omega_{\mathcal{T}}`, and is the natural filtration for the canonical process $`(X_t)_{t \in \mathbb{N}}`.
+
+:::lemma_ "IT.adapted_history" (parent := "ionescu_tulcea") (lean := "Learning.IT.adapted_step, Learning.IT.adapted_hist")
+The random variables $`X_t` and $`H_t` ({uses "IT.history"}[]) are $`\mathcal{F}_t`-measurable.
+Said differently, the processes $`(X_t)_{t \in \mathbb{N}}` and $`(H_t)_{t \in \mathbb{N}}` are adapted to the {uses "IT.filtration"}[filtration] $`(\mathcal{F}_t)_{t \in \mathbb{N}}`.
+:::
+
+
+:::lemma_ "IT.condDistrib_X_add_one" (parent := "ionescu_tulcea") (lean := "ProbabilityTheory.Kernel.condDistrib_trajMeasure")
+For any $`t \in \mathbb{N}`, $`P_{\mathcal{T}}\left(X_{t+1} \mid H_t\right) = \kappa_t`.
+
+Uses: {uses "IT.history"}[], {uses "ionescu-tulcea"}[], {uses "trajMeasure"}[]
+:::
+
+:::proof "IT.condDistrib_X_add_one"
+This is proved through the defining property of the conditional distribution: it is the almost surely unique Markov kernel $`\eta` such that $`((H_t)_* P_{\mathcal{T}}) \otimes \eta = (H_t, X_{t+1})_*P_{\mathcal{T}}`.
+
+TODO: complete proof.
+:::
+
+
+:::lemma_ "IT.law_X_zero" (parent := "ionescu_tulcea") (lean := "Learning.IsAlgEnvSeq.hasLaw_step_zero")
+The law of $`X_0` under $`P_{\mathcal{T}}` is $`\mu`.
+
+Uses: {uses "IT.history"}[], {uses "trajMeasure"}[].
+:::
+
+
+
+## Case of an algorithm-environment interaction
+
+We now go back to the setting of an algorithm interacting with an environment and suppose that $`\Omega_t = \mathcal{A} \times \mathcal{R}` for some measurable spaces $`\mathcal{A}` and $`\mathcal{R}`, and that for all $`t \in \mathbb{N}`, $`\kappa_t = \pi_t \otimes \nu_t` for policy kernels $`\pi_t : (\mathcal{A} \times \mathcal{R})^{t+1} \rightsquigarrow \mathcal{A}` and feedback kernels $`\nu_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times \mathcal{A} \rightsquigarrow \mathcal{R}`.
+Likewise, $`\mu = P_0 \otimes \nu'_0` for a probability measure $`P_0` on $`\mathcal{A}` and a Markov kernel $`\nu'_0 : \mathcal{A} \rightsquigarrow \mathcal{R}`.
+The step random variable $`X_t` takes values in $`\mathcal{A} \times \mathcal{R}`.
+
+:::definition "IT.actionReward" (parent := "ionescu_tulcea") (lean := "Learning.IT.action, Learning.IT.reward")
+We write $`A_t` and $`R_t` for the projections of $`X_t` ({uses "IT.history"}[]) on $`\mathcal{A}` and $`\mathcal{R}` respectively.
+$`A_t` is the action taken at time $`t` and $`R_t` is the reward received at time $`t`.
+Formally, $`A_t(\omega) = \omega_{t,1}` and $`R_t(\omega) = \omega_{t,2}` for $`\omega = \prod_{t=0}^{+\infty}(\omega_{t,1}, \omega_{t,2}) \in \Omega_{\mathcal{T}} = \prod_{t=0}^{+\infty} \mathcal{A} \times \mathcal{R}`.
+:::
+
+
+:::lemma_ "IT.adapted_action_reward" (parent := "ionescu_tulcea") (lean := "Learning.IT.adapted_action, Learning.IT.adapted_reward")
+The random variables $`A_t` and $`R_t` ({uses "IT.actionReward"}[]) are $`\mathcal{F}_t`-measurable.
+Said differently, the processes $`(A_t)_{t \in \mathbb{N}}` and $`(R_t)_{t \in \mathbb{N}}` are adapted to the {uses "IT.filtration"}[filtration] $`(\mathcal{F}_t)_{t \in \mathbb{N}}`.
+:::
+
+:::proof "IT.adapted_action_reward"
+Uses: {uses "IT.adapted_history"}[].
+:::
+
+
+We need to check that the random variables $`A_t` and $`R_t` have the expected conditional distributions.
+
+:::lemma_ "IT.condDistrib_A_add_one" (parent := "ionescu_tulcea") (lean := "Learning.IT.condDistrib_action")
+For any $`t \in \mathbb{N}`, $`P_{\mathcal{T}}\left(A_{t+1} \mid H_t\right) = \pi_t`.
+
+Uses: {uses "environment"}[], {uses "algorithm"}[], {uses "ionescu-tulcea"}[], {uses "IT.actionReward"}[], {uses "trajMeasure"}[], {uses "IT.history"}[].
+:::
+
+:::proof "IT.condDistrib_A_add_one"
+By {uses "IT.condDistrib_X_add_one"}[], $`P_{\mathcal{T}}\left(X_{t+1} \mid H_t\right) = \kappa_t = \pi_t \otimes \nu_t`.
+Since $`A_{t+1}` is the projection of $`X_{t+1}` on $`\mathcal{A}`, $`P_{\mathcal{T}}\left(A_{t+1} \mid H_t\right)` is $`((H_t)_* P_{\mathcal{T}})`-almost surely equal to the projection of $`\kappa_t` on $`\mathcal{A}`, which is $`\pi_t`.
+:::
+
+
+:::lemma_ "IT.condDistrib_R_add_one" (parent := "ionescu_tulcea") (lean := "Learning.IT.condDistrib_reward")
+For any $`t \in \mathbb{N}`, $`P_{\mathcal{T}}\left(R_{t+1} \mid H_t, A_{t+1}\right) = \nu_t`.
+
+Uses: {uses "environment"}[], {uses "algorithm"}[], {uses "ionescu-tulcea"}[], {uses "IT.actionReward"}[], {uses "trajMeasure"}[], {uses "IT.history"}[].
+:::
+
+:::proof "IT.condDistrib_R_add_one"
+It suffices to show that $`((H_t, A_{t+1})_* P_{\mathcal{T}}) \otimes \nu_t = (H_t, A_{t+1}, R_{t+1})_* P_{\mathcal{T}} = (H_t, X_{t+1})_* P_{\mathcal{T}}`.
+By {uses "IT.condDistrib_X_add_one"}[], $`P_{\mathcal{T}}\left(X_{t+1} \mid H_t\right) = \pi_t \otimes \nu_t`.
+Thus $`((H_t)_* P_{\mathcal{T}}) \otimes (\pi_t \otimes \nu_t) = (H_t, X_{t+1})_* P_{\mathcal{T}}`.
+
+We thus have to prove that $`((H_t)_* P_{\mathcal{T}}) \otimes (\pi_t \otimes \nu_t) = ((H_t, A_{t+1})_* P_{\mathcal{T}}) \otimes \nu_t`.
+
+By {uses "IT.condDistrib_A_add_one"}[], $`(H_t, A_{t+1})_* P_{\mathcal{T}} = (H_t)_* P_{\mathcal{T}} \otimes \pi_t`, and replacing this in the right-hand side gives the left-hand side (using associativity of the composition-product).
+:::
+
+
+:::lemma_ "IT.law_A_zero" (parent := "ionescu_tulcea") (lean := "Learning.IT.hasLaw_action_zero")
+The law of $`A_0` under $`P_{\mathcal{T}}` is $`P_0`.
+
+Uses: {uses "environment"}[], {uses "algorithm"}[], {uses "IT.actionReward"}[], {uses "trajMeasure"}[].
+:::
+
+:::proof "IT.law_A_zero"
+$`X_0` has law $`\mu = P_0 \otimes \nu'_0`. $`A_0` is the projection of $`X_0` on the first space $`\mathcal{A}` and $`\nu_0'` is Markov, so $`A_0` has law $`P_0`.
+
+Uses: {uses "ionescu-tulcea"}[], {uses "IT.history"}[], {uses "IT.law_X_zero"}[].
+:::
+
+
+:::lemma_ "IT.condDistrib_R_zero" (parent := "ionescu_tulcea") (lean := "Learning.IT.condDistrib_reward_zero")
+$`P_{\mathcal{T}}\left(R_0 \mid A_0\right) = \nu'_0`.
+
+Uses: {uses "environment"}[], {uses "algorithm"}[], {uses "IT.actionReward"}[], {uses "trajMeasure"}[], {uses "ionescu-tulcea"}[].
+:::
+
+:::proof "IT.condDistrib_R_zero"
+To prove almost sure equality, it is enough to prove that $`(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left(R_0 \mid A_0\right) = (A_{0*} P_{\mathcal{T}}) \otimes \nu'_0`.
+By definition of the conditional distribution, we have $`(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left(R_0 \mid A_0\right) = (A_0, R_0)_* P_{\mathcal{T}} = X_{0*} P_{\mathcal{T}}`.
+By {uses "IT.law_X_zero"}[], $`X_{0*} P_{\mathcal{T}} = \mu = P_0 \otimes \nu'_0`.
+By {uses "IT.law_A_zero"}[], $`A_{0*} P_{\mathcal{T}} = P_0`.
+Thus the two sides are equal.
+:::
+
+
+:::theorem "isAlgEnvSeq_trajMeasure" (parent := "ionescu_tulcea") (lean := "Learning.IT.isAlgEnvSeq_trajMeasure")
+In the {uses "trajMeasure"}[probability space $`(\Omega_{\mathcal{T}}, P_{\mathcal{T}})`] constructed from an algorithm $`\mathfrak{A}` and an environment $`\mathfrak{E}` as above, the sequences of random variables $`A : \mathbb{N} \to \Omega_{\mathcal{T}} \to \mathcal{A}` and $`R : \mathbb{N} \to \Omega_{\mathcal{T}} \to \mathcal{R}` form an {uses "IsAlgEnvSeq"}[algorithm-environment interaction] for $`\mathfrak{A}` and $`\mathfrak{E}`.
+
+Uses: {uses "ionescu-tulcea"}[], {uses "IT.actionReward"}[].
+:::
+
+:::proof "isAlgEnvSeq_trajMeasure"
+The four conditions of {uses "IsAlgEnvSeq"}[] are exactly the statements of {uses "IT.law_A_zero"}[], {uses "IT.condDistrib_R_zero"}[], {uses "IT.condDistrib_A_add_one"}[] and {uses "IT.condDistrib_R_add_one"}[].
+:::
+
+
+
+# Finitely many actions
+
+:::group "finite_actions"
+Finite action space
+:::
+
+When the number of actions is finite, it makes sense to count how many times each action was chosen up to a certain time.
+We can also define the time step at which an action was chosen a certain number of times, and the value of the reward obtained when pulling an action for the $m$-th time.
+
+:::definition "pullCount" (parent := "finite_actions") (lean := "Learning.pullCount")
+For an action $`a \in \mathcal{A}` and a time $`t \in \mathbb{N}`, we denote by $`N_{t,a}` the number of times that action $`a` has been chosen before time $`t`, that is $`N_{t,a} = \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\}`.
+:::
+
+Note that the sum goes up to $`t-1`, so that $`N_{t,a}` counts the number of times action $`a` was chosen _before_ time $`t`.
+
+
+*Remark: Building vs analyzing algorithms*
+
+When we describe an algorithm, we give the data of the policies $`\pi_t`, which are functions of the partial history up to time $`t`, in $`(\mathcal{A} \times \mathcal{R})^{t+1}`.
+That means that any tool used to define a policy must be a function defined on $`(\mathcal{A} \times \mathcal{R})^{t+1}`.
+For example a definition of the empirical mean of an action must be a function $`t : \mathbb{N} \to (\mathcal{A} \times \mathcal{R})^{t+1} \to \mathbb{R}`.
+
+When we analyze an algorithm, we work on the other hand on a probability space $`(\Omega, P)`, in which $`\Omega` could be for example $`(\mathcal{A} \times \mathcal{R})^{\mathbb{N}}`, the full history, which describes the whole sequence of actions and rewards.
+As a stochastic process, the empirical mean of an action is a function $`\mathbb{N} \to (\mathcal{A} \times \mathcal{R})^{\mathbb{N}} \to \mathbb{R}`.
+
+Thus there are two similar but still distinct types of objects: those defined on the partial history, which are used to build algorithms, and those defined on a generic probability space (the full history in the Ionescu-Tulcea construction), which are used to analyze algorithms.
+
+
+:::lemma_ "pullCount_basic" (parent := "finite_actions") (lean := "Learning.pullCount_zero, Learning.pullCount_mono, Learning.pullCount_add_one, Learning.pullCount_le, Learning.pullCount_congr")
+We note the following basic properties of {uses "pullCount"}[$`N_{t,a}`]:
+- $`N_{0,a} = 0`.
+- $`N_{t,a}` is non-decreasing in $`t`.
+- $`N_{t + 1, A_t} = N_{t, A_t} + 1` and for $`a \ne A_t`, $`N_{t + 1, a} = N_{t, a}`.
+- $`N_{t, a} \le t`.
+- If for all $`s \le t`, $`A_s(\omega) = A_s(\omega')`, then $`N_{t+1, a}(\omega) = N_{t+1, a}(\omega')`.
+:::
+
+
+:::lemma_ "predictable_pullCount" (parent := "finite_actions") (lean := "Learning.isPredictable_pullCount")
+Let $`a \in \mathcal{A}`. The process {uses "pullCount"}[$`(N_{t,a})_{t \in \mathbb{N}}`] is predictable with respect to the {uses "IsAlgEnvSeq.filtration"}[filtration $`\mathcal{F}`] of the algorithm-environment interaction.
+:::
+
+:::proof "predictable_pullCount"
+Uses: {uses "history"}[], {uses "pullCount_basic"}[]
+:::
+
+
+:::definition "stepsUntil" (parent := "finite_actions") (lean := "Learning.stepsUntil")
+For an action $`a \in \mathcal{A}` and a time $`n \in \mathbb{N}`, we denote by $`T_{n,a} \in \mathbb{N} \cup \{+\infty\}` the time at which action $`a` was chosen for the $`n`-th time, that is $`T_{n,a} = \min\{s \in \mathbb{N} \mid N_{s+1,a} = n\}`.
+Note that $`T_{n, a}` can be infinite if the action is not chosen $`n` times.
+
+Uses: {uses "pullCount"}[]
+:::
+
+By definition, $`T_{n, a}` is the hitting time of the set $`\{n\}` by the process $`t \mapsto N_{t+1,a}`, which is adapted since $`N_{t,a}` is predictable.
+Equivalently, $`T_{n, a}` is the hitting time of the set $`[n, +\infty]` by that process.
+
+
+:::lemma_ "stepsUntil_basic" (parent := "finite_actions") (lean := "Learning.stepsUntil_zero_of_ne, Learning.stepsUntil_zero_of_eq, Learning.stepsUntil_pullCount_le, Learning.stepsUntil_pullCount_eq, Learning.action_stepsUntil, Learning.pullCount_stepsUntil_add_one, Learning.pullCount_stepsUntil")
+We note the following basic properties of {uses "stepsUntil"}[$`T_{n,a}`]:
+- $`T_{0,a} = 0` for $`a \ne A_0`. $`T_{0,A_0} = \infty`.
+- $`T_{N_{t+1, a}, a} \le t`.
+- $`T_{N_{t + 1, A_t}, A_t} = t`.
+- If $`T_{n, a} \ne \infty` and $`n > 0`, then $`A_{T_{n, a}} = a`.
+- If $`T_{n, a} \ne \infty`, then $`N_{T_{n, a} + 1, a} = n`.
+- If $`T_{n, a} \ne \infty` and $`n > 0`, then $`N_{T_{n, a}, a} = n - 1`.
+- If for all $`s \le t`, $`A_s(\omega) = A_s(\omega')`, then $`T_{n, a}(\omega) = t \iff T_{n, a}(\omega') = t`.
+:::
+
+:::proof "stepsUntil_basic"
+Uses: {uses "pullCount_basic"}[]
+:::
+
+
+:::lemma_ "isStoppingTime_stepsUntil" (parent := "finite_actions") (lean := "Learning.isStoppingTime_stepsUntil")
+Let $`a \in \mathcal{A}`. For any $`n > 0`, the random variable {uses "stepsUntil"}[$`T_{n,a}`] is a stopping time with respect to the {uses "IsAlgEnvSeq.filtration"}[filtration $`\mathcal{F}`].
+:::
+
+:::proof "isStoppingTime_stepsUntil"
+A hitting time of a set by an adapted process is a stopping time.
+
+Uses: {uses "pullCount_basic"}[]
+:::
+
+
+Let $`\Omega' = \mathcal{R}^{\mathbb{N} \times \mathcal{A}}` and let $`\Omega = \Omega_{\mathcal{T}} \times \Omega'` (which will be an extension of the trajectory probability space once we choose a measure on $`\Omega'`).
+Let $`Z_{n, a} : \Omega \to \mathcal{R}` be the projection on the coordinate indexed by $`(n,a)` in $`\Omega'`.
+Extending the probability space in that way allows us to define without ambiguity the reward received when choosing an action for the $`n`-th time, even if that action is never actually chosen $`n` times.
+
+
+:::definition "rewardByCount" (parent := "finite_actions") (lean := "Learning.rewardByCount")
+We define $`Y_{n, a} = R_{T_{n,a}} \mathbb{I}\{T_{n, a} < \infty\} + Z_{n,a} \mathbb{I}\{T_{n, a} = \infty\}`, the reward received when choosing action $`a` for the $`n`-th time if {uses "stepsUntil"}[that time] is finite, and equal to $`Z_{n,a}` otherwise.
+In that expression, we see $`R_{T_{n,a}}` and $`T_{n, a}` as random variables on $`\Omega` instead of $`\Omega_{\mathcal{T}}`.
+:::
+
+
+:::lemma_ "rewardByCount_pullCount" (parent := "finite_actions") (lean := "Learning.rewardByCount_pullCount_add_one_eq_reward")
+$`Y_{N_{t, A_t} + 1, A_t} = R_t`.
+
+Uses: {uses "rewardByCount"}[], {uses "pullCount"}[]
+:::
+
+:::proof "rewardByCount_pullCount"
+This is perhaps hard to parse at first sight, but it follows directly from the definitions.
+At time $t$, the action chosen is $`A_t` and we see a reward $`R_t`.
+That action had already been chosen $`N_{t, A_t}` times before time $t$, so the reward $`R_t` is the reward received when choosing action $`A_t` for the $`(N_{t, A_t} + 1)`-th time, which is $`Y_{N_{t, A_t} + 1, A_t}` by definition.
+
+Uses: {uses "stepsUntil_basic"}[].
+:::
+
+
+
+# Scalar rewards
+
+TODO: change the name _reward_ to _observation_ throughout the chapter?
+
+We now focus on the case where the reward space is $`\mathcal{R} = \mathbb{R}`.
+
+:::group "scalar_rewards"
+Scalar rewards
+:::
+
+:::definition "sumRewards" (parent := "scalar_rewards") (lean := "Learning.sumRewards")
+Let $`S_{t, a} = \sum_{s=0}^{t-1} R_s \mathbb{I}\{A_s = a\}` be the sum of the rewards obtained by chosing action $`a` before time $`t`.
+:::
+
+
+:::definition "empMean" (parent := "scalar_rewards") (lean := "Learning.empMean")
+Let $`\hat{\mu}_{t, a} = \frac{S_{t, a}}{N_{t, a}} = \frac{1}{N_{t,a}} \sum_{s=0}^{t-1} R_s \mathbb{I}\{A_s = a\}` if $`N_{t, a} > 0`, and $`\hat{\mu}_{t, a} = 0` otherwise.
+This is the empirical mean of the rewards obtained by choosing action $`a` before time $`t`.
+
+Uses: {uses "sumRewards"}[], {uses "pullCount"}[]
+:::
+
+Note: in bandit papers it is common to (implicitly) define the empirical mean as $`+\infty` when the action was never chosen, but in Lean it has to be a real number, and the Lean default value for division by zero is $`0`.
+
+
+:::lemma_ "isPredictable_sumRewards" (parent := "scalar_rewards") (lean := "Learning.IsAlgEnvSeq.isPredictable_sumRewards, Learning.IsAlgEnvSeq.isPredictable_empMean")
+The processes {uses "sumRewards"}[$`(S_{t,a})_{t \in \mathbb{N}}`] and {uses "empMean"}[$`(\hat{\mu}_{t,a})_{t \in \mathbb{N}}`] are predictable with respect to the {uses "IsAlgEnvSeq.filtration"}[filtration $`\mathcal{F}`] of the algorithm-environment interaction.
+:::
+
+:::proof "isPredictable_sumRewards"
+Uses: {uses "predictable_pullCount"}[], {uses "sumRewards"}[], {uses "empMean"}[]
+:::
+
+
+The following lemma is very useful to relate the two ways of indexing the rewards: by time step and by pull count.
+
+:::lemma_ "sum_rewardByCount" (parent := "scalar_rewards") (lean := "Learning.sum_rewardByCount_eq_sumRewards")
+The sum of the first {uses "pullCount"}[$`N_{t, a}`] rewards received when choosing action $`a` is equal to the sum of the rewards obtained by choosing action $`a` before time $`t`:
+$$`\sum_{n=1}^{N_{t, a}} Y_{n, a} = S_{t,a} \: .`
+
+Uses: {uses "rewardByCount"}[], {uses "sumRewards"}[].
+:::
+
+:::proof "sum_rewardByCount"
+Uses:  {uses "rewardByCount_pullCount"}[].
+:::
diff --git a/verso_blueprint/LMLBlueprint/Chapters/Bandit.lean b/verso_blueprint/LMLBlueprint/Chapters/Bandit.lean
new file mode 100644
index 00000000..c3a5c74b
--- /dev/null
+++ b/verso_blueprint/LMLBlueprint/Chapters/Bandit.lean
@@ -0,0 +1,543 @@
+import Verso
+import VersoManual
+import VersoBlueprint
+import LeanMachineLearning.SequentialLearning.Deterministic
+import LeanMachineLearning.SequentialLearning.FiniteActions
+import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
+import LeanMachineLearning.SequentialLearning.StationaryEnv
+import LeanMachineLearning.Online.Bandit.ArrayProbSpace
+import LeanMachineLearning.Online.Bandit.Regret
+import LeanMachineLearning.Online.Bandit.RewardByCountMeasure
+import LMLBlueprint.References
+import LMLBlueprint.TeXPrelude
+
+open Verso.Genre
+open Verso.Genre.Manual
+open Informal
+
+#doc (Manual) "Stochastic multi-armed bandits" =>
+
+A bandit algorithm is an algorithm in the sense of Definition TODO FIND OUT HOW TO REFERENCE OUTSIDE OF ENVIRONMENTS.
+We call the actions _arms_ and the observations _rewards_.
+
+The first arm pulled by the algorithm is sampled from $`P_0`, the arm pulled at time $`1` is sampled from $`\pi_0(H_0)`, in which $`H_0 \in \mathcal{A} \times \mathcal{R}` is the data of the first arm pulled and the first observation received, and so on.
+
+A stochastic bandit is simply a reward distribution for each arm: a Markov kernel $`\nu : \mathcal{A} \rightsquigarrow \mathbb{R}`, conditional distribution of the rewards given the arm pulled.
+It is a stationary environment in which the observation space is $`\mathcal{R} = \mathbb{R}`.
+
+An algorithm can interact with a bandit to produce a sequence of arms and rewards: after a time $`t`, the history $`H_t \in (\mathcal{A} \times \mathcal{R})^{t+1}` contains the arms pulled and rewards received up to that time,
+- the algorithm chooses an arm $`A_{t+1}` sampled according to its policy $`\pi_t(H_t)`,
+- the bandit generates a reward $`R_{t+1}` according to the distribution $`\nu(A_{t+1})`,
+- the history is updated to $`H_{t+1} = ((A_0, R_0), \ldots, (A_{t+1}, R_{t+1}))`.
+
+
+
+# The array model of rewards
+
+:::group "bandit_space"
+Probability space for stochastic multi-armed bandits
+:::
+
+We previously built a probability space on which we can define the sequence of arms and rewards generated by the interaction between the algorithm and the bandit, using the Ionescu-Tulcea theorem.
+From Theorem isAlgEnvSeq\_unique (TODO REF), we know that the law of the sequence of arms and rewards is independent of the probability space used to define them.
+Nonetheless, we now build an alternative model of the rewards, on which it will be easier to prove concentration inequalities.
+By the uniqueness of the law, these statements will then transfer to any algorithm-environment interaction.
+
+In the _array model_, we consider a probability space on which we have an infinite array of rewards from each arm, independent from each other.
+When pulling an arm, the algorithm sees the next previously unseen reward from that arm in the array.
+
+:::definition "arrayMeasure" (parent := "bandit_space") (lean := "Bandits.ArrayModel.arrayMeasure, Bandits.ArrayModel.probSpace")
+Let $`I = [0,1]` and let $`P_U` be the uniform distribution on $`I`. We define the probability space $`(\Omega_{\mathcal{A}}, P_{\mathcal{A}})`, where
+- $` \Omega_{\mathcal{A}} := I^{\mathbb{N}} \times \mathcal{R}^{\mathbb{N} \times \mathcal{A}}` ,
+- $`P_{\mathcal{A}} := \left( \bigotimes_{n \in \mathbb{N}} P_U \right) \otimes \left( \bigotimes_{n \in \mathbb{N}, a \in \mathcal{A}} \nu(a) \right)` .
+
+Uses: {uses "ionescu-tulcea"}[].
+:::
+
+
+:::definition "algFunction" (parent := "bandit_space") (lean := "Bandits.ArrayModel.algFunction, Bandits.ArrayModel.initAlgFunction")
+Let $`\mathfrak{A}` be an {uses "algorithm"}[algorithm] with action space $`\mathcal{A}` and reward space $`\mathcal{R}`, policy $`\pi` and initial distribution $`P_0`.
+For $`\mathcal{A}` and $`\mathcal{R}` standard Borel spaces, there exists jointly measurable functions $`f'_0 : I \to \mathcal{A}` and $`f_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times I \to \mathcal{A}` such that
+- the law of $`f'_0` is $`P_0`,
+- for all history $`h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}`, the law of $`f_t(h_t, \cdot)` is $`\pi_t(h_t)`.
+:::
+
+
+:::definition "AM.history" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hist, Bandits.ArrayModel.action, Bandits.ArrayModel.reward")
+The history, actions and rewards on the {uses "arrayMeasure"}[array model probability space] $`(\Omega_{\mathcal{A}}, P_{\mathcal{A}})` are defined as follows:
+- the action at time $`0` is $`A_0(\omega) = f'_0(\omega_{1,0})`, the reward at time $`0` is $`R_0(\omega) = \omega_{2,0,A_0(\omega)}`, and the history at time $`0` is $`H_0(\omega) = (A_0(\omega), R_0(\omega))`,
+- for $`t \ge 0`, the action at time $`t+1` is $`A_{t+1}(\omega) = f_t(H_t(\omega), \omega_{1,t+1})`, the reward at time $`t+1` is $`R_{t+1}(\omega) = \omega_{2,N_{t+1,A_{t+1}(\omega)},A_{t+1}(\omega)}`, and the history at time $`t+1` is $`H_{t+1}(\omega) = (H_t(\omega), (A_{t+1}(\omega), R_{t+1}(\omega)))`.
+
+Uses: {uses "algFunction"}[], {uses "pullCount"}[].
+:::
+
+
+The goal of this section is to show that $`(\Omega_{\mathcal{A}}, P_{\mathcal{A}})` with the actions and rewards defined above is an algorithm-environment sequence.
+
+
+
+## Measurability
+
+TODO: some of those results are proved for $`\mathcal{A}` countable. Add that assumption where needed.
+
+*Remark: Proving measurability with respect to a sub-sigma-algebra*
+
+In this section, we often need to prove that a random variable $`X` is measurable with respect to the sigma-algebra generated by a subset of the independent random variables defining the probability space $`\Omega_{\mathcal{A}}`.
+We want to prove that $`X : \Omega_{\mathcal{A}} \to \mathcal{X}` is measurable with respect to the sigma-algebra $`\sigma((\omega_p)_{p \in S})`, where $`S` is a subset of the indices of the independent random variables defining $`\Omega_{\mathcal{A}}`.
+In most cases, this is due to $`X` being defined (possibly recursively in a complicated way) only using those random variables.
+However, it might be difficult to exhibit an explicit function $`f` such that $`X = f((\omega_p)_{p \in S})`.
+
+Here is a general strategy to prove such measurability results in Lean:
+1. Prove that $`X` is measurable with respect to the full sigma-algebra on $`\Omega_{\mathcal{A}}`.
+2. Prove a congruence lemma: for any $`\omega, \omega' \in \Omega_{\mathcal{A}}`, if $`\omega_p = \omega'_p` for all $`p \in S`, then $`X(\omega) = X(\omega')`.
+3. Define $`g : (\prod_{p \in S} \Omega_p) \to \Omega` by $`g((\omega_p)_{p \in S}) = \omega'`, where $`\omega'_p = \omega_p` for $`p \in S` and $`\omega'_p` is some fixed value for $`p \notin S`.
+4. Write $`X = X \circ g \circ \mathrm{proj}_S`, where $`\mathrm{proj}_S : \Omega_{\mathcal{A}} \to \prod_{p \in S} \Omega_p` is the projection on the coordinates in $`S`.
+5. Conclude that $`X` is the composition of a measurable function $`(X \circ g)` and the random variable generating the sub-sigma-algebra, and thus is measurable with respect to that sub-sigma-algebra.
+
+
+:::lemma_ "AM.measurable_hist" (parent := "bandit_space") (lean := "Bandits.ArrayModel.measurable_hist, Bandits.ArrayModel.measurable_action, Bandits.ArrayModel.measurable_reward")
+$`H_t`, $`N_{t,A_t}`, $`A_t` and $`R_t` are measurable for all $`t \in \mathbb{N}`.
+
+Uses: {uses "AM.history"}[], {uses "algorithm"}[].
+:::
+
+:::proof "AM.measurable_hist"
+Uses: {uses "AM.history"}[].
+:::
+
+
+:::lemma_ "AM.hist_congr" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hist_congr")
+Let $`\omega, \omega' \in \Omega_{\mathcal{A}}` and $`t \in \mathbb{N}`.
+Suppose that
+- $`\forall s \le t, \ \omega_{1,s} = \omega'_{1,s}` ,
+- $`\forall a \in \mathcal{A}, \forall s < N_{t+1,a}, \ \omega_{2,s,a} = \omega'_{2,s,a}` .
+
+Then $`H_t(\omega) = H_t(\omega')`.
+
+Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[].
+:::
+
+:::proof "AM.hist_congr"
+Uses: {uses "AM.history"}[], {uses "pullCount_basic"}[].
+:::
+
+
+:::lemma_ "AM.stepsUntil_congr" (parent := "bandit_space") (lean := "Bandits.ArrayModel.stepsUntil_congr")
+Let $`\omega, \omega' \in \Omega_{\mathcal{A}}`, $`t, m \in \mathbb{N}` and $`a \in \mathcal{A}`.
+Suppose that
+- $` \omega_{1} = \omega'_{1}` ,
+- $`\forall s < m, \ \omega_{2,s,a} = \omega'_{2,s,a}` ,
+- $`\forall b \ne a, \forall s \in \mathbb{N}, \ \omega_{2,s,b} = \omega'_{2,s,b}` .
+
+Then $`(N_{t+1, a}(\omega) = m \wedge A_{t+1}(\omega) = a) \iff (N_{t+1, a}(\omega') = m \wedge A_{t+1}(\omega') = a)`.
+
+Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[].
+:::
+
+:::proof "AM.stepsUntil_congr"
+Uses: {uses "AM.history"}[], {uses "AM.hist_congr"}[].
+:::
+
+
+:::definition "AM.probSpaceSubsets" (parent := "bandit_space") (lean := "Bandits.ArrayModel.truePast")
+We define the following functions on $`\Omega_{\mathcal{A}}`:
+- $`F_{1, t}(\omega) = ((\omega_{1,s})_{s \le t}, (\omega_{2,s})_{s \in \mathbb{N}})` ,
+- $`F_{2, a, t}(\omega) = ((\omega_{1,s})_{s \in \mathbb{N}}, (\omega_{2, \min\{s,N_{t+1,a}(\omega)-1\}, a})_{s \in \mathbb{N}}, (\omega_{2, s, b})_{s \in \mathbb{N}, b \ne a})` ,
+- $`F_{2, a}^m(\omega) = ((\omega_{1,s})_{s \in \mathbb{N}}, (\omega_{2, \min\{s,m-1\}, a})_{s \in \mathbb{N}}, (\omega_{2, s, b})_{s \in \mathbb{N}, b \ne a})` .
+
+In the definition of $`F_{2, a, t}` and $`F_{2, a}^m`, if $`N_{t+1,a}(\omega) = 0` (resp. $`m = 0`), then the second component is a constant sequence equal to an arbitrary value.
+
+$`F_{1, t}(\omega)` contains all the information in $`\omega` except for the action selection randomness after time $`t`.
+
+$`F_{2, a, t}(\omega)` contains all the information in $`\omega` except the rewards for arm $`a` indexed by $`N_{t+1,a}(\omega)` or more.
+$`F_{2, a}^m(\omega)` is similar, but removes the rewards for arm $`a` indexed by $`m` or more.
+
+Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[].
+:::
+
+
+:::lemma_ "AM.measurable_hist_todo" (parent := "bandit_space") (lean := "Bandits.ArrayModel.measurable_hist_todo, Bandits.ArrayModel.measurable_hist_truePast")
+For all $`t \in \mathbb{N}`, $`H_t` is measurable with respect to the sigma-algebra generated by $`F_{1, t}`, and with respect to the sigma-algebra generated by $`F_{2, a, t}` for any arm $`a \in \mathcal{A}`.
+
+Uses : {uses "algorithm"}[], {uses "AM.probSpaceSubsets"}[].
+:::
+
+:::proof "AM.measurable_hist_todo"
+Uses: {uses "AM.measurable_hist"}[], {uses "pullCount"}[], {uses "AM.hist_congr"}[].
+:::
+
+
+:::lemma_ "AM.measurable_action_add_one_truePast" (parent := "bandit_space") (lean := "Bandits.ArrayModel.measurable_action_add_one_truePast")
+$`A_{t+1}` is measurable with respect to the sigma-algebra generated by $`F_{2, a, t}` for any arm $`a \in \mathcal{A}`.
+
+Uses : {uses "algorithm"}[], {uses "AM.probSpaceSubsets"}[].
+:::
+
+:::proof "AM.measurable_action_add_one_truePast"
+  Uses: {uses "AM.measurable_hist_todo"}[], .
+:::
+
+
+:::lemma_ "AM.measurable_pullCount_add_one_truePast" (parent := "bandit_space") (lean := "Bandits.ArrayModel.measurable_pullCount_add_one_truePast")
+$`N_{t+1,a}` is measurable with respect to the sigma-algebra generated by $`F_{2, a, t}`.
+
+Uses: {uses "AM.history"}[], {uses "arrayMeasure"}[], {uses "algorithm"}[], {uses "AM.probSpaceSubsets"}[], {uses "pullCount"}[].
+:::
+
+:::proof "AM.measurable_pullCount_add_one_truePast"
+  Uses: {uses "AM.measurable_hist_todo"}[].
+:::
+
+
+:::lemma_ "AM.measurable_stepsUntil" (parent := "bandit_space") (lean := "Bandits.ArrayModel.measurable_stepsUntil")
+For $`t, m \in \mathbb{N}` and $`a \in \mathcal{A}`, the indicator function $`\mathbb{I}\{N_{t+1,a} = m \wedge A_{t+1} = a\} : \Omega_{\mathcal{A}} \to \{0, 1\}` is measurable with respect to the sigma-algebra generated by $`F_{2, a}^m`.
+
+Uses: {uses "AM.history"}[], {uses "arrayMeasure"}[], {uses "algorithm"}[], {uses "pullCount"}[], {uses "AM.probSpaceSubsets"}[].
+:::
+
+:::proof "AM.measurable_stepsUntil"
+  Uses: {uses "AM.measurable_hist"}[], {uses "AM.stepsUntil_congr"}[].
+:::
+
+
+:::lemma_ "AM.measurable_pullCount_action_add_one_hist" (parent := "bandit_space") (lean := "Bandits.ArrayModel.measurable_pullCount_action_add_one_hist")
+For $`t \in \mathbb{N}`, the function $`N_{t+1, A_{t+1}}` is measurable with respect to the sigma-algebra generated by $`H_t` and $`A_{t+1}`.
+
+Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[].
+:::
+
+:::proof "AM.measurable_pullCount_action_add_one_hist"
+:::
+
+
+
+## Independence
+
+
+:::lemma_ "AM.indepFun_fst_add_one_aux" (parent := "bandit_space") (lean := "Bandits.ArrayModel.indepFun_fst_add_one_aux")
+$`\omega \mapsto \omega_{1, t+1}` is independent of $`F_{1, t}`.
+
+Uses: {uses "AM.probSpaceSubsets"}[].
+:::
+
+
+:::lemma_ "AM.indepFun_fst_add_one_hist" (parent := "bandit_space") (lean := "Bandits.ArrayModel.indepFun_fst_add_one_hist")
+$`\omega \mapsto \omega_{1, t+1}` is independent of $`H_t`.
+
+Uses: {uses "algorithm"}[], {uses "AM.probSpaceSubsets"}[].
+:::
+
+:::proof "AM.indepFun_fst_add_one_hist"
+  Uses: {uses "AM.measurable_hist_todo"}[], {uses "AM.indepFun_fst_add_one_aux"}[]
+:::
+
+
+:::lemma_ "AM.indepFun_snd_apply_aux" (parent := "bandit_space") (lean := "Bandits.ArrayModel.indepFun_snd_apply_aux")
+For $`a \in \mathcal{A}` and $`m \in \mathbb{N}`, $`\omega \mapsto \omega_{2, m, a}` is independent of $`F_{2, a}^m`.
+
+Uses: {uses "AM.probSpaceSubsets"}[].
+:::
+
+
+
+:::lemma_ "AM.indepFun_snd_apply_pullCount_action" (parent := "bandit_space") (lean := "Bandits.ArrayModel.indepFun_snd_apply_pullCount_action")
+For $`a \in \mathcal{A}` and $`m \in \mathbb{N}`, $`\omega \mapsto \omega_{2, m, a}` is independent of the indicator function $`\mathbb{I}\{N_{t+1,a} = m \wedge A_{t+1} = a\}`.
+
+Uses: {uses "algorithm"}[], {uses "pullCount"}[], {uses "AM.probSpaceSubsets"}[].
+:::
+
+:::proof "AM.indepFun_snd_apply_pullCount_action"
+  Uses: {uses "AM.indepFun_snd_apply_aux"}[], {uses "AM.measurable_stepsUntil"}[]
+:::
+
+
+:::lemma_ "AM.indepFun_snd_hist_cond" (parent := "bandit_space") (lean := "Bandits.ArrayModel.indepFun_snd_hist_cond")
+For $`a \in \mathcal{A}` and $`t, m \in \mathbb{N}`, $`\omega \mapsto \omega_{2, m, a}` is independent of $`H_t` given that $`N_{t+1,a} = m` and $`A_{t+1} = a`.
+
+Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[].
+:::
+
+:::proof "AM.indepFun_snd_hist_cond"
+  Uses: {uses "AM.measurable_hist_todo"}[], {uses "AM.measurable_hist"}[], {uses "AM.indepFun_snd_apply_aux"}[], {uses "AM.measurable_stepsUntil"}[], {uses "AM.probSpaceSubsets"}[].
+:::
+
+
+
+
+## Laws
+
+
+:::lemma_ "AM.hasLaw_action_zero" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hasLaw_action_zero")
+The law of $`A_0` in the array model is $`P_0`.
+
+Uses : {uses "AM.history"}[], {uses "algorithm"}[].
+:::
+
+:::proof "AM.hasLaw_action_zero"
+  Uses: {uses "AM.measurable_hist"}[]
+:::
+
+
+:::lemma_ "AM.hasCondDistrib_reward_zero" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hasCondDistrib_reward_zero")
+In the array model, $`P_{\mathcal{A}}(R_0 \mid A_0) = \nu`.
+
+Uses: {uses "AM.history"}[], {uses "algorithm"}[].
+:::
+
+:::proof "AM.hasCondDistrib_reward_zero"
+  Uses: {uses "AM.measurable_hist"}[], {uses "condDistrib_ae_eq_cond"}[]
+:::
+
+
+:::lemma_ "AM.hasCondDistrib_action" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hasCondDistrib_action")
+In the array model, $`P_{\mathcal{A}}(A_{t+1} \mid H_t) = \pi_t`.
+
+Uses: {uses "AM.history"}[], {uses "algorithm"}[].
+:::
+
+:::proof "AM.hasCondDistrib_action"
+  Uses: {uses "AM.measurable_hist"}[], {uses "AM.indepFun_fst_add_one_hist"}[]
+:::
+
+
+:::lemma_ "AM.hasCondDistrib_reward_pullCount_action" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hasCondDistrib_reward_pullCount_action")
+In the array model, $`P_{\mathcal{A}}(R_{t+1} \mid N_{t+1,A_{t+1}}, A_{t+1}) = \nu`.
+
+Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[].
+:::
+
+:::proof "AM.hasCondDistrib_reward_pullCount_action"
+  Uses: {uses "AM.indepFun_snd_apply_pullCount_action"}[], {uses "AM.measurable_hist"}[], {uses "pullCount_basic"}[], {uses "condDistrib_ae_eq_cond"}[]
+:::
+
+
+:::lemma_ "AM.hasCondDistrib_reward_hist_action_pullCount" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hasCondDistrib_reward_hist_action_pullCount")
+In the array model, $`P_{\mathcal{A}}(R_{t+1} \mid H_t, A_{t+1}, N_{t+1,A_{t+1}}) = \nu`.
+
+Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[].
+:::
+
+:::proof "AM.hasCondDistrib_reward_hist_action_pullCount"
+  Uses: {uses "AM.indepFun_snd_apply_pullCount_action"}[], {uses "AM.indepFun_snd_hist_cond"}[], {uses "AM.measurable_hist"}[], {uses "pullCount_basic"}[]
+:::
+
+
+:::lemma_ "AM.condIndepFun_reward_hist" (parent := "bandit_space") (lean := "Bandits.ArrayModel.condIndepFun_reward_hist")
+For $`t \ge 0`, $`R_{t+1} \ind H_t \mid A_{t+1}, N_{t+1, A_{t+1}}`.
+
+Uses: {uses "AM.history"}[], {uses "algorithm"}[], {uses "pullCount"}[], {uses "AM.measurable_hist"}[].
+:::
+
+:::proof "AM.condIndepFun_reward_hist"
+  Uses: {uses "AM.measurable_hist"}[], {uses "AM.hasCondDistrib_reward_hist_action_pullCount"}[]
+:::
+
+
+:::lemma_ "AM.hasCondDistrib_reward" (parent := "bandit_space") (lean := "Bandits.ArrayModel.hasCondDistrib_reward")
+In the array model, $`P_{\mathcal{A}}(R_{t+1} \mid H_t, A_{t+1}) = \nu`.
+
+Uses: {uses "AM.history"}[], {uses "stationaryEnv"}[], {uses "environment"}[], {uses "algorithm"}[].
+:::
+
+:::proof "AM.hasCondDistrib_reward"
+  Uses: {uses "AM.measurable_pullCount_action_add_one_hist"}[], {uses "AM.hasCondDistrib_reward_pullCount_action"}[], {uses "AM.measurable_hist"}[], {uses "AM.condIndepFun_reward_hist"}[], {uses "pullCount"}[]
+:::
+
+
+:::theorem "isAlgEnvSeq_arrayMeasure" (parent := "bandit_space") (lean := "Bandits.ArrayModel.isAlgEnvSeq_arrayMeasure")
+The actions and rewards defined on the array model probability space $`(\Omega_{\mathcal{A}}, P_{\mathcal{A}})` form an algorithm-environment sequence for the algorithm $`\mathfrak{A}` and bandit $`\nu`.
+
+Uses: {uses "AM.history"}[], {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[].
+:::
+
+:::proof "isAlgEnvSeq_arrayMeasure"
+The four conditions of {uses "IsAlgEnvSeq"}[] are satisfied by {uses "AM.hasLaw_action_zero"}[], {uses "AM.hasCondDistrib_reward_zero"}[], {uses "AM.hasCondDistrib_action"}[] and {uses "AM.hasCondDistrib_reward"}[].
+:::
+
+
+
+# Law of the n-th pull
+
+:::group "rewardByCount_law"
+Law of the n-th pull
+:::
+
+This section describes the law of $`Y_{n, a}` the $`n^{th}` reward obtained from an arm $`a \in \mathcal{A}`.
+
+We augment the probability space $`\Omega` on which we have an algorithm-environment sequence with $`\Omega' = \mathbb{R}^{\mathbb{N} \times \mathcal{A}}`, on which we put the product measure $`\bigotimes_{n \in \mathbb{N}, a \in \mathcal{A}} \nu(a)`.
+With that measure, the law of $`Z_{n,a}` is $`\nu(a)`.
+
+
+:::lemma_ "measurable_comap_indicator_stepsUntil_eq" (parent := "rewardByCount_law") (lean := "Learning.measurable_comap_indicator_stepsUntil_eq")
+The function $`\mathbb{I}\{T_{n,a} = t\} : \Omega \to \{0, 1\}` is measurable with respect to the sigma-algebra generated by $`(H_{t-1}, A_t)`.
+
+Uses: {uses "history"}[], {uses "stepsUntil"}[].
+:::
+
+:::proof "measurable_comap_indicator_stepsUntil_eq"
+  Uses: {uses "stepsUntil_basic"}[], {uses "pullCount_basic"}[], {uses "pullCount"}[], {uses "IsAlgEnvSeq.filtration"}[].
+:::
+
+
+:::lemma_ "CondIndepFun.prod_right" (lean := "ProbabilityTheory.CondIndepFun.prod_right")
+If $`X \ind Y \mid Z`, then $`X \ind (Y, Z) \mid Z`.
+:::
+
+
+:::lemma_ "condIndepFun_reward_stepsUntil_arm" (parent := "rewardByCount_law") (lean := "Bandits.condIndepFun_reward_stepsUntil_action")
+For $`t > 0`, $`R_t \ind \mathbb{I}\{T_{n, a} = t\} \mid A_t`.
+
+Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "ionescu-tulcea"}[], {uses "stepsUntil"}[].
+:::
+
+:::proof "condIndepFun_reward_stepsUntil_arm"
+$`\mathbb{I}\{T_{n, a} = t\}` is measurable with respect to the sigma-algebra generated by $`(H_{t-1}, A_t)` by {uses "measurable_comap_indicator_stepsUntil_eq"}[].
+
+It thus suffices to show that $`R_t \ind (H_{t-1}, A_t) \mid A_t`, which is implied by $`R_t \ind H_{t-1} \mid A_t` ({uses "CondIndepFun.prod_right"}[]), which is {uses "condIndepFun_reward_hist_action"}[].
+
+Uses: {uses "condIndepFun_reward_hist_action"}[], {uses "CondIndepFun.prod_right"}[], {uses "stepsUntil_basic"}[], {uses "measurable_comap_indicator_stepsUntil_eq"}[], {uses "history"}[], {uses "pullCount"}[].
+:::
+
+
+:::lemma_ "reward_cond_stepsUntil" (parent := "rewardByCount_law") (lean := "Bandits.reward_cond_stepsUntil")
+Let $`n > 0`, $`t \in \mathbb{N}` and suppose that $`P(T_{n, a} = t) > 0`.
+Then $`P(R_t \mid T_{n, a} = t) = \nu(a)`.
+
+Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "ionescu-tulcea"}[], {uses "stepsUntil"}[].
+:::
+
+:::proof "reward_cond_stepsUntil"
+First, if $`T_{n, a} = t`, then $`A_t = a` ({uses "stepsUntil_basic"}[]), such that $`P(R_t \mid T_{n, a} = t) = P(R_t \mid T_{n, a} = t, A_t = a)`.
+
+Then, using first the independence from {uses "condIndepFun_reward_stepsUntil_arm"}[] and then the conditional distribution from {uses "condDistrib_reward_stationaryEnv"}[], we have
+$$`
+  P(R_t \mid T_{n, a} = t, A_t = a)
+  = P(R_t \mid A_t = a)
+  = \nu(a)
+  \: .
+`
+
+Uses: {uses "environment"}[], {uses "stepsUntil_basic"}[], {uses "condIndepFun_reward_stepsUntil_arm"}[], {uses "pullCount"}[], {uses "condDistrib_ae_eq_cond"}[], {uses "condDistrib_reward_stationaryEnv"}[]
+:::
+
+
+:::lemma_ "condDistrib_ae_eq_cond" (lean := "ProbabilityTheory.condDistrib_ae_eq_cond")
+For a random variable $`X` on a countable space with the discrete sigma algebra, $`P(Y \mid X) = (x \mapsto P(Y \mid X = x))`, $`(X_*P)`-almost surely.
+Furthermore, that almost sure equality means that for all $`x` such that $`P(X = x) > 0`, we have $`P(Y \mid X = x) = P(Y \mid X)(x)`.
+:::
+
+
+:::lemma_ "condDistrib_rewardByCount_stepsUntil" (parent := "rewardByCount_law") (lean := "Bandits.condDistrib_rewardByCount_stepsUntil")
+For $`n > 0` and $`t \in \mathbb{N}`, $`P(Y_{n,a} \mid T_{n,a}) = \nu(a)` (in which the measure on the r.h.s. is seen as a constant kernel).
+
+Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "ionescu-tulcea"}[], {uses "rewardByCount"}[], {uses "stepsUntil"}[].
+:::
+
+:::proof "condDistrib_rewardByCount_stepsUntil"
+It suffices to show that for all $`t \in \mathbb{N} \cup \{\infty\}` such that $`P(T_{n, a} = t) > 0`, the law of $`Y_{n,a}` conditioned on $`T_{n,a} = t` is $`\nu(a)`.
+
+If $`t < \infty`, then $`P(Y_{n, a} \mid T_{n, a = t}) = P(R_t \mid T_{n, a} = t) = \nu(a)` by {uses "reward_cond_stepsUntil"}[].
+
+If $`t = \infty`, then $`P(Y_{n, a} \mid T_{n, a} = \infty) = P(Z_{n, a} \mid T_{n, a} = \infty)`. By independence of $`Z_{n,a}` and $`T_{n, a}`, this is just $`\nu(a)`, the law of $`Z_{n,a}`.
+
+Uses: {uses "environment"}[], {uses "reward_cond_stepsUntil"}[], {uses "pullCount"}[], {uses "condDistrib_ae_eq_cond"}[]
+:::
+
+
+:::lemma_ "hasLaw_rewardByCount" (parent := "rewardByCount_law") (lean := "Bandits.hasLaw_rewardByCount")
+For $`n > 0` and $`a \in \mathcal{A}`, $`(Y_{n,a})_*P = \nu(a)`.
+
+Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "ionescu-tulcea"}[], {uses "rewardByCount"}[]
+:::
+
+:::proof "hasLaw_rewardByCount"
+The law of $`Y_{n,a}` is given by $`(Y_{n, a})_*P = P(Y_{n, a} \mid T_{n, a}) \circ (T_{n, a})_*P`.
+By {uses "condDistrib_rewardByCount_stepsUntil"}[], $`P(Y_{n, a} \mid T_{n, a}) = \nu(a)`, a constant kernel.
+Thus the composition is just $`\nu(a)`.
+
+Uses: {uses "environment"}[], {uses "condDistrib_rewardByCount_stepsUntil"}[], {uses "stepsUntil"}[], {uses "pullCount"}[].
+:::
+
+
+
+# Regret and other bandit quantities
+
+:::group "regret"
+Regret and other bandit quantities
+:::
+
+For an arm $`a \in \mathcal{A}`, we denote by $`\mu_a` the mean of the rewards for that arm, that is $`\mu_a = \nu(a)[\mathrm{id}]`.
+We denote by $`\mu^*` the mean of the best arm, that is $`\mu^* = \max_{a \in \mathcal{A}} \mu_a`.
+
+
+:::definition "regret" (parent := "regret") (lean := "Bandits.regret")
+The regret $`R_T` of a sequence of arms $`A_0, \ldots, A_{T-1}` after $`T` pulls is the difference between the cumulative reward of always playing the best arm and the cumulative reward of the sequence:
+$$`
+  R_T = T \mu^* - \sum_{t=0}^{T-1} \mu_{A_t} \: .
+`
+:::
+
+TODO: the $`R_T` notation clashes with the random variable $`R_t`.
+
+:::definition "gap" (parent := "regret") (lean := "Bandits.gap")
+For an arm $`a \in \mathcal{A}`, its gap is defined as the difference between the mean of the best arm and the mean of that arm: $`\Delta_a = \mu^* - \mu_a`.
+:::
+
+
+:::lemma_ "sum_pullCount_mul" (parent := "regret") (lean := "Learning.sum_pullCount_mul")
+Let $`f : \mathcal{A} \to \mathbb{R}` be a function on the arms. For all $`t \in \mathbb{N}`,
+$$`
+  \sum_{a \in \mathcal{A}} N_{t,a} f(a) = \sum_{s=0}^{t-1} f(A_s) \: .
+`
+
+Uses: {uses "pullCount"}[].
+:::
+
+:::proof "sum_pullCount_mul"
+$$`
+  \sum_{a \in \mathcal{A}} N_{t,a} f(a)
+  &= \sum_{a \in \mathcal{A}} \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\} f(a)
+  \\
+  &= \sum_{s=0}^{t-1} \sum_{a \in \mathcal{A}} \mathbb{I}\{A_s = a\} f(a)
+  \\
+  &= \sum_{s=0}^{t-1} f(A_s)
+  \: .
+`
+:::
+
+
+:::lemma_ "regret_eq_sum_pullCount_mul_gap" (parent := "regret") (lean := "Bandits.regret_eq_sum_pullCount_mul_gap")
+For $`\mathcal{A}` finite, the {uses "regret"}[regret] $`R_T` can be expressed as a sum over the arms and their {uses "gap"}[gaps]:
+$$`
+  R_T = \sum_{a \in \mathcal{A}} N_{T,a} \Delta_a \: .
+`
+
+Uses: {uses "pullCount"}[].
+:::
+
+:::proof "regret_eq_sum_pullCount_mul_gap"
+Apply {uses "sum_pullCount_mul"}[] with $`f(a) = \Delta_a` to obtain:
+$$`
+  \sum_{a \in \mathcal{A}} N_{T,a} \Delta_a
+  &= \sum_{s=0}^{T-1} \Delta_{A_s}
+  \\
+  &= \sum_{s=0}^{T-1} \mu^* - \sum_{s=0}^{T-1} \mu_{A_s}
+  \\
+  &= R_T
+  \: .
+`
+:::
+
+
+:::lemma_ "integral_regret_eq_sum_mul" (parent := "regret") (lean := "Bandits.integral_regret_eq_sum_gap_mul_integral_pullCount")
+For $`\mathcal{A}` finite, the expected {uses "regret"}[regret] can be expressed as a sum over the arms and their {uses "gap"}[gaps]:
+$$`
+  P[R_T] = \sum_{a \in \mathcal{A}}P[N_{T,a}] \Delta_a \: .
+`
+
+Uses: {uses "pullCount"}[].
+:::
+
+:::proof "integral_regret_eq_sum_mul"
+Uses: {uses "regret_eq_sum_pullCount_mul_gap"}[].
+:::
diff --git a/verso_blueprint/LMLBlueprint/Chapters/BanditAlgs.lean b/verso_blueprint/LMLBlueprint/Chapters/BanditAlgs.lean
new file mode 100644
index 00000000..61b21a58
--- /dev/null
+++ b/verso_blueprint/LMLBlueprint/Chapters/BanditAlgs.lean
@@ -0,0 +1,332 @@
+import Verso
+import VersoManual
+import VersoBlueprint
+import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
+import LeanMachineLearning.SequentialLearning.Deterministic
+import LeanMachineLearning.SequentialLearning.FiniteActions
+import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
+import LeanMachineLearning.SequentialLearning.StationaryEnv
+import LeanMachineLearning.Online.Bandit.Algorithms.ETC
+import LeanMachineLearning.Online.Bandit.Algorithms.UCB
+import LeanMachineLearning.Online.Bandit.ArrayProbSpace
+import LeanMachineLearning.Online.Bandit.Regret
+import LeanMachineLearning.Online.Bandit.RewardByCountMeasure
+import LeanMachineLearning.Online.Bandit.SumRewards
+import LeanMachineLearning.Probability.Moments.SubGaussian
+import LMLBlueprint.References
+import LMLBlueprint.TeXPrelude
+import Mathlib.Probability.Moments.SubGaussian
+
+open Verso.Genre
+open Verso.Genre.Manual
+open Informal
+
+#doc (Manual) "Bandit algorithms" =>
+
+:::group "banditAlgorithms"
+Bandit algorithms
+:::
+
+
+# Round-Robin
+
+This is not an interesting bandit algorithm per se, but it is used as a subroutine in other algorithms and can be a simple baseline.
+This algorithm simply cycles through the arms in order.
+
+:::definition "roundRobinAlgorithm" (parent := "banditAlgorithms") (lean := "Learning.RoundRobin.nextAction, Learning.roundRobinAlgorithm")
+The Round-Robin algorithm is the {uses "detAlgorithm"}[deterministic algorithm] defined as follows: at time $`t \in \mathbb{N}`, $`A_t = t \mod K`.
+:::
+
+
+:::lemma_ "pullCount_roundRobinAlgorithm" (parent := "banditAlgorithms") (lean := "Learning.RoundRobin.pullCount_mul")
+For the Round-Robin algorithm, for any arm $`a \in [K]`, at time $`Km` we have
+$$`
+  N_{Km,a} = m \: .
+`
+
+Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[] , {uses "pullCount"}[], {uses "roundRobinAlgorithm"}[].
+:::
+
+:::proof "pullCount_roundRobinAlgorithm"
+  Uses {uses "environment"}[], {uses "history"}[], {uses "pullCount_basic"}[], {uses "roundRobinAlgorithm"}[]
+:::
+
+
+TODO: regret.
+
+
+
+
+# Explore-Then-Commit
+
+Note: times start at 0 to be consistent with Lean.
+
+Note: we will describe the algorithm by writing $`A_t = ...`, but our formal bandit model needs a policy $`\pi_t` that gives the distribution of the arm to pull. What me mean is that $`\pi_t` is a Dirac distribution at that arm.
+
+:::definition "etcAlgorithm" (parent := "banditAlgorithms") (lean := "Bandits.ETC.nextArm, Bandits.etcAlgorithm")
+The Explore-Then-Commit (ETC) algorithm with parameter $`m \in \mathbb{N}` is the {uses "detAlgorithm"}[deterministic algorithm] defined as follows:
+1. for $`t < Km`, $`A_t = t \mod K` (pull each arm $`m` times),
+2. compute $`\hat{A}_m^* = \arg\max_{a \in [K]} \hat{\mu}_a`, where $`\hat{\mu}_a = \frac{1}{m} \sum_{t=0}^{Km-1} \mathbb{I}(A_t = a) X_t` is the empirical mean of the rewards for arm $`a`,
+3. for $`t \ge Km`, $`A_t = \hat{A}_m^*` (pull the empirical best arm).
+:::
+
+:::lemma_ "ETC.isAlgEnvSeqUntil_roundRobinAlgorithm" (parent := "banditAlgorithms") (lean := "Bandits.ETC.isAlgEnvSeqUntil_roundRobinAlgorithm")
+
+An {uses "IsAlgEnvSeq"}[algorithm-environment sequence] for the {uses "etcAlgorithm"}[Explore-Then-Commit algorithm] with parameter $`m` is an algorithm-environment sequence for the {uses "roundRobinAlgorithm"}[Round-Robin algorithm] until time $`Km - 1`.
+That is, ETC plays the same as Round-Robin until time $`Km - 1`.
+
+Uses {uses "stationaryEnv"}[].
+:::
+
+
+:::lemma_ "pullCount_etcAlgorithm" (parent := "banditAlgorithms") (lean := "Bandits.ETC.pullCount_of_ge")
+For the {uses "etcAlgorithm"}[Explore-Then-Commit algorithm] with parameter $`m`, for any arm $`a \in [K]` and any time $`t \ge Km`, we have
+$$`
+  N_{t,a}
+  = m + (t - Km) \mathbb{I}\{\hat{A}_m^* = a\}
+  \: .
+`
+
+Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "pullCount"}[].
+:::
+
+:::proof "pullCount_etcAlgorithm"
+  Uses: {uses "pullCount_roundRobinAlgorithm"}[], {uses "ETC.isAlgEnvSeqUntil_roundRobinAlgorithm"}[]
+:::
+
+:::lemma_ "sumRewards_bestArm_le_of_arm_mul_eq" (parent := "banditAlgorithms") (lean := "Bandits.ETC.sumRewards_bestArm_le_of_arm_mul_eq")
+If $`\hat{A}_m^* = a`, then we have $`S_{Km, a^*} \le S_{Km, a}`.
+
+Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "sumRewards"}[], {uses "etcAlgorithm"}[]
+:::
+
+:::proof "sumRewards_bestArm_le_of_arm_mul_eq"
+  Uses: {uses "environment"}[], {uses "history"}[], {uses "pullCount"}[], {uses "empMean"}[], {uses "etcAlgorithm"}[]
+:::
+
+
+:::lemma_ "prob_etc_error_le_exp" (parent := "banditAlgorithms") (lean := "Bandits.ETC.prob_arm_mul_eq_le")
+Suppose that $`\nu(a)` is $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] for all arms $`a \in [K]`.
+Then for the {uses "etcAlgorithm"}[Explore-Then-Commit algorithm] with parameter $`m`, for any arm $`a \in [K]` with $`\Delta_a > 0`, we have $`P(\hat{A}_m^* = a) \le \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)`.
+
+Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "gap"}[]
+:::
+
+:::proof "prob_etc_error_le_exp"
+By {uses "sumRewards_bestArm_le_of_arm_mul_eq"}[],
+$$`
+  P(\hat{A}_m^* = a)
+  \le P(S_{Km, a} \ge S_{Km, a^*})
+  \: .
+`
+By {uses "prob_sumRewards_le_sumRewards_le"}[], and then the concentration inequality of {uses "probReal_sum_le_sum_streamMeasure"}[] we have
+$$`
+  P\left(S_{Km, a^*} \le S_{Km, a}\right)
+  &\le (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m-1} \omega_{s, a^*} \le \sum_{s=0}^{m-1} \omega_{s, a} \right)
+  \\
+  &\le \exp\left( -m \frac{\Delta_a^2}{4 \sigma^2} \right)
+  \: .
+`
+
+Uses: {uses "environment"}[], {uses "pullCount"}[], {uses "etcAlgorithm"}[]
+:::
+
+
+:::theorem "regret_etc_le" (parent := "banditAlgorithms") (lean := "Bandits.ETC.regret_le")
+Suppose that $`\nu(a)` is $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] for all arms $`a \in [K]`.
+Then for {uses "etcAlgorithm"}[Explore-Then-Commit algorithm] with parameter $`m`, the expected regret after $`T` pulls with $`T \ge Km` is bounded by
+$$`
+  P[R_T]
+  \le m \sum_{a=1}^K \Delta_a + (T - Km) \sum_{a=1}^K \Delta_a \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)
+  \: .
+`
+
+Uses: {uses "stationaryEnv"}[], {uses "regret"}[], {uses "IsAlgEnvSeq"}[], {uses "gap"}[]
+:::
+
+:::proof "regret_etc_le"
+By {uses "regret_eq_sum_pullCount_mul_gap"}[], we have $`P[R_T] = \sum_{a=1}^K P\left[N_{T,a}\right] \Delta_a`~.
+It thus suffices to bound $`P[N_{T,a}]` for each arm $`a` with $`\Delta_a > 0`.
+It suffices to prove that
+$$`
+  P[N_{T,a}]
+  \le m + (T - Km) \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)
+  \: .
+`
+
+By {uses "pullCount_etcAlgorithm"}[],
+$$`
+  N_{T,a}
+  = m + (T - Km) \mathbb{I}\{\hat{A}_m^* = a\}
+  \: .
+`
+
+It thus suffices to prove the inequality $`P(\hat{A}_m^* = a) \le \exp\left(- \frac{m \Delta_a^2}{4 \sigma^2}\right)` for $`\Delta_a > 0`.
+This is done in {uses "prob_etc_error_le_exp"}[].
+
+
+Uses: {uses "integral_regret_eq_sum_mul"}[], {uses "pullCount_basic"}[],
+:::
+
+
+# UCB
+
+:::definition "ucbAlgorithm" (parent := "banditAlgorithms") (lean := "Bandits.UCB.nextArm, Bandits.ucbAlgorithm")
+The UCB algorithm with parameter $`c \in \mathbb{R}_+` is the {uses "detAlgorithm"}[deterministic algorithm] defined as follows:
+1. for $`t < K`, $`A_t = t \mod K` (pull each arm once),
+2. for $`t \ge K`, $`A_t = \arg\max_{a \in [K]} \left( \hat{\mu}_{t,a} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,a}}} \right)`, where $`\hat{\mu}_{t,a} = \frac{1}{N_{t,a}} \sum_{s=0}^{t-1} \mathbb{I}(A_s = a) X_s` is the empirical mean of the rewards for arm `a`.
+:::
+
+
+Note: the argmax in the second step is chosen in a measurable way.
+
+
+:::lemma_ "UCB.isAlgEnvSeqUntil_roundRobinAlgorithm" (parent := "banditAlgorithms") (lean := "Bandits.UCB.isAlgEnvSeqUntil_roundRobinAlgorithm")
+An {uses "IsAlgEnvSeq"}[algorithm-environment sequence] for the {uses "ucbAlgorithm"}[UCB algorithm] is an algorithm-environment sequence for the {uses "roundRobinAlgorithm"}[Round-Robin algorithm] until time $`K - 1`.
+That is, UCB plays the same as Round-Robin until time $`K - 1`.
+
+Uses: {uses "stationaryEnv"}[].
+:::
+
+
+:::lemma_ "ucbIndex_le_ucbIndex_arm" (parent := "banditAlgorithms") (lean := "Bandits.UCB.ucbIndex_le_ucbIndex_arm")
+For the {uses "ucbAlgorithm"}[UCB algorithm], for all time $`t \ge K` and arm $`a \in [K]`, we have
+$$`
+  \hat{\mu}_{t,a} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,a}}}
+  \le \hat{\mu}_{t,A_t} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,A_t}}}
+  \: .
+`
+
+Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "pullCount"}[], {uses "empMean"}[]
+:::
+
+:::proof "ucbIndex_le_ucbIndex_arm"
+By definition of the algorithm.
+:::
+
+
+:::lemma_ "gap_arm_le_two_mul_ucbWidth" (parent := "banditAlgorithms") (lean := "Bandits.UCB.gap_arm_le_two_mul_ucbWidth, Bandits.UCB.pullCount_arm_le")
+Suppose that we have the 3 following conditions:
+1. $`\mu^* \le \hat{\mu}_{t, a^*} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,a^*}}}`,
+2. $`\hat{\mu}_{t,A_t} - \sqrt{\frac{2 c \log(t + 1)}{N_{t,A_t}}} \le \mu_{A_t}`,
+3. $`\hat{\mu}_{t, a^*} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,a^*}}} \le \hat{\mu}_{t,A_t} + \sqrt{\frac{2 c \log(t + 1)}{N_{t,A_t}}}`.
+
+Then if $`N_{t,A_t} > 0` we have
+$$`
+  \Delta_{A_t}
+  \le 2 \sqrt{\frac{2 c \log(t + 1)}{N_{t,A_t}}}
+  \: .
+`
+
+And in turn, if $`\Delta_{A_t} > 0` we get
+$$`
+  N_{t,A_t}
+  \le \frac{8 c \log(t + 1)}{\Delta_{A_t}^2}
+  \: .
+`
+
+Note that the third condition is always satisfied for UCB by {uses "ucbIndex_le_ucbIndex_arm"}[], but this lemma, as stated, is independent of the UCB algorithm.
+
+Uses: {uses "pullCount"}[], {uses "gap"}[], {uses "empMean"}[].
+:::
+
+
+:::lemma_ "prob_ucbIndex_le" (parent := "banditAlgorithms") (lean := "Bandits.UCB.prob_ucbIndex_le")
+Suppose that $`\nu(a)` is $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] for all arms $`a \in [K]`.
+Let $`c \ge 0` be a real number.
+Then for any time $`n \in \mathbb{N}` and any arm $`a \in [K]`, we have
+$$`
+  P\left(0 < N_{n, a} \ \wedge \ \hat{\mu}_{n, a} + \sqrt{\frac{2 c \sigma^2 \log(n + 1)}{N_{n,a}}} \le \mu_a\right)
+  \le \frac{1}{(n + 1)^{c - 1}}
+  \: .
+`
+
+And also,
+$$`
+  P\left(0 < N_{n, a} \ \wedge \ \hat{\mu}_{n, a} - \sqrt{\frac{2 c \sigma^2 \log(n + 1)}{N_{n,a}}} \ge \mu_a\right)
+  \le \frac{1}{(n + 1)^{c - 1}}
+  \: .
+`
+
+Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "pullCount"}[], {uses "empMean"}[]
+:::
+
+:::proof "prob_ucbIndex_le"
+  Uses: {uses "prob_sum_le_sqrt_log"}[], {uses "ionescu-tulcea"}[], {uses "prob_pullCount_prod_sumRewards_mem_le"}[].
+:::
+
+
+:::lemma_ "pullCount_le_add_three" (parent := "banditAlgorithms")
+For $`C` a natural number, for any time $`n \in \mathbb{N}` and any arm $`a \in [K]`, we have
+$$`
+  N_{n,a}
+  &\le C + 1
+  \\&\quad +
+      \sum_{s=1}^{n-1} \mathbb{I}\{A_s = a \ \wedge \ C < N_{s,a} \ \wedge \
+        \mu^* \le \hat{\mu}_{s, a^*} + \sqrt{\frac{2 c \sigma^2 \log(s + 1)}{N_{s,a^*}}} \ \wedge \
+        \hat{\mu}_{s, A_s} - \sqrt{\frac{2 c \sigma^2 \log(s + 1)}{N_{s,A_s}}} \le \mu_{A_s}\}
+  \\&\quad +
+      \sum_{s=1}^{n-1}
+        \mathbb{I}\{0 < N_{s, a^*} \ \wedge \ \hat{\mu}_{s, a^*} + \sqrt{\frac{2 c \sigma^2 \log(s + 1)}{N_{s,a^*}}} <
+          \mu^*\}
+  \\&\quad +
+      \sum_{s=1}^{n-1}
+        \mathbb{I}\{0 < N_{s, a} \ \wedge \ \mu_a <
+          \hat{\mu}_{s, a} - \sqrt{\frac{2 c \sigma^2 \log(s + 1)}{N_{s,a}}}\}
+`
+
+Uses: {uses "pullCount"}[], {uses "empMean"}[], {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "ucbAlgorithm"}[].
+:::
+
+:::proof "pullCount_le_add_three"
+  Uses: {uses "environment"}[], {uses "ucbAlgorithm"}[], {uses "pullCount_basic"}[]
+:::
+
+
+:::lemma_ "some_sum_eq_zero" (parent := "banditAlgorithms")
+For the {uses "ucbAlgorithm"}[UCB algorithm] with parameter $`c \sigma^2 \ge 0`, for any time $`n \in \mathbb{N}` and any arm $`a \in [K]` with positive gap, the first sum in {uses "pullCount_le_add_three"}[] is equal to zero for positive $`C` such that $`C \ge \frac{8 c \sigma^2 \log(n + 1)}{\Delta_a^2}`.
+
+Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "ucbAlgorithm"}[], {uses "pullCount"}[], {uses "gap"}[], {uses "empMean"}[].
+
+The Lean declaration is "Bandits.UCB.some\_sum\_eq\_zero" but adding it causes a strange error, so I removed it.
+:::
+
+:::proof "some_sum_eq_zero"
+  Uses: {uses "environment"}[], {uses "ucbAlgorithm"}[], {uses "ucbIndex_le_ucbIndex_arm"}[], {uses "pullCount_basic"}[], {uses "gap_arm_le_two_mul_ucbWidth"}[]
+:::
+
+
+:::lemma_ "expectation_pullCount_le" (parent := "banditAlgorithms") (lean := "Bandits.UCB.expectation_pullCount_le")
+Suppose that $`\nu(a)` is $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] for all arms $`a \in [K]`.
+For the {uses "ucbAlgorithm"}[UCB algorithm] with parameter $`c \sigma^2 > 0`, for any time $`n \in \mathbb{N}` and any arm $`a \in [K]` with positive {uses "gap"}[gap], we have
+$$`
+  P[N_{n,a}]
+  \le \frac{8 c \sigma^2 \log(n + 1)}{\Delta_a^2} + 2 + 2 \sum_{s=0}^{n-1} \frac{1}{(s + 1)^{c - 1}}
+  \: .
+`
+
+Uses: {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[], {uses "pullCount"}[].
+:::
+
+:::proof "expectation_pullCount_le"
+  Uses: {uses "some_sum_eq_zero"}[], {uses "prob_ucbIndex_le"}[], {uses "pullCount_basic"}[], {uses "pullCount_le_add_three"}[]
+:::
+
+
+:::lemma_ "ucb_regret_le" (parent := "banditAlgorithms") (lean := "Bandits.UCB.regret_le")
+Suppose that $`\nu(a)` is $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] for all arms $`a \in [K]`.
+For the {uses "ucbAlgorithm"}[UCB algorithm] with parameter $`c \sigma^2 > 0`, for any time $`n \in \mathbb{N}`, we have
+$$`
+  P[R_n]
+  \le \sum_{a : \Delta_a > 0} \left(\frac{8 c \sigma^2 \log(n + 1)}{\Delta_a} + 2 \Delta_a\left(1 + \sum_{s=0}^{n-1} \frac{1}{(s + 1)^{c - 1}}\right)\right)
+  \: .
+`
+
+Uses: {uses "stationaryEnv"}[], {uses "regret"}[], {uses "IsAlgEnvSeq"}[], {uses "gap"}[].
+:::
+
+:::proof "ucb_regret_le"
+  Uses: {uses "integral_regret_eq_sum_mul"}[], {uses "pullCount_basic"}[], {uses "expectation_pullCount_le"}[]
+:::
+
+TODO: for $`c > 2`, the sum converges to a constant, so we get a logarithmic regret bound.
diff --git a/verso_blueprint/LMLBlueprint/Chapters/Concentration.lean b/verso_blueprint/LMLBlueprint/Chapters/Concentration.lean
new file mode 100644
index 00000000..21ed82c3
--- /dev/null
+++ b/verso_blueprint/LMLBlueprint/Chapters/Concentration.lean
@@ -0,0 +1,189 @@
+import Verso
+import VersoManual
+import VersoBlueprint
+import LeanMachineLearning.SequentialLearning.Deterministic
+import LeanMachineLearning.SequentialLearning.FiniteActions
+import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
+import LeanMachineLearning.SequentialLearning.StationaryEnv
+import LeanMachineLearning.Online.Bandit.ArrayProbSpace
+import LeanMachineLearning.Online.Bandit.Regret
+import LeanMachineLearning.Online.Bandit.RewardByCountMeasure
+import LeanMachineLearning.Online.Bandit.SumRewards
+import LeanMachineLearning.Probability.Moments.SubGaussian
+import LMLBlueprint.References
+import LMLBlueprint.TeXPrelude
+import Mathlib.Probability.Moments.SubGaussian
+
+open Verso.Genre
+open Verso.Genre.Manual
+open Informal
+
+#doc (Manual) "Concentration inequalities" =>
+
+# Sub-Gaussian random variables
+
+:::group "subGaussian"
+Sub-Gaussian random variables
+:::
+
+:::definition "subGaussian" (parent := "subGaussian") (lean := "ProbabilityTheory.HasSubgaussianMGF")
+A real valued random variable $`X` is $`\sigma^2`-sub-Gaussian if for any $`\lambda \in \mathbb{R}`,
+$$`
+  P\left[e^{\lambda X}\right]
+  \le e^{\frac{\lambda^2 \sigma^2}{2}}
+  \: .
+`
+:::
+
+
+:::lemma_ "subGaussian_add_of_indepFun" (parent := "subGaussian") (lean := "ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun")
+If $`X` is $`\sigma_1^2`-{uses "subGaussian"}[sub-Gaussian] and $`Y` is $`\sigma_2^2`-sub-Gaussian, and $`X` and $`Y` are independent, then $`X + Y` is $`(\sigma_1^2 + \sigma_2^2)`-sub-Gaussian.
+:::
+
+
+:::lemma_ "hoeffding_one" (parent := "subGaussian") (lean := "ProbabilityTheory.HasSubgaussianMGF.measure_ge_le")
+For $`X` a $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] random variable, for any $`t \ge 0`,
+$$`
+  P(X \ge t)
+  \le \exp\left(- \frac{t^2}{2 \sigma^2}\right)
+  \: .
+`
+:::
+
+
+:::theorem "hoeffding" (parent := "subGaussian") (lean := "ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun")
+Let $`X_1, \ldots, X_n` be independent random variables such that $`X_i` is $`\sigma_i^2`-{uses "subGaussian"}[sub-Gaussian] for $`i \in [n]`.
+Then for any $`t \ge 0`,
+$$`
+  P\left(\sum_{i=1}^n X_i \ge t\right)
+  \le \exp\left(- \frac{t^2}{2 \sum_{i=1}^n \sigma_i^2}\right)
+  \: .
+`
+:::
+
+:::proof "hoeffding"
+Uses: {uses "subGaussian_add_of_indepFun"}[], {uses "hoeffding_one"}[].
+:::
+
+
+:::lemma_ "measure_sum_le_sum_le'" (parent := "subGaussian")
+Let $`X_1, \ldots, X_n` be random variables such that $`X_i - P[X_i]` is $`\sigma_{X,i}^2`-{uses "subGaussian"}[sub-Gaussian] for $`i \in [n]`.
+Let $`Y_1, \ldots, Y_m` be random variables such that $`Y_i - P[Y_i]` is $`\sigma_{Y,i}^2`-{uses "subGaussian"}[sub-Gaussian] for $`i \in [m]`.
+Suppose further that the vectors $`X` and $`Y` are independent and that $`\sum_{i = 1}^m P[Y_i] \le \sum_{i = 1}^n P[X_i]`.
+Then
+$$`
+  P\left(\sum_{i=1}^m Y_i \ge \sum_{i=1}^n X_i\right)
+  \le \exp\left(- \frac{\left(\sum_{i = 1}^n P[X_i] - \sum_{i=1}^m P[Y_i]\right)^2}{2 \sum_{i=1}^n (\sigma_{X,i}^2 + \sigma_{Y,i}^2)}\right)
+  \: .
+`
+
+This is "ProbabilityTheory.HasSubgaussianMGF.measure\_sum\_le\_sum\_le'" in Lean, but I get a strange error if I add that information.
+:::
+
+:::proof "measure_sum_le_sum_le'"
+Uses: {uses "subGaussian_add_of_indepFun"}[], {uses "hoeffding_one"}[].
+:::
+
+
+
+# Concentration of the sums of rewards in bandit models
+
+:::group "concentrationBandits"
+Concentration of the sums of rewards in bandit models
+:::
+
+:::lemma_ "identDistrib_pullCount_prod_sumRewards" (parent := "concentrationBandits") (lean := "Bandits.ArrayModel.identDistrib_pullCount_prod_sumRewards")
+In the array model, for $`t \in \mathbb{N}`, the random variable $`(N_{t,a}, S_{t, a})_{a \in \mathcal{A}}` has the same distribution as $`(N_{t,a}, \sum_{s=0}^{N_{t,a}-1} \omega_{2, s, a})_{a \in \mathcal{A}}`.
+
+Uses: {uses "arrayMeasure"}[] ,{uses "AM.history"}[], {uses "algorithm"}[], {uses "sumRewards"}[], {uses "pullCount"}[].
+:::
+
+:::proof "identDistrib_pullCount_prod_sumRewards"
+Uses: {uses "AM.history"}[], {uses "stepsUntil_basic"}[], {uses "ionescu-tulcea"}[], {uses "algFunction"}[], {uses "AM.measurable_hist"}[], {uses "rewardByCount"}[], {uses "pullCount_basic"}[], {uses "stepsUntil"}[], {uses "sum_rewardByCount"}[].
+:::
+
+
+:::lemma_ "AM.identDistrib_sum_range_snd" (parent := "concentrationBandits") (lean := "Bandits.ArrayModel.identDistrib_sum_range_snd")
+In the {uses "arrayMeasure"}[array model], for $`k \in \mathbb{N}`, the random variable $`\sum_{s=0}^{k-1} \omega_{2, s, a}` has the same distribution as a sum of $`k` i.i.d. random variables with law $`\nu(a)`.
+:::
+
+:::proof "AM.identDistrib_sum_range_snd"
+By definition of {uses "arrayMeasure"}[$`P_{\mathcal{A}}`].
+:::
+
+
+:::lemma_ "prob_pullCount_prod_sumRewards_mem_le" (parent := "concentrationBandits") (lean := "Bandits.ArrayModel.prob_pullCount_prod_sumRewards_mem_le, Bandits.prob_pullCount_prod_sumRewards_mem_le")
+In the {uses "arrayMeasure"}[array model], for $`t \in \mathbb{N}`, $`a \in \mathcal{A}`, and a measurable set $`B \subseteq \mathbb{N} \times \mathbb{R}`,
+$$`
+  P_{\mathcal{A}}\left((N_{t,a}, S_{t, a}) \in B\right)
+  \le \sum_{k < t, \exists r, (k, r) \in B} \nu(a)^{\otimes \mathbb{N}} \left(\sum_{s=0}^{k-1} \omega_{s} \in \{x \mid \exists n, (n, x) \in B\}\right)
+  \: .
+`
+As a consequence, this also holds for any algorithm-environment sequence.
+
+Uses: {uses "AM.history"}[], {uses "sumRewards"}[], {uses "pullCount"}[], {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[].
+:::
+
+:::proof "prob_pullCount_prod_sumRewards_mem_le"
+  Uses: {uses "AM.identDistrib_sum_range_snd"}[], {uses "identDistrib_pullCount_prod_sumRewards"}[], {uses "AM.measurable_hist"}[], {uses "pullCount_basic"}[], {uses "isAlgEnvSeq_arrayMeasure"}[], {uses "AM.measurable_hist"}[], {uses "isAlgEnvSeq_unique"}[]
+:::
+
+
+:::lemma_ "prob_sumRewards_le_sumRewards_le" (parent := "concentrationBandits") (lean := "Bandits.ArrayModel.prob_sumRewards_le_sumRewards_le, Bandits.probReal_sumRewards_le_sumRewards_le")
+In the array model,
+$$`
+  P_{\mathcal{A}}\left( N_{t, a^*} = m_1 \wedge N_{t, a} = m_2 \wedge S_{t, a^*} \le S_{t, a}\right)
+  \le (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m_1-1} \omega_{s, a^*} \le \sum_{s=0}^{m_2-1} \omega_{s, a} \right)
+  \: .
+`
+As a consequence, this also holds for any algorithm-environment sequence.
+
+Uses: {uses "AM.history"}[], {uses "sumRewards"}[], {uses "pullCount"}[], {uses "stationaryEnv"}[], {uses "IsAlgEnvSeq"}[]
+:::
+
+:::proof "prob_sumRewards_le_sumRewards_le"
+  Uses: {uses "identDistrib_pullCount_prod_sumRewards"}[], {uses "AM.measurable_hist"}[], {uses "pullCount_basic"}[], {uses "isAlgEnvSeq_arrayMeasure"}[], {uses "AM.measurable_hist"}[], {uses "isAlgEnvSeq_unique"}[]
+:::
+
+
+
+## Sub-Gaussian rewards
+
+:::lemma_ "probReal_sum_le_sum_streamMeasure" (parent := "concentrationBandits") (lean := "Bandits.probReal_sum_le_sum_streamMeasure")
+Let $`\nu(a)` be a $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] distribution on $`\mathbb{R}` for each arm $`a \in \mathcal{A}`.
+$$`
+  (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m-1} \omega_{s, a^*} \le \sum_{s=0}^{m-1} \omega_{s, a} \right)
+  \le \exp\left( -m \frac{\Delta_a^2}{4 \sigma^2} \right)
+`
+
+Uses: {uses "ionescu-tulcea"}[], {uses "gap"}[]
+:::
+
+:::proof "probReal_sum_le_sum_streamMeasure"
+  Uses: {uses "measure_sum_le_sum_le'"}[]
+:::
+
+
+:::lemma_ "prob_sum_le_sqrt_log" (parent := "concentrationBandits") (lean := "Bandits.prob_sum_le_sqrt_log, Bandits.prob_sum_ge_sqrt_log")
+Let $`\nu(a)` be a $`\sigma^2`-{uses "subGaussian"}[sub-Gaussian] distribution on $`\mathbb{R}` for each arm $`a \in \mathcal{A}`.
+Let $`c \ge 0` be a real number and $`k` a positive natural number.
+Then
+$$`
+  \nu(a)^{\otimes \mathbb{N}} \left( \sum_{s=0}^{k-1} (\omega_{s} - \mu_a) \le - \sqrt{2 c k \sigma^2 \log(n + 1)} \right)
+  \le \frac{1}{(n + 1)^{c}}
+  \: .
+`
+
+The same upper bound holds for the upper tail:
+$$`
+  \nu(a)^{\otimes \mathbb{N}} \left( \sum_{s=0}^{k-1} (\omega_{s} - \mu_a) \ge \sqrt{2 c k \sigma^2 \log(n + 1)} \right)
+  \le \frac{1}{(n + 1)^{c}}
+  \: .
+`
+
+Uses: {uses "ionescu-tulcea"}[]
+:::
+
+:::proof "prob_sum_le_sqrt_log"
+  Uses: {uses "hoeffding"}[].
+:::
diff --git a/verso_blueprint/LMLBlueprint/Chapters/Intro.lean b/verso_blueprint/LMLBlueprint/Chapters/Intro.lean
new file mode 100644
index 00000000..ced3462c
--- /dev/null
+++ b/verso_blueprint/LMLBlueprint/Chapters/Intro.lean
@@ -0,0 +1,36 @@
+import Verso
+import VersoManual
+import VersoBlueprint
+
+open Verso.Genre
+open Verso.Genre.Manual
+open Informal
+
+#doc (Manual) "Introduction" =>
+%%%
+htmlSplit := .never
+%%%
+
+A bandit algorithm sequentially chooses actions and then observes rewards, whose distribution depends on the action chosen.
+The algorithm does not know the distribution of the rewards and sees only a reward from the chosen action at any given time.
+A key part of the interaction is that the algorithm can choose the next action based on all the previous actions and rewards.
+The goal of the algorithm is typically to maximize the cumulative reward over time.
+The researcher studying bandit algorithms is interested in the performance of the algorithm, which is measured by the _regret_ $`R_T` after choosing $`T` actions, that is the difference between the cumulative reward of always playing the best action and the cumulative reward of the algorithm.
+A theoretical guarantee will be of the form $`\mathbb{E}[R_T] \le f(T)` for some function $`f`.
+Here the expectation is taken over the randomness of the algorithm and the rewards.
+In parallel to the theoretical study, the researcher may also be interested in the practical performance of the algorithm, which is usually measured by the average regret over several runs of the algorithm with rewards sampled from standard probability distributions.
+
+From that description, we highlight three key components of research work on bandit algorithms:
+- A bandit algorithm is both a subject of theoretical study and a practical tool, that we should be able to implement and run,
+- the bandit model defines a probability space, on which we want to take expectations, and the theoretical study deals with random variables on that space using tools like concentration inequalities,
+- for the experimental part, we need to be able to sample rewards from a range of probability distributions.
+
+# Notations
+
+$`P(E)` is the probability of event $`E` under the probability distribution $`P`.
+
+$`P[X]` is the expectation of random variable $`X`.
+
+$`P[X \mid Y]` is the conditional expectation of random variable $`X` given random variable $`Y`.
+
+$`P(X \mid Y)` is the conditional distribution of random variable $`X` given random variable $`Y`.
diff --git a/verso_blueprint/LMLBlueprint/References.lean b/verso_blueprint/LMLBlueprint/References.lean
new file mode 100644
index 00000000..61f45e1e
--- /dev/null
+++ b/verso_blueprint/LMLBlueprint/References.lean
@@ -0,0 +1,24 @@
+import VersoManual.Bibliography
+import VersoBlueprint.Cite
+
+open Verso.Genre.Manual
+open Verso.Genre.Manual.Bibliography
+
+@[bib "lattimore2020bandit"]
+def lattimore2020bandit : Verso.Genre.Manual.Bibliography.Citable := .article {
+  title := inlines!"Bandit algorithms"
+  authors := #[inlines!"Tor Lattimore", inlines!"Csaba Szepesvári"]
+  year := 2020
+  journal := inlines!"Cambridge University Press"
+  month := none
+  volume := inlines!"0"
+  number := inlines!"0"
+}
+
+@[bib "marion2025formalization"]
+def marion2025formalization : Verso.Genre.Manual.Bibliography.Citable := .arXiv {
+  title := inlines!"A Formalization of the Ionescu-Tulcea Theorem in Mathlib"
+  authors := #[inlines!"Etienne Marion"]
+  year := 2025
+  id := "2506.18616"
+}
diff --git a/verso_blueprint/LMLBlueprint/TeXPrelude.lean b/verso_blueprint/LMLBlueprint/TeXPrelude.lean
new file mode 100644
index 00000000..92f0bc1e
--- /dev/null
+++ b/verso_blueprint/LMLBlueprint/TeXPrelude.lean
@@ -0,0 +1,8 @@
+import Verso
+import VersoManual
+import VersoBlueprint
+
+open Informal
+
+tex_prelude
+  r#"\providecommand{\ind}{\perp\!\!\!\!\perp}"#
diff --git a/verso_blueprint/Main.lean b/verso_blueprint/Main.lean
new file mode 100644
index 00000000..f9acc76c
--- /dev/null
+++ b/verso_blueprint/Main.lean
@@ -0,0 +1,25 @@
+import VersoManual
+import VersoBlueprint.PreviewManifest
+import LMLBlueprint.Blueprint
+
+open Verso Doc
+open Verso.Genre Manual Verso.Output.Html
+
+
+def extraHead : Array Verso.Output.Html := #[
+  {{<link rel="icon" type="image/x-icon" href="static/favicon.svg"/>}},
+  {{<link rel="stylesheet" href="static/style.css"/>}},
+]
+
+def config : RenderConfig := {
+  extraHead := extraHead,
+  sourceLink := some "https://github.com/LeanMachineLearning/LML",
+  issueLink := some "https://github.com/LeanMachineLearning/LML/issues",
+}
+
+def main (args : List String) : IO UInt32 :=
+  Informal.PreviewManifest.manualMainWithSharedPreviewManifest
+    (%doc LMLBlueprint.Blueprint)
+    args
+    (extensionImpls := by exact extension_impls%)
+    (config := config)
diff --git a/verso_blueprint/lake-manifest.json b/verso_blueprint/lake-manifest.json
new file mode 100644
index 00000000..75b90a4a
--- /dev/null
+++ b/verso_blueprint/lake-manifest.json
@@ -0,0 +1,152 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"type": "path",
+   "scope": "",
+   "name": "LeanMachineLearning",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/ejgallego/verso-blueprint",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c7a5d720d37c919e9b459e5d974415b1dab5c460",
+   "name": "VersoBlueprint",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/verso",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "7ae82ac2ae54ae5dcc9948a701669e9b596e5cae",
+   "name": "verso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/subverso",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "52b9dfbd2658408e37ae6e8b72601ddeaaa25a0c",
+   "name": "subverso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/PatrickMassot/checkdecls.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4",
+   "name": "checkdecls",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.95",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"}],
+ "name": "LMLBlueprint",
+ "lakeDir": ".lake"}
diff --git a/verso_blueprint/lakefile.lean b/verso_blueprint/lakefile.lean
new file mode 100644
index 00000000..b8c56b80
--- /dev/null
+++ b/verso_blueprint/lakefile.lean
@@ -0,0 +1,16 @@
+import Lake
+open Lake DSL
+
+require verso from git "https://github.com/leanprover/verso"@"v4.29.0"
+require VersoBlueprint from git "https://github.com/ejgallego/verso-blueprint"
+require LeanMachineLearning from "../"
+
+package LMLBlueprint where
+  precompileModules := false
+  leanOptions := #[⟨`experimental.module, true⟩]
+
+@[default_target]
+lean_lib LMLBlueprint where
+
+lean_exe «blueprint-gen» where
+  root := `Main
diff --git a/verso_blueprint/lean-toolchain b/verso_blueprint/lean-toolchain
new file mode 100644
index 00000000..14791d72
--- /dev/null
+++ b/verso_blueprint/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.29.0
diff --git a/verso_blueprint/scripts/ci-pages.sh b/verso_blueprint/scripts/ci-pages.sh
new file mode 100644
index 00000000..0d1309e7
--- /dev/null
+++ b/verso_blueprint/scripts/ci-pages.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+
+lake build
+lake exe blueprint-gen --output _out/site
+mkdir -p _out/site/html-multi/static
+cp static_files/* _out/site/html-multi/static
+
+test -f _out/site/html-multi/index.html
+test -f _out/site/html-multi/-verso-data/blueprint-preview-manifest.json
diff --git a/verso_blueprint/static_files/LigaMenlo-Regular.ttf b/verso_blueprint/static_files/LigaMenlo-Regular.ttf
new file mode 100644
index 00000000..b1ca21e2
Binary files /dev/null and b/verso_blueprint/static_files/LigaMenlo-Regular.ttf differ
diff --git a/verso_blueprint/static_files/favicon.svg b/verso_blueprint/static_files/favicon.svg
new file mode 100644
index 00000000..ea497ae3
--- /dev/null
+++ b/verso_blueprint/static_files/favicon.svg
@@ -0,0 +1 @@
+<svg xmlns="http://www.w3.org/2000/svg" version="1.1" xmlns:xlink="http://www.w3.org/1999/xlink" width="1000" height="1000"><metadata><rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:dc="http://purl.org/dc/elements/1.1/"><rdf:Description><dc:creator>RealFaviconGenerator</dc:creator><dc:source>https://realfavicongenerator.net</dc:source></rdf:Description></rdf:RDF></metadata><g clip-path="url(#SvgjsClipPath1001)"><rect width="1000" height="1000" fill="#ffffff"></rect><g transform="matrix(3.5,0,0,3.5,150,150)"><svg xmlns="http://www.w3.org/2000/svg" version="1.1" xmlns:xlink="http://www.w3.org/1999/xlink" viewBox="0 0 200 200" width="200" height="200"><rect width="200" height="200" fill="url('#gradient')"></rect><defs><linearGradient id="gradient" gradientTransform="rotate(45 0.5 0.5)"><stop offset="0%" stop-color="#ffffff"></stop><stop offset="100%" stop-color="#ffffff"></stop></linearGradient><clipPath id="SvgjsClipPath1001"><rect width="1000" height="1000" x="0" y="0" rx="350" ry="350"></rect></clipPath></defs><g><g fill="#c52727" transform="matrix(4.766485647788984,0,0,4.766485647788984,4.88372315123064,133.88908845865976)" stroke="#f71412" stroke-width="0.2"><path d="M4.50-14.22L4.50-2.64L10.47-2.64L10.47 0L1.07 0L1.07-14.22L4.50-14.22ZM11.91-14.22L16.42-14.22L19.59-4.33L22.75-14.22L27.27-14.22L27.27 0L23.83 0L23.83-3.32L24.16-10.12L20.72 0L18.46 0L15.01-10.13L15.34-3.32L15.34 0L11.91 0L11.91-14.22ZM32.87-14.22L32.87-2.64L38.84-2.64L38.84 0L29.44 0L29.44-14.22L32.87-14.22Z"></path></g></g></svg></g></g></svg>
\ No newline at end of file
diff --git a/verso_blueprint/static_files/scripts.js b/verso_blueprint/static_files/scripts.js
new file mode 100644
index 00000000..64c37a8d
--- /dev/null
+++ b/verso_blueprint/static_files/scripts.js
@@ -0,0 +1,23 @@
+window.addEventListener('load', function () {
+  document.querySelectorAll('.has-info, .warning').forEach(function (el) {
+    el.classList.remove('has-info', 'warning');
+
+    el.querySelectorAll('span.hover-container').forEach(function (hoverSpan) {
+      hoverSpan.remove();
+    });
+  });
+
+  document.querySelectorAll('p').forEach(function (p) {
+    if (p.querySelector('img')) {
+      p.setAttribute('align', 'center');
+    }
+  });
+
+  document.querySelectorAll('a[href]').forEach(function (link) {
+    const url = new URL(link.href, window.location.href);
+    if (url.hostname !== window.location.hostname) {
+      link.setAttribute('target', '_blank');
+      link.setAttribute('rel', 'noopener noreferrer');
+    }
+  });
+});
diff --git a/verso_blueprint/static_files/style.css b/verso_blueprint/static_files/style.css
new file mode 100644
index 00000000..b329089b
--- /dev/null
+++ b/verso_blueprint/static_files/style.css
@@ -0,0 +1,57 @@
+:root {
+  --accent: #d65d5d;
+  --accent-compl: #e8a0a0;
+  --background: #fef9f9;
+  --background-lighter: #fefcfc;
+}
+
+@font-face {
+  font-family: "LigaMenlo";
+  src: url("LigaMenlo-Regular.ttf");
+}
+
+body {
+  text-align: justify;
+  background-color: var(--background);
+}
+
+p a:visited,
+p a:link {
+  text-decoration: none;
+  color: var(--accent);
+}
+
+p a:hover {
+  text-decoration: underline;
+}
+
+.toc {
+  background-color: var(--background-lighter);
+}
+
+.keyword {
+  color: var(--accent) !important;
+}
+
+.hl.lean .token.binding-hl,
+.hl.lean .literal.string:hover,
+.hl.lean .token.typed:hover {
+  background-color: var(--accent-compl) !important;
+  border-radius: 2px !important;
+}
+
+.block {
+  background-color: var(--background-lighter);
+  padding: 0.4em;
+  border: 2px solid black;
+  border-radius: 0.5em;
+}
+
+.tippy-box[data-theme~='lean'] {
+  background-color: var(--background-lighter) !important;
+}
+
+code {
+  font-family: "LigaMenlo";
+  font-variant-ligatures: normal;
+}