BanditRLProof.OFULHistoryEnvironmentRewardLaw

For any canonical history algorithm, the time-zero reward marginal is the environment feedback law at that algorithm's initial action.

theorem canonicalHistoryTrajectory_initialReward_map_eq_historyAlgorithmInitialFeedback {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (initialAction : Fin K) (hinitial : algorithm.initialAction = Measure.dirac initialAction) (environment : Thompson.HistoryEnvironment (Fin K) Real) : Measure.map (fun trajectory : Nat -> Fin K × Real => trajectory 0 |>.2) (Thompson.canonicalHistoryTrajectoryMeasure algorithm environment) = environment.initialFeedback initialAction

For any canonical history algorithm, the successor reward conditioned on its finite pair prefix has the reward marginal of the history-step kernel.

theorem canonicalHistoryTrajectory_reward_succ_condDistrib_eq_historyStepReward {K : Nat} (hK : 0 < K) (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) : ProbabilityTheory.condDistrib (fun trajectory : Nat -> Fin K × Real => (trajectory (n + 1)).2) (Preorder.frestrictLe n) (Thompson.canonicalHistoryTrajectoryMeasure algorithm environment) =ᵐ[ (Thompson.canonicalHistoryTrajectoryMeasure algorithm environment).map (Preorder.frestrictLe n)] (Thompson.historyStepKernel algorithm environment n).map Prod.snd

Algorithm-parametric trimmed conditional-expectation reward law at successor time for a canonical history trajectory.

theorem canonicalHistoryTrajectory_reward_succ_condExpKernel_map_eq_historyStepReward_comap {K : Nat} (hK : 0 < K) (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) : Filter.Eventually (fun trajectory : Nat -> Fin K × Real => Measure.map (fun y : Nat -> Fin K × Real => (y (n + 1)).2) (ProbabilityTheory.condExpKernel (Thompson.canonicalHistoryTrajectoryMeasure algorithm environment) ((inferInstance : MeasurableSpace (History.FinitePairHistory (Fin K) Real n)).comap (Preorder.frestrictLe n)) trajectory) = (Thompson.historyStepKernel algorithm environment n).map Prod.snd (Preorder.frestrictLe n trajectory)) (ae ((Thompson.canonicalHistoryTrajectoryMeasure algorithm environment).trim ((History.measurable_finitePairHistoryOfTrace Thompson.canonicalHistoryTrajectoryAction Thompson.canonicalHistoryTrajectoryReward Thompson.measurable_canonicalHistoryTrajectoryAction_apply Thompson.measurable_canonicalHistoryTrajectoryReward_apply n).comap_le)))

Algorithm-parametric time-zero conditional reward law on the trivial sigma-algebra.

theorem canonicalHistoryTrajectory_initialReward_condExpKernel_map_eq_historyAlgorithmInitialFeedback_unitComap {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (initialAction : Fin K) (hinitial : algorithm.initialAction = Measure.dirac initialAction) (environment : Thompson.HistoryEnvironment (Fin K) Real) : Filter.Eventually (fun trajectory : Nat -> Fin K × Real => Measure.map (fun y : Nat -> Fin K × Real => (y 0).2) (ProbabilityTheory.condExpKernel (Thompson.canonicalHistoryTrajectoryMeasure algorithm environment) ((inferInstance : MeasurableSpace Unit).comap (fun _trajectory : Nat -> Fin K × Real => ())) trajectory) = environment.initialFeedback initialAction) (ae ((Thompson.canonicalHistoryTrajectoryMeasure algorithm environment).trim ((show Measurable (fun _trajectory : Nat -> Fin K × Real => ()) from measurable_const).comap_le)))

For the deterministic finite-history OFUL policy, the reward marginal of the next pair kernel is exactly the environment feedback kernel selected by the current history.

theorem finiteHistoryScalarRidge_historyStepKernel_map_snd {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R algorithmDelta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : (Thompson.historyStepKernel (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment n).map Prod.snd history = environment.feedback n (history, finiteHistoryScalarRidgeOptimisticAction hK lambda actionFeature R algorithmDelta S n history)

The initial canonical reward marginal is the initial-arm feedback law.

theorem canonicalHistoryTrajectory_initialReward_map_eq_scalarRidgeInitialFeedback {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R algorithmDelta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) : Measure.map (fun trajectory : Nat -> Fin K × Real => trajectory 0 |>.2) (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment) = environment.initialFeedback ⟨0, hK⟩

The successor canonical reward conditioned on the finite pair prefix has the reward marginal of the concrete history step kernel.

theorem canonicalHistoryTrajectory_reward_succ_condDistrib_eq_scalarRidgeStepReward {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R algorithmDelta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) : ProbabilityTheory.condDistrib (fun trajectory : Nat -> Fin K × Real => (trajectory (n + 1)).2) (Preorder.frestrictLe n) (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment) =ᵐ[ (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment).map (Preorder.frestrictLe n)] (Thompson.historyStepKernel (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment n).map Prod.snd

Trimmed conditional-expectation reward law at successor time for the concrete canonical OFUL trajectory.

theorem canonicalHistoryTrajectory_reward_succ_condExpKernel_map_eq_scalarRidgeStepReward_comap {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R algorithmDelta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (n : Nat) : Filter.Eventually (fun trajectory : Nat -> Fin K × Real => Measure.map (fun y : Nat -> Fin K × Real => (y (n + 1)).2) (ProbabilityTheory.condExpKernel (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment) ((inferInstance : MeasurableSpace (History.FinitePairHistory (Fin K) Real n)).comap (Preorder.frestrictLe n)) trajectory) = (Thompson.historyStepKernel (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment n).map Prod.snd (Preorder.frestrictLe n trajectory)) (ae ((Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment).trim ((History.measurable_finitePairHistoryOfTrace Thompson.canonicalHistoryTrajectoryAction Thompson.canonicalHistoryTrajectoryReward Thompson.measurable_canonicalHistoryTrajectoryAction_apply Thompson.measurable_canonicalHistoryTrajectoryReward_apply n).comap_le)))

At time zero, conditioning on the trivial sigma-algebra leaves the canonical initial reward law equal to the initial-arm feedback measure.

theorem canonicalHistoryTrajectory_initialReward_condExpKernel_map_eq_scalarRidgeInitialFeedback_unitComap {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (actionFeature : Fin K -> Feature -> Real) (R algorithmDelta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) : Filter.Eventually (fun trajectory : Nat -> Fin K × Real => Measure.map (fun y : Nat -> Fin K × Real => (y 0).2) (ProbabilityTheory.condExpKernel (Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment) ((inferInstance : MeasurableSpace Unit).comap (fun _trajectory : Nat -> Fin K × Real => ())) trajectory) = environment.initialFeedback ⟨0, hK⟩) (ae ((Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R algorithmDelta S) environment).trim ((show Measurable (fun _trajectory : Nat -> Fin K × Real => ()) from measurable_const).comap_le)))

A concrete linear reward contract on the kernels of a history environment. The initial and successor fields are unconditional sub-Gaussian laws of each kernel section around the linear response of the supplied action.

structure CanonicalLinearSubgaussianEnvironmentLaw {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) : Prop where

The kernel-level linear sub-Gaussian environment contract constructs the strict-past predictable residual law required by the OFUL confidence route.

noncomputable def canonicalPredictableScalarRidgeResidualLaw_of_linearSubgaussianEnvironment {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] (hK : 0 < K) (lambda : Real) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R algorithmDelta S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (horizon : Nat) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : CanonicalPredictableScalarRidgeResidualLaw hK lambda thetaStar actionFeature R algorithmDelta S environment horizon where

Concrete successor-gap tail obtained directly from a linear sub-Gaussian `HistoryEnvironment` contract.

theorem measure_canonicalHistoryTrajectorySumRangeSuccGapViolationSet_le_of_linearSubgaussianEnvironment {K : Nat} {Feature : Type u} [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (hK : 0 < K) (lambda : Real) (hlambda : 0 < lambda) (thetaStar : Feature -> Real) (actionFeature : Fin K -> Feature -> Real) (R : Real) (hR : 0 < R) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (S : Real) (environment : Thompson.HistoryEnvironment (Fin K) Real) (horizon : Nat) (comparator : Nat -> Fin K) (source : CanonicalLinearSubgaussianEnvironmentLaw hK thetaStar actionFeature R S environment) : Thompson.canonicalHistoryTrajectoryMeasure (finiteHistoryScalarRidgeOptimisticAlgorithm hK lambda actionFeature R (delta / ((horizon + 1 : Nat) : Real)) S) environment (canonicalHistoryTrajectorySumRangeSuccGapViolationSet lambda thetaStar actionFeature R delta S horizon comparator) <= ENNReal.ofReal delta