Lean module · OFUL

BanditRLProof.OFULScheduledPowerOfTwoForcedPseudoRegretDecomposition

# Pseudo-regret decomposition for power-of-two forced telescoping OFUL This module separates the complete finite-horizon pseudo-regret of the horizon-independent power-of-two forced policy into the initial action, power-of-two forced successor actions, and ordinary optimistic successor actions. The successor index `n` denotes the history used to select action `n + 1`.

Module map

Source: BanditRLProof/OFULScheduledPowerOfTwoForcedPseudoRegretDecomposition.lean
Teaching chapter: 5. OFUL, self-normalized confidence, and stopping times
Declarations: 10
Placeholders: 0

Imports

BanditRLProof.OFULScheduledPowerOfTwoForcedHistoryAlgorithm

Imported by

BanditRLProof, BanditRLProof.OFULScheduledPowerOfTwoForcedAllTimeConfidence

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

theorem BanditRLProof.OFUL.finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction_eq_of_not_forced Compiled

Away from forced indices, the modified selector is the telescoping selector.

theorem finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction_eq_of_not_forced {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (forcedAction : Nat -> Fin K) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (hnonforced : ¬ isPowerOfTwoForcedIndex n) : finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction n history = finiteHistoryTelescopingScalarRidgeOptimisticAction hK lambda actionFeature R delta S n history

Source line 23 Chapter context: OFUL

theorem BanditRLProof.OFUL.finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction_eq_forcedAction Compiled

At a forced index, the selector uses the action indexed by its exponent.

theorem finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction_eq_forcedAction {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (forcedAction : Nat -> Fin K) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (hforced : isPowerOfTwoForcedIndex n) : finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction n history = forcedAction (Nat.log2 (n + 1))

Source line 44 Chapter context: OFUL

theorem

BanditRLProof.OFUL.canonicalHistoryTrajectory_action_succ_ae_eq_finiteHistoryTelescopingScalarRidgeOptimisticAction_of_not_powerOfTwoForced

Compiled

Under the modified policy's own trajectory law, every nonforced successor action agrees almost surely with the ordinary telescoping OFUL selector.

theorem canonicalHistoryTrajectory_action_succ_ae_eq_finiteHistoryTelescopingScalarRidgeOptimisticAction_of_not_powerOfTwoForced {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (forcedAction : Nat -> Fin K) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) (hnonforced : ¬ isPowerOfTwoForcedIndex n) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment, (trajectory (n + 1)).1 = finiteHistoryTelescopingScalarRidgeOptimisticAction hK lambda actionFeature R delta S n (Preorder.frestrictLe n trajectory)

Source line 67 Chapter context: OFUL

theorem BanditRLProof.OFUL.canonicalHistoryTrajectory_action_succ_ae_eq_forcedAction_of_powerOfTwoForced Compiled

At any forced successor index, the generated action is the indexed arm.

theorem canonicalHistoryTrajectory_action_succ_ae_eq_forcedAction_of_powerOfTwoForced {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R delta S : Real) (forcedAction : Nat -> Fin K) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) (hforced : isPowerOfTwoForcedIndex n) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment, (trajectory (n + 1)).1 = forcedAction (Nat.log2 (n + 1))

Source line 99 Chapter context: OFUL

def BanditRLProof.OFUL.powerOfTwoForcedSuccessorPseudoRegret Compiled

Successor pseudo-regret charged at power-of-two forced indices.

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

Source line 129 Chapter context: OFUL

def BanditRLProof.OFUL.powerOfTwoForcedActionSuccessorPseudoRegret Compiled

Deterministic successor charge of the prescribed forced actions.

noncomputable def powerOfTwoForcedActionSuccessorPseudoRegret {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (best : Fin K) (forcedAction : Nat -> Fin K) (horizon : Nat) : Real

Source line 144 Chapter context: OFUL

def BanditRLProof.OFUL.powerOfTwoOptimisticSuccessorPseudoRegret Compiled

Successor pseudo-regret charged to nonforced optimistic actions.

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

Source line 158 Chapter context: OFUL

theorem BanditRLProof.OFUL.canonicalStandardHighProbabilityPseudoRegret_eq_initial_add_powerOfTwoForced_add_optimistic Compiled

Complete pseudo-regret through action `horizon` is the initial gap plus the power-of-two forced and nonforced optimistic successor charges.

theorem canonicalStandardHighProbabilityPseudoRegret_eq_initial_add_powerOfTwoForced_add_optimistic {K : Nat} {Feature : Type u} [Fintype Feature] (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (best : Fin K) (horizon : Nat) (trajectory : Nat -> Fin K × Real) : canonicalStandardHighProbabilityPseudoRegret thetaStar actionFeature best horizon trajectory = (linearValue thetaStar (actionFeature best) - linearValue thetaStar (actionFeature (Thompson.canonicalHistoryTrajectoryAction trajectory 0))) + powerOfTwoForcedSuccessorPseudoRegret thetaStar actionFeature best horizon trajectory + powerOfTwoOptimisticSuccessorPseudoRegret thetaStar actionFeature best horizon trajectory

Source line 177 Chapter context: OFUL

theorem BanditRLProof.OFUL.powerOfTwoForcedSuccessorPseudoRegret_ae_eq_forcedActionCharge Compiled

Under the power-of-two forced policy, its trajectory-valued forced successor charge is almost surely the deterministic prescribed-action charge.

theorem powerOfTwoForcedSuccessorPseudoRegret_ae_eq_forcedActionCharge {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) (horizon : Nat) (best : Fin K) : powerOfTwoForcedSuccessorPseudoRegret thetaStar actionFeature best horizon =ᵐ[ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment] fun _trajectory => powerOfTwoForcedActionSuccessorPseudoRegret thetaStar actionFeature best forcedAction horizon

Source line 210 Chapter context: OFUL

theorem BanditRLProof.OFUL.canonicalStandardHighProbabilityPseudoRegret_ae_eq_initial_add_powerOfTwoForcedAction_add_optimistic Compiled

The complete pathwise decomposition with its forced term already replaced by the deterministic prescribed-action charge almost surely.

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

Source line 272 Chapter context: OFUL