BanditRLProof.OFULScheduledPowerOfTwoForcedAllTimeConfidence

Scheduled radius-width charge over nonforced successor actions.

noncomputable def powerOfTwoOptimisticSuccessorRadiusWidthCharge {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (horizon : Nat) (trajectory : Nat -> Fin K × Real) : Real

On the all-time confidence event, the nonforced successor pseudo-regret is bounded by its matching scheduled radius-width charge.

theorem powerOfTwoOptimisticSuccessorPseudoRegret_le_radiusWidthCharge_ae_of_not_mem_allTimeConfidenceFailure {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 delta S : Real) (forcedAction : Nat -> Fin K) (environment : Thompson.HistoryEnvironment (Fin K) Real) (horizon : Nat) (best : Fin K) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment, trajectory ∉ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta -> powerOfTwoOptimisticSuccessorPseudoRegret thetaStar actionFeature best horizon trajectory <= powerOfTwoOptimisticSuccessorRadiusWidthCharge lambda actionFeature R delta S horizon trajectory

On the confidence event, complete pseudo-regret is bounded by the initial gap, generated forced charge, and nonforced radius-width charge.

theorem canonicalStandardHighProbabilityPseudoRegret_le_initial_add_powerOfTwoForced_add_radiusWidthCharge_ae_of_not_mem_allTimeConfidenceFailure {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 delta S : Real) (forcedAction : Nat -> Fin K) (environment : Thompson.HistoryEnvironment (Fin K) Real) (horizon : Nat) (best : Fin K) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment, trajectory ∉ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta -> canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory <= (linearValue thetaStar (actionFeature best) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory 0))) + powerOfTwoForcedSuccessorPseudoRegret thetaStar actionFeature best horizon trajectory + powerOfTwoOptimisticSuccessorRadiusWidthCharge lambda actionFeature R delta S horizon trajectory

The confidence-event finite-horizon bound with the forced charge written directly in terms of the prescribed actions.

theorem canonicalStandardHighProbabilityPseudoRegret_le_initial_add_powerOfTwoForcedActionCharge_add_radiusWidthCharge_ae_of_not_mem_allTimeConfidenceFailure {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 delta S : Real) (forcedAction : Nat -> Fin K) (environment : Thompson.HistoryEnvironment (Fin K) Real) (horizon : Nat) (best : Fin K) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment, trajectory ∉ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta -> canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory <= (linearValue thetaStar (actionFeature best) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory 0))) + powerOfTwoForcedActionSuccessorPseudoRegret thetaStar actionFeature best forcedAction horizon + powerOfTwoOptimisticSuccessorRadiusWidthCharge lambda actionFeature R delta S horizon trajectory

The linear environment law supplies the residual law for this selector.

noncomputable def canonicalPowerOfTwoForcedPredictableScalarRidgeResidualLaw_of_linearSubgaussianEnvironment {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (forcedAction : Nat -> Fin K) (environment : Thompson.HistoryEnvironment (Fin K) Real) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : CanonicalDeterministicHistoryPredictableScalarRidgeResidualLaw hK thetaStar actionFeature R S (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction) (measurable_finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction) environment

Source-level all-time confidence tail for the power-of-two policy.

theorem measure_powerOfTwoForcedCanonicalHistoryTrajectory_allTimeConfidenceFailureSet_le {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) (forcedAction : Nat -> Fin K) (environment : Thompson.HistoryEnvironment (Fin K) Real) (source : CanonicalDeterministicHistoryPredictableScalarRidgeResidualLaw hK thetaStar actionFeature R S (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction) (measurable_finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction) environment) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment (allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta) <= ENNReal.ofReal delta

Environment-backed all-time confidence tail for the power-of-two policy.

theorem measure_powerOfTwoForcedCanonicalHistoryTrajectory_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) (forcedAction : Nat -> Fin K) (environment : Thompson.HistoryEnvironment (Fin K) Real) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment (allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta) <= ENNReal.ofReal delta

The nonforced charge is bounded by the full pathwise width budget.

theorem powerOfTwoOptimisticSuccessorRadiusWidthCharge_le_telescopingStandardScalarRadiusWidthBound {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (lambda : Real) (hlambda : 0 < lambda) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (hdelta : 0 < delta) (hS : 0 <= S) (horizon : Nat) (L2 : Real) (hL2 : 0 <= L2) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (hL2lambda : L2 <= lambda) (trajectory : Nat -> Fin K × Real) : powerOfTwoOptimisticSuccessorRadiusWidthCharge lambda actionFeature R delta S horizon trajectory <= telescopingStandardScalarRadiusWidthBound (Feature

The fixed initial arm has the standard deterministic gap envelope.

theorem powerOfTwoForcedCanonicalHistoryTrajectory_initialGap_le_ae {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (hS : 0 <= S) (forcedAction : Nat -> Fin K) (environment : Thompson.HistoryEnvironment (Fin K) Real) (L2 : Real) (hactionFeatureBound : forall action, dotProduct (actionFeature action) (actionFeature action) <= L2) (best : Fin K) (htheta : euclideanLength thetaStar <= S) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment, linearValue thetaStar (actionFeature best) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory 0)) <= standardScalarInitialGapBound S L2

On one all-time confidence event, every horizon is bounded by the deterministic forced charge plus the explicit telescoping OFUL rate.

theorem powerOfTwoForcedCanonicalStandardHighProbabilityPseudoRegret_le_forcedActionCharge_add_explicitBound_ae {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) (forcedAction : Nat -> Fin K) (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) (htheta : euclideanLength thetaStar <= S) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment, forall horizon, trajectory ∉ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta -> canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory <= powerOfTwoForcedActionSuccessorPseudoRegret thetaStar actionFeature best forcedAction horizon + telescopingHighProbabilityPseudoRegretBound (Feature

All-horizon violation event for the power-of-two forced policy.

noncomputable def powerOfTwoForcedCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet {K : Nat} {Feature : Type u} [Fintype Feature] (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R delta S L2 : Real) (forcedAction : Nat -> Fin K) (best : Fin K) : Set (Nat -> Fin K × Real)

Every all-horizon violation is a confidence failure almost surely.

theorem powerOfTwoForcedCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet_subset_confidenceFailure_ae {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) (forcedAction : Nat -> Fin K) (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) (htheta : euclideanLength thetaStar <= S) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment, trajectory ∈ powerOfTwoForcedCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 forcedAction best -> trajectory ∈ allTimeTelescopingScalarRidgeConfidenceFailureSet lambda thetaStar S (canonicalHistoryTrajectoryFeature actionFeature) canonicalHistoryTrajectoryResponse R delta

Complete all-horizon high-probability pseudo-regret theorem for the fixed power-of-two forced policy, with deterministic forced charge explicit.

theorem powerOfTwoForcedCanonicalStandardHighProbabilityPseudoRegret_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) (forcedAction : Nat -> Fin K) (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 (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment (powerOfTwoForcedCanonicalStandardHighProbabilityPseudoRegretAllHorizonViolationSet lambda thetaStar actionFeature R delta S L2 forcedAction best) <= ENNReal.ofReal delta