Lean module · UCB
BanditRLProof.Algorithms.UCBBoundedFiniteArmRewardLaw
This module instantiates the centered-kernel canonical Real theorem with stationary action-indexed reward laws. It supports both one common interval and arm-dependent nondegenerate intervals.
Module map
Imports
BanditRLProof.Algorithms.UCBConditionalRewardLawCenteredKernelReal, BanditRLProof.FiniteArmRewardKernelLaw
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.UCB.integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_boundedFiniteArmLaws
Compiled
Canonical Real expected pseudo-regret bound for finite-arm stationary reward laws supported almost surely on one nondegenerate interval. The initial reward is sampled from the default arm law. Successor rewards use the context-independent action law kernel, while the context is `Unit`.
Used in these reading views: Bandit Book · Reinforcement Learning Book
4. UCB: confidence events to regret
Canonical node identity
declaration:BanditRLProof.UCB.integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_boundedFiniteArmLawsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_boundedFiniteArmLaws {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hlohi : lo < hi) (hmeas : forall arm, AEMeasurable (fun reward : Rat => ((reward : Rat) : Real)) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc lo hi ((reward : Rat) : Real)) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (defaultAction : Fin K) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) : let sigma2 := Concentration.intervalVarianceProxy lo hi let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context := Unit) armLaw hprob let context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Unit := fun _ _ => () MeasureTheory.integral (selectedPolicySuccessorRewardTrajMeasure model.hK (armLaw defaultAction) rewardKernel context (fun _ => measurable_const) 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))
theorem
BanditRLProof.UCB.integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_armwiseBoundedFiniteArmLaws
Compiled
Canonical Real expected pseudo-regret bound for finite-arm stationary reward laws with arm-dependent nondegenerate support intervals. The UCB variance parameter is the maximum of the armwise Hoeffding proxies, computed internally with `Finset.sup` over all arms.
Used in these reading views: Bandit Book · Reinforcement Learning Book
4. UCB: confidence events to regret
Canonical node identity
declaration:BanditRLProof.UCB.integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_armwiseBoundedFiniteArmLawsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_armwiseBoundedFiniteArmLaws {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Fin K -> Real) (hlohi : forall arm, lo arm < hi arm) (hmeas : forall arm, AEMeasurable (fun reward : Rat => ((reward : Rat) : Real)) (armLaw arm)) (hbound : forall arm, Filter.Eventually (fun reward : Rat => Set.Icc (lo arm) (hi arm) ((reward : Rat) : Real)) (ae (armLaw arm))) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (defaultAction : Fin K) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) : let sigma2 := Concentration.finiteArmIntervalVarianceProxy lo hi let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context := Unit) armLaw hprob let context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Unit := fun _ _ => () MeasureTheory.integral (selectedPolicySuccessorRewardTrajMeasure model.hK (armLaw defaultAction) rewardKernel context (fun _ => measurable_const) 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))