BanditRLProof.TsallisFTRLInteriority

A one-sided transfer from a positive donor to a zero coordinate stays in the finite simplex.

theorem finiteSimplex_simplexPairShift_of_eq_zero_of_le {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p : Action -> Real) (i j : Action) (t : Real) (hij : i ≠ j) (hp : FTRL.finiteSimplex arms p) (hi : i ∈ arms) (hj : j ∈ arms) (hpi : p i = 0) (ht : 0 <= t) (htj : t <= p j) : FTRL.finiteSimplex arms (simplexPairShift p i j t)

Exact linear-loss change under a two-coordinate simplex transfer.

theorem linearLoss_simplexPairShift_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p score : Action -> Real) (i j : Action) (t : Real) (hi : i ∈ arms) (hj : j ∈ arms) : FTRL.linearLoss arms (simplexPairShift p i j t) score = FTRL.linearLoss arms p score + t * (score i - score j)

Exact square-root-sum change when mass enters a zero coordinate.

theorem sum_sqrt_simplexPairShift_eq_of_eq_zero {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p : Action -> Real) (i j : Action) (t : Real) (hij : i ≠ j) (hi : i ∈ arms) (hj : j ∈ arms) (hpi : p i = 0) : arms.sum (fun a => Real.sqrt (simplexPairShift p i j t a)) = arms.sum (fun a => Real.sqrt (p a)) + Real.sqrt t + Real.sqrt (p j - t) - Real.sqrt (p j)

Removing mass `t` from a positive coordinate loses at most `t / sqrt r` of square-root mass.

theorem sqrt_sub_sqrt_sub_le_div_sqrt {r t : Real} (hr : 0 < r) (ht : 0 <= t) (htr : t <= r) : Real.sqrt r - Real.sqrt (r - t) <= t / Real.sqrt r

At a zero coordinate, the square-root gain dominates any fixed linear slope for a sufficiently small positive transfer from a positive donor.

theorem exists_transfer_strictly_improves_half_objective (r d : Real) (hr : 0 < r) : exists t, 0 < t ∧ t < r ∧ d * t < 2 * (Real.sqrt t + Real.sqrt (r - t) - Real.sqrt r)

Every supported coordinate of a half-Tsallis finite-simplex minimizer is strictly positive. No sign condition on `eta` or boundedness condition on the finite score is needed.

theorem isRegularizedMinimizer_pos {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score p : Action -> Real) (hpMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score p) : forall action, action ∈ arms -> 0 < p action

A half-Tsallis simplex minimizer automatically supplies the interior stationarity certificate used by the one-step stability route.

theorem exists_halfTsallisInteriorStationary_of_isRegularizedMinimizer_auto {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score p : Action -> Real) (hpMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score p) : exists multiplier, HalfTsallisInteriorStationary arms eta score p multiplier

Sampling-law half-Tsallis stability directly from current and chosen-update minimizer certificates. Strict positivity and common multipliers are derived internally.

theorem sum_prob_mul_linearLoss_sub_next_importanceWeightedLoss_le_powerSum_half_of_minimizers {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score prob loss : Action -> Real) (next : Action -> Action -> Real) (heta : 0 < eta) (hprobMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score prob) (hnextMin : forall chosen, chosen ∈ arms -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun action => score action + Exp3.importanceWeightedLoss prob loss chosen action) (next chosen)) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) : 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