`Bandits.TS.integral_regret_le`🔗

Theorem

If Thompson sampling has the correct prior over environments and every environment has K actions, each of which has a corresponding reward between l and u that is sub-Gaussian with variance proxy σ2 after its mean is subtracted, then the Bayesian regret at time n is at most (2 * K + 1) * (u - l) + 8 * √(σ2 * K * n * Real.log n).

Types

Ω : Type u_1MeasurableSpace ΩA measurable space is a space equipped with a σ-algebra.
𝓔 : Type u_2MeasurableSpace 𝓔StandardBorelSpace 𝓔A standard Borel space is a measurable space arising as the Borel sets of some Polish topology.Nonempty 𝓔

Given

K : ℕNonempty (Fin K)
l : ℝ
u : ℝ
σ2 : ℝ
Q : MeasureTheory.Measure 𝓔A measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.MeasureTheory.IsProbabilityMeasure QA measure μ is called a probability measure if μ univ = 1.
κ : ProbabilityTheory.Kernel (𝓔 × Fin K) ℝA kernel from a measurable space α to another measurable space β is a measurable function κ : α → Measure β.ProbabilityTheory.IsMarkovKernel κA kernel is a Markov kernel if every measure in its image is a probability measure.
E : Ω → 𝓔
A : ℕ → Ω → Fin K
R : ℕ → Ω → ℝ
P : MeasureTheory.Measure ΩMeasureTheory.IsProbabilityMeasure P
n : ℕ

Assuming

hK : 0 < K
h : Learning.IsBayesAlgEnvSeq Q κ (tsAlgorithm hK Q κ) E A R PIsBayesAlgEnvSeq Q κ alg E A Y P states that there is a measure P : Measure Ω such that the parameter E : Ω → 𝓔 has law Q and that the sequences of actions A : ℕ → Ω → 𝓐 and feedbacks Y : ℕ…
hlu : l ≤ u
hm : ∀ (e : 𝓔) (a : Fin K), ∫ (x : ℝ), id x ∂κ (e, a) ∈ Set.Icc l u
hσ2 : 0 < σ2
hs : ∀ (e : 𝓔) (a : Fin K), ProbabilityTheory.HasSubgaussianMGF (fun x => x - ∫ (x : ℝ), id x ∂κ (e, a)) ⟨σ2, ⋯⟩ (κ (e, a))A random variable X has a sub-Gaussian moment-generating function with parameter c with respect to a measure μ if for all t : ℝ, exp (t * X) is μ-integrable and the moment-generating funct…

Then

∫ (x : Ω), Learning.IsBayesAlgEnvSeq.regret κ E A n x ∂P ≤ (2 * ↑K + 1) * (u - l) + 8 * √(σ2 * ↑K * ↑n * Real.log ↑n)

MeasurableSpace : Type u_6 → Type u_6

A measurable space is a space equipped with a σ-algebra.

StandardBorelSpace : (α : Type u_1) → [MeasurableSpace α] → Prop

A standard Borel space is a measurable space arising as the Borel sets of some Polish topology.
This is useful in situations where a space has no natural topology or
the natural topology in a space is non-Polish.

To endow a standard Borel space `α` with a compatible Polish topology, use
`letI := upgradeStandardBorel α`. One can then use `eq_borel_upgradeStandardBorel α` to
rewrite the `MeasurableSpace α` instance to `borel α t`, where `t` is the new topology.

Nonempty : Sort u → Prop

`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.

Fin : ℕ → Type

Natural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.

Nat : Type

The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

Real : Type

The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.

MeasureTheory.IsProbabilityMeasure : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop

A measure `μ` is called a probability measure if `μ univ = 1`.

MeasureTheory.Measure : (α : Type u_5) → [MeasurableSpace α] → Type u_5

A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.

ProbabilityTheory.IsMarkovKernel : {α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → ProbabilityTheory.Kernel α β → Prop

A kernel is a Markov kernel if every measure in its image is a probability measure.

ProbabilityTheory.Kernel : (α : Type u_1) → (β : Type u_2) → [MeasurableSpace α] → [MeasurableSpace β] → Type (max u_1 u_2)

A kernel from a measurable space `α` to another measurable space `β` is a measurable function
`κ : α → Measure β`. The measurable space structure on `MeasureTheory.Measure β` is given by
`MeasureTheory.Measure.instMeasurableSpace`. A map `κ : α → MeasureTheory.Measure β` is measurable
iff `∀ s : Set β, MeasurableSet s → Measurable (fun a ↦ κ a s)`.

Prod : Type u → Type v → Type (max u v)

The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.

LT.lt : {α : Type u} → [self : LT α] → α → α → Prop

The less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`.

Learning.IsBayesAlgEnvSeq : {𝓔 : Type u_1} →
  {𝓐 : Type u_2} →
    {𝓨 : Type u_3} →
      {Ω : Type u_4} →
        [inst : MeasurableSpace 𝓔] →
          [inst_1 : MeasurableSpace 𝓐] →
            [inst_2 : MeasurableSpace 𝓨] →
              [inst_3 : MeasurableSpace Ω] →
                MeasureTheory.Measure 𝓔 →
                  ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨 →
                    Learning.Algorithm 𝓐 𝓨 →…

`IsBayesAlgEnvSeq Q κ alg E A Y P` states that there is a measure `P : Measure Ω` such
that the parameter `E : Ω → 𝓔` has law `Q` and that the sequences of actions `A : ℕ → Ω → 𝓐`
and feedbacks `Y : ℕ → Ω → 𝓨` are generated by the algorithm `alg : Algorithm 𝓐 𝓨` interacting
with an underlying environment that depends on `E` and `κ` (`stationaryEnv (κ.sectR (E ω))`).

Go to its page

Bandits.tsAlgorithm : {K : ℕ} →
  {𝓔 : Type u_1} →
    [inst : MeasurableSpace 𝓔] →
      [StandardBorelSpace 𝓔] →
        [Nonempty 𝓔] →
          0 < K →
            (Q : MeasureTheory.Measure 𝓔) →
              [MeasureTheory.IsProbabilityMeasure Q] →
                (κ : ProbabilityTheory.Kernel (𝓔 × Fin K) ℝ) →
                  [ProbabilityTheory.IsMarkovKernel κ] → Learning.Algorithm (Fin K) ℝ

The Thompson sampling algorithm with actions in `Fin K`, where `Q : Measure 𝓔` is a prior
distribution over parameters, and `κ : Kernel (𝓔 × Fin K) ℝ` is a Markov kernel that defines the
stationary environment `stationaryEnv (κ.sectR e)` that corresponds to a parameter `e : 𝓔`.

At every time `n`, the Thompson sampling policy uses the posterior over the parameters given the
history up to time `n` to derive the probability of each action being optimal. The action for time
`n` is sampled according to these probabilities.

Go to its page

LE.le : {α : Type u} → [self : LE α] → α → α → Prop

The less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

Membership.mem : {α : outParam (Type u)} → {γ : Type v} → [self : Membership α γ] → γ → α → Prop

The membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.

MeasureTheory.integral : {α : Type u_6} →
  {G : Type u_7} →
    [inst : NormedAddCommGroup G] → [NormedSpace ℝ G] → {x : MeasurableSpace α} → MeasureTheory.Measure α → (α → G) → G

The Bochner integral

id : {α : Sort u} → α → α

The identity function. `id` takes an implicit argument `α : Sort u`
(a type in any universe), and an argument `a : α`, and returns `a`.

Although this may look like a useless function, one application of the identity
function is to explicitly put a type on an expression. If `e` has type `T`,
and `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and Lean
knows that this expression has type `T'` rather than `T`. This can make a
difference for typeclass inference, since `T` and `T'` may have different
typeclass instances on them. `show T' from e` is sugar for an `@id T' e`
expression.

Prod.mk : {α : Type u} → {β : Type v} → α → β → α × β

Constructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.

Set.Icc : {α : Type u_1} → [Preorder α] → α → α → Set α

`Icc a b` is the left-closed right-closed interval $[a, b]$.

ProbabilityTheory.HasSubgaussianMGF : {Ω : Type u_1} →
  {mΩ : MeasurableSpace Ω} →
    (Ω → ℝ) → NNReal → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasSubgaussianMGF._auto_1 → Prop

A random variable `X` has a sub-Gaussian moment-generating function with parameter `c`
with respect to a measure `μ` if for all `t : ℝ`, `exp (t * X)` is `μ`-integrable and
the moment-generating function of `X` is bounded by `exp (c * t ^ 2 / 2)` for all `t : ℝ`.
This implies in particular that `X` has expectation 0.

This is equivalent to `Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())`,
as proved in `HasSubgaussianMGF_iff_kernel`.
Properties about sub-Gaussian moment-generating functions should be proved first for
`Kernel.HasSubgaussianMGF` when possible.

HSub.hSub : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HSub α β γ] → α → β → γ

`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).

Subtype.mk : {α : Sort u} → {p : α → Prop} → (val : α) → p val → Subtype p

Learning.IsBayesAlgEnvSeq.regret : {𝓔 : Type u_1} →
  {𝓐 : Type u_2} →
    {Ω : Type u_4} →
      [inst : MeasurableSpace 𝓔] →
        [inst_1 : MeasurableSpace 𝓐] → ProbabilityTheory.Kernel (𝓔 × 𝓐) ℝ → (Ω → 𝓔) → (ℕ → Ω → 𝓐) → ℕ → Ω → ℝ

A random variable that gives the regret at time `n`.

Go to its page

HMul.hMul : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HMul α β γ] → α → β → γ

`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.

HAdd.hAdd : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HAdd α β γ] → α → β → γ

`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.

Real.sqrt : ℝ → ℝ

The square root of a real number. This returns 0 for negative inputs.

This has notation `√x`. Note that `√x⁻¹` is parsed as `√(x⁻¹)`.

Real.log : ℝ → ℝ

The real logarithm function, equal to the inverse of the exponential for `x > 0`,
to `log |x|` for `x < 0`, and to `0` for `0`. We use this unconventional extension to
`(-∞, 0]` as it gives the formula `log (x * y) = log x + log y` for all nonzero `x` and `y`, and
the derivative of `log` is `1/x` away from `0`.

Code

theorem integral_regret_le (hK : 0 < K) (h : IsBayesAlgEnvSeq Q κ (tsAlgorithm hK Q κ) E A R P)
    (hlu : l ≤ u) (hm : ∀ e a, (κ (e, a))[id] ∈ (Set.Icc l u)) (hσ2 : 0 < σ2)
    (hs : ∀ e a, HasSubgaussianMGF (fun x ↦ x - (κ (e, a))[id]) ⟨σ2, hσ2.le⟩ (κ (e, a))) (n : ℕ) :
    P[IsBayesAlgEnvSeq.regret κ E A n]
      ≤ (2 * K + 1) * (u - l) + 8 * √(σ2 * K * n * Real.log n)

Proof

by
  by_cases hn : n = 0
  · simp [hn, IsBayesAlgEnvSeq.regret, Bandits.regret]
    nlinarith
  have hδ : (0 : ℝ) < 1 / n ^ 2 := by positivity
  calc P[IsBayesAlgEnvSeq.regret κ E A n]
      = _ :=
        integral_regret_eq_add hK h hm n
    _ ≤ _ :=
        add_le_add
          (integral_sum_range_actionMean_bestAction_sub_ucb_bestAction_le h hlu hm hσ2 hs hδ n)
          (integral_sum_range_ucb_action_sub_actionMean_action_le h hlu hm hσ2 hs hδ n)
    _ = K * (u - l) + (K + 1) * (u - l) * ((n - 1) / n)
          + 4 * √((2 : ℝ) ^ 2 * (σ2 * K * n * Real.log n)) := by
        field_simp
        rw [Real.log_pow]
        ring_nf
    _ = K * (u - l) + (K + 1) * (u - l) * ((n - 1) / n) + 8 * √(σ2 * K * n * Real.log n) := by
        rw [Real.sqrt_mul (by positivity), Real.sqrt_sq (by norm_num)]
        ring
    _ ≤ K * (u - l) + (K + 1) * (u - l) * 1 + 8 * √(σ2 * K * n * Real.log n) := by -- loose
        have : 0 ≤ u - l := sub_nonneg.2 hlu
        gcongr
        rw [div_le_one (by positivity)]
        linarith
    _ = _ := by
        ring

Actions: Source · Open Issue

Meaning last changed in v4.34.0-rc2-39-gb743f31 (2026-09-08), the 5th recorded change.

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Audit surface: 25 project declarations, 140 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.

Bandits.TS.integral_regret_le🔗

`Bandits.TS.integral_regret_le`🔗