BanditRLProof.Algorithms.UCBConditionalRewardLawCenteredKernelReal

A positive-gap arm has a nonnegative textbook threshold contribution.

theorem selectedPolicySuccessorTextbookGapBudget_nonneg (K : Nat) (sigma2 : NNReal) (T : Nat) (delta gap : Real) (hgap : 0 < gap) : 0 <= selectedPolicySuccessorTextbookGapBudget K sigma2 T delta gap

Finite-horizon shifted UCB pseudo-regret is Bochner integrable whenever the underlying reward coordinates are measurable and the ambient measure is finite. No reward-law or concentration assumption is needed for this regularity statement.

theorem integrable_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (mu : Measure Omega) [IsFiniteMeasure mu] (model : FiniteBanditModel K) (sigma2 : NNReal) (T : Nat) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) : Integrable (fun omega : Omega => ((pseudoRegret model (selectedPolicySuccessorGeneratedUCBRegretAction hK sigma2 T delta defaultAction reward omega) T : Rat) : Real)) mu

Canonical Real/Bochner expected pseudo-regret theorem for the generated UCB trajectory measure and a centered sub-Gaussian reward kernel. The probabilistic work is inherited from the ENNReal canonical theorem. This wrapper proves finite-horizon integrability, uses nonnegativity of model gaps, and converts the finite ENNReal textbook sum term by term to `Real`.

theorem integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_trajMeasure_centeredKernel {Context : Type} {K : Nat} [MeasurableSpace Context] (model : FiniteBanditModel K) (mu0 : Measure Rat) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Fin K) Rat) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (mean : Context -> Fin K -> Rat) (varianceProxy : Context -> Fin K -> NNReal) (defaultAction : Fin K) (sigma2 : NNReal) (hcontext : forall n : Nat, Measurable (context n)) (hmean : Measurable (fun pair : Context × Fin K => mean pair.1 pair.2)) (hkernel : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (T : Nat) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hvariance : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, 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 : History.FiniteRewardHistory Rat i, forall arm : Fin K, mean (context i history) arm = model.mean arm) : 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))