Lean module · OFUL
BanditRLProof.OFULScheduledPowerOfTwoForcedHistoryAlgorithm
# Power-of-two forced scheduling for telescoping OFUL This module packages one horizon-independent deterministic history algorithm. At history indices one below a power of two it selects the arm indexed by that power's exponent; at every other index it uses the ordinary telescoping OFUL selector.
Module map
Imports
BanditRLProof.OFULScheduledBlockStartForcedHistoryAlgorithm, BanditRLProof.OFULScheduledPowerOfTwoForcedIndexCount
Imported by
BanditRLProof, BanditRLProof.OFULScheduledPowerOfTwoForcedPseudoRegretDecomposition
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.OFUL.finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction
Compiled
Use the exponent-indexed forced action at power-of-two successor indices and the ordinary telescoping OFUL selector at all other history indices.
noncomputable def finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction {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) : Fin K
theorem
BanditRLProof.OFUL.measurable_finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction
Compiled
The power-of-two forced selector is measurable in its finite history.
theorem measurable_finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction {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) : Measurable (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction n)
def
BanditRLProof.OFUL.finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm
Compiled
The power-of-two forced selector as one deterministic history algorithm.
noncomputable def finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm {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) : Thompson.HistoryAlgorithm (Fin K) Real
theorem
BanditRLProof.OFUL.finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm_policy_apply
Compiled
Every policy section is the Dirac law at the power-of-two selector.
theorem finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm_policy_apply {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) : (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction).policy n history = Measure.dirac (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction n history)
theorem
BanditRLProof.OFUL.finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction_pow_sub_one
Compiled
At history index `2 ^ exponent - 1`, the selector uses the action prescribed for that exponent.
theorem finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction_pow_sub_one {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) (exponent : Nat) (history : History.FinitePairHistory (Fin K) Real (2 ^ exponent - 1)) : finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction (2 ^ exponent - 1) history = forcedAction exponent
theorem
BanditRLProof.OFUL.canonicalHistoryTrajectory_action_succ_ae_eq_finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction
Compiled
Generated successor actions follow the power-of-two selector almost surely.
theorem canonicalHistoryTrajectory_action_succ_ae_eq_finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction {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) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment, (trajectory (n + 1)).1 = finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction n (Preorder.frestrictLe n trajectory)
theorem
BanditRLProof.OFUL.canonicalHistoryTrajectory_action_pow_ae_eq_forcedAction
Compiled
At successor round `2 ^ exponent`, the generated action is prescribed.
theorem canonicalHistoryTrajectory_action_pow_ae_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) (environment : Thompson.HistoryEnvironment (Fin K) Real) (exponent : Nat) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryPowerOfTwoForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction) environment, (trajectory (2 ^ exponent)).1 = forcedAction exponent