BanditRLProof.Algorithms.UCBContextDependentSubGaussianRewardKernel

Canonical Real expected pseudo-regret bound for a context-dependent Markov reward kernel with stationary arm means and direct centered sub-Gaussian MGF witnesses. The centered kernel law, selected reward law, trajectory law, and finite-horizon integrability are constructed internally. The caller supplies a positive common ceiling because an arbitrary measurable context space has no finite maximum operation for the pointwise variance proxies.

theorem integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_trajMeasure_contextDependentSubgaussianRewardKernel {Context : Type} [MeasurableSpace Context] {K : Nat} (model : FiniteBanditModel K) (mu0 : Measure Rat) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Fin K) Rat) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (hcontext : forall n, Measurable (context n)) (varianceProxy : Context -> Fin K -> NNReal) (sigma2 : NNReal) (hsigma2 : 0 < ((sigma2 : NNReal) : Real)) (hvariance : forall ctx arm, varianceProxy ctx arm <= sigma2) (hmean : forall ctx arm, integral (RewardKernel.selectedMeasure rewardKernel ctx arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (hsubG : forall ctx arm, HasSubgaussianMGF (fun reward : Rat => (((reward - model.mean arm : Rat) : Real))) (varianceProxy ctx arm) (RewardKernel.selectedMeasure rewardKernel ctx arm)) (defaultAction : Fin K) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) : MeasureTheory.integral (selectedPolicySuccessorRewardTrajMeasure model.hK mu0 rewardKernel context hcontext sigma2 T delta defaultAction) (fun trajectory : RewardTrace Rat => ((pseudoRegret model (selectedPolicySuccessorGeneratedUCBRegretAction model.hK sigma2 T delta defaultAction (fun y : RewardTrace Rat => y) trajectory) T : Rat) : Real)) <= ((Finset.univ : Finset (Fin K)).filter (fun arm => 0 < (((model.gap arm : Rat) : Real)))).sum (fun arm => selectedPolicySuccessorTextbookGapBudget K sigma2 T delta (((model.gap arm : Rat) : Real)) + (((model.gap arm : Rat) : Real)) * ((T : Real) * delta))

Canonical Real expected pseudo-regret bound for direct sub-Gaussian selected laws over a finite context space. The common UCB proxy is the finite maximum of all context-action proxies, so callers do not supply a separate ceiling or its pointwise domination proof.

theorem integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_trajMeasure_finiteContextDependentSubgaussianRewardKernel {Context : Type} [MeasurableSpace Context] [Fintype Context] {K : Nat} (model : FiniteBanditModel K) (mu0 : Measure Rat) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Fin K) Rat) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (hcontext : forall n, Measurable (context n)) (varianceProxy : Context -> Fin K -> NNReal) (hvariancePos : exists ctx arm, 0 < ((varianceProxy ctx arm : NNReal) : Real)) (hmean : forall ctx arm, integral (RewardKernel.selectedMeasure rewardKernel ctx arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (hsubG : forall ctx arm, HasSubgaussianMGF (fun reward : Rat => (((reward - model.mean arm : Rat) : Real))) (varianceProxy ctx arm) (RewardKernel.selectedMeasure rewardKernel ctx arm)) (defaultAction : Fin K) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) : let sigma2 := Concentration.finiteContextArmVarianceProxy varianceProxy MeasureTheory.integral (selectedPolicySuccessorRewardTrajMeasure model.hK mu0 rewardKernel context hcontext sigma2 T delta defaultAction) (fun trajectory : RewardTrace Rat => ((pseudoRegret model (selectedPolicySuccessorGeneratedUCBRegretAction model.hK sigma2 T delta defaultAction (fun y : RewardTrace Rat => y) trajectory) T : Rat) : Real)) <= ((Finset.univ : Finset (Fin K)).filter (fun arm => 0 < (((model.gap arm : Rat) : Real)))).sum (fun arm => selectedPolicySuccessorTextbookGapBudget K sigma2 T delta (((model.gap arm : Rat) : Real)) + (((model.gap arm : Rat) : Real)) * ((T : Real) * delta))

Canonical Real expected pseudo-regret bound for direct sub-Gaussian selected laws over a finite context space, including the all-zero proxy case. The UCB parameter is the finite context-action maximum padded by one, so no positivity or ceiling premise remains at the public theorem boundary.

theorem integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_trajMeasure_finiteContextDependentSubgaussianRewardKernel_without_proxy_positivity {Context : Type} [MeasurableSpace Context] [Fintype Context] {K : Nat} (model : FiniteBanditModel K) (mu0 : Measure Rat) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Fin K) Rat) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (hcontext : forall n, Measurable (context n)) (varianceProxy : Context -> Fin K -> NNReal) (hmean : forall ctx arm, integral (RewardKernel.selectedMeasure rewardKernel ctx arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (hsubG : forall ctx arm, HasSubgaussianMGF (fun reward : Rat => (((reward - model.mean arm : Rat) : Real))) (varianceProxy ctx arm) (RewardKernel.selectedMeasure rewardKernel ctx arm)) (defaultAction : Fin K) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) : let sigma2 := Concentration.finiteContextArmPositiveVarianceProxy varianceProxy MeasureTheory.integral (selectedPolicySuccessorRewardTrajMeasure model.hK mu0 rewardKernel context hcontext sigma2 T delta defaultAction) (fun trajectory : RewardTrace Rat => ((pseudoRegret model (selectedPolicySuccessorGeneratedUCBRegretAction model.hK sigma2 T delta defaultAction (fun y : RewardTrace Rat => y) trajectory) T : Rat) : Real)) <= ((Finset.univ : Finset (Fin K)).filter (fun arm => 0 < (((model.gap arm : Rat) : Real)))).sum (fun arm => selectedPolicySuccessorTextbookGapBudget K sigma2 T delta (((model.gap arm : Rat) : Real)) + (((model.gap arm : Rat) : Real)) * ((T : Real) * delta))