Also read in: Reinforcement Learning Book. This is the same chapter and the same Lean nodes.

Teaching chapter 04 of 10 · Canonical route compiled

4. UCB: confidence events to regret

History-based ordinary-UCB and KL-UCB scores, count thresholds, generated policies, arm streams, same-trajectory confidence, finite-arm reward kernels, and expected regret.

How to read the status. It describes this page's canonical local Lean route, not completion of the cited textbook chapter or every extension listed below.

Orientation

Who should read this. Read ETC first if confidence-event arguments are new to you.

Learning goals

Convert a suboptimal UCB selection into a confidence failure or a small-count event.
Trace conditional sub-Gaussian laws into a textbook-shaped gap-sum bound.
Read the compiled expected-average-regret convergence results without conflating them with every UCB variant.

Textbook crosswalk

Read the mathematics before the Lean interface

The Book Map is a curated formalization curriculum anchored in Bandit Algorithms, not a chapter-for-chapter reproduction of one book. Visible page labels use the numbered pages of its free online edition; source buttons use the PDF viewer's physical page index, which includes front matter and can therefore be larger. Companion papers cover algorithm-specific results.

Primary spine · free online edition

Bandit Algorithms

Tor Lattimore and Csaba Szepesvári

Location: Ch. 7; KL-UCB extension in Ch. 10
Pages: online pp. 102–111; KL-UCB pp. 133–141

Open at the cited pages

algorithm · ordered flow

Upper Confidence Bound policy

Read top to bottom: each step supplies the state or proof fact used by the next one.

Initialize
Pull every arm so that each empirical mean and count is defined.
Score every arm
Add a confidence bonus to the arm's empirical mean; less data means a wider bonus.
Choose optimistically
Pull an arm with maximal upper-confidence score.
Update and repeat
Update that arm's count and empirical mean, then recompute scores next round.
Read the proof
On the good event, choosing a suboptimal arm forces its count to still be small; sum gap times count to obtain regret.

Algorithm · explicit conventions

Textbook Algorithm 3: UCB(δ)

This compact form fixes the horizon convention, confidence index, maximizing rule, and update order used in the textbook route.

UCB score after initialization. Formula renderer unavailable; readable fallback: At round t, score arm a by its empirical mean before t plus square root of 2 log(1/delta) divided by its previous pull count; choose the least-encoded maximizing arm.\[U_a(t)=\widehat\mu_a(t-1)+\sqrt{\frac{2\log(1/\delta)}{N_a(t-1)}},\qquad A_t=\min\operatorname*{arg\,max}_{a\in[k]}U_a(t).\]

input: k arms, horizon n, confidence δ = 1/n²
for t = 1,…,k: pull arm t; observe X_t; update N_t and μ̂_t
for t = k+1,…,n:
    compute every U_a(t) from rewards observed before round t
    choose the least-encoded arm in argmax_a U_a(t)
    observe its reward; update only that arm's count and empirical mean

Source/Lean boundary. The textbook also describes an unpulled arm as having infinite index; the explicit round-robin prefix realizes the same initialization requirement. BanditRLlib's canonical generated route uses round-robin initialization and a least-encoded maximizer, but its native score is parameterized as √(2c log(t+1)/N_a(t)); the source theorem card and exact Lean declarations remain authoritative for constants and indexing.

Worked example · follow one decision

Why UCB may deliberately choose the arm with the lower empirical mean

Take a two-arm UCB(δ) decision near the end of a horizon n = 20, so δ = 1/n² = 1/400. Before round 20, arm 1 has been sampled 15 times and arm 2 only 4 times.

Start from the observed history
Arm 1 currently looks better, but arm 2 is much less explored.
Worked example step 1. Formula renderer unavailable; readable fallback: Arm 1 has count 15 and empirical mean 0.60; arm 2 has count 4 and empirical mean 0.30.\[N_1=15,\quad \widehat\mu_1=0.60,\qquad N_2=4,\quad \widehat\mu_2=0.30.\]
Add uncertainty, not just reward
With 2 log(400) approximately 11.98, the under-sampled arm receives the wider confidence bonus.
Worked example step 2. Formula renderer unavailable; readable fallback: The two upper-confidence scores are approximately 1.49 for arm 1 and 2.03 for arm 2.\[U_1\approx0.60+\sqrt{11.98/15}=1.49,\qquad U_2\approx0.30+\sqrt{11.98/4}=2.03.\]
Choose optimism and shrink it with data
UCB selects arm 2 even though its empirical mean is lower. Each additional pull increases N₂, narrows its bonus, and makes persistent suboptimal selection harder to justify.
Worked example step 3. Formula renderer unavailable; readable fallback: At round 20 the policy chooses arm 2 because its upper-confidence score is larger; its bonus decreases as its sample count increases.\[A_{20}=2\quad\text{because}\quad U_2>U_1;\qquad \sqrt{2\log(1/\delta)/N_2}\downarrow\text{ as }N_2\uparrow.\]

Takeaway. UCB is not greedily choosing the largest empirical mean. It chooses the largest plausible mean, so uncertainty creates exploration and the count-dependent radius eventually limits repeated pulls of a genuinely suboptimal arm.

Scope. The numbers illustrate one UCB(δ) decision; they are not a simulated regret result or a new Lean theorem. The source card and compiled declarations below control the exact assumptions and constants.

Proof bridge · source to Lean

Why an optimistic choice becomes a regret bound

The source proof and the local Lean route use the same four conceptual joints. Read this bridge before comparing constants or implementation details.

Control every empirical mean
Work on a confidence event where each empirical mean stays within its declared radius of the true arm mean.
Step 1 equation. Formula renderer unavailable; readable fallback: For every relevant arm and round, the empirical mean error is at most its confidence radius.\[|\widehat\mu_a(t)-\mu_a|\le r_a(t).\]
Use optimism at the selected arm
If a suboptimal arm is chosen on that event, its upper-confidence score must still compete with the optimal arm's mean.
Step 2 equation. Formula renderer unavailable; readable fallback: Selecting a suboptimal arm on the confidence event forces its gap to be no larger than twice its current radius.\[A_t=a\ne a^\star\Longrightarrow \Delta_a\le 2r_a(t).\]
Turn the radius into a count threshold
Because the radius shrinks with the number of samples, the preceding inequality can hold only while the arm has been pulled comparatively few times.
Step 3 equation. Formula renderer unavailable; readable fallback: The pull count of a suboptimal arm is controlled by a logarithmic term divided by the squared arm gap.\[N_a(T)\lesssim \frac{\log(T/\delta_a)}{\Delta_a^2}.\]
Charge every pull by its gap
Apply the pathwise gap-sum identity, then account explicitly for the confidence-event failure probability under the generated trajectory law.
Step 4 equation. Formula renderer unavailable; readable fallback: Expected pseudo-regret is at most the sum of each positive gap times its pull-count bound plus its explicit failure-event charge.\[\mathbb E\bar R_T\le\sum_{a:\Delta_a>0}\Delta_a\bigl(B_a(T)+T\delta_a\bigr).\]

Reading boundary. This is a reading aid for the shared proof shape. The source theorem card and exact Lean statement below remain authoritative for the model, constants, horizon convention, and confidence schedule.

Source theorem · faithful restatement

Theorem 7.2 (finite-time UCB regret)

Original at online p. 108 ↗

Confidence validity implies a suboptimal arm can be selected only while its sample count is small enough to keep its bonus competitive.

Model: A finite stochastic k-armed bandit in the textbook's 1-sub-Gaussian environment class.
Assumptions: Each arm has a fixed mean and 1-sub-Gaussian noise; the chapter's canonical independent reward-table model supplies the samples used by the proof.
Algorithm parameters: Algorithm 3, UCB(δ), at horizon n with δ = 1/n²; an unpulled arm has infinite index, otherwise the index is its empirical mean plus √(2 log(1/δ) / count).
Regret notion: The textbook expected regret Rₙ over n rounds.
Guarantee: A worst-case finite-time upper bound 8√(nk log n) plus three times the sum of arm gaps.

Source mathematical statement. Formula renderer unavailable; readable fallback: The textbook UCB policy has a finite-time regret bound with a leading square-root term in horizon, arm count, and log horizon.\[R_n\le 8\sqrt{nk\log n}+3\sum_{i=1}^{k}\Delta_i.\]

BanditRLlib relationship. BanditRLlib's ordinary-UCB route uses an explicit generated trajectory and confidence schedule. Its exact hypotheses, constants, gap-sum form, and Tδ failure term are therefore not presented as a line-for-line formalization of Theorem 7.2; KL-UCB remains a separate extension.

The mathematical content is restated in this site's notation; wording is ours. See online p. 108 in the linked source for the original statement and full assumptions.

Natural-language and Lean side by side

The mathematical readings are explanatory summaries. The exact generated Lean statement and its source link remain authoritative for hypotheses, types, constants, and indexing.

A curated route through definitions, key bridges, and canonical terminals stays visible. 2 additional dependency, extension, or research-frontier notes are grouped below.

Mathematics ↔ LeanClosest local match to the source theorem

Textbook gap-sum regret for generated UCB

Lean declarationBanditRLProof.UCB.integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_finiteArmSubgaussianLaws_without_proxy_positivity

Compiled

Plain-English statement. The generated finite-arm UCB policy has a textbook-shaped expected pseudo-regret gap-sum bound for sub-Gaussian arm laws, including zero variance proxies.

Mathematical reading. Formula renderer unavailable; readable fallback: The generated finite-arm UCB policy has a textbook-shaped expected pseudo-regret gap-sum bound for sub-Gaussian arm laws, including zero variance proxies.\(\mathbb E\bar R_T\le\sum_{a:\Delta_a>0}\Delta_a\bigl(B_a(T)+T\delta_a\bigr),\quad B_a(T)\asymp v_a\log(T/\delta_a)/\Delta_a^2.\)

Intuition: A suboptimal arm can be chosen many times only while it has too few samples or while a confidence event fails.
Why it is needed: This is the practical model-facing UCB endpoint that connects arm laws, the generated adaptive trace, confidence widths, pull counts, and regret.
Place in the proof: It is the finite-horizon regret node in the compiled horizon-indexed ordinary-UCB chain; the separately compiled fixed-policy anytime route has its own telescoping policy and terminal.

Proof and Lean reading notes

Proof idea: Construct the finite-arm reward kernel, obtain selected conditional MGF bounds, split selections at an explicit count threshold, sum the failure probabilities, and apply the gap-times-count regret decomposition.
Lean reading notes: The suffix without_proxy_positivity matters: the theorem handles the all-zero proxy case separately instead of adding a false global positivity assumption.
Teaching dependencies: BanditRLProof.pseudoRegret_eq_finset_sum_gap_mul_pullCount

Exact Lean statement

theorem integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_finiteArmSubgaussianLaws_without_proxy_positivity {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (varianceProxy : Fin K -> NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (hsubG : forall arm, HasSubgaussianMGF (fun reward : Rat => (((reward - model.mean arm : Rat) : Real))) (varianceProxy arm) (armLaw arm)) (defaultAction : Fin K) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) : let sigma2 := Concentration.finiteArmPositiveVarianceProxy varianceProxy let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context := Unit) armLaw hprob let context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Unit := fun _ _ => () MeasureTheory.integral (selectedPolicySuccessorRewardTrajMeasure model.hK (armLaw defaultAction) rewardKernel context (fun _ => measurable_const) sigma2 T delta defaultAction) (fun trajectory : RewardTrace Rat => ((pseudoRegret model (selectedPolicySuccessorGeneratedUCBRegretAction model.hK sigma2 T delta defaultAction (fun y : RewardTrace Rat => y) trajectory) T : Rat) : Real)) <= ((Finset.univ : Finset (Fin K)).filter (fun arm => 0 < (((model.gap arm : Rat) : Real)))).sum (fun arm => selectedPolicySuccessorTextbookGapBudget K sigma2 T delta (((model.gap arm : Rat) : Real)) + (((model.gap arm : Rat) : Real)) * ((T : Real) * delta))

Open in the declaration catalog Open source at line 119

Mathematics ↔ LeanDownstream consumer

Expected average UCB regret vanishes

Lean declarationBanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedAveragePseudoRegret_tendsto_zero

Compiled

Plain-English statement. For the canonical finite-arm sub-Gaussian horizon-indexed UCB family, expected pseudo-regret divided by the horizon converges to zero.

Mathematical reading. Formula renderer unavailable; readable fallback: For the canonical finite-arm sub-Gaussian horizon-indexed UCB family, expected pseudo-regret divided by the horizon converges to zero.\[\mathbb E[\bar R_T]/(T+1)\to0.\]

Intuition: Choosing the confidence budget as a function of the terminal horizon turns the finite-time confidence/count/regret theorem into a logarithmic envelope, which vanishes after normalization.
Why it is needed: This is the stated asymptotic consumer of the ordinary-UCB Book Map route.
Place in the proof: It terminates the public chain from finite-arm/time confidence through generated score selection, pull counts, finite-arm expected regret, and asymptotic normalization.

Proof and Lean reading notes

Proof idea: Specialize the canonical family at delta(T)=1/(T+1), bound expected regret by a fixed model coefficient times 1+log(T+1), prove this is little-o of T+1, and divide.
Lean reading notes: The theorem concerns a horizon-indexed policy/measure family. It is not a single fixed-policy anytime, pathwise, almost-sure, or maximal-confidence result.
Teaching dependencies: BanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret_nonneg_and_le

Exact Lean statement

theorem selectedPolicySuccessorFiniteArmSubgaussianExpectedAveragePseudoRegret_tendsto_zero {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (varianceProxy : Fin K -> NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (hsubG : forall arm, HasSubgaussianMGF (fun reward : Rat => (((reward - model.mean arm : Rat) : Real))) (varianceProxy arm) (armLaw arm)) (defaultAction : Fin K) : Tendsto (selectedPolicySuccessorFiniteArmSubgaussianExpectedAveragePseudoRegret model armLaw hprob varianceProxy defaultAction) atTop (nhds 0)

Open in the declaration catalog Open source at line 244

Explore 2 additional Lean teaching notes

Mathematics ↔ LeanCompiled extension

A single horizon-free telescoping-scheduled UCB policy has one all-time…

Lean declarationBanditRLProof.UCB.lintegral_ofReal_pseudoRegret_selectedPolicySuccessorTelescoping_le_trajMeasure

Compiled

Plain-English statement. A single horizon-free telescoping-scheduled UCB policy has one all-time confidence event on one generated trajectory measure, simultaneous positive-gap pull-count bounds for all finite horizons, and an explicit finite-time expected pseudo-regret bound.

Mathematical reading. Formula renderer unavailable; readable fallback: A single horizon-free telescoping-scheduled UCB policy has one all-time confidence event on one generated trajectory measure, simultaneous positive-gap pull-count bounds for all finite horizons, and an explicit finite-time expected pseudo-regret bound.\[\mu(G^c)\le\delta,\quad G\Rightarrow\forall T,a:\ N_a(T)\le B_a(T),\quad \mathbb E R_T\le\sum_a\Delta_a(B_a(T)+T\delta).\]

Intuition: The policy chooses its round-t bonus from the summable telescoping share assigned to that round, so asking for a later terminal horizon never reconstructs or changes the past policy.
Why it is needed: It closes the semantic gap between an all-time concentration producer and an actual fixed-policy ordinary-UCB regret consumer.
Place in the proof: This is the fixed-policy terminal of Chapter 4. The older horizon-indexed chain remains a separate compiled family and supplies its own expected-average consistency theorem.

Proof and Lean reading notes

Proof idea: Reconstruct actions recursively from finite reward histories, prove exact score/count/mean alignment, transport the sampled pair action to the reconstructed action almost everywhere on the same trajectory measure, apply the telescoping all-time event, invert the scheduled radius after initialization, and integrate the finite-horizon count tail.
Lean reading notes: The policy, state, generated action, and trajectory-measure declarations contain no terminal horizon. A horizon appears only in count/regret consumers and deterministic thresholds. The expected theorem retains T times delta, so it is not a fixed-delta average-consistency or almost-sure result.
Teaching dependencies: BanditRLProof.ConditionalExpectationReward.actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_fintype_telescopingAllTime_abs_tail_ennreal_delta_trajMeasure, BanditRLProof.UCB.meanGap_le_two_radius_of_confidenceScore_max, BanditRLProof.pseudoRegret_eq_finset_sum_gap_mul_pullCount

Exact Lean statement

theorem lintegral_ofReal_pseudoRegret_selectedPolicySuccessorTelescoping_le_trajMeasure {Context : Type} {K : Nat} [MeasurableSpace Context] (model : FiniteBanditModel K) (mu0 : Measure (Prod (Fin K) Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (mean : Context -> Fin K -> Rat) (varianceProxy : Context -> Fin K -> NNReal) (defaultAction : Fin K) (sigma2 : NNReal) (delta : Real) (T : Nat) (hcontext : forall n : Nat, Measurable (context n)) (hmean : Measurable (fun pair : Prod Context (Fin K) => mean pair.1 pair.2)) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((selectedPolicySuccessorTelescopingHistoryPolicy model.hK sigma2 delta defaultAction i).action (selectedPolicySuccessorTelescopingHistoryState model.hK sigma2 delta defaultAction i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, mean (context i history) arm = model.mean arm) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (hdelta : 0 < delta) : let mu := selectedPolicySuccessorTelescopingActionRewardTrajMeasure model.hK mu0 rewardKernel context hcontext sigma2 delta defaultAction let reward : (Nat -> Prod (Fin K) Rat) -> RewardTrace Rat := fun trajectory t => (trajectory t).2 let action := selectedPolicySuccessorTelescopingGeneratedUCBRegretAction model.hK sigma2 delta defaultAction reward ∫⁻ trajectory, ENNReal.ofReal (((pseudoRegret model (action trajectory) T : Rat) : Real)) ∂mu <= (Finset.univ : Finset (Fin K)).sum (fun arm => ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((selectedPolicySuccessorTelescopingPullThreshold K sigma2 T delta (((model.gap arm : Rat) : Real)) : Nat) : ENNReal) + ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((T : ENNReal) * ENNReal.ofReal delta))

Open in the declaration catalog Open source at line 1314

Mathematics ↔ LeanCompiled extension

A horizon-free generated policy uses the actual Bernoulli-KL confidence-set…

Lean declarationBanditRLProof.KLUCB.lintegral_ofReal_pseudoRegret_generatedKLUCBBounded_le_trajMeasure

Compiled

Plain-English statement. A horizon-free generated policy uses the actual Bernoulli-KL confidence-set supremum, aligns it with its own reward history, and has a conservative finite-time expected pseudo-regret bound on the same canonical trajectory measure.

Mathematical reading. Formula renderer unavailable; readable fallback: A horizon-free generated policy uses the actual Bernoulli-KL confidence-set supremum, aligns it with its own reward history, and has a conservative finite-time expected pseudo-regret bound on the same canonical trajectory measure.\[\mu(G_{\mathrm{KL}}^c)\le\delta,\quad G_{\mathrm{KL}}\Rightarrow\forall T,a:\ N_a(T)\le B_a^{\mathrm{KL}}(T),\quad \mathbb E R_T\le\sum_a\Delta_a(B_a^{\mathrm{KL}}(T)+T\delta).\]

Intuition: The optimal mean is feasible in its KL confidence set on the all-time good event. The selected arm has maximal KL index, so a positive-gap arm can keep winning only while its telescoping radius and count remain below an explicit threshold.
Why it is needed: It is the first local KL-UCB terminal that runs on a real generated action/reward trajectory instead of stopping at a scalar KL inequality or reusing an ordinary additive UCB score.
Place in the proof: This is the conservative finite-time endpoint of the generated bounded KL-UCB extension to Chapter 4.

Proof and Lean reading notes

Proof idea: Define Bernoulli KL with explicit endpoint semantics and its confidence-set sSup; reconstruct the score from the generated reward history; use an interior KL upper comparison to transport the accepted telescoping empirical-mean event to KL optimism; combine selected-index maximality with the KL lower comparison; invert the radius into all-horizon counts and integrate the finite-arm gap decomposition.
Lean reading notes: The theorem assumes AE rewards in [0,1], stationary means in [margin,1-margin] with 0 < margin <= 1/2, a centered sub-Gaussian kernel law, and positive sigma2 and delta. It retains T times delta and does not claim a sharp KL-Chernoff exponent, the Garivier-Cappe leading constant, or asymptotic optimality.
Teaching dependencies: BanditRLProof.KLUCB.bernoulliKLCore_le_sq_div, BanditRLProof.KLUCB.generatedIndexAt_le_selected_of_K_le, BanditRLProof.ConditionalExpectationReward.actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_fintype_telescopingAllTime_abs_tail_ennreal_delta_trajMeasure, BanditRLProof.pseudoRegret_eq_finset_sum_gap_mul_pullCount

Exact Lean statement

theorem lintegral_ofReal_pseudoRegret_generatedKLUCBBounded_le_trajMeasure {Context : Type} {K : Nat} [MeasurableSpace Context] (model : FiniteBanditModel K) (mu0 : Measure (Prod (Fin K) Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (mean : Context -> Fin K -> Rat) (varianceProxy : Context -> Fin K -> NNReal) (defaultAction : Fin K) (sigma2 : NNReal) (delta margin : Real) (T : Nat) (hdelta : 0 < delta) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (harmMargin : forall arm : Fin K, (model.mean arm : Real) ∈ Set.Icc margin (1 - margin)) (hcontext : forall n : Nat, Measurable (context n)) (hraw : ∀ᵐ trajectory ∂(actionRewardTrajMeasure model.hK mu0 rewardKernel context hcontext sigma2 delta margin defaultAction), forall i : Nat, ((((trajectory i).2 : Rat) : Real)) ∈ Set.Icc (0 : Real) 1) (hmean : Measurable (fun pair : Prod Context (Fin K) => mean pair.1 pair.2)) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((historyPolicy model.hK sigma2 delta margin defaultAction i).action (historyState model.hK sigma2 delta margin defaultAction i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, mean (context i history) arm = model.mean arm) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) : let mu := actionRewardTrajMeasure model.hK mu0 rewardKernel context hcontext sigma2 delta margin defaultAction let reward : (Nat -> Prod (Fin K) Rat) -> RewardTrace Rat := fun trajectory t => (trajectory t).2 let action := generatedRegretAction model.hK sigma2 delta margin defaultAction reward ∫⁻ trajectory, ENNReal.ofReal (((pseudoRegret model (action trajectory) T : Rat) : Real)) ∂mu <= (Finset.univ : Finset (Fin K)).sum (fun arm => ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((pullThreshold K sigma2 T delta margin (((model.gap arm : Rat) : Real)) : Nat) : ENNReal) + ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((T : ENNReal) * ENNReal.ofReal delta))

Open in the declaration catalog Open source at line 1380

Maintainer contract

Open the canonical completion definition and blockers

Complete within the ordinary-UCB Book Map scope when (i) the canonical horizon-indexed generated UCB family connects simultaneous finite-arm/time confidence to pull counts, finite-arm expected regret, and its expected-average asymptotic consumer, and (ii) one separate horizon-free scheduled policy and trajectory measure connect the telescoping all-time confidence event to a simultaneous all-horizon positive-gap pull-count theorem and a finite-time expected pseudo-regret consumer. Public imports, typed canaries, explicit initialization/positivity contracts, and a clean full gate are required. Fixed-policy expected-average consistency and upstream compatibility are separate unless proved explicitly.

Remaining blockers

No remaining blocker inside the declared ordinary-UCB scope: the horizon-indexed chain reaches expected-average convergence, and the new horizon-free scheduled policy uses the telescoping radius on its own generated history, explicitly transports sampled/generated actions on the same trajectory measure, controls all finite horizons on one good event, and supplies a finite-time expected pseudo-regret bound.

Chapter implementation status

The compact summary keeps the reading route visible. Open it for source-linked declarations and exact remaining gaps.

Open 19 implementation records18 compiled · 1 partial · 0 blocked · 0 planned

Milestone	Status	Lean declaration	Remaining gap
Repaired parallel causal allocation and actual expected simple regret	Compiled	`BanditRLProof.Causal.ParallelParameters.allocation_cost_leBanditRLProof.Causal.ParallelParameters.graph_designCostBanditRLProof.Causal.ParallelParameters.expected_simpleRegret_parallel` Open 1 more declarations `BanditRLProof.Causal.ParallelParameters.expected_simpleRegret_parallel_optimal`	—
Causal actual-sampling expected simple regret on a common finite alphabet	Compiled	`BanditRLProof.Causal.GraphModel.expected_simpleRegret_source_boundBanditRLProof.Causal.GraphModel.expected_simpleRegret_explicit_rateBanditRLProof.Causal.GraphModel.expected_simpleRegret_uniform` Open 1 more declarations `BanditRLProof.Causal.GraphModel.expected_simpleRegret_optimal`	—
HOO full expected regret for arbitrary reward families	Compiled	`BanditRLProof.HOO.RegularCovering.expected_pseudoRegret_rate_familyBanditRLProof.HOO.RegularCovering.expected_actual_eq_pseudoRegret_familyBanditRLProof.HOO.RegularCovering.expected_actualRegret_rate_family`	—
Finite raw-moment regret supremum and actual-law adapter	Compiled	`BanditRLProof.HeavyTail.GenaltiAudit.normalized_sSup_ne_topBanditRLProof.HeavyTail.GenaltiAudit.process_value_memBanditRLProof.HeavyTail.GenaltiAudit.normalized_sSup_two_eq`	—
Finite counterexample to the printed source-policy regret coefficient	Compiled	`BanditRLProof.HeavyTail.SourceCounterexample.literal_printed_bound_falseBanditRLProof.HeavyTail.SourceCounterexample.kernel_raw_moment`	—
Clipped-prefix confidence under consumed-sample corruption	Compiled	`BanditRLProof.HeavyTail.adaptive_corrupted_clipped_mean_tailBanditRLProof.HeavyTail.observed_corrupted_clipped_mean_tailBanditRLProof.HeavyTail.arm_corrupted_clipped_mean_tail`	—
Corrected expected regret for source-parameter robust UCB	Compiled	`BanditRLProof.HeavyTail.SourcePolicy.robust_expected_regretBanditRLProof.HeavyTail.SourcePolicy.robust_integral_count_le_budget`	—
Source-schedule causal robust-UCB confidence budgets	Compiled	`BanditRLProof.HeavyTail.SourcePolicy.robustMean_upper_tail_sumBanditRLProof.HeavyTail.SourcePolicy.robustMean_lower_tail_sum`	—
Fixed-policy telescoping anytime UCB confidence and regret	Compiled	`BanditRLProof.UCB.selectedPolicySuccessorTelescopingHistoryPolicyBanditRLProof.UCB.selectedPolicySuccessorTelescopingPairHistory_eq_finitePairHistoryOfTraceBanditRLProof.UCB.measure_selectedPolicySuccessorTelescoping_allTimeBadEvent_le_trajMeasure` Open 2 more declarations `BanditRLProof.UCB.selectedPolicySuccessorTelescoping_allHorizonPullCount_of_not_badEventBanditRLProof.UCB.lintegral_ofReal_pseudoRegret_selectedPolicySuccessorTelescoping_le_trajMeasure`	The finite-time expectation keeps the explicit T times delta failure contribution; fixed-delta expected-average consistency is not claimed. The compiled bounded KL-UCB extension is mapped separately; literal pinned-LML identity remains cross-toolchain work.
Finite-arm sub-Gaussian UCB gap-sum bound	Compiled	`BanditRLProof.UCB.integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_finiteArmSubgaussianLaws_without_proxy_positivity`	—
Finite-arm UCB expected-average consistency	Compiled	`BanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedAveragePseudoRegret_tendsto_zero`	—
Canonical horizon-indexed UCB confidence-to-consistency chain	Compiled	`BanditRLProof.UCB.measure_selectedPolicySuccessorLargeGapEvent_generatedUCB_le_ennreal_delta_actionRewardTrajMeasure_centeredKernelBanditRLProof.UCB.measure_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_gt_explicitPullThreshold_le_ennreal_delta_actionRewardTrajMeasure_centeredKernelBanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret_nonneg_and_le` Open 1 more declarations `BanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedAveragePseudoRegret_tendsto_zero`	This is a horizon-indexed policy family, not a single fixed-policy anytime UCB theorem.
Pinned LML UCB theorem-card port	Partial	`BanditRLProof.UCB.integral_realKernelRegret_armStreamAction_le_lml_sum`	Direct imported-LML symbol and toolchain identity remain cross-toolchain work; the local expected pull-count ledger is already compiled. Do not treat the upstream theorem card as a local proof term.
Generated bounded-reward KL-UCB confidence and regret	Compiled	`BanditRLProof.KLUCB.bernoulliKLBanditRLProof.KLUCB.indexBanditRLProof.KLUCB.historyPolicy` Open 5 more declarations `BanditRLProof.KLUCB.pairHistory_eq_finitePairHistoryOfTraceBanditRLProof.KLUCB.generatedIndexAt_le_selected_of_K_leBanditRLProof.KLUCB.measure_generatedKLAllTimeBadEvent_le_trajMeasureBanditRLProof.KLUCB.allHorizonPullCount_of_not_badEventBanditRLProof.KLUCB.lintegral_ofReal_pseudoRegret_generatedKLUCBBounded_le_trajMeasure`	The finite-time conservative route assumes AE [0,1] rewards and means in [margin,1-margin], and retains T times delta. Sharp KL-Chernoff concentration, the Garivier-Cappe leading constant, and asymptotic optimality are not claimed.
Full triggered CUCB approximation regret with explicit analysis repairs	Compiled	`BanditRLProof.CUCB.SourceModel.theorem_one_refined_regretBanditRLProof.CUCB.SourceModel.theorem_two_deterministicBanditRLProof.CUCB.SourceModel.theorem_two_probabilistic`	—
Native heterogeneous finite-node causal expected simple regret	Compiled	`BanditRLProof.Causal.NodeGraphModel.expected_simpleRegret_source_boundBanditRLProof.Causal.NodeGraphModel.expected_simpleRegret_explicit_rateBanditRLProof.Causal.NodeGraphModel.expected_simpleRegret_uniform` Open 1 more declarations `BanditRLProof.Causal.NodeGraphModel.expected_simpleRegret_optimal`	—
Static Musical Chairs actual coordination and finite expected occupation	Compiled	`BanditRLProof.MusicalChairs.transition_unfixed_hazard_quarterBanditRLProof.MusicalChairs.unfixed_survivalBanditRLProof.MusicalChairs.expected_unfixed_occupation_le`	—
Static Musical Chairs actual finite expected coordination mean regret	Compiled	`BanditRLProof.MusicalChairs.roundPseudoRegret_le_twice_unfixedBanditRLProof.MusicalChairs.expectedCoordinationRegret_real_le`	—
Static unknown-N learner: actual expected visible regret	Compiled	`BanditRLProof.MusicalChairs.source_expected_learnerRegret_coarseBanditRLProof.MusicalChairs.realizedLearnerRegret_expected_eq_pseudoBanditRLProof.MusicalChairs.source_expected_visibleRegret_le`	—

Open boundaries

The fixed-policy telescoping anytime confidence/count/finite-time expected-regret route is compiled. Its bound retains the explicit T times delta failure term, so fixed-delta expected-average consistency is not claimed.
The geometric all-time radius is retained as a valid confidence producer but its exponentially shrinking share is not the route to logarithmic fixed-policy UCB regret.
A distinct generated KL-UCB extension now compiles Bernoulli-KL endpoint semantics, confidence-set supremum, a horizon-free policy, same-source all-time confidence, all-horizon counts, and conservative finite-time expected pseudo-regret under AE unit support and a common interior-mean margin.
Sharp KL-Chernoff concentration, the Garivier-Cappe leading constant, KL-UCB limsup asymptotic optimality, and exact pinned-LML compatibility remain separate.

All Lean modules in this chapter

Open the complete module list (35 modules)

Module	Declarations	Project imports	Status
`BanditRLProof.Algorithms.UCB`	142	8	Compiled
`BanditRLProof.Algorithms.UCBArmStreamAsymptotics`	15	2	Compiled
`BanditRLProof.Algorithms.UCBArmStreamConditionalReward`	46	2	Compiled
`BanditRLProof.Algorithms.UCBArmStreamExpectedPullCount`	39	7	Compiled
`BanditRLProof.Algorithms.UCBArmStreamFiniteArmRewardLaws`	15	2	Compiled
`BanditRLProof.Algorithms.UCBArmStreamProcess`	19	1	Compiled
`BanditRLProof.Algorithms.UCBArmStreamSource`	6	1	Compiled
`BanditRLProof.Algorithms.UCBArmStreamTail`	38	3	Compiled
`BanditRLProof.Algorithms.UCBArmwiseBoundedFiniteArmSampledAsymptotics`	6	1	Compiled
`BanditRLProof.Algorithms.UCBBoundedFiniteArmRewardLaw`	2	2	Compiled
`BanditRLProof.Algorithms.UCBBoundedFiniteArmSampledAsymptotics`	5	1	Compiled
`BanditRLProof.Algorithms.UCBConditionalRewardLaw`	7	2	Compiled
`BanditRLProof.Algorithms.UCBConditionalRewardLawCenteredKernel`	12	1	Compiled
`BanditRLProof.Algorithms.UCBConditionalRewardLawCenteredKernelReal`	3	2	Compiled
`BanditRLProof.Algorithms.UCBConditionalRewardLawPolicy`	46	3	Compiled
`BanditRLProof.Algorithms.UCBConditionalRewardLawRegret`	12	3	Compiled
`BanditRLProof.Algorithms.UCBConditionalRewardLawTrajMeasure`	6	1	Compiled
`BanditRLProof.Algorithms.UCBConditionalRewardPairTrajectory`	6	4	Compiled
`BanditRLProof.Algorithms.UCBConditionalRewardPairTrajectoryReal`	1	2	Compiled
`BanditRLProof.Algorithms.UCBConditionalRewardPairTrajectorySampledAsymptotics`	18	1	Compiled
`BanditRLProof.Algorithms.UCBConditionalRewardPairTrajectorySampledReal`	3	1	Compiled
`BanditRLProof.Algorithms.UCBContextDependentBoundedRewardKernel`	1	2	Compiled
`BanditRLProof.Algorithms.UCBContextDependentSubGaussianRewardKernel`	3	3	Compiled
`BanditRLProof.Algorithms.UCBFiniteArmSubGaussianRewardLaw`	2	2	Compiled
`BanditRLProof.Algorithms.UCBFiniteArmSubGaussianSampledAsymptotics`	8	2	Compiled
`BanditRLProof.Algorithms.UCBFixedCountPeeling`	8	2	Compiled
`BanditRLProof.Algorithms.UCBFixedPolicyTelescopingAnytimeRegret`	43	3	Compiled
`BanditRLProof.Algorithms.UCBRealHistoryIndex`	22	4	Compiled
`BanditRLProof.Algorithms.UCBRealLMLCompat`	4	1	Compiled
`BanditRLProof.Algorithms.UCBRealStationaryCanonicalKernelTrajectory`	9	2	Compiled
`BanditRLProof.Algorithms.UCBRealStationaryExplicitPolicy`	13	1	Compiled
`BanditRLProof.Algorithms.UCBRealStationaryFiniteArmRewardLaws`	9	2	Compiled
`BanditRLProof.Algorithms.UCBRealStationaryMeasurePreservingSource`	10	1	Compiled
`BanditRLProof.Algorithms.UCBRealStationarySelectedRewardConsistency`	4	1	Compiled
`BanditRLProof.UCBSummability`	3	1	Compiled