BanditRLProof.TsallisFTRLStationarity

The zero-sum direction that transfers mass from `j` to `i`.

def pairDirection {Action : Type u} [DecidableEq Action] (i j : Action) (a : Action) : Real

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

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

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

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

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)

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

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

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

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

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

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

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

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

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

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

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

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

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