Lean module · Tsallis-FTRL
BanditRLProof.TsallisSelfBoundingBetaRoot
This module isolates the scalar intermediate-value step used by the refined self-bounding tuning route. It proves existence of a root in the paper's admissible beta interval without assuming a Lambert-W API. Quantitative bounds on that root remain downstream obligations.
Module map
Imports
BanditRLProof.TsallisSqrtScheduleSelfBoundingTuning
Imported by
BanditRLProof, BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedScalar
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.selfBoundingBetaEquation
Compiled
The scalar equation used to tune the refined self-bounding parameter.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.selfBoundingBetaEquationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def selfBoundingBetaEquation (scale reciprocalGap corruption beta : Real) : Real
theorem
BanditRLProof.Tsallis.continuousOn_selfBoundingBetaEquation
Compiled
The beta equation is continuous on every interval bounded below by one.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.continuousOn_selfBoundingBetaEquationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem continuousOn_selfBoundingBetaEquation (scale reciprocalGap corruption upper : Real) : ContinuousOn (selfBoundingBetaEquation scale reciprocalGap corruption) (Icc 1 upper)
theorem
BanditRLProof.Tsallis.exists_selfBoundingBetaEquation_eq_zero
Compiled
Under the corruption window used by the refined Tsallis-INF analysis, the scalar beta equation has a zero between one and `scale / reciprocalGap ^ 2`. This is the intermediate-value certificate that precedes any quantitative Lambert-W estimate.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.exists_selfBoundingBetaEquation_eq_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exists_selfBoundingBetaEquation_eq_zero (scale reciprocalGap corruption : Real) (hscale : 0 < scale) (hreciprocalGap : 0 < reciprocalGap) (hupper : 1 <= scale / reciprocalGap ^ 2) (hcorruptionUpper : corruption * reciprocalGap <= scale) (hcorruptionLower : reciprocalGap * (Real.log (scale / reciprocalGap ^ 2) + 1) <= corruption) : exists beta, beta ∈ Icc 1 (scale / reciprocalGap ^ 2) ∧ selfBoundingBetaEquation scale reciprocalGap corruption beta = 0