Teaching chapter 05 of 10 · Canonical route compiled

5. OFUL, self-normalized confidence, and stopping times

The scoped canonical finite-action linear-bandit route compiles from elliptical potential and self-normalized ridge confidence through one horizon-free generated OFUL policy with all-horizon regret and stopping consumers, plus a separately identified horizon-indexed expected-consistency family.

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 the Probability layer and UCB chapter before this linear-bandit route.

Learning goals

Understand the log-determinant proof of the elliptical-potential inequality.
Follow a conditional MGF source through ridge confidence and optimistic action selection.
Separate deterministic horizons, simultaneous one-policy confidence, and square-integrable stopping-time conclusions.

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. 19–20; stopping times in §3.3
Pages: online pp. 238–262; stopping-time basics pp. 50–54

Open at the cited pages

Algorithm-specific companion

Improved Algorithms for Linear Stochastic Bandits

Yasin Abbasi-Yadkori, Dávid Pál, and Csaba Szepesvári

Location: OFUL algorithm and Theorem 3
Pages: paper pp. 3–5

Open at the cited pages

algorithm · ordered flow

OFUL confidence-ellipsoid loop

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

Update geometry
Accumulate the regularized feature Gram matrix from past actions.
Estimate
Compute the ridge least-squares parameter estimate.
Build confidence
Place plausible parameters in an ellipsoid around the estimate.
Act optimistically
Choose the action and plausible parameter pair with the largest predicted reward.
Charge widths
Bound regret by confidence widths and use the elliptical-potential sum.

Algorithm · explicit conventions

OFUL optimistic ridge loop

The compact loop separates the state carried between rounds from the confidence maximization performed at the current round.

Ridge estimate and optimistic score. Formula renderer unavailable; readable fallback: Form the regularized Gram matrix and ridge estimate, then choose the feasible action with the largest estimated reward plus its confidence width.\[V_t=\lambda I+\sum_{s<t}x_sx_s^\top,\quad \widehat\theta_t=V_t^{-1}\sum_{s<t}x_sy_s,\quad x_t\in\operatorname*{arg\,max}_{x\in\mathcal D_t}\left(\langle\widehat\theta_t,x\rangle+\beta_t\lVert x\rVert_{V_t^{-1}}\right).\]

input: regularization λ > 0, confidence δ, feasible action sets D_t
initialize V_1 = λ I and b_1 = 0
for t = 1,…,n:
    set θ̂_t = V_t^{-1} b_t and compute confidence radius β_t
    choose a documented maximizer of <θ̂_t,x> + β_t ||x||_{V_t^{-1}}
    observe y_t; update V_{t+1} = V_t + x_t x_t^T and b_{t+1} = b_t + x_t y_t

Source/Lean boundary. The source algorithm permits time-varying feasible sets. BanditRLlib's canonical route is a finite-action measurable construction with explicit confidence, all-horizon, expectation, and stopping-time interfaces; the exact Lean statements determine the feature, regularity, and scheduling contracts.

Worked example · follow one decision

Why an unexplored direction can beat a better estimate

Use two-dimensional features with actions e₁ and e₂, regularization λ = 1, and confidence radius β₂ = 0.5. After one modest reward from e₁, OFUL compares estimated reward and directional uncertainty.

Record one observed direction
The first action is e₁ and its reward is 0.2, so only the first coordinate enters the data vector.
Worked example step 1. Formula renderer unavailable; readable fallback: The policy observes reward 0.2 after choosing the first basis vector, so the data vector is (0.2, 0).\[x_1=e_1,\qquad y_1=0.2,\qquad b_2=x_1y_1=(0.2,0)^\top.\]
See uncertainty in the Gram geometry
The observed direction receives an extra rank-one update; the untouched direction retains the larger inverse-Gram width.
Worked example step 2. Formula renderer unavailable; readable fallback: The Gram matrix is diagonal with entries 2 and 1; the estimate is (0.1, 0), and the unexplored second direction has the wider confidence norm.\[V_2=I+e_1e_1^\top=\operatorname{diag}(2,1),\quad \widehat\theta_2=V_2^{-1}b_2=(0.1,0)^\top,\quad \lVert e_1\rVert_{V_2^{-1}}=\frac1{\sqrt2}<\lVert e_2\rVert_{V_2^{-1}}=1.\]
Let optimism choose information
The small estimated advantage of e₁ is outweighed by e₂'s wider confidence interval, so the optimistic score explores e₂.
Worked example step 3. Formula renderer unavailable; readable fallback: The optimistic scores are about 0.454 for the first direction and 0.5 for the unexplored second direction, so OFUL chooses the second direction.\[U_2(e_1)=0.1+\frac{0.5}{\sqrt2}\approx0.454,\qquad U_2(e_2)=0+0.5=0.5,\qquad x_2=e_2.\]

Takeaway. OFUL explores directions, not named arms in isolation. The same inverse-Gram norm that makes e₂ attractive here is later summed by the elliptical-potential argument.

Scope. This two-dimensional calculation illustrates one optimistic score comparison. It is not a trajectory benchmark and does not instantiate every boundedness, measurability, or confidence-radius hypothesis in the compiled theorem.

Proof bridge · source to Lean

How confidence geometry pays for linear-bandit regret

OFUL replaces one confidence interval per arm by one ellipsoid for the unknown parameter. The same inverse-Gram norm measures both uncertainty and the cost charged to the trajectory.

Put the parameter in an ellipsoid
A self-normalized concentration result bounds the ridge-estimation error in the geometry accumulated from earlier features.
Step 1 equation. Formula renderer unavailable; readable fallback: The true parameter lies within beta t of the ridge estimate in the Gram-matrix norm.\[\lVert\widehat\theta_t-\theta_\star\rVert_{V_t}\le\beta_t.\]
Convert optimism into one width
Maximizing over the confidence set makes the instantaneous regret no larger than a constant multiple of the selected feature's inverse-Gram width.
Step 2 equation. Formula renderer unavailable; readable fallback: One-step regret is controlled by twice the confidence radius times the selected feature's inverse-Gram norm.\[r_t\le 2\beta_t\lVert x_t\rVert_{V_t^{-1}}.\]
Sum widths through determinant growth
The elliptical-potential lemma says that repeatedly visiting a direction increases the Gram determinant and prevents that direction from remaining wide forever.
Step 3 equation. Formula renderer unavailable; readable fallback: The sum of clipped squared confidence widths is at most twice the logarithmic growth of the Gram determinant.\[\sum_{t=1}^{n}\min\{1,\lVert x_t\rVert_{V_t^{-1}}^2\}\le 2\log\frac{\det V_{n+1}}{\det V_1}.\]
Finish with Cauchy-Schwarz
Combining the confidence radius with the potential bound yields the familiar dimension-times-square-root-horizon scale, with the source assumptions determining the logarithms and constants.
Step 4 equation. Formula renderer unavailable; readable fallback: Cumulative regret is controlled by the final confidence radius times the square root of horizon and determinant growth, giving dimension times square-root horizon up to logs.\[R_n\lesssim\beta_n\sqrt{n\log\frac{\det V_{n+1}}{\det V_1}}=\widetilde O(d\sqrt n).\]

Reading boundary. This bridge identifies the source proof joints and their local counterparts; it is not a claim that the finite-action Lean route reproduces every OFUL variant or the paper's sharp constants verbatim.

Source theorem · faithful restatement

Abbasi-Yadkori–Pál–Szepesvári, Theorem 3

Original at paper pp. 4–5 ↗

The paper combines a self-normalized confidence ellipsoid with optimism and an elliptical-potential argument.

Model: A d-dimensional stochastic linear bandit with round-dependent feasible action sets and linear conditional mean rewards.
Assumptions: The paper's preceding bounded-parameter, bounded-feature, conditionally sub-Gaussian noise, and regularization conditions hold; Theorem 3 also assumes every feasible mean reward lies in [-1,1].
Algorithm parameters: Dimension d, horizon n, feature and parameter bounds, noise scale, regularization λ, and confidence δ.
Regret notion: High-probability cumulative pseudo-regret of the OFUL policy.
Guarantee: An explicit confidence-dependent bound of order d√n up to logarithmic factors.

Source mathematical statement. Formula renderer unavailable; readable fallback: OFUL achieves dimension times square-root-horizon regret, up to logarithmic factors, under the paper's stated assumptions.\[R_n=\widetilde O\!\left(d\sqrt n\right)\quad\text{under the theorem's bounded-feature and sub-Gaussian assumptions}.\]

BanditRLlib relationship. The local finite-action scalar route compiles the confidence, optimistic policy, all-time, expected-consistency, and stopping-time interfaces under its own explicit contracts; consult the exact Lean statements for the narrower model.

The mathematical content is restated in this site's notation; wording is ours. See paper pp. 4–5 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. 4 additional dependency, extension, or research-frontier notes are grouped below.

Mathematics ↔ Lean

Elliptical-potential control of cumulative width

Lean declarationBanditRLProof.OFUL.sum_range_min_prefix_update_le_two_trace_average_log

Compiled

Plain-English statement. The cumulative clipped inverse-Gram quadratic width is at most twice a dimension-scaled logarithmic growth term.

Mathematical reading. Formula renderer unavailable; readable fallback: The cumulative clipped inverse-Gram quadratic width is at most twice a dimension-scaled logarithmic growth term.\(\sum_{t<T}\min\{1,\|x_t\|^2_{V_t^{-1}}\}\le2d\log\!\left(1+\frac{TL^2}{d\lambda}\right).\)

Intuition: Each new feature direction increases the determinant of the regularized Gram matrix; the determinant cannot grow too fast under a norm bound.
Why it is needed: This is the geometric summation step that turns per-round confidence widths into a finite linear-bandit regret scale.
Place in the proof: It is the deterministic geometric core reused by the now-compiled self-normalized confidence, finite-window regret, expected-rate, all-time, and stopping-time consumers.

Proof and Lean reading notes

Proof idea: Use the matrix determinant update identity, telescope logarithms, bound the final determinant by a trace-average inequality, and compare min(1,u) with log(1+u).
Lean reading notes: Finite-dimensionality, positive regularization, nonemptiness, and the feature norm bound are explicit. Matrix inverse and determinant side conditions are proved locally.
Teaching dependencies: No direct teaching dependency recorded.

Exact Lean statement

theorem sum_range_min_prefix_update_le_two_trace_average_log {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (history : Nat -> Feature -> Real) (T : Nat) (L2 : Real) (hL2 : 0 <= L2) (hbound : forall t : Nat, t < T -> dotProduct (history t) (history t) <= L2) : (Finset.range T).sum (fun t => min 1 (dotProduct (history t) (Matrix.mulVec ((regularizedPrefixFeatureGram lambda history t)⁻¹) (history t)))) <= 2 * ((Fintype.card Feature : Real) * Real.log (1 + (T * L2) / ((Fintype.card Feature : Real) * lambda)))

Open in the declaration catalog Open source at line 2054

Mathematics ↔ Lean

Fixed-horizon ridge confidence ellipsoid

Lean declarationBanditRLProof.OFUL.measure_finiteHorizonRidgeEstimate_error_matrixNorm_gt_confidenceRadius_le

Compiled

Plain-English statement. At a fixed horizon, the ridge estimator lies in its regularized confidence ellipsoid except on a set of measure at most delta.

Mathematical reading. Formula renderer unavailable; readable fallback: At a fixed horizon, the ridge estimator lies in its regularized confidence ellipsoid except on a set of measure at most delta.\(\Pr\{\|\widehat\theta_n-\theta_\star\|_{V_n}>\beta_n(\delta)\}\le\delta.\)

Intuition: The estimation error splits into self-normalized noise plus deterministic ridge bias, both measured in the same positive-definite Gram geometry.
Why it is needed: Optimism needs a confidence set for the unknown linear parameter, not only a scalar reward tail.
Place in the proof: It consumes the Gaussian-mixture self-normalized bound and feeds the optimistic finite-action score.

Proof and Lean reading notes

Proof idea: Rewrite the ridge error into noise and regularization terms, control the first by the determinant-ratio tail, bound the second by the supplied bias radius, and use the matrix-norm triangle inequality.
Lean reading notes: Positive definiteness, feature/noise measurability, adaptation, response identity, positive variance scale, delta domain, and the bias bound are explicit in the signature.
Teaching dependencies: BanditRLProof.OFUL.fixedDirectionCompensatedScore_hasMGFUpperBoundAt

Exact Lean statement

theorem measure_finiteHorizonRidgeEstimate_error_matrixNorm_gt_confidenceRadius_le [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (thetaStar : Feature -> Real) (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (response noise : Nat -> Omega -> Real) (R : Real) (hR : 0 < R) (projectionBound : EuclideanSpace Real Feature -> Nat -> Real) (hfeature : forall i j, StronglyMeasurable[F i] (fun omega => feature i omega j)) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall theta i, 0 <= projectionBound theta i) (hprojectionBound : forall theta i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound theta i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (constantSquaredVarianceProxy R i) mu) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (biasRadius : Real) (hresponse : forall omega i, i < n -> response i omega = dotProduct thetaStar (feature i omega) + noise i omega) (hbias : forall omega, matrixNorm (V0 + finiteHorizonFeatureGram feature n omega) ((V0 + finiteHorizonFeatureGram feature n omega)⁻¹.mulVec (V0.mulVec thetaStar)) <= biasRadius) : mu {omega | matrixNorm (V0 + finiteHorizonFeatureGram feature n omega) (finiteHorizonRidgeEstimate V0 feature response n omega - thetaStar) > finiteHorizonConfidenceRadius V0 feature R delta biasRadius n omega} <= ENNReal.ofReal delta

Open in the declaration catalog Open source at line 401

Mathematics ↔ Lean

A measurable horizon-free optimistic linear-bandit policy

Lean declarationBanditRLProof.OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm

Compiled

Plain-English statement. One measurable history algorithm chooses the strict-fold maximizer of a ridge estimate plus a telescoping-scheduled confidence width at every round, without taking a terminal horizon.

Mathematical reading. Formula renderer unavailable; readable fallback: One measurable history algorithm chooses the strict-fold maximizer of a ridge estimate plus a telescoping-scheduled confidence width at every round, without taking a terminal horizon.\(A_t\in\arg\max_{a\in[K]}\{\langle\widehat\theta_t,x_a\rangle+\beta_t(\delta_t)\|x_a\|_{V_t^{-1}}\}.\)

Intuition: The schedule is indexed by the current history length, so the same policy can run forever while every finite prefix is analyzed later.
Why it is needed: A genuine all-time result needs one policy and one trajectory law rather than a different policy for each stopping horizon.
Place in the proof: It is the algorithm node between measurable optimistic selection and the generated all-time confidence/regret consumers.

Proof and Lean reading notes

Proof idea: Build ridge statistics from the finite history, compute scheduled scores for every finite arm, and use the measurable strict-improvement fold to choose a deterministic tie-breaking maximizer.
Lean reading notes: The arguments include arm count, regularization, features, noise scale, outer confidence budget, and parameter-radius bound, but no terminal horizon. The definition itself is not a regret theorem.
Teaching dependencies: BanditRLProof.OFUL.measure_finiteHorizonRidgeEstimate_error_matrixNorm_gt_confidenceRadius_le

Exact Lean statement

noncomputable def finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) : Thompson.HistoryAlgorithm (Fin K) Real

Open in the declaration catalog Open source at line 159

Mathematics ↔ Lean

One event controls OFUL regret at every horizon

Lean declarationBanditRLProof.OFUL.telescopingCanonicalStandardHighProbabilityPseudoRegret_nonneg_and_allHorizon_tail_le_explicitBound_of_linearSubgaussianEnvironment_of_featureBound_le_regularization

Compiled

Plain-English statement. One failure event on the canonical horizon-free OFUL trajectory controls the explicit nonnegative pseudo-regret bound at every finite horizon.

Mathematical reading. Formula renderer unavailable; readable fallback: One failure event on the canonical horizon-free OFUL trajectory controls the explicit nonnegative pseudo-regret bound at every finite horizon.\(\Pr\{\exists T,\;R_T> B_T(\delta)\}\le\delta.\)

Intuition: Outside the all-time confidence failure set, optimism bounds every instantaneous gap by a selected confidence width; elliptical potential sums those widths for any prefix.
Why it is needed: It is the generated one-policy all-horizon endpoint required by the Chapter 5 completion contract.
Place in the proof: It joins all-time ridge confidence, finite-action optimism, selected-width summation, and the initial-round gap bound.

Proof and Lean reading notes

Proof idea: Transport confidence to each selected action, convert optimism to gap bounds, sum widths with Cauchy-Schwarz and the log-determinant inequality, then show every violation belongs to the all-time failure event.
Lean reading notes: Finite actions/features, positive regularization/noise scale, 0<delta<=1, nonnegative S and L2, L2<=lambda, a feature-square bound, an optimal arm, and the canonical kernel-law producer are explicit. Sharp/minimax constants are not claimed.
Teaching dependencies: BanditRLProof.OFUL.measure_telescopingCanonicalHistoryTrajectory_allTimeConfidenceFailureSet_le_of_linearSubgaussianEnvironment, BanditRLProof.OFUL.sum_range_min_prefix_update_le_two_trace_average_log

Exact Lean statement

theorem telescopingCanonicalStandardHighProbabilityPseudoRegret_nonneg_and_allHorizon_tail_le_explicitBound_of_linearSubgaussianEnvironment_of_featureBound_le_regularization {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (hK : 0 < K) (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (hR : 0 < R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (S : Real) (hS : 0 <= S) (environment : Thompson.HistoryEnvironment (Fin K) Real) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (best : Fin K) (hbest : IsOptimalLinearArm thetaStar actionFeature best) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : (forall horizon trajectory, 0 <= canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory) /\ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment (telescopingCanonicalExplicitHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 best) <= ENNReal.ofReal delta

Open in the declaration catalog Open source at line 225

Explore 4 additional Lean teaching notes

Mathematics ↔ Lean

Every fixed predictable feature direction turns the centered reward noise…

Lean declarationBanditRLProof.OFUL.fixedDirectionCompensatedScore_hasMGFUpperBoundAt

Compiled

Plain-English statement. Every fixed predictable feature direction turns the centered reward noise into a compensated exponential supermartingale-style MGF bound.

Mathematical reading. Formula renderer unavailable; readable fallback: Every fixed predictable feature direction turns the centered reward noise into a compensated exponential supermartingale-style MGF bound.\(\mathbb E\exp\!\left(\sum_{i<n}\langle\theta,x_i\rangle\varepsilon_i-\tfrac12\sigma_i^2\langle\theta,x_i\rangle^2\right)\le1.\)

Intuition: The direction is known from the past, so conditional sub-Gaussian control survives multiplication by that predictable coefficient.
Why it is needed: This scalar statement is what the Gaussian-mixture argument integrates to obtain a vector self-normalized confidence event.
Place in the proof: It connects the generated conditional reward law to the self-normalized matrix layer.

Proof and Lean reading notes

Proof idea: Apply the conditional sub-Gaussian MGF lemma at each round, use predictable measurability and the projection bound, and assemble the compensated sum.
Lean reading notes: The theorem explicitly requires a probability measure, filtration, strong adaptation, predictable projections, nonnegative projection bounds, and per-round conditional MGF witnesses. It is not an independence-only Hoeffding statement.
Teaching dependencies: BanditRLProof.ConditionalExpectationReward.historyStepKernelFamily_centeredReward_succ_hasCondSubgaussianMGF_trajMeasure

Exact Lean statement

theorem fixedDirectionCompensatedScore_hasMGFUpperBoundAt {Omega : Type v} {Feature : Type w} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (theta : Feature -> Real) (projectionBound : Nat -> Real) (hprojection : forall i, StronglyMeasurable[F i] (fun omega => dotProduct theta (feature i omega))) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall i, 0 <= projectionBound i) (hprojectionBound : forall i omega, |dotProduct theta (feature i omega)| <= projectionBound i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (varianceProxy i) mu) : Concentration.HasMGFUpperBoundAt (fun omega => (Finset.range (n + 1)).sum (fun t => match t with | 0 => 0 | i + 1 => dotProduct theta (feature i omega) * noise i omega - (((varianceProxy i : NNReal) : Real) * (dotProduct theta (feature i omega)) ^ 2 / 2))) 1 0 mu

Open in the declaration catalog Open source at line 259

Mathematics ↔ Lean

On the trajectory generated by the horizon-free telescoping OFUL policy…

Lean declarationBanditRLProof.OFUL.measure_telescopingCanonicalHistoryTrajectory_allTimeConfidenceFailureSet_le_of_linearSubgaussianEnvironment

Compiled

Plain-English statement. On the trajectory generated by the horizon-free telescoping OFUL policy, the union of ridge-confidence failures over all finite times has measure at most the outer confidence budget.

Mathematical reading. Formula renderer unavailable; readable fallback: On the trajectory generated by the horizon-free telescoping OFUL policy, the union of ridge-confidence failures over all finite times has measure at most the outer confidence budget.\(\Pr\{\exists n,\;\theta_\star\notin\mathcal C_n(\delta_n)\}\le\delta.\)

Intuition: The confidence shares telescope, so countably many fixed-time ellipsoid failures fit inside one budget without changing the policy later.
Why it is needed: This is the same-process producer needed before any all-horizon optimism or stopping argument is sound.
Place in the proof: It consumes the kernel-level linear sub-Gaussian producer and is the probability parent of the all-horizon regret terminal.

Proof and Lean reading notes

Proof idea: Convert the environment's initial/successor centered MGF laws into the canonical predictable residual source, apply every scheduled fixed-time ridge tail, and sum the telescoping shares.
Lean reading notes: CanonicalLinearSubgaussianEnvironmentLaw stores theta norm and kernel MGF laws, not this conclusion. The displayed trajectory measure uses exactly finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm.
Teaching dependencies: BanditRLProof.OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm, BanditRLProof.OFUL.CanonicalLinearSubgaussianEnvironmentLaw

Exact Lean statement

theorem measure_telescopingCanonicalHistoryTrajectory_allTimeConfidenceFailureSet_le_of_linearSubgaussianEnvironment {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (hK : 0 < K) (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (hR : 0 < R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment (allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta) <= ENNReal.ofReal delta

Open in the declaration catalog Open source at line 1279

Mathematics ↔ Lean

For a finite canonical stopping time whose round count has a finite second…

Lean declarationBanditRLProof.OFUL.integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_stoppingTimeRoundSecondMoment_add_initialGap_mul_sqrt_stoppingTimeRoundSecondMoment_mul_sqrt_delta_and_stoppedViolation_measure_le_of_squareIntegrableFiniteStoppingTime

Compiled

Plain-English statement. For a finite canonical stopping time whose round count has a finite second moment, the stopped OFUL pseudo-regret is integrable and its expectation is controlled by that second moment plus an explicit bad-event term.

Mathematical reading. Formula renderer unavailable; readable fallback: For a finite canonical stopping time whose round count has a finite second moment, the stopped OFUL pseudo-regret is integrable and its expectation is controlled by that second moment plus an explicit bad-event term.\(0\le\mathbb E R_\tau\le C\,\mathbb E(\tau+1)^2+G\sqrt{\mathbb E(\tau+1)^2}\sqrt\delta,\quad\Pr(B_\tau)\le\delta.\)

Intuition: The pathwise all-horizon budget can be evaluated at a random time; Cauchy-Schwarz controls the rare bad-event contribution using square integrability.
Why it is needed: Random stopping is not justified by substituting a random horizon into a deterministic theorem unless filtration, measurability, finiteness, and integrability are preserved.
Place in the proof: It is the strongest random-horizon consumer inside the scoped Chapter 5 completion route.

Proof and Lean reading notes

Proof idea: Use stopped-value measurability and adaptation, split good and bad trajectories, integrate the quadratic envelope at tau, and bound the bad indicator by the stopping-round second moment times sqrt(delta).
Lean reading notes: The theorem explicitly requires the canonical all-round filtration, IsStoppingTime, and SquareIntegrableFiniteStoppingTime, which includes a.e. finiteness and integrability/second-moment control. It is not universal optional stopping or an almost-sure consistency theorem.
Teaching dependencies: BanditRLProof.OFUL.telescopingCanonicalStandardHighProbabilityPseudoRegret_nonneg_and_allHorizon_tail_le_explicitBound_of_linearSubgaussianEnvironment_of_featureBound_le_regularization

Exact Lean statement

theorem integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_stoppingTimeRoundSecondMoment_add_initialGap_mul_sqrt_stoppingTimeRoundSecondMoment_mul_sqrt_delta_and_stoppedViolation_measure_le_of_squareIntegrableFiniteStoppingTime {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (hK : 0 < K) (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (hR : 0 < R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (S : Real) (hS : 0 <= S) (environment : Thompson.HistoryEnvironment (Fin K) Real) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (best : Fin K) (hbest : IsOptimalLinearArm thetaStar actionFeature best) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) (tau : (Nat -> Fin K × Real) -> WithTop Nat) (htau : IsStoppingTime (canonicalHistoryTrajectoryAllRoundFiltration (K := K)) tau) (hstop : SquareIntegrableFiniteStoppingTime (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment) tau) : let mu := Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm hK lambda actionFeature R delta S) environment let stoppedRegret := stoppedValue (fun horizon trajectory => canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory) tau let bad := telescopingCanonicalExplicitHighProbabilityPseudoRegretStoppedViolationSet lambda thetaStar actionFeature R delta S L2 best tau 0 <= integral mu stoppedRegret ∧ integral mu stoppedRegret <= telescopingHighProbabilityPseudoRegretQuadraticCoefficient (Feature := Feature) R delta lambda S L2 * stoppingTimeRoundSecondMoment mu tau hstop + standardScalarInitialGapBound S L2 * Real.sqrt (stoppingTimeRoundSecondMoment mu tau hstop) * Real.sqrt delta ∧ mu bad <= ENNReal.ofReal delta

Open in the declaration catalog Open source at line 44

Mathematics ↔ Lean

For the canonical finite-action scalar linear-bandit model, the compiled…

Lean declarationBanditRLProof.OFUL.canonicalStandardExpectedAveragePseudoRegret_tendsto_zero

Compiled

Plain-English statement. For the canonical finite-action scalar linear-bandit model, the compiled expected pseudo-regret bound divided by the number of rounds converges to zero.

Mathematical reading. Formula renderer unavailable; readable fallback: For the canonical finite-action scalar linear-bandit model, the compiled expected pseudo-regret bound divided by the number of rounds converges to zero.\(\displaystyle \frac{\mathbb E R_T}{T+1}\longrightarrow 0.\)

Intuition: The finite-horizon regret grows strictly slower than the horizon, so the expected cost per decision vanishes even though cumulative regret can still grow.
Why it is needed: A finite-time square-root-log bound is useful quantitatively; this theorem records its asymptotic statistical meaning as a Lean limit statement.
Place in the proof: It is the fixed-model asymptotic consumer of the compiled ridge-confidence, optimism, width-summation, and bad-event expectation route.

Proof and Lean reading notes

Proof idea: First prove the explicit expected bound is little-o of the natural horizon scale, transfer the bound to the canonical generated regret, and rewrite division as the expected-average definition.
Lean reading notes: The limit is for the horizon-indexed generated family in the theorem's fixed model. It is not a one-policy anytime, pathwise, minimax, or uniform-over-parameter consistency claim.
Teaching dependencies: BanditRLProof.OFUL.sum_range_min_prefix_update_le_two_trace_average_log

Exact Lean statement

theorem canonicalStandardExpectedAveragePseudoRegret_tendsto_zero {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (hK : 0 < K) (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (hR : 0 < R) (S : Real) (hS : 0 <= S) (environment : Thompson.HistoryEnvironment (Fin K) Real) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (best : Fin K) (hbest : IsOptimalLinearArm thetaStar actionFeature best) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : Tendsto (canonicalStandardExpectedAveragePseudoRegret hK lambda thetaStar actionFeature R S environment best) atTop (nhds 0)

Open in the declaration catalog Open source at line 94

Maintainer contract

Open the canonical completion definition and blockers

Complete in the canonical textbook scope when finite-dimensional Gram geometry, rank-one determinant and log-determinant arguments, conditional-MGF/self-normalized ridge confidence, regularization bias, measurable finite-action optimism, and a kernel-law-produced generated trajectory compile; one horizon-free telescoping policy must carry all-time confidence, all-horizon high-probability pseudo-regret, and bounded plus square-integrable stopping-time consumers, while the distinct horizon-indexed fixed-model family carries finite-horizon expectation and expected-average consistency. One public external canary must distinguish and type both families.

Remaining blockers

No remaining blocker inside this canonical scope: Tests/BookMapChaptersFiveAndSixCanary.lean gives full-conclusion typed applications for the same horizon-free telescoping policy/environment/trajectory chain through all-horizon and both stopping consumers, and separately types the horizon-indexed expected-consistency family. The items below are explicitly out-of-scope extensions.

Chapter implementation status

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

Open 8 implementation records8 compiled · 0 partial · 0 blocked · 0 planned

Milestone	Status	Lean declaration	Remaining gap
Logarithmic elliptical-potential inequality	Compiled	`BanditRLProof.OFUL.sum_range_min_prefix_update_le_two_trace_average_log`	—
Conditional-MGF to ridge confidence ellipsoid	Compiled	`BanditRLProof.OFUL.fixedDirectionCompensatedScore_hasMGFUpperBoundAtBanditRLProof.OFUL.measure_finiteHorizonRidgeEstimate_error_matrixNorm_gt_confidenceRadius_le`	—
Measurable horizon-free optimistic policy	Compiled	`BanditRLProof.OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm`	—
One-policy all-time OFUL confidence	Compiled	`BanditRLProof.OFUL.measure_telescopingCanonicalHistoryTrajectory_allTimeConfidenceFailureSet_le_of_linearSubgaussianEnvironment`	—
One-policy all-horizon OFUL pseudo-regret	Compiled	`BanditRLProof.OFUL.telescopingCanonicalStandardHighProbabilityPseudoRegret_nonneg_and_allHorizon_tail_le_explicitBound_of_linearSubgaussianEnvironment_of_featureBound_le_regularization`	—
Fixed-model OFUL expected-average consistency	Compiled	`BanditRLProof.OFUL.canonicalStandardExpectedAveragePseudoRegret_tendsto_zero`	—
Bounded stopping-time OFUL expected regret	Compiled	`BanditRLProof.OFUL.integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_endpoint_add_envelope_mul_delta_of_linearSubgaussianEnvironment_of_featureBound_le_regularization`	—
Square-integrable random-horizon OFUL expected regret	Compiled	`BanditRLProof.OFUL.integral_stoppedValue_canonicalStandardHighProbabilityPseudoRegret_nonneg_and_le_quadraticCoefficient_mul_stoppingTimeRoundSecondMoment_add_initialGap_mul_sqrt_stoppingTimeRoundSecondMoment_mul_sqrt_delta_and_stoppedViolation_measure_le_of_squareIntegrableFiniteStoppingTime`	—

Open boundaries

Contextual or time-varying action sets, dynamic linear bandits, paper-sharp/minimax constants, uniform-over-parameter guarantees, and infinite-dimensional Hilbert-space OFUL remain extensions.
Arbitrary history environments without a centered conditional-MGF producer, pathwise/almost-sure/universal optional-stopping consistency, and full primal-dual Bandits-with-Knapsacks remain outside the completed scope.
Budget-forced schedules compile under explicit contracts, but they are not labeled as a complete BwK theorem.

All Lean modules in this chapter

Open the complete module list (65 modules)

Module	Declarations	Project imports	Status
`BanditRLProof.OFULAllTimeConfidence`	17	1	Compiled
`BanditRLProof.OFULConcreteHistoryRidgeSelection`	26	1	Compiled
`BanditRLProof.OFULConfidenceEllipsoid`	18	1	Compiled
`BanditRLProof.OFULEllipticalPotential`	115	0	Compiled
`BanditRLProof.OFULEllipticalPotentialFoundation`	1	1	Compiled
`BanditRLProof.OFULExpectedRegret`	20	1	Compiled
`BanditRLProof.OFULExpectedRegretAsymptotics`	7	1	Compiled
`BanditRLProof.OFULExpectedRegretConsistency`	5	1	Compiled
`BanditRLProof.OFULExpectedRegretRate`	6	1	Compiled
`BanditRLProof.OFULFiniteActionOptimism`	16	1	Compiled
`BanditRLProof.OFULFiniteHorizonScoreGram`	14	2	Compiled
`BanditRLProof.OFULGaussianCovarianceMixture`	9	1	Compiled
`BanditRLProof.OFULGaussianEvaluatedMixture`	6	1	Compiled
`BanditRLProof.OFULGaussianMixture`	4	1	Compiled
`BanditRLProof.OFULGaussianMixtureMeasurability`	7	1	Compiled
`BanditRLProof.OFULGaussianSpectralMixture`	8	1	Compiled
`BanditRLProof.OFULGeneratedTrajectoryConfidenceGap`	13	2	Compiled
`BanditRLProof.OFULGeneratedTrajectoryPredictableConfidence`	20	2	Compiled
`BanditRLProof.OFULGeneratedTrajectoryRadiusWidth`	14	2	Compiled
`BanditRLProof.OFULGeneratedTrajectoryUniformConfidence`	4	1	Compiled
`BanditRLProof.OFULHighProbabilityRegretRate`	6	1	Compiled
`BanditRLProof.OFULHistoryEnvironmentRewardLaw`	12	2	Compiled
`BanditRLProof.OFULInitialRoundGap`	9	1	Compiled
`BanditRLProof.OFULMeasurableRecursiveSelection`	9	3	Compiled
`BanditRLProof.OFULNormalizedRadiusWidth`	5	1	Compiled
`BanditRLProof.OFULScalarRegularizationBias`	6	1	Compiled
`BanditRLProof.OFULScheduledAEAlignedWindowPositiveActionCostBudgetExhaustionExpectedRegret`	11	2	Compiled
`BanditRLProof.OFULScheduledAllHorizonAllRoundGap`	7	2	Compiled
`BanditRLProof.OFULScheduledAllHorizonCumulativeGap`	12	2	Compiled
`BanditRLProof.OFULScheduledAllHorizonHighProbabilityRegretRate`	9	1	Compiled
`BanditRLProof.OFULScheduledAllTimeConfidence`	33	2	Compiled
`BanditRLProof.OFULScheduledBlockStartForcedActionChargeBound`	8	1	Compiled
`BanditRLProof.OFULScheduledBlockStartForcedAllTimeConfidence`	21	2	Compiled
`BanditRLProof.OFULScheduledBlockStartForcedHistoryAlgorithm`	11	1	Compiled
`BanditRLProof.OFULScheduledBlockStartForcedHorizonIndexedHighProbabilityRegretRate`	5	1	Compiled
`BanditRLProof.OFULScheduledBlockStartForcedHorizonWindowFiniteHorizonTail`	6	1	Compiled
`BanditRLProof.OFULScheduledBlockStartForcedPositiveActionCostBudgetExhaustionExpectedRegret`	6	1	Compiled
`BanditRLProof.OFULScheduledBlockStartForcedPseudoRegretDecomposition`	13	1	Compiled
`BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegret`	9	2	Compiled
`BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegretAsymptotics`	4	2	Compiled
`BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegretConsistency`	4	2	Compiled
`BanditRLProof.OFULScheduledBoundedStoppingTimeExpectedRegretRate`	7	2	Compiled
`BanditRLProof.OFULScheduledBoundedStoppingTimeHighProbabilityRegretRate`	13	1	Compiled
`BanditRLProof.OFULScheduledBudgetExhaustionExpectedRegret`	6	2	Compiled
`BanditRLProof.OFULScheduledCumulativeAlignedWindowPositiveCostBudgetExhaustionExpectedRegret`	7	1	Compiled
`BanditRLProof.OFULScheduledCumulativePositiveCostBudgetExhaustionExpectedRegret`	6	1	Compiled
`BanditRLProof.OFULScheduledPositiveActionCostBudgetExhaustionExpectedRegret`	8	1	Compiled
`BanditRLProof.OFULScheduledPowerOfTwoForcedAllTimeConfidence`	13	2	Compiled
`BanditRLProof.OFULScheduledPowerOfTwoForcedHighProbabilityAverageConsistency`	4	1	Compiled
`BanditRLProof.OFULScheduledPowerOfTwoForcedHighProbabilityAverageRegret`	6	2	Compiled
`BanditRLProof.OFULScheduledPowerOfTwoForcedHighProbabilityRegretRate`	9	2	Compiled
`BanditRLProof.OFULScheduledPowerOfTwoForcedHistoryAlgorithm`	7	2	Compiled
`BanditRLProof.OFULScheduledPowerOfTwoForcedIndexCount`	7	0	Compiled
`BanditRLProof.OFULScheduledPowerOfTwoForcedPseudoRegretDecomposition`	10	1	Compiled
`BanditRLProof.OFULScheduledPowerOfTwoForcedScalarChargeBound`	6	1	Compiled
`BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegret`	9	1	Compiled
`BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretClosed`	7	1	Compiled
`BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretExactMoment`	3	1	Compiled
`BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretRate`	5	1	Compiled
`BanditRLProof.OFULScheduledUnboundedStoppingTimeExpectedRegretSecondMoment`	2	1	Compiled
`BanditRLProof.OFULScheduledUnitGrowthBudgetExhaustionExpectedRegret`	5	1	Compiled
`BanditRLProof.OFULSelectedWidthSummation`	7	2	Compiled
`BanditRLProof.OFULSelfNormalizedConfidence`	4	3	Compiled
`BanditRLProof.OFULSelfNormalizedMarkov`	12	1	Compiled
`BanditRLProof.OFULUniformTimeConfidence`	7	2	Compiled