Lean module · Tsallis-FTRL
BanditRLProof.TsallisFTRLOneStepStability
# Half-Tsallis FTRL one-step stability This module proves the deterministic one-step stability estimate used by the `alpha = 1 / 2` Tsallis-INF route. It consumes explicit interior stationarity certificates for the current and importance-weighted updated distributions. The certificates expose exactly the KKT equation for the local objective `eta * <p, score> + negEntropyRegularizer arms (1 / 2) p`. The final theorem averages the pathwise stability term over the current finite simplex and bounds it by `2 * eta * sum_a sqrt (p a)`. It does not derive the stationarity certificates from minimizer certificates, prove minimizer interiority/existence, or perform a conditional-expectation transport. This is a valid but looser route for the stability term in the local FTRL decomposition, not a literal port of the conjugate-potential stability bound in Tsallis-INF Lemmas 11/19. Matching the paper's half-Tsallis regularizer scaling uses `eta_local = eta_paper / 2` up to simplex-constant terms; the bound here is then `eta_paper * sum_a sqrt (p a)`, twice the comparable Lemma 11 coefficient.
Module map
Imports
BanditRLProof.TsallisFTRLRegret, BanditRLProof.TsallisImportanceWeightedMoment
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.HalfTsallisInteriorStationary
Compiled
Interior first-order stationarity for the half-Tsallis regularizer. For `alpha = 1 / 2`, the coordinate derivative of the local negative Tsallis entropy is `-p_a^(-1/2)`. The common multiplier records the simplex equality constraint; positivity and normalization are kept as separate theorem inputs.
def HalfTsallisInteriorStationary {Action : Type u} (arms : Finset Action) (eta : Real) (score p : Action -> Real) (multiplier : Real) : Prop
theorem
BanditRLProof.Tsallis.halfTsallisInteriorStationary_rpow_sub_rpow_eq
Compiled
Subtracting two half-Tsallis stationarity equations isolates the update.
theorem halfTsallisInteriorStationary_rpow_sub_rpow_eq {Action : Type u} (arms : Finset Action) (eta : Real) (score increment p q : Action -> Real) (multiplier nextMultiplier : Real) (hp : HalfTsallisInteriorStationary arms eta score p multiplier) (hq : HalfTsallisInteriorStationary arms eta (fun action => score action + increment action) q nextMultiplier) {action : Action} (haction : action ∈ arms) : (q action) ^ (-(1 / 2 : Real)) - (p action) ^ (-(1 / 2 : Real)) = eta * increment action - (nextMultiplier - multiplier)
theorem
BanditRLProof.Tsallis.sub_le_two_mul_rpow_three_halves_mul_neg_half_rpow_sub
Compiled
Scalar half-Tsallis curvature inequality on the positive cone. This is the one-dimensional inequality that converts a negative-half-power gradient displacement into a displacement of probability mass.
theorem sub_le_two_mul_rpow_three_halves_mul_neg_half_rpow_sub {p q : Real} (hp : 0 < p) (hq : 0 < q) (hqp : q <= p) : p - q <= 2 * p ^ (3 / 2 : Real) * (q ^ (-(1 / 2 : Real)) - p ^ (-(1 / 2 : Real)))
theorem
BanditRLProof.Tsallis.linearLoss_sub_next_importanceWeightedLoss_le
Compiled
Pathwise half-Tsallis FTRL stability for one importance-weighted observation. The current and updated distributions are normalized and strictly positive on `arms`. Their stationarity certificates force the multiplier displacement to lie between zero and the selected coordinate update; the scalar curvature lemma then controls the one-step linear-loss difference.
theorem linearLoss_sub_next_importanceWeightedLoss_le {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score prob next loss : Action -> Real) (chosen : Action) (multiplier nextMultiplier : Real) (hchosen : chosen ∈ arms) (heta : 0 < eta) (hprobSimplex : FTRL.finiteSimplex arms prob) (hnextSimplex : FTRL.finiteSimplex arms next) (hprobPos : forall action, action ∈ arms -> 0 < prob action) (hnextPos : forall action, action ∈ arms -> 0 < next action) (hlossNonneg : forall action, action ∈ arms -> 0 <= loss action) (hprobStationary : HalfTsallisInteriorStationary arms eta score prob multiplier) (hnextStationary : HalfTsallisInteriorStationary arms eta (fun action => score action + Exp3.importanceWeightedLoss prob loss chosen action) next nextMultiplier) : FTRL.linearLoss arms prob (Exp3.importanceWeightedLoss prob loss chosen) - FTRL.linearLoss arms next (Exp3.importanceWeightedLoss prob loss chosen) <= 2 * eta * powerWeightedSquaredImportanceWeightedLoss arms (1 / 2 : Real) prob loss chosen
theorem
BanditRLProof.Tsallis.sum_prob_mul_linearLoss_sub_next_importanceWeightedLoss_le_powerSum_half
Compiled
Sampling-law finite-sum half-Tsallis stability bound. For every possible sampled action, `next chosen` carries its own updated stationarity certificate. Averaging the pathwise FTRL stability terms with the current simplex masses is bounded by `2 * eta` times the half-power sum.
theorem sum_prob_mul_linearLoss_sub_next_importanceWeightedLoss_le_powerSum_half {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score prob loss : Action -> Real) (next : Action -> Action -> Real) (multiplier : Real) (nextMultiplier : Action -> Real) (heta : 0 < eta) (hprobSimplex : FTRL.finiteSimplex arms prob) (hprobPos : forall action, action ∈ arms -> 0 < prob action) (hnextSimplex : forall chosen, chosen ∈ arms -> FTRL.finiteSimplex arms (next chosen)) (hnextPos : forall chosen, chosen ∈ arms -> forall action, action ∈ arms -> 0 < next chosen action) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) (hprobStationary : HalfTsallisInteriorStationary arms eta score prob multiplier) (hnextStationary : forall chosen, chosen ∈ arms -> HalfTsallisInteriorStationary arms eta (fun action => score action + Exp3.importanceWeightedLoss prob loss chosen action) (next chosen) (nextMultiplier chosen)) : arms.sum (fun chosen => prob chosen * (FTRL.linearLoss arms prob (Exp3.importanceWeightedLoss prob loss chosen) - FTRL.linearLoss arms (next chosen) (Exp3.importanceWeightedLoss prob loss chosen))) <= 2 * eta * powerSum arms (1 / 2 : Real) prob