Lean module · Tsallis-FTRL
BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedScalar
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.refinedLocalBetaEquationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.continuousOn_refinedLocalBetaEquationReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.sq_sqrt_sub_one_le_sub_log_sub_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.refinedLocalBetaWeight_bounds_of_eq_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.exists_refinedLocalBetaEquation_eq_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.exists_refinedLocalBetaEquation_eq_zero_and_weight_boundsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.refinedLocalAlphaReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def refinedLocalAlpha (scale reciprocalGap beta : Real) : Real
def
BanditRLProof.Tsallis.refinedLocalLambda
Compiled
The inverse of `alpha = 2 * lambda / (1 + lambda)`.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.refinedLocalLambdaReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.refinedLocalAlpha_sqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.refinedLocalAlpha_posReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.refinedLocalAlpha_le_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.refinedLocalLambda_mem_IocReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.one_add_refinedLocalLambda_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.two_mul_refinedLocalLambda_div_one_add_eq_alphaReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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