BanditRLProof.OFULExpectedRegret

The complete finite-window linear gap along one canonical trajectory.

noncomputable def canonicalHistoryTrajectorySumRangeAllGap {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (horizon : Nat) (comparator : Nat -> Fin K) (trajectory : Nat -> Fin K × Real) : Real

A fixed arm maximizes the true linear value over the finite action set.

def IsOptimalLinearArm {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (best : Fin K) : Prop

Gap to an optimal fixed arm is pointwise nonnegative.

theorem canonicalHistoryTrajectorySumRangeAllFixedComparatorGap_nonneg {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (horizon : Nat) (best : Fin K) (hbest : IsOptimalLinearArm thetaStar actionFeature best) (trajectory : Nat -> Fin K × Real) : 0 <= canonicalHistoryTrajectorySumRangeAllGap thetaStar actionFeature horizon (fun _t => best) trajectory

The all-round cumulative linear gap is measurable on trajectory space.

theorem measurable_canonicalHistoryTrajectorySumRangeAllGap {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (horizon : Nat) (comparator : Nat -> Fin K) : Measurable (canonicalHistoryTrajectorySumRangeAllGap thetaStar actionFeature horizon comparator)

The absolute linear-value difference between any two bounded arm features is at most `2*S*sqrt L2`.

theorem abs_linearValue_sub_linearValue_le_two_mul_parameterFeatureBound {Feature : Type u} [Fintype Feature] (theta x y : Feature -> Real) (S L2 : Real) (hS : 0 <= S) (htheta : euclideanLength theta <= S) (hx : dotProduct x x <= L2) (hy : dotProduct y y <= L2) : |linearValue theta x - linearValue theta y| <= 2 * S * Real.sqrt L2

Uniform absolute envelope for the complete finite-window cumulative gap.

noncomputable def standardScalarAllRoundGapEnvelope (S : Real) (horizon : Nat) (L2 : Real) : Real

Every trajectory satisfies the deterministic all-round gap envelope.

theorem abs_canonicalHistoryTrajectorySumRangeAllGap_le_envelope {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (S : Real) (hS : 0 <= S) (horizon : Nat) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (comparator : Nat -> Fin K) (htheta : euclideanLength thetaStar <= S) (trajectory : Nat -> Fin K × Real) : |canonicalHistoryTrajectorySumRangeAllGap thetaStar actionFeature horizon comparator trajectory| <= standardScalarAllRoundGapEnvelope S horizon L2

The deterministic all-round gap envelope is nonnegative.

theorem standardScalarAllRoundGapEnvelope_nonneg (S : Real) (hS : 0 <= S) (horizon : Nat) (L2 : Real) : 0 <= standardScalarAllRoundGapEnvelope S horizon L2

The standard all-round high-probability budget is nonnegative.

theorem standardScalarAllRoundGapBound_nonneg {Feature : Type u} [Fintype Feature] (R delta lambda S : Real) (hS : 0 <= S) (horizon : Nat) (L2 : Real) : 0 <= standardScalarAllRoundGapBound (Feature

The complete finite-window cumulative gap is integrable under a finite measure.

theorem integrable_canonicalHistoryTrajectorySumRangeAllGap {K : Nat} {Feature : Type u} [Fintype Feature] (mu : Measure (Nat -> Fin K × Real)) [IsFiniteMeasure mu] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (S : Real) (hS : 0 <= S) (horizon : Nat) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (comparator : Nat -> Fin K) (htheta : euclideanLength thetaStar <= S) : Integrable (canonicalHistoryTrajectorySumRangeAllGap thetaStar actionFeature horizon comparator) mu

The named violation set is measurable.

theorem measurableSet_canonicalHistoryTrajectorySumRangeAllGapStandardViolationSet {K : Nat} {Feature : Type u} [Fintype Feature] (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (horizon : Nat) (L2 : Real) (comparator : Nat -> Fin K) : MeasurableSet (canonicalHistoryTrajectorySumRangeAllGapStandardViolationSet lambda thetaStar actionFeature R delta S horizon L2 comparator)

Generic expectation assembly: the all-round gap is charged by the standard budget off the violation set and by the deterministic envelope on it.

theorem integral_canonicalHistoryTrajectorySumRangeAllGap_le_standard_add_envelope_mul_real_measure {K : Nat} {Feature : Type u} [Fintype Feature] (mu : Measure (Nat -> Fin K × Real)) [IsProbabilityMeasure mu] (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (hS : 0 <= S) (horizon : Nat) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (comparator : Nat -> Fin K) (htheta : euclideanLength thetaStar <= S) : integral mu (canonicalHistoryTrajectorySumRangeAllGap thetaStar actionFeature horizon comparator) <= standardScalarAllRoundGapBound (Feature

Finite-window expected cumulative linear-gap theorem for the canonical OFUL trajectory. The additive bad-event contribution is the deterministic all-round envelope times `delta`.

theorem integral_canonicalHistoryTrajectorySumRangeAllGap_le_standard_add_envelope_mul_delta_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) (horizon : Nat) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (comparator : Nat -> Fin K) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : integral (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S) environment) (canonicalHistoryTrajectorySumRangeAllGap thetaStar actionFeature horizon comparator) <= standardScalarAllRoundGapBound (Feature

Fixed-comparator form of the expected cumulative linear-gap theorem, matching the usual stochastic linear-bandit pseudo-regret surface.

theorem integral_canonicalHistoryTrajectorySumRangeAllFixedComparatorGap_le_standard_add_envelope_mul_delta_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) (horizon : Nat) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (best : Fin K) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : integral (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S) environment) (canonicalHistoryTrajectorySumRangeAllGap thetaStar actionFeature horizon (fun _t => best)) <= standardScalarAllRoundGapBound (Feature

Expected finite-window OFUL pseudo-regret theorem for a certified optimal fixed arm. The conjunction records both nonnegativity and the explicit upper bound.

theorem integral_canonicalHistoryTrajectoryPseudoRegret_nonneg_and_le_standard_add_envelope_mul_delta_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) (horizon : Nat) (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) : let expectedPseudoRegret := integral (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S) environment) (canonicalHistoryTrajectorySumRangeAllGap thetaStar actionFeature horizon (fun _t => best)) 0 <= expectedPseudoRegret ∧ expectedPseudoRegret <= standardScalarAllRoundGapBound (Feature

Canonical horizon-tuned outer failure budget for expected regret.

noncomputable def standardExpectedRegretDelta (horizon : Nat) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem standardExpectedRegretDelta_pos (horizon : Nat) : 0 < standardExpectedRegretDelta horizon

No declaration docstring is present; use the chapter context and exact statement below.

theorem standardExpectedRegretDelta_le_one (horizon : Nat) : standardExpectedRegretDelta horizon <= 1

At `delta_T=1/(T+1)`, the bad-event envelope charge is one arm-gap envelope.

theorem standardScalarAllRoundGapEnvelope_mul_standardExpectedRegretDelta (S : Real) (horizon : Nat) (L2 : Real) : standardScalarAllRoundGapEnvelope S horizon L2 * standardExpectedRegretDelta horizon = standardScalarInitialGapBound S L2

Horizon-tuned finite-window expected OFUL pseudo-regret corollary obtained by choosing the outer failure budget `delta_T=1/(T+1)`. The algorithm receives the local parameter `delta_T/(T+1)=1/(T+1)^2`, and the bad-event expectation contributes exactly one additional `2*S*sqrt L2` charge.

theorem integral_canonicalHistoryTrajectoryPseudoRegret_nonneg_and_le_standardExpectedBound_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) (S : Real) (hS : 0 <= S) (environment : Thompson.HistoryEnvironment (Fin K) Real) (horizon : Nat) (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) : let delta := standardExpectedRegretDelta horizon let expectedPseudoRegret := integral (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S) environment) (canonicalHistoryTrajectorySumRangeAllGap thetaStar actionFeature horizon (fun _t => best)) 0 <= expectedPseudoRegret ∧ expectedPseudoRegret <= standardScalarAllRoundGapBound (Feature