Lean module · UCB
BanditRLProof.Algorithms.UCBFiniteArmSubGaussianRewardLaw
# Canonical UCB expected regret for sub-Gaussian finite-arm reward laws This module instantiates the centered-kernel canonical Real theorem directly from stationary action-indexed sub-Gaussian reward laws, without bounded-support assumptions.
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_finiteArmSubgaussianLaws
Compiled
Canonical Real expected pseudo-regret bound for stationary finite-arm reward laws with direct centered sub-Gaussian MGF witnesses. The UCB variance parameter is the maximum of the armwise proxies. At least one proxy must be positive because the existing canonical UCB route requires a strictly positive common proxy; zero proxies for other arms are allowed.
theorem integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_finiteArmSubgaussianLaws {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (varianceProxy : Fin K -> NNReal) (hvariancePositive : exists arm, 0 < ((varianceProxy arm : NNReal) : Real)) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (hsubG : forall arm, HasSubgaussianMGF (fun reward : Rat => (((reward - model.mean arm : Rat) : Real))) (varianceProxy arm) (armLaw arm)) (defaultAction : Fin K) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) : let sigma2 := Concentration.finiteArmVarianceProxy varianceProxy let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context
theorem
BanditRLProof.UCB.integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_finiteArmSubgaussianLaws_without_proxy_positivity
Compiled
Canonical Real expected pseudo-regret bound for stationary finite-arm reward laws with direct centered sub-Gaussian MGF witnesses, including an all-zero proxy family. The common UCB tuning proxy is the finite maximum padded by one, so callers provide neither a positivity witness nor a separate ceiling.
theorem integral_real_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_finiteArmSubgaussianLaws_without_proxy_positivity {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (varianceProxy : Fin K -> NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => ((reward : Rat) : Real)) = ((model.mean arm : Rat) : Real)) (hsubG : forall arm, HasSubgaussianMGF (fun reward : Rat => (((reward - model.mean arm : Rat) : Real))) (varianceProxy arm) (armLaw arm)) (defaultAction : Fin K) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) : let sigma2 := Concentration.finiteArmPositiveVarianceProxy varianceProxy let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context