Lean module · Tsallis-FTRL
BanditRLProof.TsallisFiniteArmIndependentDriftingMeanRefinedRegret
# Refined regret for independent reward laws with drifting means This module connects the explicit mean-deviation budget of independent, nonidentical finite-arm reward laws to the compiled refined local self-bounding optimizer. The comparator remains the fixed baseline arm `model.bestArm`.
Module map
Imports
BanditRLProof.TsallisFiniteArmIndependentDriftingMeanRewardLaw, BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedTuning, BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedWindow
Imported by
BanditRLProof, BanditRLProof.TsallisFiniteArmIndependentDriftingMeanAllRegimes
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.finiteArmIndependentDriftingMeanRefinedCorruptionWindow
Compiled
The coefficient-aware refined corruption window specialized to the explicit mean-deviation budget.
noncomputable def finiteArmIndependentDriftingMeanRefinedCorruptionWindow {K : Nat} (model : FiniteBanditModel K) (horizon : Nat) (meanDeviation : Nat -> Fin K -> Real) : Prop
theorem
BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIndependentDriftingMeanRewardLawRegret_le_refinedLocalExplicit_of_window
Compiled
Refined local square-root regret against the fixed baseline comparator for independent, nonidentical reward laws whose means drift within an explicit armwise envelope. This is not dynamic regret.
theorem integral_sampledScheduledHalfTsallisFiniteArmIndependentDriftingMeanRewardLawRegret_le_refinedLocalExplicit_of_window {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (hprob : forall t arm, IsProbabilityMeasure (armLaw t arm)) (hbound : forall t arm, ∀ᵐ reward ∂armLaw t arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (meanDeviation : Nat -> Fin K -> Real) (hmeanDeviation : forall t arm, |finiteArmIndependentRewardMean armLaw t arm - ((model.mean arm : Rat) : Real)| <= meanDeviation t arm) (hsuboptimal : ((Finset.univ : Finset (Fin K)).erase model.bestArm).Nonempty) (hgapPos : forall arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (hgapLeOne : forall arm, arm ≠ model.bestArm -> ((model.gap arm : Rat) : Real) <= 1) (horizon : Nat) (hwindow : finiteArmIndependentDriftingMeanRefinedCorruptionWindow model horizon meanDeviation) : letI : Nonempty (Fin K)