Lean Machine Learning

4. Defining an Algorithm🔗

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.

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

🔗def
Learning.Round.{u_5, u_6, u_7} (𝓞 : Type u_5) (𝓐 : Type u_6)
  (𝓨 : Type u_7) : Type (max u_5 u_7 u_6)
Learning.Round.{u_5, u_6, u_7}
  (𝓞 : Type u_5) (𝓐 : Type u_6)
  (𝓨 : Type u_7) : Type (max u_5 u_7 u_6)

One round of interaction: an observation, then an action, then a feedback.

🔗def
Learning.Hist.{u_5, u_6, u_7} (𝓞 : Type u_5) (𝓐 : Type u_6)
  (𝓨 : Type u_7) (n : ℕ) : Type (max (max u_7 u_6) u_5)
Learning.Hist.{u_5, u_6, u_7}
  (𝓞 : Type u_5) (𝓐 : Type u_6)
  (𝓨 : Type u_7) (n : ℕ) :
  Type (max (max u_7 u_6) u_5)

History of n complete rounds; n = 0 is the empty history.

The Algorithm structure is defined as follows:

🔗structure
Learning.Algorithm.{u_5, u_6, u_7} (𝓞 : Type u_5) (𝓐 : Type u_6)
  (𝓨 : Type u_7) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] : Type (max (max u_5 u_6) u_7)
Learning.Algorithm.{u_5, u_6, u_7}
  (𝓞 : Type u_5) (𝓐 : Type u_6)
  (𝓨 : Type u_7) [MeasurableSpace 𝓞]
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] :
  Type (max (max u_5 u_6) u_7)

A stochastic, sequential algorithm. At each round, it sees an observation in 𝓞, then takes an action in 𝓐, and finally receives feedback in 𝓨. The action is a random function of the past rounds and the current observation.

Constructor

Learning.Algorithm.mk.{u_5, u_6, u_7}

Fields

policy : (n : ℕ) → ProbabilityTheory.Kernel (Hist 𝓞 𝓐 𝓨 n × 𝓞) 𝓐

Law of the action of round n given the past rounds and the current observation.

isMarkovKernel_policy : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (self.policy n)

The policy is a Markov kernel.

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

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

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

🔗def
Learning.Algorithm.deterministic.{u_1, u_2, u_3} {𝓞 : Type u_1}
  {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐)
  (h_next : ∀ (n : ℕ), Measurable (nextA n)) : Algorithm 𝓞 𝓐 𝓨
Learning.Algorithm.deterministic.{u_1,
    u_2, u_3}
  {𝓞 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐)
  (h_next :
    ∀ (n : ℕ), Measurable (nextA n)) :
  Algorithm 𝓞 𝓐 𝓨

A deterministic algorithm, which chooses the action given by the function nextA. The initial action is fun o ↦ nextA 0 (default, o).

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.

🔗structure
Learning.Environment.{u_5, u_6, u_7} (𝓞 : Type u_5) (𝓐 : Type u_6)
  (𝓨 : Type u_7) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] : Type (max (max u_5 u_6) u_7)
Learning.Environment.{u_5, u_6, u_7}
  (𝓞 : Type u_5) (𝓐 : Type u_6)
  (𝓨 : Type u_7) [MeasurableSpace 𝓞]
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] :
  Type (max (max u_5 u_6) u_7)

A stochastic environment. At each round, an observation is drawn prior to the algorithm taking an action. Then the environment provides feedback based on the observation and the action.

Constructor

Learning.Environment.mk.{u_5, u_6, u_7}

Fields

obs : (n : ℕ) → ProbabilityTheory.Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞

Law of the observation of round n given the past rounds.

feedback : (n : ℕ) → ProbabilityTheory.Kernel ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐) 𝓨

Law of the feedback of round n given the past rounds, the observation and the action.

isMarkovKernel_obs : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (self.obs n)

The observation kernel is a Markov kernel.

isMarkovKernel_feedback : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (self.feedback n)

The feedback kernel is a Markov kernel.

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.obsZero. The distribution of the first feedback given the first observation and action is feedback 0 applied to the empty history; it is called Environment.feedbackZero.

In many applications neither the observation nor the feedback depends on the prior history: the observation at time n has a fixed law, and the feedback depends only on the current observation and action. We provide an Environment.oblivious definition that builds an environment for those cases from a sequence of observation laws and a sequence of feedback kernels.

🔗def
Learning.Environment.oblivious.{u_1, u_2, u_3} {𝓞 : Type u_1}
  {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (μ : ℕ → MeasureTheory.Measure 𝓞)
  [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)]
  (ν : ℕ → ProbabilityTheory.Kernel (𝓞 × 𝓐) 𝓨)
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (ν n)] :
  Environment 𝓞 𝓐 𝓨
Learning.Environment.oblivious.{u_1, u_2,
    u_3}
  {𝓞 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (μ : ℕ → MeasureTheory.Measure 𝓞)
  [∀ (n : ℕ),
      MeasureTheory.IsProbabilityMeasure
        (μ n)]
  (ν :
    ℕ →
      ProbabilityTheory.Kernel (𝓞 × 𝓐) 𝓨)
  [∀ (n : ℕ),
      ProbabilityTheory.IsMarkovKernel
        (ν n)] :
  Environment 𝓞 𝓐 𝓨

The oblivious environment in which the observation at time n has law μ n and the feedback at time n is drawn from ν n applied to the observation and the action at time n, whatever the past history.

If furthermore those sequences do not change with time, we can use the Environment.stationary definition to build the environment.

🔗def
Learning.Environment.stationary.{u_1, u_2, u_3} {𝓞 : Type u_1}
  {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (μ : MeasureTheory.Measure 𝓞) [MeasureTheory.IsProbabilityMeasure μ]
  (ν : ProbabilityTheory.Kernel (𝓞 × 𝓐) 𝓨)
  [ProbabilityTheory.IsMarkovKernel ν] : Environment 𝓞 𝓐 𝓨
Learning.Environment.stationary.{u_1, u_2,
    u_3}
  {𝓞 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (μ : MeasureTheory.Measure 𝓞)
  [MeasureTheory.IsProbabilityMeasure μ]
  (ν : ProbabilityTheory.Kernel (𝓞 × 𝓐) 𝓨)
  [ProbabilityTheory.IsMarkovKernel ν] :
  Environment 𝓞 𝓐 𝓨

The stationary environment in which the observations have law μ and the feedback is drawn from ν applied to the observation and the action, whatever the past history.

When there is no observation (𝓞 = Unit) and the feedback depends only on the current action (and possibly on the time), we get bandit environments. Environment.banditSeq builds such an environment from a sequence of kernels ν : ℕ → Kernel 𝓐 𝓨, and Environment.bandit from a single kernel ν : Kernel 𝓐 𝓨 used at every time.

🔗def
Learning.Environment.bandit.{u_2, u_3} {𝓐 : Type u_2} {𝓨 : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (ν : ProbabilityTheory.Kernel 𝓐 𝓨)
  [ProbabilityTheory.IsMarkovKernel ν] : Environment Unit 𝓐 𝓨
Learning.Environment.bandit.{u_2, u_3}
  {𝓐 : Type u_2} {𝓨 : Type u_3}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (ν : ProbabilityTheory.Kernel 𝓐 𝓨)
  [ProbabilityTheory.IsMarkovKernel ν] :
  Environment Unit 𝓐 𝓨

The stationary environment without observations in which the feedback is drawn from ν applied to the action, whatever the past history: a stochastic bandit.

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

🔗structure
Learning.IsAlgEnvSeq.{u_1, u_2, u_3, u_4} {𝓞 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  {mΩ : MeasurableSpace Ω} (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐)
  (Y : ℕ → Ω → 𝓨) (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨)
  (P : MeasureTheory.Measure Ω) : Prop
Learning.IsAlgEnvSeq.{u_1, u_2, u_3, u_4}
  {𝓞 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {Ω : Type u_4}
  {m𝓞 : MeasurableSpace 𝓞}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  {mΩ : MeasurableSpace Ω} (O : ℕ → Ω → 𝓞)
  (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨)
  (alg : Algorithm 𝓞 𝓐 𝓨)
  (env : Environment 𝓞 𝓐 𝓨)
  (P : MeasureTheory.Measure Ω) : Prop

An algorithm-environment sequence: a sequence of observations, actions and feedbacks generated by an algorithm interacting with an environment.

Constructor

Learning.IsAlgEnvSeq.mk.{u_1, u_2, u_3, u_4}

Fields

measurable_obs : ∀ (n : ℕ), Measurable (O n)

The observation sequence is measurable.

measurable_action : ∀ (n : ℕ), Measurable (A n)

The action sequence is measurable.

measurable_feedback : ∀ (n : ℕ), Measurable (Y n)

The feedback sequence is measurable.

hasCondDistrib_obs : ∀ (n : ℕ), ProbabilityTheory.HasCondDistrib (O n) (history O A Y n) (env.obs n) P

The observation at time n has the correct conditional distribution given the history.

hasCondDistrib_action : ∀ (n : ℕ), ProbabilityTheory.HasCondDistrib (A n) (fun ω ↦ (history O A Y n ω, O n ω)) (alg.policy n) P

The action at time n has the correct conditional distribution given the history and the observation at time n.

hasCondDistrib_feedback : ∀ (n : ℕ), ProbabilityTheory.HasCondDistrib (Y n) (fun ω ↦ ((history O A Y n ω, O n ω), A n ω)) (env.feedback n) P

The feedback at time n has the correct conditional distribution given the history, the observation and the action at time n.

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. The conditional distributions are expressed with HasCondDistrib: HasCondDistrib Y X κ P states that the joint law of (X, Y) under P is the law of X composed with the kernel κ. This definition makes no assumption on the measurable spaces. Some results about algorithm-environment sequences, for example those using Mathlib's conditional distribution condDistrib or conditional independence, require the spaces to be nonempty standard Borel spaces. All spaces of interest in machine learning are standard Borel, so this is not a restriction in practice.

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.

🔗theorem
Learning.isAlgEnvSeq_unique.{u_1, u_2, u_3, u_5, u_6} {𝓞 : Type u_1}
  {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_5}
  {Ω' : Type u_6} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
  {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨}
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {P' : MeasureTheory.Measure Ω'}
  [MeasureTheory.IsProbabilityMeasure P'] {O₁ : ℕ → Ω → 𝓞}
  {A₁ : ℕ → Ω → 𝓐} {Y₁ : ℕ → Ω → 𝓨} {O₂ : ℕ → Ω' → 𝓞} {A₂ : ℕ → Ω' → 𝓐}
  {Y₂ : ℕ → Ω' → 𝓨} (h1 : IsAlgEnvSeq O₁ A₁ Y₁ alg env P)
  (h2 : IsAlgEnvSeq O₂ A₂ Y₂ alg env P') :
  MeasureTheory.Measure.map (trajectory O₁ A₁ Y₁) P =
    MeasureTheory.Measure.map (trajectory O₂ A₂ Y₂) P'
Learning.isAlgEnvSeq_unique.{u_1, u_2,
    u_3, u_5, u_6}
  {𝓞 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_5}
  {Ω' : Type u_6} {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'}
  {alg : Algorithm 𝓞 𝓐 𝓨}
  {env : Environment 𝓞 𝓐 𝓨}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {P' : MeasureTheory.Measure Ω'}
  [MeasureTheory.IsProbabilityMeasure P']
  {O₁ : ℕ → Ω → 𝓞} {A₁ : ℕ → Ω → 𝓐}
  {Y₁ : ℕ → Ω → 𝓨} {O₂ : ℕ → Ω' → 𝓞}
  {A₂ : ℕ → Ω' → 𝓐} {Y₂ : ℕ → Ω' → 𝓨}
  (h1 : IsAlgEnvSeq O₁ A₁ Y₁ alg env P)
  (h2 : IsAlgEnvSeq O₂ A₂ Y₂ alg env P') :
  MeasureTheory.Measure.map
      (trajectory O₁ A₁ Y₁) P =
    MeasureTheory.Measure.map
      (trajectory O₂ A₂ Y₂) P'

The law of the sequence of rounds generated by an algorithm-environment pair is unique: it does not depend on the probability space used.

4.3. 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 Environment.bandit ν for some kernel ν : Kernel (Fin K) ℝ.

4.3.1. 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 Algorithm.deterministic to build the algorithm. We also need to prove that the next action function is measurable, which is done by the measurable_nextArm lemma. Note that we are careful to use a measurable version of the argmax function, argmax.

🔗def
Bandits.UCB.ucbWidth' {K : ℕ} (c : ℝ) (n : ℕ)
  (h : Hist Unit (Fin K) ℝ n) (a : Fin K) : ℝ
Bandits.UCB.ucbWidth' {K : ℕ} (c : ℝ)
  (n : ℕ) (h : Hist Unit (Fin K) ℝ n)
  (a : Fin K) : ℝ

The exploration bonus of the UCB algorithm, which corresponds to the width of a confidence interval.

🔗def
Bandits.UCB.nextArm (K : ℕ) [NeZero K] (c : ℝ) (n : ℕ)
  (h : Hist Unit (Fin K) ℝ n) : Fin K
Bandits.UCB.nextArm (K : ℕ) [NeZero K]
  (c : ℝ) (n : ℕ)
  (h : Hist Unit (Fin K) ℝ n) : Fin K

Arm pulled by the UCB algorithm at time n, as a function of the history before n.

🔗theorem
Bandits.UCB.measurable_nextArm {K : ℕ} [NeZero K] (c : ℝ) (n : ℕ) :
  Measurable (Bandits.UCB.nextArm K c n)
Bandits.UCB.measurable_nextArm {K : ℕ}
  [NeZero K] (c : ℝ) (n : ℕ) :
  Measurable (Bandits.UCB.nextArm K c n)

The next-arm function of UCB is measurable.

🔗def
Bandits.ucbAlgorithm (K : ℕ) [NeZero K] (c : ℝ) :
  Algorithm Unit (Fin K) ℝ
Bandits.ucbAlgorithm (K : ℕ) [NeZero K]
  (c : ℝ) : Algorithm Unit (Fin K) ℝ

The UCB algorithm.

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

4.3.2. 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 sum of the mean rewards that the algorithm would have obtained if it had always played the best action, and the sum of the mean rewards of the actions played.

🔗def
Bandits.regret.{u_1, u_2} {𝓐 : Type u_1} {Ω : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} (ν : ProbabilityTheory.Kernel 𝓐 ℝ)
  (A : ℕ → Ω → 𝓐) (t : ℕ) (ω : Ω) : ℝ
Bandits.regret.{u_1, u_2} {𝓐 : Type u_1}
  {Ω : Type u_2} {m𝓐 : MeasurableSpace 𝓐}
  (ν : ProbabilityTheory.Kernel 𝓐 ℝ)
  (A : ℕ → Ω → 𝓐) (t : ℕ) (ω : Ω) : ℝ

Regret of a sequence of pulls A : ℕ → Ω → 𝓐 at time t for the reward kernel ν : Kernel 𝓐 ℝ: difference between t times the highest mean and the sum of the means of the actions pulled before time t.

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.

🔗theorem
Bandits.UCB.regret_le.{u_1} {K : ℕ} [NeZero K] {c : ℝ}
  {ν : ProbabilityTheory.Kernel (Fin K) ℝ}
  [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_1}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → Unit}
  {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {σ2 : NNReal}
  (h :
    IsAlgEnvSeq O A R (Bandits.ucbAlgorithm K c) (Environment.bandit ν)
      P)
  (hν :
    ∀ (a : Fin K),
      ProbabilityTheory.HasSubgaussianMGF
        (fun x ↦ x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a))
  (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (n : ℕ) :
  ∫ (x : Ω), Bandits.regret ν A n x ∂P ≤
    ∑ a,
      (8 * c * Real.log (↑n + 1) / Bandits.gap ν a +
        Bandits.gap ν a * (2 + 2 * Bandits.UCB.constSum (c / ↑σ2) n))
Bandits.UCB.regret_le.{u_1} {K : ℕ}
  [NeZero K] {c : ℝ}
  {ν : ProbabilityTheory.Kernel (Fin K) ℝ}
  [ProbabilityTheory.IsMarkovKernel ν]
  {Ω : Type u_1} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {O : ℕ → Ω → Unit} {A : ℕ → Ω → Fin K}
  {R : ℕ → Ω → ℝ} {σ2 : NNReal}
  (h :
    IsAlgEnvSeq O A R
      (Bandits.ucbAlgorithm K c)
      (Environment.bandit ν) P)
  (hν :
    ∀ (a : Fin K),
      ProbabilityTheory.HasSubgaussianMGF
        (fun x ↦ x - ∫ (x : ℝ), id x ∂ν a)
        σ2 (ν a))
  (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (n : ℕ) :
  ∫ (x : Ω), Bandits.regret ν A n x ∂P ≤
    ∑ a,
      (8 * c * Real.log (↑n + 1) /
          Bandits.gap ν a +
        Bandits.gap ν a *
          (2 +
            2 *
              Bandits.UCB.constSum
                (c / ↑σ2) n))

Regret bound for the UCB algorithm with exploration parameter c, for σ2-sub-Gaussian rewards.

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 (σ2 is a nonnegative real number, so σ2 ≠ 0 means that it is positive).

  • n is the time horizon.

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

4.4. Building vs analyzing algorithms🔗

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

🔗def
Learning.empMean'.{u_1, u_2} {𝓞 : Type u_1} {𝓐 : Type u_2}
  [DecidableEq 𝓐] (n : ℕ) (h : Hist 𝓞 𝓐 ℝ n) (a : 𝓐) : ℝ
Learning.empMean'.{u_1, u_2}
  {𝓞 : Type u_1} {𝓐 : Type u_2}
  [DecidableEq 𝓐] (n : ℕ)
  (h : Hist 𝓞 𝓐 ℝ n) (a : 𝓐) : ℝ

Empirical mean of arm a in the history before time n.

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

🔗def
Learning.empMean.{u_2, u_4} {𝓐 : Type u_2} {Ω : Type u_4}
  [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (R : ℕ → Ω → ℝ) (a : 𝓐) (t : ℕ)
  (ω : Ω) : ℝ
Learning.empMean.{u_2, u_4} {𝓐 : Type u_2}
  {Ω : Type u_4} [DecidableEq 𝓐]
  (A : ℕ → Ω → 𝓐) (R : ℕ → Ω → ℝ) (a : 𝓐)
  (t : ℕ) (ω : Ω) : ℝ

Empirical mean reward obtained when pulling action a up to time t (exclusive).

empMean A R a is a stochastic process with type ℕ → Ω → ℝ that gives the empirical mean of action a at each time. The two definitions agree along any sequence: empMean A R a n ω = empMean' n (history O A R n ω) a (lemma empMean_eq_empMean'), which is how properties of the algorithm, stated with empMean', are transferred to the analysis, stated with empMean.