Lean module · Tsallis-FTRL
BanditRLProof.TsallisRegularizer
# Tsallis finite-simplex regularizer wrappers 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. It does not prove convexity, stability/penalty bounds, self-bounding conversion, learning-rate optimization, or regret.
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`.
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.
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.
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`.
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.
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`.
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))