Lean module · UCB

BanditRLProof.Algorithms.UCBFiniteArmSubGaussianSampledAsymptotics

# Sampled-pair UCB consistency for finite-arm sub-Gaussian laws This module instantiates the canonical sampled pair-trajectory asymptotic UCB route from stationary action-indexed reward laws. The fixed initial action is paired with a reward sampled from its arm law, while all successor laws use the context-independent Markov reward kernel.

Module map

Source: BanditRLProof/Algorithms/UCBFiniteArmSubGaussianSampledAsymptotics.lean
Teaching chapter: 4. UCB: confidence events to regret
Declarations: 8
Placeholders: 0

Imports

BanditRLProof.Algorithms.UCBConditionalRewardPairTrajectorySampledAsymptotics, BanditRLProof.FiniteArmRewardKernelLaw

Imported by

BanditRLProof, BanditRLProof.Algorithms.UCBArmwiseBoundedFiniteArmSampledAsymptotics, BanditRLProof.Algorithms.UCBBoundedFiniteArmSampledAsymptotics

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.UCB.finiteArmSubgaussianInitialActionRewardMeasure Compiled

Initial pair law obtained by attaching a fixed action to its reward law.

noncomputable def finiteArmSubgaussianInitialActionRewardMeasure {K : Nat} (armLaw : Fin K -> Measure Rat) (defaultAction : Fin K) : Measure (Prod (Fin K) Rat)

Source line 22 Chapter context: UCB

theorem BanditRLProof.UCB.finiteArmSubgaussianInitialActionRewardMeasure_isProbabilityMeasure Compiled

The fixed-action reward pushforward remains a probability measure.

theorem finiteArmSubgaussianInitialActionRewardMeasure_isProbabilityMeasure {K : Nat} (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (defaultAction : Fin K) : IsProbabilityMeasure (finiteArmSubgaussianInitialActionRewardMeasure armLaw defaultAction)

Source line 28 Chapter context: UCB

def BanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret Compiled

Exact sampled-successor expected pseudo-regret for stationary finite-arm sub-Gaussian laws. The UCB proxy is the armwise maximum padded by one and the confidence schedule is `1 / (T + 1)`.

noncomputable def selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (varianceProxy : Fin K -> NNReal) (defaultAction : Fin K) (T : Nat) : Real

Source line 43 Chapter context: UCB

theorem BanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret_nonneg_and_le Compiled

The exact practical sampled-successor expected pseudo-regret is nonnegative and satisfies the fixed-model logarithmic envelope at every large horizon.

theorem selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret_nonneg_and_le {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) (hlarge : 2 * K <= T + 1) : 0 <= selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret model armLaw hprob varianceProxy defaultAction T /\ selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret model armLaw hprob varianceProxy defaultAction T <= selectedPolicySuccessorAsymptoticModelCoefficient model (Concentration.finiteArmPositiveVarianceProxy varianceProxy) * (1 + Real.log (((T + 1 : Nat) : Real)))

Source line 69 Chapter context: UCB

theorem BanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret_isBigO_log Compiled

The exact practical expected pseudo-regret family is logarithmic.

theorem selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret_isBigO_log {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) : (selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret model armLaw hprob varianceProxy defaultAction) =O[atTop] (fun T : Nat => Real.log (((T + 1 : Nat) : Real)))

Source line 142 Chapter context: UCB

theorem BanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret_isLittleO_natCast_succ Compiled

The exact practical expected pseudo-regret is little-o of `T + 1`.

theorem selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret_isLittleO_natCast_succ {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) : (selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret model armLaw hprob varianceProxy defaultAction) =o[atTop] (fun T : Nat => (((T + 1 : Nat) : Real)))

Source line 204 Chapter context: UCB

def BanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedAveragePseudoRegret Compiled

Expected practical sampled-successor pseudo-regret normalized by `T + 1`.

noncomputable def selectedPolicySuccessorFiniteArmSubgaussianExpectedAveragePseudoRegret {K : Nat} (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (varianceProxy : Fin K -> NNReal) (defaultAction : Fin K) (T : Nat) : Real

Source line 226 Chapter context: UCB

theorem BanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedAveragePseudoRegret_tendsto_zero Compiled

For stationary finite-arm sub-Gaussian reward laws, the expected pseudo-regret of the horizon-indexed canonical sampled-pair UCB family, normalized by `T + 1`, tends to zero.

theorem selectedPolicySuccessorFiniteArmSubgaussianExpectedAveragePseudoRegret_tendsto_zero {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) : Tendsto (selectedPolicySuccessorFiniteArmSubgaussianExpectedAveragePseudoRegret model armLaw hprob varianceProxy defaultAction) atTop (nhds 0)

Source line 244 Open teaching explanation Chapter context: UCB