Lean module · UCB
BanditRLProof.Algorithms.UCBRealStationaryFiniteArmRewardLaws
# External stationary UCB expected consistency This module transports the canonical one-policy arm-stream asymptotics through the complete observable law supplied by `RealStationaryUCBSequence`. The final endpoint instantiates the route from armwise-bounded Real reward laws.
Module map
Imports
BanditRLProof.Algorithms.UCBRealLMLCompat, BanditRLProof.Algorithms.UCBArmStreamFiniteArmRewardLaws
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCBRealStationaryCanonicalKernelTrajectory, BanditRLProof.Algorithms.UCBRealStationaryMeasurePreservingSource
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.UCB.realStationaryExpectedRegret
Compiled
Expected Real pseudo-regret of one fixed external action process.
noncomputable def realStationaryExpectedRegret {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (nu : Kernel (Fin K) Real) (action : Omega -> ActionTrace (Fin K)) (n : Nat) : Real
theorem
BanditRLProof.UCB.realStationaryExpectedRegret_eq_armStreamExpectedRegret
Compiled
The stationary UCB field bundle identifies each external expected-regret term exactly with the corresponding canonical arm-stream term at `c = 4`.
theorem realStationaryExpectedRegret_eq_armStreamExpectedRegret {Omega : Type u} {K : Nat} [NeZero K] [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (hK : 0 < K) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (h : RealStationaryUCBSequence mu hK 4 sigma2 nu action reward) (n : Nat) : realStationaryExpectedRegret mu nu action n = armStreamExpectedRegret hK sigma2 nu n
def
BanditRLProof.UCB.realStationaryExpectedAverageRegret
Compiled
External expected regret normalized by `n + 1`.
noncomputable def realStationaryExpectedAverageRegret {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (nu : Kernel (Fin K) Real) (action : Omega -> ActionTrace (Fin K)) (n : Nat) : Real
theorem
BanditRLProof.UCB.realStationaryExpectedAverageRegret_tendsto_zero
Compiled
Any fixed external process satisfying the stationary UCB field bundle inherits the canonical sub-Gaussian expected-average consistency theorem.
theorem realStationaryExpectedAverageRegret_tendsto_zero {Omega : Type u} {K : Nat} [NeZero K] [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (hK : 0 < K) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (h : RealStationaryUCBSequence mu hK 4 sigma2 nu action reward) (hsigma2 : Ne sigma2 0) (hsubG : forall arm : Fin K, HasSubgaussianMGF (fun x => x - realKernelMean nu arm) sigma2 (nu arm)) : Tendsto (realStationaryExpectedAverageRegret mu nu action) atTop (nhds 0)
def
BanditRLProof.UCB.realStationaryArmwiseBoundedFiniteArmExpectedRegret
Compiled
Expected regret of an external process over finite Real arm laws.
noncomputable def realStationaryArmwiseBoundedFiniteArmExpectedRegret {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (armLaw : Fin K -> Measure Real) (action : Omega -> ActionTrace (Fin K)) (n : Nat) : Real
def
BanditRLProof.UCB.realStationaryArmwiseBoundedFiniteArmModelCoefficient
Compiled
Canonical logarithmic-envelope coefficient for armwise-bounded laws.
noncomputable def realStationaryArmwiseBoundedFiniteArmModelCoefficient {K : Nat} (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Fin K -> Real) : Real
theorem
BanditRLProof.UCB.realStationaryArmwiseBoundedFiniteArmExpectedRegret_nonneg_and_le
Compiled
External armwise-bounded laws inherit the canonical logarithmic envelope.
theorem realStationaryArmwiseBoundedFiniteArmExpectedRegret_nonneg_and_le {Omega : Type u} {K : Nat} [NeZero K] [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Fin K -> Real) (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (hbound : forall arm, Filter.Eventually (fun x : Real => Set.Icc (lo arm) (hi arm) x) (ae (armLaw arm))) (h : @RealStationaryUCBSequence Omega K _ _ mu _ hK 4 (Concentration.finiteArmPositiveVarianceProxy (fun arm => Concentration.intervalVarianceProxy (lo arm) (hi arm))) (finiteArmRealRewardKernel armLaw) (finiteArmRealRewardKernel_isMarkov armLaw hprob) action reward) (n : Nat) : 0 <= realStationaryArmwiseBoundedFiniteArmExpectedRegret mu armLaw action n /\ realStationaryArmwiseBoundedFiniteArmExpectedRegret mu armLaw action n <= realStationaryArmwiseBoundedFiniteArmModelCoefficient armLaw hprob lo hi * (1 + Real.log ((n + 1 : Nat) : Real))
def
BanditRLProof.UCB.realStationaryArmwiseBoundedFiniteArmExpectedAverageRegret
Compiled
External finite-arm expected regret normalized by `n + 1`.
noncomputable def realStationaryArmwiseBoundedFiniteArmExpectedAverageRegret {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (armLaw : Fin K -> Measure Real) (action : Omega -> ActionTrace (Fin K)) (n : Nat) : Real
theorem
BanditRLProof.UCB.realStationaryArmwiseBoundedFiniteArmExpectedAverageRegret_tendsto_zero
Compiled
An external stationary UCB process driven by armwise-bounded finite Real laws has vanishing expected average regret. The same external measure, action trace, and reward trace are used at every horizon.
theorem realStationaryArmwiseBoundedFiniteArmExpectedAverageRegret_tendsto_zero {Omega : Type u} {K : Nat} [NeZero K] [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Fin K -> Real) (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (hbound : forall arm, Filter.Eventually (fun x : Real => Set.Icc (lo arm) (hi arm) x) (ae (armLaw arm))) (h : @RealStationaryUCBSequence Omega K _ _ mu _ hK 4 (Concentration.finiteArmPositiveVarianceProxy (fun arm => Concentration.intervalVarianceProxy (lo arm) (hi arm))) (finiteArmRealRewardKernel armLaw) (finiteArmRealRewardKernel_isMarkov armLaw hprob) action reward) : Tendsto (realStationaryArmwiseBoundedFiniteArmExpectedAverageRegret mu armLaw action) atTop (nhds 0)