Lean module · Tsallis-FTRL
BanditRLProof.TsallisRegularizer
This module records the first deterministic Real.rpow surface for Tsallis-INF/FTRL routes. It defines the finite-action Tsallis power sum, Tsallis entropy, and the negative-entropy regularizer used as an FTRL regularizer, then packages the small well-definedness side conditions over the finite simplex.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.TsallisFTRLRegret, BanditRLProof.TsallisImportanceWeightedMoment
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.powerSum
Compiled
Finite Tsallis power sum `sum_a p_a^alpha`.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.powerSumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def powerSum {Action : Type u} (arms : Finset Action) (alpha : Real) (p : Action -> Real) : Real
def
BanditRLProof.Tsallis.entropy
Compiled
Tsallis entropy on a finite action set, with denominator left explicit.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.entropyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def entropy {Action : Type u} (arms : Finset Action) (alpha : Real) (p : Action -> Real) : Real
def
BanditRLProof.Tsallis.negEntropyRegularizer
Compiled
Negative Tsallis entropy as the FTRL regularizer convention.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.negEntropyRegularizerReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def negEntropyRegularizer {Action : Type u} (arms : Finset Action) (alpha : Real) (p : Action -> Real) : Real
theorem
BanditRLProof.Tsallis.one_sub_exponent_ne_zero
Compiled
The Tsallis denominator is nonzero when `alpha != 1`.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.one_sub_exponent_ne_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem one_sub_exponent_ne_zero {alpha : Real} (halpha : alpha ≠ 1) : 1 - alpha ≠ 0
theorem
BanditRLProof.Tsallis.powerSum_nonneg_of_finiteSimplex
Compiled
The Tsallis power sum is nonnegative on the finite simplex.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.powerSum_nonneg_of_finiteSimplexReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem powerSum_nonneg_of_finiteSimplex {Action : Type u} (arms : Finset Action) (alpha : Real) (p : Action -> Real) (hp : FTRL.finiteSimplex arms p) : 0 <= powerSum arms alpha p
theorem
BanditRLProof.Tsallis.negEntropyRegularizer_wellDefined_on_finiteSimplex
Compiled
Well-definedness package for the finite-simplex Tsallis regularizer. The two facts exposed here are the local obligations needed before later Tsallis/FTRL leaves can use `Real.rpow` algebra and division by `1 - alpha`.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.negEntropyRegularizer_wellDefined_on_finiteSimplexReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem negEntropyRegularizer_wellDefined_on_finiteSimplex {Action : Type u} (arms : Finset Action) (alpha : Real) (p : Action -> Real) (hp : FTRL.finiteSimplex arms p) (halpha : alpha ≠ 1) : 0 <= powerSum arms alpha p ∧ 1 - alpha ≠ 0 ∧ negEntropyRegularizer arms alpha p = - ((powerSum arms alpha p - 1) / (1 - alpha))