BanditRLProof.TsallisRegularizer

Finite Tsallis power sum `sum_a p_a^alpha`.

noncomputable def powerSum {Action : Type u} (arms : Finset Action) (alpha : Real) (p : Action -> Real) : Real

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

Negative Tsallis entropy as the FTRL regularizer convention.

noncomputable def negEntropyRegularizer {Action : Type u} (arms : Finset Action) (alpha : Real) (p : Action -> Real) : Real

The Tsallis denominator is nonzero when `alpha != 1`.

theorem one_sub_exponent_ne_zero {alpha : Real} (halpha : alpha ≠ 1) : 1 - alpha ≠ 0

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

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))