Lean module · Tsallis-FTRL
BanditRLProof.TsallisFTRLStationarity
# Half-Tsallis FTRL minimizer and stationarity transport This module connects the finite-simplex minimizer certificate used by the generic FTRL route to the explicit interior stationarity certificate consumed by the half-Tsallis one-step stability theorem. The proof perturbs two simplex coordinates in opposite directions, differentiates the resulting scalar objective at an interior minimizer, and uses the vanishing derivative to identify a common multiplier. Strict positivity is an explicit input. This module does not prove existence or interiority of a half-Tsallis minimizer and does not construct the stochastic Tsallis-INF update.
Module map
Imports
BanditRLProof.TsallisFTRLOneStepStability
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.pairDirection
Compiled
The zero-sum direction that transfers mass from `j` to `i`.
def pairDirection {Action : Type u} [DecidableEq Action] (i j : Action) (a : Action) : Real
def
BanditRLProof.Tsallis.simplexPairShift
Compiled
Transfer scalar mass `t` from coordinate `j` to coordinate `i`.
def simplexPairShift {Action : Type u} [DecidableEq Action] (p : Action -> Real) (i j : Action) (t : Real) : Action -> Real
theorem
BanditRLProof.Tsallis.simplexPairShift_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem simplexPairShift_zero {Action : Type u} [DecidableEq Action] (p : Action -> Real) (i j : Action) : simplexPairShift p i j 0 = p
theorem
BanditRLProof.Tsallis.sum_pairDirection_mul
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sum_pairDirection_mul {Action : Type u} [DecidableEq Action] (arms : Finset Action) (i j : Action) (f : Action -> Real) (hi : i ∈ arms) (hj : j ∈ arms) : arms.sum (fun a => pairDirection i j a * f a) = f i - f j
theorem
BanditRLProof.Tsallis.sum_simplexPairShift
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sum_simplexPairShift {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p : Action -> Real) (i j : Action) (t : Real) (hi : i ∈ arms) (hj : j ∈ arms) : arms.sum (simplexPairShift p i j t) = arms.sum p
theorem
BanditRLProof.Tsallis.finiteSimplex_simplexPairShift_of_abs_lt_min
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem finiteSimplex_simplexPairShift_of_abs_lt_min {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) (ht : |t| < min (p i) (p j)) : FTRL.finiteSimplex arms (simplexPairShift p i j t)
theorem
BanditRLProof.Tsallis.regularizedObjective_half_eq
Compiled
The half-Tsallis objective is a linear term minus twice the square-root sum.
theorem regularizedObjective_half_eq {Action : Type u} (arms : Finset Action) (eta : Real) (score p : Action -> Real) : FTRL.regularizedObjective arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score p = eta * FTRL.linearLoss arms p score - 2 * arms.sum (fun a => Real.sqrt (p a)) + 2
theorem
BanditRLProof.Tsallis.hasDerivAt_simplexPairShift
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem hasDerivAt_simplexPairShift {Action : Type u} [DecidableEq Action] (p : Action -> Real) (i j a : Action) : HasDerivAt (fun t => simplexPairShift p i j t a) (pairDirection i j a) 0
theorem
BanditRLProof.Tsallis.hasDerivAt_linearLoss_simplexPairShift
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem hasDerivAt_linearLoss_simplexPairShift {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p score : Action -> Real) (i j : Action) (hi : i ∈ arms) (hj : j ∈ arms) : HasDerivAt (fun t => FTRL.linearLoss arms (simplexPairShift p i j t) score) (score i - score j) 0
theorem
BanditRLProof.Tsallis.sum_pairDirection_div_two_sqrt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sum_pairDirection_div_two_sqrt {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p : Action -> Real) (i j : Action) (hi : i ∈ arms) (hj : j ∈ arms) : arms.sum (fun a => pairDirection i j a / (2 * Real.sqrt (p a))) = 1 / (2 * Real.sqrt (p i)) - 1 / (2 * Real.sqrt (p j))
theorem
BanditRLProof.Tsallis.hasDerivAt_sum_sqrt_simplexPairShift
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem hasDerivAt_sum_sqrt_simplexPairShift {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p : Action -> Real) (i j : Action) (hi : i ∈ arms) (hj : j ∈ arms) (hpPos : forall a, a ∈ arms -> 0 < p a) : HasDerivAt (fun t => arms.sum (fun a => Real.sqrt (simplexPairShift p i j t a))) (1 / (2 * Real.sqrt (p i)) - 1 / (2 * Real.sqrt (p j))) 0
theorem
BanditRLProof.Tsallis.hasDerivAt_regularizedObjective_half_simplexPairShift
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem hasDerivAt_regularizedObjective_half_simplexPairShift {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score p : Action -> Real) (i j : Action) (hi : i ∈ arms) (hj : j ∈ arms) (hpPos : forall a, a ∈ arms -> 0 < p a) : HasDerivAt (fun t => FTRL.regularizedObjective arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score (simplexPairShift p i j t)) (eta * (score i - score j) - (1 / Real.sqrt (p i) - 1 / Real.sqrt (p j))) 0
theorem
BanditRLProof.Tsallis.isLocalMin_regularizedObjective_half_simplexPairShift
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem isLocalMin_regularizedObjective_half_simplexPairShift {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score p : Action -> Real) (i j : Action) (hij : i ≠ j) (hi : i ∈ arms) (hj : j ∈ arms) (hpMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score p) (hpPos : forall a, a ∈ arms -> 0 < p a) : IsLocalMin (fun t => FTRL.regularizedObjective arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score (simplexPairShift p i j t)) 0
theorem
BanditRLProof.Tsallis.halfTsallis_pairwise_stationary_of_isRegularizedMinimizer
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem halfTsallis_pairwise_stationary_of_isRegularizedMinimizer {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) (hpPos : forall a, a ∈ arms -> 0 < p a) {i j : Action} (hi : i ∈ arms) (hj : j ∈ arms) : eta * score i - (p i) ^ (-(1 / 2 : Real)) = eta * score j - (p j) ^ (-(1 / 2 : Real))
theorem
BanditRLProof.Tsallis.exists_halfTsallisInteriorStationary_of_isRegularizedMinimizer
Compiled
An explicitly interior half-Tsallis simplex minimizer admits the stationarity certificate consumed by the one-step stability theorem.
theorem exists_halfTsallisInteriorStationary_of_isRegularizedMinimizer {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) (hpPos : forall a, a ∈ arms -> 0 < p a) : exists multiplier, HalfTsallisInteriorStationary arms eta score p multiplier
theorem
BanditRLProof.Tsallis.two_mul_sqrt_sub_sqrt_le_sub_div_sqrt
Compiled
The supporting-line inequality for the square root at a positive point.
theorem two_mul_sqrt_sub_sqrt_le_sub_div_sqrt {p q : Real} (hp : 0 < p) (hq : 0 <= q) : 2 * (Real.sqrt q - Real.sqrt p) <= (q - p) / Real.sqrt p
theorem
BanditRLProof.Tsallis.isRegularizedMinimizer_of_halfTsallisInteriorStationary
Compiled
A positive simplex point satisfying half-Tsallis stationarity globally minimizes the corresponding regularized objective on the finite simplex.
theorem isRegularizedMinimizer_of_halfTsallisInteriorStationary {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score p : Action -> Real) (multiplier : Real) (hp : FTRL.finiteSimplex arms p) (hpPos : forall a, a ∈ arms -> 0 < p a) (hstationary : HalfTsallisInteriorStationary arms eta score p multiplier) : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score p
theorem
BanditRLProof.Tsallis.isRegularizedMinimizer_iff_exists_halfTsallisInteriorStationary
Compiled
Interior half-Tsallis stationarity is equivalent to simplex minimality.
theorem isRegularizedMinimizer_iff_exists_halfTsallisInteriorStationary {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score p : Action -> Real) (hp : FTRL.finiteSimplex arms p) (hpPos : forall a, a ∈ arms -> 0 < p a) : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score p ↔ exists multiplier, HalfTsallisInteriorStationary arms eta score p multiplier
theorem
BanditRLProof.Tsallis.sum_prob_mul_linearLoss_sub_next_importanceWeightedLoss_le_powerSum_half_of_positive_minimizers
Compiled
Sampling-law half-Tsallis stability directly from concrete regularized-minimizer certificates. Common multipliers are constructed internally from interiority.
theorem sum_prob_mul_linearLoss_sub_next_importanceWeightedLoss_le_powerSum_half_of_positive_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) (hprobPos : forall action, action ∈ arms -> 0 < prob action) (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)) (hnextPos : forall chosen, chosen ∈ arms -> forall action, action ∈ arms -> 0 < next chosen action) (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