Lean module · Tsallis-FTRL
BanditRLProof.TsallisFiniteArmIndependentDriftingMeanRefinedRegret
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.finiteArmIndependentDriftingMeanRefinedCorruptionWindowReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIndependentDriftingMeanRewardLawRegret_le_refinedLocalExplicit_of_windowReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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)