Lean module · Tsallis-FTRL
BanditRLProof.TsallisFTRLMinimizerUniqueness
The square-root sum is strictly concave on a nonempty standard simplex, so the half-Tsallis regularized objective is strictly convex there. The project-level finite simplex leaves coordinates outside arms unconstrained; accordingly, the public uniqueness theorem identifies exactly the supported coordinates.
Module map
Imports
BanditRLProof.TsallisFTRLMinimizerExistence
Imported by
BanditRLProof, BanditRLProof.TsallisFTRLMinimizerMeasurability
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Tsallis.strictConcaveOn_sum_sqrt_stdSimplex
Compiled
The finite sum of square roots is strictly concave on every nonempty standard simplex.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.strictConcaveOn_sum_sqrt_stdSimplexReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem strictConcaveOn_sum_sqrt_stdSimplex {Action : Type u} [Fintype Action] [Nonempty Action] : StrictConcaveOn Real (stdSimplex Real Action) (fun p : Action -> Real => (Finset.univ : Finset Action).sum (fun action => Real.sqrt (p action)))
theorem
BanditRLProof.Tsallis.strictConvexOn_regularizedObjective_half_stdSimplex
Compiled
On a nonempty finite standard simplex, the half-Tsallis regularized objective is strictly convex in the probability vector.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.strictConvexOn_regularizedObjective_half_stdSimplexReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem strictConvexOn_regularizedObjective_half_stdSimplex {Action : Type u} [Fintype Action] [Nonempty Action] (eta : Real) (score : Action -> Real) : StrictConvexOn Real (stdSimplex Real Action) (fun p => FTRL.regularizedObjective Finset.univ eta (negEntropyRegularizer Finset.univ (1 / 2 : Real)) score p)
theorem
BanditRLProof.Tsallis.isRegularizedMinimizer_half_eq_on_arms
Compiled
Two half-Tsallis minimizers have identical coordinates on the explicit arm set. Coordinates outside `arms` are intentionally not constrained by the project finite-simplex predicate or objective.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.isRegularizedMinimizer_half_eq_on_armsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem isRegularizedMinimizer_half_eq_on_arms {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score p q : Action -> Real) (hp : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score p) (hq : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score q) : forall action, action ∈ arms -> p action = q action
theorem
BanditRLProof.Tsallis.halfTsallisMinimizer_eq_on_arms
Compiled
The canonical selected minimizer agrees on every supported coordinate with any other half-Tsallis minimizer certificate.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.halfTsallisMinimizer_eq_on_armsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem halfTsallisMinimizer_eq_on_arms {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score p : Action -> Real) (hp : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score p) : forall action, action ∈ arms -> halfTsallisMinimizer arms harms eta score action = p action