DefiningAlgorithm.lean

/-
Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
module

public import VersoManual
public import LeanMachineLearning
-- `import all` is needed to load the docstrings for the `{docstring}` blocks below.
import all LeanMachineLearning.Online.Bandit.Algorithms.Regret.UCB
import all LeanMachineLearning.Online.Bandit.Algorithms.UCB
import all LeanMachineLearning.Online.Bandit.Regret
import all LeanMachineLearning.SequentialLearning.Algorithm
import all LeanMachineLearning.SequentialLearning.Deterministic
import all LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
import all LeanMachineLearning.SequentialLearning.StationaryEnv
import all LeanMachineLearning.SequentialLearning.SumRewards

set_option linter.style.header false
set_option linter.style.setOption false
set_option linter.hashCommand false
set_option linter.style.longLine false
set_option pp.rawOnError true
set_option verso.code.warnLineLength 100

set_option verso.docstring.allowMissing true

@[expose] public section

open Verso.Genre Manual Verso.Genre.Manual.InlineLean Verso.Code.External
  Learning

#doc (Manual) "Defining an Algorithm" =>
%%%
htmlSplit := .never
%%%

This tutorial explains the structures used in the Lean Machine Learning library to describe algorithms, the environment they interact with, and how to state theorems about their interaction.
We then illustrate them with the UCB bandit algorithm.

# Algorithm and environment

In LML, we prove theorems about the interaction of an algorithm with an environment.
Each round of the interaction consists of three stages: the environment draws an observation (e.g., the context in a contextual bandit), the algorithm takes an action based on that observation, and the environment responds with feedback (e.g., rewards for the bandit case, the gradient of a function in optimization problems).
In general, observation, action and feedback can depend on the entire history up to the current time and can be randomized.
One round is recorded by the `Round` abbreviation and a history of `n` rounds by the `Hist` abbreviation.

{docstring Round}

{docstring Hist}

The `Algorithm` structure is defined as follows:

{docstring Algorithm}

This structure refers to three types, the type of observations `𝓞`, the type of actions `𝓐` and the type of feedback `𝓨`.
All three are measurable spaces, since we consider stochastic algorithms and environments.
Before time `n`, there is a history of `n` complete rounds `Hist 𝓞 𝓐 𝓨 n = Fin n → 𝓞 × 𝓐 × 𝓨` (the observation-action-feedback triples at times `0, ..., n - 1`; the processes are 0-indexed).
The `policy` field contains for each time `n` a kernel from that history together with the observation at time `n` to the action space.
That is, it maps every possible history and current observation to a random action at time `n` (and that map is measurable).
The `isMarkovKernel_policy` field records that the measure describing the action is a probability measure (and it is in square brackets to tell Lean to infer it automatically whenever possible).
At time `0` the history is empty: `Hist 𝓞 𝓐 𝓨 0` has a unique element, and the distribution of the first action given the first observation is `policy 0` applied to that element.
That kernel is called `Algorithm.p0`.

Many settings have no observations at all: the algorithm sees only the past rounds. Those are described by taking `𝓞 = Unit`, and we write `noObs Ω` for the corresponding (constant) observation process.

If the algorithms actions are not random, we can use the `detAlgorithm` definition to build an algorithm from the data of a measurable function for the action at each time, as a function of the history before that time and of the current observation.
The first action is the value of that function at time `0` on the empty history.

{docstring detAlgorithm}

We can see here that we did not need to prove that the kernels are `IsMarkovKernel`.
Lean knows that deterministic kernels are Markov.

The `Environment` structure is the mirror of the `Algorithm` structure, with a kernel for the observation and a kernel for the feedback instead of the actions.

{docstring Environment}

`obs n` gives the distribution of the observation at time `n` given the history before `n`.
`feedback n` gives the distribution of the feedback at time `n` given the history before `n`, the observation and the action at time `n`.
The distribution of the first observation is `obs 0` applied to the empty history; it is called `Environment.obs0`.
The distribution of the first feedback given the first observation and action is `feedback 0` applied to the empty history; it is called `Environment.ν0`.

In many applications there is no observation and the feedback depends only on the last action, not on the prior history.
We provide an `obliviousEnv` definition that builds an environment for those cases.

{docstring obliviousEnv}

`(ν n).prodMkLeft _` is the kernel `ν n` seen as a `Kernel ((Hist Unit 𝓐 𝓨 n × Unit) × 𝓐) 𝓨` by ignoring the history and the observation.

If furthermore the feedback kernel does not change with time, we can use the `stationaryEnv` definition to build the environment.

{docstring stationaryEnv}


# Sequences of actions and feedback, probability space

Once algorithm and environment are defined, we can introduce sequences of actions and feedback and assume that they are generated by the interaction of the algorithm with the environment.
This is done by the `IsAlgEnvSeq` structure.

{docstring IsAlgEnvSeq}

This structure takes as input three sequences of random variables (three stochastic processes), `O`, `A` and `Y`, which represent the observations, actions and feedback generated by the interaction of the algorithm with the environment.
It states that those sequences are measurable and that they have the correct conditional distributions given by the algorithm and environment.
The measurable space `Ω` and the measure `P` are not imposed: they can be chosen as we want, as long as the conditions of `IsAlgEnvSeq` are satisfied.
This definition requires `𝓐` and `𝓨` to be nonempty standard Borel spaces, because Mathlib's theory about conditional distributions requires those assumptions.
All spaces of interest in machine learning are standard Borel, so this is not a restriction.

Given any algorithm and environment, there always exists a sequence of actions and feedback that satisfies `IsAlgEnvSeq` by the Ionescu-Tulcea theorem.
However other constructions of such sequences are possible, and it is easier to work with generic sequences satisfying `IsAlgEnvSeq` than with a specific construction.
Which sequence we choose does not matter for the results we prove, since all such sequences are equal in distribution, as stated by the following theorem.

{docstring isAlgEnvSeq_unique}


# Example: the UCB algorithm and a stochastic bandit environment

We now illustrate the use of `Algorithm`, `Environment`, and `IsAlgEnvSeq` by defining the UCB bandit algorithm, a bandit environment, and stating a theorem about the regret of UCB in that environment.

In a stochastic bandit, an algorithm chooses at each time an action from a finite set (here `Fin K`, the type of natural numbers less than `K`) and receives a reward drawn from a distribution that depends only on the action, not on the prior history.

The environment is thus simply `stationaryEnv ν` for some kernel `ν : Kernel (Fin K) ℝ`.

## Algorithm

The UCB algorithm chooses at time `n` the action that maximizes the sum of the empirical mean reward and an exploration bonus.
It starts by choosing each action once and then chooses $`\arg\max_a (\hat{\mu}_{n,a} + \sqrt{\frac{2c \log (n + 1)}{N_{n,a}}})`, in which $`\hat{\mu}_{n,a}` is the empirical mean reward of action `a` before time `n` (`empMean'` in the code), $`N_{n,a}` is the number of times action `a` has been chosen before time `n` (`pullCount'` in the code), and `c` is a parameter of the algorithm.

To define the algorithm, we first define the exploration bonus and the next action function, and then we use `detAlgorithm` to build the algorithm.
We also need to prove that the next action function is measurable, which is done by the `measurable_nextArm` lemma.
Note that we are careful to use a measurable version of the argmax function, `argmax`.

{docstring Bandits.UCB.ucbWidth'}

{docstring Bandits.UCB.nextArm}

{docstring Bandits.UCB.measurable_nextArm}

{docstring Bandits.ucbAlgorithm}

The last line builds the algorithm using `detAlgorithm` and the function `UCB.nextArm`.
Its measurability is proved by the `fun_prop` tactic, which proves measurability of functions by using lemmas tagged with `@[fun_prop]`.
The first action of the algorithm is `UCB.nextArm K c 0` applied to the empty history, which is 0 as an element of `Fin K`.

## A theorem about UCB

We can now state a theorem about the regret of UCB in a stochastic bandit environment (which we won't prove here).
Let's first define the regret, which for stochastic bandits is the difference between the mean rewar that the algorithm would have obtained if it played always the best action, and the sum of mean rewards of the actions played.

{docstring Bandits.regret}

The quantity `(ν a)[id]` is the mean reward of action `a` in the environment defined by `ν`.

We can now state the regret bound for UCB.

{docstring Bandits.UCB.regret_le}

The arguments of the theorem are the following:
- `h` states that the sequence of actions and rewards we are considering is generated by the interaction of UCB with parameter `c * σ2` with the stationary environment defined by `ν`.
- `hν` states that the reward distribution of each arm is subgaussian with variance proxy `σ2`.
- `hσ2` and `hc` state that the parameters `σ2` and `c` are positive.
- `n` is the time horizon.

The theorem gives an upper bound on the expected regret of UCB at time `n`.



# Building vs analyzing algorithms

When building an algorithm, we describe it with functions from the history and the current observation `(Hist 𝓞 𝓐 R n × 𝓞)` to the action space `𝓐`.
Thus, to construct UCB, we used the following empirical mean function.

{docstring empMean'}


When analyzing an algorithm, we work with sequences of actions and rewards `A : ℕ → Ω → 𝓐` and `R' : ℕ → Ω → R` that satisfy `IsAlgEnvSeq`.
For the analysis, the empirical mean is defined as a stochastic process on the same probability space `Ω`.

{docstring empMean}

`empMean A R' a` is a stochastic process with type `ℕ → Ω → ℝ` that gives the empirical mean of action `a` at each time.