Lean module · Tsallis-FTRL
BanditRLProof.FTRLOneStep
# FTRL one-step finite-sum wrapper This module records the deterministic optimization primitive used by FTRL/OMD routes. It consumes an explicit minimizer certificate for the regularized finite-action objective and returns the one-step linear-loss inequality against any feasible comparator. It does not prove convexity, minimizer existence, a Tsallis regularizer, a stability/penalty decomposition, or a regret theorem.
Module map
Imports
No project-local imports.
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.FTRL.linearLoss
Compiled
Finite-action linear loss of a weight vector against a loss vector.
noncomputable def linearLoss {Action : Type u} (arms : Finset Action) (p loss : Action -> Real) : Real
def
BanditRLProof.FTRL.finiteSimplex
Compiled
The finite probability-simplex predicate over an explicit action set.
def finiteSimplex {Action : Type u} (arms : Finset Action) (p : Action -> Real) : Prop
def
BanditRLProof.FTRL.regularizedObjective
Compiled
Regularized one-round FTRL objective `eta * <p, loss> + R p`. The learning-rate positivity contract is kept on the theorem, not the definition, so future leaves can reuse the objective algebraically.
noncomputable def regularizedObjective {Action : Type u} (arms : Finset Action) (eta : Real) (regularizer : (Action -> Real) -> Real) (loss : Action -> Real) (p : Action -> Real) : Real
def
BanditRLProof.FTRL.IsRegularizedMinimizer
Compiled
A point `p` minimizes the regularized objective over a feasible predicate.
def IsRegularizedMinimizer {Action : Type u} (feasible : (Action -> Real) -> Prop) (arms : Finset Action) (eta : Real) (regularizer : (Action -> Real) -> Real) (loss : Action -> Real) (p : Action -> Real) : Prop
theorem
BanditRLProof.FTRL.linearLoss_sub_le_regularizer_sub_div_of_isRegularizedMinimizer
Compiled
FTRL one-step inequality from an explicit regularized-objective minimizer. The conclusion is the deterministic algebraic form used before later leaves choose a concrete regularizer or prove a stability/penalty sum.
theorem linearLoss_sub_le_regularizer_sub_div_of_isRegularizedMinimizer {Action : Type u} (feasible : (Action -> Real) -> Prop) (arms : Finset Action) (eta : Real) (regularizer : (Action -> Real) -> Real) (loss : Action -> Real) (p q : Action -> Real) (heta : 0 < eta) (hp : IsRegularizedMinimizer feasible arms eta regularizer loss p) (hq : feasible q) : linearLoss arms p loss - linearLoss arms q loss <= (regularizer q - regularizer p) / eta
theorem
BanditRLProof.FTRL.linearLoss_sub_le_regularizer_sub_div_of_simplex_minimizer
Compiled
FTRL one-step inequality specialized to the finite simplex.
theorem linearLoss_sub_le_regularizer_sub_div_of_simplex_minimizer {Action : Type u} (arms : Finset Action) (eta : Real) (regularizer : (Action -> Real) -> Real) (loss : Action -> Real) (p q : Action -> Real) (heta : 0 < eta) (hp : IsRegularizedMinimizer (finiteSimplex arms) arms eta regularizer loss p) (hq : finiteSimplex arms q) : linearLoss arms p loss - linearLoss arms q loss <= (regularizer q - regularizer p) / eta