4. UCB: confidence events to regret

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.

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

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

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.

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

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

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.

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

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

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

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

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)