Lean module · Tsallis-FTRL
BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedWindow
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedScalar
Imported by
BanditRLProof, BanditRLProof.TsallisFiniteArmIIDHistoryAdaptiveRefinedCorruptedRewardLaw, BanditRLProof.TsallisFiniteArmIndependentDriftingMeanRefinedRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.RefinedLocalCorruptionWindow
Compiled
A compact sufficient window for the coefficient-aware refined optimizer. Here `armCount` is the number of suboptimal arms, `horizonMass = T + 1`, `reciprocalGap` is the sum of inverse gaps, and `corruption` is the self-bound allowance.
def RefinedLocalCorruptionWindow (armCount horizonMass reciprocalGap corruption : Real) : Prop
theorem
BanditRLProof.Tsallis.refinedLocalCorruptionWindow_scalar_bounds
Compiled
The compact window plus `armCount <= reciprocalGap` supplies all scalar contracts used by the generated refined theorem.
theorem refinedLocalCorruptionWindow_scalar_bounds (armCount horizonMass reciprocalGap corruption : Real) (harmCount : 1 <= armCount) (hhorizonMass : 0 < horizonMass) (hreciprocalGap : 0 < reciprocalGap) (hcountGap : armCount <= reciprocalGap) (hwindow : RefinedLocalCorruptionWindow armCount horizonMass reciprocalGap corruption) : 2 <= (2 * armCount * horizonMass) / (25 * reciprocalGap ^ 2) ∧ (2 * armCount * horizonMass) / (25 * reciprocalGap ^ 2) <= 2 * horizonMass ∧ 2 * (corruption * reciprocalGap) <= 2 * armCount * horizonMass ∧ 25 * reciprocalGap * (Real.log ((2 * armCount * horizonMass) / (25 * reciprocalGap ^ 2)) + 2) <= corruption ∧ 0 < corruption