BanditRLProof.TsallisTimeVaryingPenalty

The paper-normalized regularizer mass carried by the local potential.

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

The regularizer mass is `2 * sum sqrt(p_a) - 1`.

theorem halfTsallisPotentialMass_eq_two_mul_powerSum_sub_one {Action : Type u} (arms : Finset Action) (p : Action -> Real) : halfTsallisPotentialMass arms p = 2 * powerSum arms (1 / 2 : Real) p - 1

A supported point mass has paper-normalized potential mass one.

theorem halfTsallisPotentialMass_pointMass {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (hbest : best ∈ arms) : halfTsallisPotentialMass arms (pointMass best) = 1

The potential is linear loss with the regularizer mass divided by `eta`.

theorem halfTsallisPotentialValue_eq_neg_linearLoss_add_mass_div {Action : Type u} (arms : Finset Action) (eta : Real) (score p : Action -> Real) (heta : eta ≠ 0) : halfTsallisPotentialValue arms eta score p = -FTRL.linearLoss arms p score + halfTsallisPotentialMass arms p / eta

A regularized-objective minimizer maximizes the corresponding potential.

theorem halfTsallisPotentialValue_le_of_isRegularizedMinimizer {Action : Type u} (arms : Finset Action) (eta : Real) (score p q : Action -> Real) (heta : 0 < eta) (hp : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score p) (hq : FTRL.finiteSimplex arms q) : halfTsallisPotentialValue arms eta score q <= halfTsallisPotentialValue arms eta score p

Changing the learning rate at a fixed score costs the reciprocal-rate increment times the mass of the new minimizer.

theorem halfTsallisPotentialValue_new_sub_old_le_rateChange_mul_mass {Action : Type u} (arms : Finset Action) (etaOld etaNew : Real) (score pOld pNew : Action -> Real) (hetaOld : 0 < etaOld) (hetaNew : 0 < etaNew) (hpOld : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms etaOld (negEntropyRegularizer arms (1 / 2 : Real)) score pOld) (hpNew : FTRL.finiteSimplex arms pNew) : halfTsallisPotentialValue arms etaNew score pNew - halfTsallisPotentialValue arms etaOld score pOld <= (1 / etaNew - 1 / etaOld) * halfTsallisPotentialMass arms pNew

A zero-score minimizer maximizes the half-Tsallis regularizer mass.

theorem halfTsallisPotentialMass_le_of_zero_isRegularizedMinimizer {Action : Type u} (arms : Finset Action) (eta : Real) (p q : Action -> Real) (heta : 0 < eta) (hp : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun _ => 0) p) (hq : FTRL.finiteSimplex arms q) : halfTsallisPotentialMass arms q <= halfTsallisPotentialMass arms p

Algebraic telescope with different left and right endpoint processes.

theorem sum_range_succ_sub_eq_first_sub_last_add_cross (A B : Nat -> Real) (n : Nat) : (Finset.range (n + 1)).sum (fun t => A t - B t) = A 0 - B n + (Finset.range n).sum (fun t => A (t + 1) - B t)

Canonical scheduled minimizer before round `t`.

noncomputable def halfTsallisScheduledMinimizer {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Nat -> Action -> Real) (t : Nat) : Action -> Real

Canonical same-rate auxiliary minimizer after appending round `t`.

noncomputable def halfTsallisScheduledSameRateNext {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Nat -> Action -> Real) (t : Nat) : Action -> Real

Deterministic time-varying potential penalty with its terminal comparator contribution left explicit.

theorem sum_halfTsallisScheduledPotentialPenalty_le {Action : Type u} (arms : Finset Action) (eta : Nat -> Real) (loss : Nat -> Action -> Real) (current sameRateNext : Nat -> Action -> Real) (q : Action -> Real) (n : Nat) (heta : forall t, t <= n -> 0 < eta t) (hcurrent : forall t, t <= n -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms (eta t) (negEntropyRegularizer arms (1 / 2 : Real)) (FTRL.cumulativeLoss loss t) (current t)) (hnext : forall t, t <= n -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms (eta t) (negEntropyRegularizer arms (1 / 2 : Real)) (FTRL.cumulativeLoss loss (t + 1)) (sameRateNext t)) (hq : FTRL.finiteSimplex arms q) : (Finset.range (n + 1)).sum (fun t => halfTsallisPotentialValue arms (eta t) (FTRL.cumulativeLoss loss t) (current t) - halfTsallisPotentialValue arms (eta t) (FTRL.cumulativeLoss loss (t + 1)) (sameRateNext t) - FTRL.linearLoss arms q (loss t)) <= halfTsallisPotentialMass arms (current 0) / eta 0 + (Finset.range n).sum (fun t => (1 / eta (t + 1) - 1 / eta t) * halfTsallisPotentialMass arms (current (t + 1))) - halfTsallisPotentialMass arms q / eta n

Under a nonincreasing positive schedule, every rate-change mass is bounded by the initial zero-score mass, so the reciprocal-rate increments telescope.

theorem sum_halfTsallisScheduledPotentialPenalty_le_initial_sub_comparator_div {Action : Type u} (arms : Finset Action) (eta : Nat -> Real) (loss : Nat -> Action -> Real) (current sameRateNext : Nat -> Action -> Real) (q : Action -> Real) (n : Nat) (heta : forall t, t <= n -> 0 < eta t) (hetaMono : forall t, t < n -> eta (t + 1) <= eta t) (hcurrent : forall t, t <= n -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms (eta t) (negEntropyRegularizer arms (1 / 2 : Real)) (FTRL.cumulativeLoss loss t) (current t)) (hnext : forall t, t <= n -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms (eta t) (negEntropyRegularizer arms (1 / 2 : Real)) (FTRL.cumulativeLoss loss (t + 1)) (sameRateNext t)) (hq : FTRL.finiteSimplex arms q) : (Finset.range (n + 1)).sum (fun t => halfTsallisPotentialValue arms (eta t) (FTRL.cumulativeLoss loss t) (current t) - halfTsallisPotentialValue arms (eta t) (FTRL.cumulativeLoss loss (t + 1)) (sameRateNext t) - FTRL.linearLoss arms q (loss t)) <= (halfTsallisPotentialMass arms (current 0) - halfTsallisPotentialMass arms q) / eta n

Canonical minimizer endpoint for the deterministic scheduled penalty.

theorem sum_halfTsallisCanonicalScheduledPotentialPenalty_le {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Nat -> Action -> Real) (q : Action -> Real) (n : Nat) (heta : forall t, t <= n -> 0 < eta t) (hetaMono : forall t, t < n -> eta (t + 1) <= eta t) (hq : FTRL.finiteSimplex arms q) : (Finset.range (n + 1)).sum (fun t => halfTsallisPotentialValue arms (eta t) (FTRL.cumulativeLoss loss t) (halfTsallisScheduledMinimizer arms harms eta loss t) - halfTsallisPotentialValue arms (eta t) (FTRL.cumulativeLoss loss (t + 1)) (halfTsallisScheduledSameRateNext arms harms eta loss t) - FTRL.linearLoss arms q (loss t)) <= (halfTsallisPotentialMass arms (halfTsallisScheduledMinimizer arms harms eta loss 0) - halfTsallisPotentialMass arms q) / eta n

Best-arm specialization retaining the explicit terminal `-1 / eta n` contribution encoded by the point-mass comparator.

theorem sum_halfTsallisCanonicalScheduledPotentialPenalty_pointMass_le {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Nat -> Action -> Real) {best : Action} (hbest : best ∈ arms) (n : Nat) (heta : forall t, t <= n -> 0 < eta t) (hetaMono : forall t, t < n -> eta (t + 1) <= eta t) : (Finset.range (n + 1)).sum (fun t => halfTsallisPotentialValue arms (eta t) (FTRL.cumulativeLoss loss t) (halfTsallisScheduledMinimizer arms harms eta loss t) - halfTsallisPotentialValue arms (eta t) (FTRL.cumulativeLoss loss (t + 1)) (halfTsallisScheduledSameRateNext arms harms eta loss t) - FTRL.linearLoss arms (pointMass best) (loss t)) <= halfTsallisPotentialMass arms (halfTsallisScheduledMinimizer arms harms eta loss 0) / eta n - 1 / eta n