Lean module · Tsallis-FTRL
BanditRLProof.TsallisFTRLMinimizerUniqueness
# Uniqueness of half-Tsallis finite-simplex minimizers 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.
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.
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.
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.
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