BanditRLProof.OFULMeasurableRecursiveSelection

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

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

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)

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)

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

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)

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)

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

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)