Lean module · Tsallis-FTRL
BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedScalar
# Coefficient-aware refined self-bounding scalar tuning The local refined stability envelope has coefficient `5`. After the change of variables used by the square-root schedule, its scalar objective therefore has a beta equation with offset `2`, rather than the paper's idealized offset `1`. This module records the corrected root interval and an elementary root estimate that does not require Lambert W.
Module map
Imports
BanditRLProof.TsallisSelfBoundingBetaRoot
Imported by
BanditRLProof, BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedTuning, BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedWindow
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.refinedLocalBetaEquation
Compiled
The beta equation produced by the local coefficient-five envelope.
noncomputable def refinedLocalBetaEquation (scale reciprocalGap corruption beta : Real) : Real
theorem
BanditRLProof.Tsallis.continuousOn_refinedLocalBetaEquation
Compiled
The local beta equation is continuous on every interval bounded below by one.
theorem continuousOn_refinedLocalBetaEquation (scale reciprocalGap corruption upper : Real) : ContinuousOn (refinedLocalBetaEquation scale reciprocalGap corruption) (Icc 1 upper)
theorem
BanditRLProof.Tsallis.sq_sqrt_sub_one_le_sub_log_sub_one
Compiled
The elementary inequality behind the Lambert-free beta estimate.
theorem sq_sqrt_sub_one_le_sub_log_sub_one (weight : Real) (hweight : 1 <= weight) : (Real.sqrt weight - 1) ^ 2 <= weight - Real.log weight - 1
theorem
BanditRLProof.Tsallis.refinedLocalBetaWeight_bounds_of_eq_zero
Compiled
A root of the coefficient-five equation admits the same kind of elementary upper estimate as the paper's Lambert-W expression, with the offset correction appearing as `+1` under the outer square root.
theorem refinedLocalBetaWeight_bounds_of_eq_zero (scale reciprocalGap corruption beta : Real) (hscale : 0 < scale) (hreciprocalGap : 0 < reciprocalGap) (hcorruption : 0 < corruption) (hbeta : 1 <= beta) (hcorruptionUpper : corruption * reciprocalGap <= scale) (hroot : refinedLocalBetaEquation scale reciprocalGap corruption beta = 0) : let weight := corruption * reciprocalGap / scale * beta 1 <= weight ∧ weight <= (1 + Real.sqrt (Real.log (scale / (corruption * reciprocalGap)) + 1)) ^ 2
theorem
BanditRLProof.Tsallis.exists_refinedLocalBetaEquation_eq_zero
Compiled
Under the coefficient-aware corruption window, the corrected beta equation has a root in the interval that corresponds to `alpha` between the local horizon threshold and one.
theorem exists_refinedLocalBetaEquation_eq_zero (scale reciprocalGap corruption : Real) (hscale : 0 < scale) (hreciprocalGap : 0 < reciprocalGap) (hupper : 2 <= scale / (25 * reciprocalGap ^ 2)) (hcorruptionUpper : 2 * (corruption * reciprocalGap) <= scale) (hcorruptionLower : 25 * reciprocalGap * (Real.log (scale / (25 * reciprocalGap ^ 2)) + 2) <= corruption) : exists beta, beta ∈ Icc 2 (scale / (25 * reciprocalGap ^ 2)) ∧ refinedLocalBetaEquation scale reciprocalGap corruption beta = 0
theorem
BanditRLProof.Tsallis.exists_refinedLocalBetaEquation_eq_zero_and_weight_bounds
Compiled
The coefficient-aware corruption window yields a beta root together with the elementary quantitative weight estimate needed by the refined regret route.
theorem exists_refinedLocalBetaEquation_eq_zero_and_weight_bounds (scale reciprocalGap corruption : Real) (hscale : 0 < scale) (hreciprocalGap : 0 < reciprocalGap) (hcorruption : 0 < corruption) (hupper : 2 <= scale / (25 * reciprocalGap ^ 2)) (hcorruptionUpper : 2 * (corruption * reciprocalGap) <= scale) (hcorruptionLower : 25 * reciprocalGap * (Real.log (scale / (25 * reciprocalGap ^ 2)) + 2) <= corruption) : exists beta, beta ∈ Icc 2 (scale / (25 * reciprocalGap ^ 2)) ∧ refinedLocalBetaEquation scale reciprocalGap corruption beta = 0 ∧ let weight := corruption * reciprocalGap / scale * beta 1 <= weight ∧ weight <= (1 + Real.sqrt (Real.log (scale / (corruption * reciprocalGap)) + 1)) ^ 2
def
BanditRLProof.Tsallis.refinedLocalAlpha
Compiled
The coefficient-aware change of variables from beta to alpha.
noncomputable def refinedLocalAlpha (scale reciprocalGap beta : Real) : Real
def
BanditRLProof.Tsallis.refinedLocalLambda
Compiled
The inverse of `alpha = 2 * lambda / (1 + lambda)`.
noncomputable def refinedLocalLambda (scale reciprocalGap beta : Real) : Real
theorem
BanditRLProof.Tsallis.refinedLocalAlpha_sq
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem refinedLocalAlpha_sq (scale reciprocalGap beta : Real) (hscale : 0 < scale) (hbeta : 0 <= beta) : refinedLocalAlpha scale reciprocalGap beta ^ 2 = 25 * reciprocalGap ^ 2 * beta / scale
theorem
BanditRLProof.Tsallis.refinedLocalAlpha_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem refinedLocalAlpha_pos (scale reciprocalGap beta : Real) (hscale : 0 < scale) (hreciprocalGap : 0 < reciprocalGap) (hbeta : 0 < beta) : 0 < refinedLocalAlpha scale reciprocalGap beta
theorem
BanditRLProof.Tsallis.refinedLocalAlpha_le_one
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem refinedLocalAlpha_le_one (scale reciprocalGap beta : Real) (hscale : 0 < scale) (hreciprocalGap : 0 < reciprocalGap) (hbeta : beta <= scale / (25 * reciprocalGap ^ 2)) : refinedLocalAlpha scale reciprocalGap beta <= 1
theorem
BanditRLProof.Tsallis.refinedLocalLambda_mem_Ioc
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem refinedLocalLambda_mem_Ioc (scale reciprocalGap beta : Real) (hscale : 0 < scale) (hreciprocalGap : 0 < reciprocalGap) (hbetaPos : 0 < beta) (hbetaUpper : beta <= scale / (25 * reciprocalGap ^ 2)) : refinedLocalLambda scale reciprocalGap beta ∈ Set.Ioc (0 : Real) 1
theorem
BanditRLProof.Tsallis.one_add_refinedLocalLambda_eq
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem one_add_refinedLocalLambda_eq (scale reciprocalGap beta : Real) (halpha : refinedLocalAlpha scale reciprocalGap beta < 2) : 1 + refinedLocalLambda scale reciprocalGap beta = 2 / (2 - refinedLocalAlpha scale reciprocalGap beta)
theorem
BanditRLProof.Tsallis.two_mul_refinedLocalLambda_div_one_add_eq_alpha
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem two_mul_refinedLocalLambda_div_one_add_eq_alpha (scale reciprocalGap beta : Real) (halpha : refinedLocalAlpha scale reciprocalGap beta < 2) : 2 * refinedLocalLambda scale reciprocalGap beta / (1 + refinedLocalLambda scale reciprocalGap beta) = refinedLocalAlpha scale reciprocalGap beta