BanditRLProof.TsallisFTRLOneStepStability

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

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)

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)))

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

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