Lean module · Tsallis-FTRL
BanditRLProof.TsallisSelfBoundingBetaRoot
# Tsallis self-bounding beta root 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.
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.
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.
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