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

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

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

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

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

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

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

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.

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

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

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.

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

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

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.

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

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

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

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

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

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.

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

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

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.

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

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)