Lean module · OFUL

BanditRLProof.OFULScheduledBlockStartForcedHistoryAlgorithm

# Concrete block-start forced scheduling for telescoping OFUL This module packages measurable finite-history selectors as deterministic history algorithms and proves their canonical successor-action graph. It then defines a modified telescoping OFUL selector that forces one prescribed action after every block-start history while retaining the ordinary optimistic selector at all other history indices. The final theorem constructs the aligned-window positive-action-cost contract under the modified algorithm's own canonical trajectory measure. No ordinary OFUL regret theorem is transported to that changed measure here; forced-round regret accounting remains a separate route.

Module map

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

Imports

BanditRLProof.OFULScheduledBlockStartForcedPositiveActionCostBudgetExhaustionExpectedRegret

Imported by

BanditRLProof, BanditRLProof.OFULScheduledBlockStartForcedPseudoRegretDecomposition, BanditRLProof.OFULScheduledPowerOfTwoForcedHistoryAlgorithm

Declarations

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

def BanditRLProof.Thompson.deterministicHistoryAlgorithm Compiled

Package a measurable finite-history selector as a deterministic algorithm.

noncomputable def deterministicHistoryAlgorithm {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] (initialAction : Action) (selector : (n : Nat) -> History.FinitePairHistory Action Reward n -> Action) (hselector : forall n, Measurable (selector n)) : HistoryAlgorithm Action Reward where

Source line 28 Chapter context: OFUL

theorem BanditRLProof.Thompson.deterministicHistoryAlgorithm_policy_apply Compiled

Every policy section of a deterministic history algorithm is a Dirac law.

theorem deterministicHistoryAlgorithm_policy_apply {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [MeasurableSpace Reward] (initialAction : Action) (selector : (n : Nat) -> History.FinitePairHistory Action Reward n -> Action) (hselector : forall n, Measurable (selector n)) (n : Nat) (history : History.FinitePairHistory Action Reward n) : (deterministicHistoryAlgorithm initialAction selector hselector).policy n history = Measure.dirac (selector n history)

Source line 41 Chapter context: OFUL

theorem BanditRLProof.Thompson.canonicalHistoryTrajectory_action_succ_ae_eq_deterministicHistorySelector Compiled

The canonical successor action of a deterministic history algorithm lies on the graph of its measurable selector almost surely.

theorem canonicalHistoryTrajectory_action_succ_ae_eq_deterministicHistorySelector {Action : Type u} {Reward : Type v} [MeasurableSpace Action] [StandardBorelSpace Action] [Nonempty Action] [MeasurableEq Action] [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] (initialAction : Action) (selector : (n : Nat) -> History.FinitePairHistory Action Reward n -> Action) (hselector : forall n, Measurable (selector n)) (environment : HistoryEnvironment Action Reward) (n : Nat) : ∀ᵐ trajectory ∂ canonicalHistoryTrajectoryMeasure (deterministicHistoryAlgorithm initialAction selector hselector) environment, canonicalHistoryTrajectoryAction trajectory (n + 1) = selector n (History.finitePairHistoryOfTrace (canonicalHistoryTrajectoryAction trajectory) (canonicalHistoryTrajectoryReward trajectory) n)

Source line 59 Chapter context: OFUL

def BanditRLProof.OFUL.finiteHistoryBlockStartForcedTelescopingScalarRidgeAction Compiled

Use the forced block action at divisible history indices and the ordinary telescoping OFUL selector at all other indices.

noncomputable def finiteHistoryBlockStartForcedTelescopingScalarRidgeAction {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) (window n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : Fin K

Source line 140 Chapter context: OFUL

theorem BanditRLProof.OFUL.measurable_finiteHistoryBlockStartForcedTelescopingScalarRidgeAction Compiled

The block-start forced selector is measurable in its finite history.

theorem measurable_finiteHistoryBlockStartForcedTelescopingScalarRidgeAction {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) (window n : Nat) : Measurable (finiteHistoryBlockStartForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction window n)

Source line 158 Chapter context: OFUL

def BanditRLProof.OFUL.finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm Compiled

The block-start forced selector packaged as a fully specified history algorithm.

noncomputable def finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm {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) (window : Nat) : Thompson.HistoryAlgorithm (Fin K) Real

Source line 181 Chapter context: OFUL

theorem BanditRLProof.OFUL.finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm_policy_apply Compiled

Every policy section is the Dirac law at the modified selector.

theorem finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm_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) (window n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window).policy n history = Measure.dirac (finiteHistoryBlockStartForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction window n history)

Source line 200 Chapter context: OFUL

theorem BanditRLProof.OFUL.finiteHistoryBlockStartForcedTelescopingScalarRidgeAction_mul_window Compiled

At a block-multiple history index, the modified selector uses that block's forced arm.

theorem finiteHistoryBlockStartForcedTelescopingScalarRidgeAction_mul_window {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) (window block : Nat) (hwindow : 0 < window) (history : History.FinitePairHistory (Fin K) Real (block * window)) : finiteHistoryBlockStartForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction window (block * window) history = forcedAction block

Source line 226 Chapter context: OFUL

theorem

BanditRLProof.OFUL.canonicalHistoryTrajectory_action_succ_ae_eq_finiteHistoryBlockStartForcedTelescopingScalarRidgeAction

Compiled

Generated successor actions follow the modified selector almost surely.

theorem canonicalHistoryTrajectory_action_succ_ae_eq_finiteHistoryBlockStartForcedTelescopingScalarRidgeAction {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) (window : Nat) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment, (trajectory (n + 1)).1 = finiteHistoryBlockStartForcedTelescopingScalarRidgeAction hK lambda actionFeature R delta S forcedAction window n (Preorder.frestrictLe n trajectory)

Source line 248 Chapter context: OFUL

theorem BanditRLProof.OFUL.canonicalHistoryTrajectory_action_blockStart_succ_ae_eq_forcedAction Compiled

The generated action after a block-start history is the prescribed forced arm.

theorem canonicalHistoryTrajectory_action_blockStart_succ_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) (window : Nat) (hwindow : 0 < window) (environment : Thompson.HistoryEnvironment (Fin K) Real) (block : Nat) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment, (trajectory (block * window + 1)).1 = forcedAction block

Source line 283 Chapter context: OFUL

theorem BanditRLProof.Budget.alignedWindowPositiveActionCostAE_finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm Compiled

Positive forced-arm costs produce one positive selected action in every aligned block under the modified algorithm's canonical law.

theorem alignedWindowPositiveActionCostAE_finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm {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) (window : Nat) (hwindow : 2 <= window) (environment : Thompson.HistoryEnvironment (Fin K) Real) (actionCost : Fin K -> Nat) (hpositive : forall block, 1 <= actionCost (forcedAction block)) : AlignedWindowPositiveActionCostAE (Thompson.canonicalHistoryTrajectoryMeasure (OFUL.finiteHistoryBlockStartForcedTelescopingScalarRidgeAlgorithm hK lambda actionFeature R delta S forcedAction window) environment) actionCost window

Source line 320 Chapter context: OFUL