BanditRLProof.Algorithms.UCBConditionalRewardPairTrajectorySampledReal

Shift sampled pair-trajectory actions at coordinates `1, 2, ...` to times `0, 1, ...`.

def actionRewardTrajectorySuccessorAction {Action Reward : Type} (trajectory : Nat -> Prod Action Reward) : ActionTrace Action

Shift sampled pair-trajectory actions at coordinates `1, 2, ...` to times `0, 1, ...`. -/ def actionRewardTrajectorySuccessorAction {Action Reward : Type} (trajectory : Nat -> Prod Action Reward) : ActionTrace Action := fun t => (trajectory (t + 1)).1 /- The shifted UCB action reconstructed from reward coordinates agrees almost everywhere with the sampled successor action trace on its canonical pair trajectory measure.

theorem selectedPolicySuccessorGeneratedUCBRegretAction_ae_eq_actionRewardTrajectorySuccessorAction_trajMeasure {Context : Type u} {K : Nat} [MeasurableSpace Context] (hK : 0 < K) (mu0 : Measure (Prod (Fin K) Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (defaultAction : Fin K) (sigma2 : NNReal) (T : Nat) (delta : Real) (hcontext : forall n : Nat, Measurable (context n)) : let policy := selectedPolicySuccessorHistoryPolicy hK sigma2 T delta defaultAction let state := selectedPolicySuccessorHistoryState hK sigma2 T delta defaultAction let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> Context

Shift sampled pair-trajectory actions at coordinates `1, 2, ...` to times `0, 1, ...`. -/ def actionRewardTrajectorySuccessorAction {Action Reward : Type} (trajectory : Nat -> Prod Action Reward) : ActionTrace Action := fun t => (trajectory (t + 1)).1 /- The shifted UCB action reconstructed from reward coordinates agrees almost everywhere with the sampled successor action trace on its canonical pair trajectory measure. -/ theorem selectedPolicySuccessorGeneratedUCBRegretAction_ae_eq_actionRewardTrajectorySuccessorAction_trajMeasure {Context : Type u} {K : Nat} [MeasurableSpace Context] (hK : 0 < K) (mu0 : Measure (Prod (Fin K) Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (defaultAction : Fin K) (sigma2 : NNReal) (T : Nat) (delta : Real) (hcontext : forall n : Nat, Measurable (context n)) : let policy := selectedPolicySuccessorHistoryPolicy hK sigma2 T delta defaultAction let state := selectedPolicySuccessorHistoryState hK sigma2 T delta defaultAction let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> Context := fun i history => context i (History.pairHistoryRewardProjection history) let pairState : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> SelectedPolicySuccessorFiniteHistoryState K := fun i history => state i (History.pairHistoryRewardProjection history) let hpairContext : forall i : Nat, Measurable (pairContext i) := fun i => (hcontext i).comp (History.measurable_pairHistoryRewardProjection (Action := Fin K) (Reward := Rat) i) let hpairState : forall i : Nat, Measurable (pairState i) := fun i => (measurable_selectedPolicySuccessorHistoryState hK sigma2 T delta defaultAction i).comp (History.measurable_pairHistoryRewardProjection (Action := Fin K) (Reward := Rat) i) let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy pairContext pairState hpairContext hpairState let mu := ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Prod (Fin K) Rat) mu0 stepKernel let reward : (Nat -> Prod (Fin K) Rat) -> RewardTrace Rat := fun trajectory t => (trajectory t).2 Filter.EventuallyEq (ae mu) (selectedPolicySuccessorGeneratedUCBRegretAction hK sigma2 T delta defaultAction reward) (fun trajectory => actionRewardTrajectorySuccessorAction trajectory) := by let policy := selectedPolicySuccessorHistoryPolicy hK sigma2 T delta defaultAction let state := selectedPolicySuccessorHistoryState hK sigma2 T delta defaultAction let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> Context := fun i history => context i (History.pairHistoryRewardProjection history) let pairState : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> SelectedPolicySuccessorFiniteHistoryState K := fun i history => state i (History.pairHistoryRewardProjection history) let hpairContext : forall i : Nat, Measurable (pairContext i) := fun i => (hcontext i).comp (History.measurable_pairHistoryRewardProjection (Action := Fin K) (Reward := Rat) i) let hpairState : forall i : Nat, Measurable (pairState i) := fun i => (measurable_selectedPolicySuccessorHistoryState hK sigma2 T delta defaultAction i).comp (History.measurable_pairHistoryRewardProjection (Action := Fin K) (Reward := Rat) i) let stepKernel := RewardKernel.actionRewardHistoryStepKernelFamily rewardKernel policy pairContext pairState hpairContext hpairState let mu := ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Prod (Fin K) Rat) mu0 stepKernel let sampledAction : (Nat -> Prod (Fin K) Rat) -> ActionTrace (Fin K) := fun trajectory t => (trajectory t).1 let reward : (Nat -> Prod (Fin K) Rat) -> RewardTrace Rat := fun trajectory t => (trajectory t).2 let generatedAction := selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward let regretAction := selectedPolicySuccessorGeneratedUCBRegretAction hK sigma2 T delta defaultAction reward let successorAction : (Nat -> Prod (Fin K) Rat) -> ActionTrace (Fin K) := fun trajectory => actionRewardTrajectorySuccessorAction trajectory change Filter.EventuallyEq (ae mu) regretAction successorAction have hcoord : forall i : Nat, Filter.EventuallyEq (ae mu) (fun trajectory => regretAction trajectory i) (fun trajectory => successorAction trajectory i) := by intro i have hcanonical := ConditionalExpectationReward.actionRewardHistoryStepKernelFamily_action_succ_ae_eq_policy_trajMeasure mu0 rewardKernel policy pairContext pairState hpairContext hpairState i have hsampled_generated : Filter.EventuallyEq (ae mu) (fun trajectory => sampledAction trajectory (i + 1)) (fun trajectory => generatedAction trajectory (i + 1)) := by simpa [mu, stepKernel, sampledAction, generatedAction, selectedPolicySuccessorGeneratedUCBAction, ConditionalExpectationReward.generatedActionFromRewardHistory, Policy.generatedActionTraceSucc, policy, state, pairState, reward, History.pairHistoryRewardProjection, History.finiteRewardHistoryOfTrace, Preorder.frestrictLe_apply] using hcanonical simpa [regretAction, successorAction, selectedPolicySuccessorGeneratedUCBRegretAction, actionRewardTrajectorySuccessorAction, generatedAction, sampledAction] using hsampled_generated.symm have hall : ∀ᵐ trajectory ∂mu, forall i : Nat, regretAction trajectory i = successorAction trajectory i := ae_all_iff.2 hcoord filter_upwards [hall] with trajectory htrajectory funext i exact htrajectory i /- Canonical pair-trajectory Real textbook pseudo-regret bound stated directly on the sampled successor action coordinates.

theorem integral_real_pseudoRegret_actionRewardTrajectorySuccessorAction_le_textbookGapSum_actionRewardTrajMeasure_centeredKernel {Context : Type u} {K : Nat} [MeasurableSpace Context] (model : FiniteBanditModel K) (mu0 : Measure (Prod (Fin K) Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (mean : Context -> Fin K -> Rat) (varianceProxy : Context -> Fin K -> NNReal) (defaultAction : Fin K) (sigma2 : NNReal) (T : Nat) (delta : Real) (hcontext : forall n : Nat, Measurable (context n)) (hmean : Measurable (fun pair : Prod Context (Fin K) => mean pair.1 pair.2)) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, i < T - 1 -> forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((selectedPolicySuccessorHistoryPolicy model.hK sigma2 T delta defaultAction i).action (selectedPolicySuccessorHistoryState model.hK sigma2 T delta defaultAction i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, mean (context i history) arm = model.mean arm) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (hdelta : 0 < delta) : let policy := selectedPolicySuccessorHistoryPolicy model.hK sigma2 T delta defaultAction let state := selectedPolicySuccessorHistoryState model.hK sigma2 T delta defaultAction let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> Context