BanditRLProof.Algorithms.ThompsonClippedUCBScore

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

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

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

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

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)

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

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)

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

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)

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)

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

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

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)

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

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

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

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

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

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

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

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)))