Lean module · OFUL

BanditRLProof.OFULMeasurableRecursiveSelection

# Measurable recursive OFUL selection This module replaces the nonconstructive finite OFUL argmax by the existing strict finite fold on `Fin K`. Under measurable score coordinates, the fold defines a deterministic history policy. The canonical history trajectory then realizes that selector at every successor time.

Module map

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

Imports

BanditRLProof.OFULFiniteActionOptimism, BanditRLProof.Algorithms.ETCRealEmpiricalMean, BanditRLProof.Algorithms.ThompsonCanonicalTrajectory

Imported by

BanditRLProof, BanditRLProof.OFULConcreteHistoryRidgeSelection

Declarations

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

def BanditRLProof.OFUL.finiteHistoryOptimisticScore Compiled

The OFUL score of one action at one inclusive finite pair history.

noncomputable def finiteHistoryOptimisticScore {K : Nat} {Reward : Type u} {Feature : Type v} [MeasurableSpace Reward] [Fintype Feature] [DecidableEq Feature] (thetaHat : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Feature -> Real) (V : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Matrix Feature Feature Real) (beta : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Real) (candidateFeature : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Fin K -> Feature -> Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Reward n) (action : Fin K) : Real

Source line 23 Chapter context: OFUL

def BanditRLProof.OFUL.finiteHistoryOptimisticAction Compiled

Deterministic history OFUL selector with the strict-update finite fold. The strict comparison gives a fixed deterministic tie behavior.

noncomputable def finiteHistoryOptimisticAction {K : Nat} {Reward : Type u} {Feature : Type v} [MeasurableSpace Reward] [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaHat : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Feature -> Real) (V : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Matrix Feature Feature Real) (beta : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Real) (candidateFeature : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Fin K -> Feature -> Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Reward n) : Fin K

Source line 46 Chapter context: OFUL

theorem BanditRLProof.OFUL.finiteHistoryOptimisticAction_score_max Compiled

The history selector maximizes the current OFUL score.

theorem finiteHistoryOptimisticAction_score_max {K : Nat} {Reward : Type u} {Feature : Type v} [MeasurableSpace Reward] [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaHat : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Feature -> Real) (V : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Matrix Feature Feature Real) (beta : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Real) (candidateFeature : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Fin K -> Feature -> Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Reward n) (action : Fin K) : finiteHistoryOptimisticScore thetaHat V beta candidateFeature n history action <= finiteHistoryOptimisticScore thetaHat V beta candidateFeature n history (finiteHistoryOptimisticAction hK thetaHat V beta candidateFeature n history)

Source line 67 Chapter context: OFUL

theorem BanditRLProof.OFUL.measurable_finiteHistoryOptimisticAction Compiled

The strict-fold history selector is measurable when each fixed-action score coordinate is measurable.

theorem measurable_finiteHistoryOptimisticAction {K : Nat} {Reward : Type u} {Feature : Type v} [MeasurableSpace Reward] [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaHat : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Feature -> Real) (V : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Matrix Feature Feature Real) (beta : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Real) (candidateFeature : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Fin K -> Feature -> Real) (n : Nat) (hscores : forall action : Fin K, Measurable (fun history : History.FinitePairHistory (Fin K) Reward n => finiteHistoryOptimisticScore thetaHat V beta candidateFeature n history action)) : Measurable (finiteHistoryOptimisticAction hK thetaHat V beta candidateFeature n)

Source line 97 Chapter context: OFUL

def BanditRLProof.OFUL.finiteHistoryOptimisticAlgorithm Compiled

The measurable history selector packaged as a deterministic algorithm.

noncomputable def finiteHistoryOptimisticAlgorithm {K : Nat} {Reward : Type u} {Feature : Type v} [MeasurableSpace Reward] [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaHat : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Feature -> Real) (V : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Matrix Feature Feature Real) (beta : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Real) (candidateFeature : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Fin K -> Feature -> Real) (hscores : forall (n : Nat) (action : Fin K), Measurable (fun history : History.FinitePairHistory (Fin K) Reward n => finiteHistoryOptimisticScore thetaHat V beta candidateFeature n history action)) : Thompson.HistoryAlgorithm (Fin K) Reward where

Source line 126 Chapter context: OFUL

theorem BanditRLProof.OFUL.finiteHistoryOptimisticAlgorithm_policy_apply Compiled

Every policy section of the history OFUL algorithm is the selector Dirac law.

@[simp] theorem finiteHistoryOptimisticAlgorithm_policy_apply {K : Nat} {Reward : Type u} {Feature : Type v} [MeasurableSpace Reward] [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaHat : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Feature -> Real) (V : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Matrix Feature Feature Real) (beta : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Real) (candidateFeature : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Fin K -> Feature -> Real) (hscores : forall (n : Nat) (action : Fin K), Measurable (fun history : History.FinitePairHistory (Fin K) Reward n => finiteHistoryOptimisticScore thetaHat V beta candidateFeature n history action)) (n : Nat) (history : History.FinitePairHistory (Fin K) Reward n) : (finiteHistoryOptimisticAlgorithm hK thetaHat V beta candidateFeature hscores).policy n history = Measure.dirac (finiteHistoryOptimisticAction hK thetaHat V beta candidateFeature n history)

Source line 155 Chapter context: OFUL

theorem BanditRLProof.OFUL.canonicalHistoryTrajectory_action_succ_ae_eq_finiteHistoryOptimisticAction Compiled

Along the canonical recursive trajectory, the successor action is almost surely the measurable OFUL selector evaluated on the realized finite history.

theorem canonicalHistoryTrajectory_action_succ_ae_eq_finiteHistoryOptimisticAction {K : Nat} {Reward : Type u} {Feature : Type v} [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaHat : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Feature -> Real) (V : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Matrix Feature Feature Real) (beta : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Real) (candidateFeature : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Fin K -> Feature -> Real) (hscores : forall (n : Nat) (action : Fin K), Measurable (fun history : History.FinitePairHistory (Fin K) Reward n => finiteHistoryOptimisticScore thetaHat V beta candidateFeature n history action)) (environment : Thompson.HistoryEnvironment (Fin K) Reward) (n : Nat) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryOptimisticAlgorithm hK thetaHat V beta candidateFeature hscores) environment, Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1) = finiteHistoryOptimisticAction hK thetaHat V beta candidateFeature n (History.finitePairHistoryOfTrace (Thompson.canonicalHistoryTrajectoryAction trajectory) (Thompson.canonicalHistoryTrajectoryReward trajectory) n)

Source line 187 Chapter context: OFUL

def BanditRLProof.OFUL.finiteHistoryOptimisticSelectedFeature Compiled

Candidate feature selected by the measurable OFUL history action.

noncomputable def finiteHistoryOptimisticSelectedFeature {K : Nat} {Reward : Type u} {Feature : Type v} [MeasurableSpace Reward] [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaHat : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Feature -> Real) (V : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Matrix Feature Feature Real) (beta : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Real) (candidateFeature : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Fin K -> Feature -> Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Reward n) : Feature -> Real

Source line 276 Chapter context: OFUL

theorem BanditRLProof.OFUL.canonicalHistoryTrajectory_candidateFeature_succ_ae_eq_selectedFeature Compiled

The feature indexed by the actual canonical successor action agrees almost surely with the feature selected from the realized history.

theorem canonicalHistoryTrajectory_candidateFeature_succ_ae_eq_selectedFeature {K : Nat} {Reward : Type u} {Feature : Type v} [MeasurableSpace Reward] [StandardBorelSpace Reward] [Nonempty Reward] [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaHat : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Feature -> Real) (V : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Matrix Feature Feature Real) (beta : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Real) (candidateFeature : (n : Nat) -> History.FinitePairHistory (Fin K) Reward n -> Fin K -> Feature -> Real) (hscores : forall (n : Nat) (action : Fin K), Measurable (fun history : History.FinitePairHistory (Fin K) Reward n => finiteHistoryOptimisticScore thetaHat V beta candidateFeature n history action)) (environment : Thompson.HistoryEnvironment (Fin K) Reward) (n : Nat) : ∀ᵐ trajectory ∂ Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryOptimisticAlgorithm hK thetaHat V beta candidateFeature hscores) environment, candidateFeature n (History.finitePairHistoryOfTrace (Thompson.canonicalHistoryTrajectoryAction trajectory) (Thompson.canonicalHistoryTrajectoryReward trajectory) n) (Thompson.canonicalHistoryTrajectoryAction trajectory (n + 1)) = finiteHistoryOptimisticSelectedFeature hK thetaHat V beta candidateFeature n (History.finitePairHistoryOfTrace (Thompson.canonicalHistoryTrajectoryAction trajectory) (Thompson.canonicalHistoryTrajectoryReward trajectory) n)

Source line 301 Chapter context: OFUL