Lean module · Thompson sampling

BanditRLProof.Algorithms.ThompsonClippedUCBScore

# Clipped UCB score for the Thompson Bayesian-regret route This module instantiates `HistoryActionScore` with the clipped upper-confidence score used by the pinned LML Thompson regret proof. The finite-history score is measurable and lies in `[l, u]`; those bounds discharge every score integrability premise in the compiled Bayesian-regret decomposition.

Module map

Source: BanditRLProof/Algorithms/ThompsonClippedUCBScore.lean
Teaching chapter: 6. Thompson sampling and Bayesian regret
Declarations: 20
Placeholders: 0

Imports

BanditRLProof.Algorithms.ThompsonBayesRegretDecomposition, BanditRLProof.Algorithms.UCBRealHistoryIndex, BanditRLProof.PullCountDecomposition

Imported by

BanditRLProof, BanditRLProof.Algorithms.ThompsonStationaryReward

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.Thompson.clippedUCB Compiled

The clipped UCB score on a complete action/reward trace.

def clippedUCB {K : Nat} (l u sigma2 delta : Real) (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (arm : Fin K) (t : Nat) : Real

Source line 24 Chapter context: Thompson sampling

def BanditRLProof.Thompson.clippedUCBHistory Compiled

The same clipped score on the inclusive history through time `n`.

def clippedUCBHistory {K : Nat} (l u sigma2 delta : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : Real

Source line 37 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.clippedUCB_zero Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem clippedUCB_zero {K : Nat} (l u sigma2 delta : Real) (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (arm : Fin K) : clippedUCB l u sigma2 delta action reward arm 0 = u

Source line 50 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.clippedUCB_mem_Icc Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem clippedUCB_mem_Icc {K : Nat} (l u sigma2 delta : Real) (hlu : l <= u) (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (arm : Fin K) (t : Nat) : clippedUCB l u sigma2 delta action reward arm t ∈ Set.Icc l u

Source line 57 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.finset_sum_sqrt_le Compiled Internal helper

No declaration docstring is present; use the chapter context and exact statement below.

private theorem finset_sum_sqrt_le {ι : Type*} (s : Finset ι) (c : ι -> Real) (hc : forall i, 0 <= c i) : ∑ i ∈ s, Real.sqrt (c i) <= Real.sqrt (s.card * ∑ i ∈ s, c i)

Source line 68 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.finset_sum_one_div_sqrt_le Compiled Internal helper

No declaration docstring is present; use the chapter context and exact statement below.

private theorem finset_sum_one_div_sqrt_le {n : Nat} (hn : 0 < n) : ∑ k ∈ Finset.range (n + 1), 1 / Real.sqrt k <= 2 * Real.sqrt n - 1

Source line 77 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.sum_clippedUCB_action_sub_mean_le Compiled

Pathwise selected-action clipped-UCB excess bound from the pinned LML Thompson route. The only hypothesis is that every positive-count empirical mean is strictly below its arm mean plus the confidence width.

theorem sum_clippedUCB_action_sub_mean_le {K : Nat} [NeZero K] (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (mean : Fin K -> Real) (l u sigma2 delta : Real) (hmeanMem : forall arm, mean arm ∈ Set.Icc l u) (hlu : l <= u) (hgood : forall s, s < n -> pullCount action (action s) s ≠ 0 -> UCB.realEmpiricalMean action reward (action s) s - mean (action s) < Real.sqrt (2 * sigma2 * Real.log (1 / delta) / (pullCount action (action s) s : Real))) : ∑ s ∈ Finset.range n, (clippedUCB l u sigma2 delta action reward (action s) s - mean (action s)) <= (u - l) * K + 4 * Real.sqrt (2 * sigma2 * Real.log (1 / delta) * K * n)

Source line 106 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.clippedUCBHistory_mem_Icc Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem clippedUCBHistory_mem_Icc {K : Nat} (l u sigma2 delta : Real) (hlu : l <= u) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : clippedUCBHistory l u sigma2 delta n history arm ∈ Set.Icc l u

Source line 237 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.measurable_clippedUCBHistory Compiled

A fixed-arm clipped score is measurable on inclusive pair histories.

theorem measurable_clippedUCBHistory {K : Nat} (l u sigma2 delta : Real) (n : Nat) (arm : Fin K) : Measurable (fun history : History.FinitePairHistory (Fin K) Real n => clippedUCBHistory l u sigma2 delta n history arm)

Source line 249 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.measurable_uncurry_clippedUCBHistory Compiled

Joint measurability in the visible history and candidate action.

theorem measurable_uncurry_clippedUCBHistory {K : Nat} (l u sigma2 delta : Real) (n : Nat) : Measurable (fun pair : History.FinitePairHistory (Fin K) Real n × Fin K => clippedUCBHistory l u sigma2 delta n pair.1 pair.2)

Source line 275 Chapter context: Thompson sampling

def BanditRLProof.Thompson.clippedUCBHistoryScore Compiled

`HistoryActionScore` instance for the pinned LML clipped-UCB formula.

def clippedUCBHistoryScore {K : Nat} (l u sigma2 delta : Real) : HistoryActionScore (Fin K) Real where

Source line 285 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.clippedUCBHistory_finitePairHistoryOfTrace Compiled

Inclusive finite-history and exclusive trace versions agree at `n + 1`.

theorem clippedUCBHistory_finitePairHistoryOfTrace {K : Nat} (l u sigma2 delta : Real) (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (n : Nat) (arm : Fin K) : clippedUCBHistory l u sigma2 delta n (History.finitePairHistoryOfTrace action reward n) arm = clippedUCB l u sigma2 delta action reward arm (n + 1)

Source line 296 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.clippedUCBHistoryScore_atTrace Compiled

Evaluating the history score at the selected action recovers `clippedUCB`.

theorem clippedUCBHistoryScore_atTrace {K : Nat} (l u sigma2 delta : Real) (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (t : Nat) : (clippedUCBHistoryScore l u sigma2 delta).atTrace action reward t = clippedUCB l u sigma2 delta action reward (action t) t

Source line 308 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.clippedUCBHistoryScore_atBestTrace Compiled

Evaluating at a comparison arm recovers the same trace score.

theorem clippedUCBHistoryScore_atBestTrace {K : Nat} (l u sigma2 delta : Real) (bestArm : Fin K) (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (t : Nat) : (clippedUCBHistoryScore l u sigma2 delta).atBestTrace bestArm action reward t = clippedUCB l u sigma2 delta action reward bestArm t

Source line 320 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.integrable_of_measurable_mem_Icc Compiled

A measurable real function with pointwise range in `[l, u]` is integrable.

theorem integrable_of_measurable_mem_Icc {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (f : Omega -> Real) (hf : Measurable f) {l u : Real} (hmem : forall omega, f omega ∈ Set.Icc l u) : Integrable f mu

Source line 334 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.integrable_trajectoryHistoryScore_clippedUCB Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem integrable_trajectoryHistoryScore_clippedUCB {Env : Type u} {K : Nat} [MeasurableSpace Env] (mu : Measure (Env × ((n : Nat) -> Fin K × Real))) [IsFiniteMeasure mu] (l u sigma2 delta : Real) (hlu : l <= u) (t : Nat) : Integrable (fun sample => trajectoryHistoryScore (clippedUCBHistoryScore l u sigma2 delta) sample t) mu

Source line 347 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.integrable_trajectoryBestHistoryScore_clippedUCB Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem integrable_trajectoryBestHistoryScore_clippedUCB {Env : Type u} {K : Nat} [MeasurableSpace Env] (mu : Measure (Env × ((n : Nat) -> Fin K × Real))) [IsFiniteMeasure mu] (bestAction : Env -> Fin K) (hbestAction : Measurable bestAction) (l u sigma2 delta : Real) (hlu : l <= u) (t : Nat) : Integrable (fun sample => trajectoryBestHistoryScore (clippedUCBHistoryScore l u sigma2 delta) bestAction sample t) mu

Source line 368 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.integrable_trajectoryMean_bestAction Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem integrable_trajectoryMean_bestAction {Env : Type u} {K : Nat} [MeasurableSpace Env] (mu : Measure (Env × ((n : Nat) -> Fin K × Real))) [IsFiniteMeasure mu] (mean : Env -> Fin K -> Real) (hmean : Measurable (fun pair : Env × Fin K => mean pair.1 pair.2)) (hmeanMem : forall env arm, mean env arm ∈ Set.Icc l u) (bestAction : Env -> Fin K) (hbestAction : Measurable bestAction) : Integrable (fun sample : Env × ((n : Nat) -> Fin K × Real) => mean sample.1 (bestAction sample.1)) mu

Source line 391 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.integrable_trajectoryMean_action Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem integrable_trajectoryMean_action {Env : Type u} {K : Nat} [MeasurableSpace Env] (mu : Measure (Env × ((n : Nat) -> Fin K × Real))) [IsFiniteMeasure mu] (mean : Env -> Fin K -> Real) (hmean : Measurable (fun pair : Env × Fin K => mean pair.1 pair.2)) (hmeanMem : forall env arm, mean env arm ∈ Set.Icc l u) (t : Nat) : Integrable (fun sample : Env × ((n : Nat) -> Fin K × Real) => mean sample.1 (environmentTrajectoryAction sample t)) mu

Source line 407 Chapter context: Thompson sampling

theorem BanditRLProof.Thompson.integral_trajectoryBayesMeanRegret_eq_add_clippedUCB Compiled

Concrete clipped-UCB specialization of the actual-trajectory Thompson Bayesian-regret decomposition. Range and measurability assumptions discharge all four integrability families from `integral_trajectoryBayesMeanRegret_eq_add_historyScore`.

theorem integral_trajectoryBayesMeanRegret_eq_add_clippedUCB {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [Nonempty (Fin K)] (prior : Measure Env) [IsProbabilityMeasure prior] (environment : MeasurableHistoryEnvironment Env (Fin K) Real) (bestAction : Env -> Fin K) (hbestAction : Measurable bestAction) (mean : Env -> Fin K -> Real) (hmean : Measurable (fun pair : Env × Fin K => mean pair.1 pair.2)) (l u sigma2 delta : Real) (hlu : l <= u) (hmeanMem : forall env arm, mean env arm ∈ Set.Icc l u) (horizon : Nat) : let algorithm := uniformReferenceThompsonAlgorithm prior environment bestAction hbestAction let actualMeasure := prior ⊗ₘ canonicalMeasurableEnvironmentTrajectoryKernel algorithm environment integral actualMeasure (fun sample => trajectoryBayesMeanRegret mean bestAction sample horizon) = integral actualMeasure (fun sample => ∑ t ∈ range horizon, (mean sample.1 (bestAction sample.1) - clippedUCB l u sigma2 delta (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) (bestAction sample.1) t)) + integral actualMeasure (fun sample => ∑ t ∈ range horizon, (clippedUCB l u sigma2 delta (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) (environmentTrajectoryAction sample t) t - mean sample.1 (environmentTrajectoryAction sample t)))

Source line 428 Open teaching explanation Chapter context: Thompson sampling