BanditRLProof.TsallisFTRLRegret

Coordinatewise cumulative loss before round `t`.

noncomputable def cumulativeLoss {Action : Type u} (loss : Nat -> Action -> Real) (t : Nat) : Action -> Real

No declaration docstring is present; use the chapter context and exact statement below.

@[simp] theorem cumulativeLoss_zero {Action : Type u} (loss : Nat -> Action -> Real) : cumulativeLoss loss 0 = 0

Adding one round appends its loss vector to the cumulative loss.

theorem cumulativeLoss_succ {Action : Type u} (loss : Nat -> Action -> Real) (t : Nat) : cumulativeLoss loss (t + 1) = fun action => cumulativeLoss loss t action + loss t action

Finite-action linear loss is additive in its loss-vector argument.

theorem linearLoss_add_right {Action : Type u} (arms : Finset Action) (p x y : Action -> Real) : linearLoss arms p (fun action => x action + y action) = linearLoss arms p x + linearLoss arms p y

A linear loss against the cumulative vector is the sum of round losses.

theorem linearLoss_cumulativeLoss {Action : Type u} (arms : Finset Action) (p : Action -> Real) (loss : Nat -> Action -> Real) (T : Nat) : linearLoss arms p (cumulativeLoss loss T) = (Finset.range T).sum (fun t => linearLoss arms p (loss t))

The cumulative regularized objective has the expected successor update.

theorem regularizedObjective_cumulativeLoss_succ {Action : Type u} (arms : Finset Action) (eta : Real) (regularizer : (Action -> Real) -> Real) (loss : Nat -> Action -> Real) (p : Action -> Real) (t : Nat) : regularizedObjective arms eta regularizer (cumulativeLoss loss (t + 1)) p = regularizedObjective arms eta regularizer (cumulativeLoss loss t) p + eta * linearLoss arms p (loss t)

Scaled regularized be-the-leader inequality for cumulative-loss minimizers. The point `p t` minimizes the objective built from losses before round `t`. Consequently the shifted choices `p (t + 1)` can be compared to the terminal cumulative objective while retaining the initial regularizer value.

theorem eta_mul_sum_next_linearLoss_add_regularizer_zero_le_objective {Action : Type u} (feasible : (Action -> Real) -> Prop) (arms : Finset Action) (eta : Real) (regularizer : (Action -> Real) -> Real) (loss : Nat -> Action -> Real) (p : Nat -> Action -> Real) (T : Nat) (hp : forall t, t <= T -> IsRegularizedMinimizer feasible arms eta regularizer (cumulativeLoss loss t) (p t)) : eta * (Finset.range T).sum (fun t => linearLoss arms (p (t + 1)) (loss t)) + regularizer (p 0) <= regularizedObjective arms eta regularizer (cumulativeLoss loss T) (p T)

Regularized be-the-leader bound against any feasible comparator.

theorem sum_next_linearLoss_sub_comparator_le_regularizer_penalty {Action : Type u} (feasible : (Action -> Real) -> Prop) (arms : Finset Action) (eta : Real) (regularizer : (Action -> Real) -> Real) (loss : Nat -> Action -> Real) (p : Nat -> Action -> Real) (q : Action -> Real) (T : Nat) (heta : 0 < eta) (hp : forall t, t <= T -> IsRegularizedMinimizer feasible arms eta regularizer (cumulativeLoss loss t) (p t)) (hq : feasible q) : (Finset.range T).sum (fun t => linearLoss arms (p (t + 1)) (loss t) - linearLoss arms q (loss t)) <= (regularizer q - regularizer (p 0)) / eta

Finite-horizon FTRL stability/penalty regret decomposition. The first sum on the right is the stability term. The second term is the regularizer penalty. No convexity or minimizer-existence theorem is hidden: all cumulative minimizer certificates are explicit inputs.

theorem cumulativeLinearLoss_sub_comparator_le_stability_add_penalty {Action : Type u} (feasible : (Action -> Real) -> Prop) (arms : Finset Action) (eta : Real) (regularizer : (Action -> Real) -> Real) (loss : Nat -> Action -> Real) (p : Nat -> Action -> Real) (q : Action -> Real) (T : Nat) (heta : 0 < eta) (hp : forall t, t <= T -> IsRegularizedMinimizer feasible arms eta regularizer (cumulativeLoss loss t) (p t)) (hq : feasible q) : (Finset.range T).sum (fun t => linearLoss arms (p t) (loss t) - linearLoss arms q (loss t)) <= (Finset.range T).sum (fun t => linearLoss arms (p t) (loss t) - linearLoss arms (p (t + 1)) (loss t)) + (regularizer q - regularizer (p 0)) / eta

Finite-simplex specialization of the FTRL decomposition.

theorem cumulativeLinearLoss_sub_comparator_le_stability_add_penalty_simplex {Action : Type u} (arms : Finset Action) (eta : Real) (regularizer : (Action -> Real) -> Real) (loss : Nat -> Action -> Real) (p : Nat -> Action -> Real) (q : Action -> Real) (T : Nat) (heta : 0 < eta) (hp : forall t, t <= T -> IsRegularizedMinimizer (finiteSimplex arms) arms eta regularizer (cumulativeLoss loss t) (p t)) (hq : finiteSimplex arms q) : (Finset.range T).sum (fun t => linearLoss arms (p t) (loss t) - linearLoss arms q (loss t)) <= (Finset.range T).sum (fun t => linearLoss arms (p t) (loss t) - linearLoss arms (p (t + 1)) (loss t)) + (regularizer q - regularizer (p 0)) / eta

Difference of negative Tsallis entropies as a power-sum difference.

theorem negEntropyRegularizer_sub_eq_powerSum_sub_div {Action : Type u} (arms : Finset Action) (alpha : Real) (p q : Action -> Real) (halpha : Ne alpha 1) : negEntropyRegularizer arms alpha q - negEntropyRegularizer arms alpha p = (powerSum arms alpha p - powerSum arms alpha q) / (1 - alpha)

Finite-horizon Tsallis-FTRL stability/penalty regret decomposition. The penalty is explicit in the finite power sums. The remaining algorithmic obligation is to bound the stability sum for the chosen Tsallis exponent and loss estimator, then supply minimizer existence and any stochastic contracts.

theorem cumulativeLinearLoss_sub_comparator_le_stability_add_powerSumPenalty {Action : Type u} (arms : Finset Action) (alpha eta : Real) (loss : Nat -> Action -> Real) (p : Nat -> Action -> Real) (q : Action -> Real) (T : Nat) (halpha : Ne alpha 1) (heta : 0 < eta) (hp : forall t, t <= T -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms alpha) (FTRL.cumulativeLoss loss t) (p t)) (hq : FTRL.finiteSimplex arms q) : (Finset.range T).sum (fun t => FTRL.linearLoss arms (p t) (loss t) - FTRL.linearLoss arms q (loss t)) <= (Finset.range T).sum (fun t => FTRL.linearLoss arms (p t) (loss t) - FTRL.linearLoss arms (p (t + 1)) (loss t)) + ((powerSum arms alpha (p 0) - powerSum arms alpha q) / (1 - alpha)) / eta