BanditRLProof.TsallisConjugatePotentialStability

The paper-normalized negative regularized-objective value. When `probability` is a certified minimizer and `eta > 0`, this is the constrained half-Tsallis potential under the local-to-paper learning-rate translation.

noncomputable def halfTsallisPotentialValue {Action : Type u} (arms : Finset Action) (eta : Real) (score probability : Action -> Real) : Real

The one-step candidate-potential expression before taking a sampling average. The low-level feasible-next bridge treats `next` only as a candidate point; the algorithm-facing theorems require both current and next minimizer certificates.

noncomputable def halfTsallisPotentialStability {Action : Type u} (arms : Finset Action) (eta : Real) (score probability estimate next : Action -> Real) : Real

The coordinate increment obtained from the explicit unconstrained conjugate. The shift is `estimate action - baseline`.

noncomputable def halfTsallisConjugateCoordinateIncrement (eta probability shift : Real) : Real

Finite sum of explicit conjugate coordinate increments.

noncomputable def halfTsallisConjugatePotentialUpper {Action : Type u} (arms : Finset Action) (eta : Real) (probability estimate : Action -> Real) (baseline : Real) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem one_add_eta_mul_shift_mul_sqrt_pos {eta probability shift : Real} (_heta : 0 < eta) (hprobability : 0 < probability) (hdomain : -1 <= 2 * eta * shift * Real.sqrt probability) : 0 < 1 + eta * shift * Real.sqrt probability

Exact rational form of the explicit conjugate coordinate increment.

theorem halfTsallisConjugateCoordinateIncrement_eq {eta probability shift : Real} (heta : 0 < eta) (hprobability : 0 < probability) (hdomain : -1 <= 2 * eta * shift * Real.sqrt probability) : halfTsallisConjugateCoordinateIncrement eta probability shift = eta * Real.sqrt probability * probability * shift ^ 2 / (1 + eta * shift * Real.sqrt probability)

Scalar translated Lemma 19 bound. The positive cubic term is active only when the shifted estimate is negative.

theorem halfTsallisConjugateCoordinateIncrement_le {eta probability shift : Real} (heta : 0 < eta) (hprobability : 0 < probability) (hdomain : -1 <= 2 * eta * shift * Real.sqrt probability) : halfTsallisConjugateCoordinateIncrement eta probability shift <= eta * Real.sqrt probability * probability * shift ^ 2 + 2 * eta ^ 2 * probability ^ 2 * (max (-shift) 0) ^ 3

Coordinatewise Fenchel upper bound for a nonnegative competitor weight.

theorem halfTsallis_fenchelCoordinate_le {eta probability competitor shift : Real} (heta : 0 < eta) (hprobability : 0 < probability) (hcompetitor : 0 <= competitor) (hdomain : -1 <= 2 * eta * shift * Real.sqrt probability) : -competitor / (eta * Real.sqrt probability) - competitor * shift + 2 * Real.sqrt competitor / eta <= Real.sqrt probability / (eta * (1 + eta * shift * Real.sqrt probability))

The explicit conjugate finite sum is bounded by shifted quadratic/cubic moments.

theorem halfTsallisConjugatePotentialUpper_le_shiftedMoments {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (probability estimate : Action -> Real) (baseline : Real) (heta : 0 < eta) (hprobability : forall action, action ∈ arms -> 0 < probability action) (hdomain : forall action, action ∈ arms -> -1 <= 2 * eta * (estimate action - baseline) * Real.sqrt (probability action)) : halfTsallisConjugatePotentialUpper arms eta probability estimate baseline <= eta * arms.sum (fun action => Real.sqrt (probability action) * probability action * (estimate action - baseline) ^ 2) + 2 * eta ^ 2 * arms.sum (fun action => probability action ^ 2 * (max (baseline - estimate action) 0) ^ 3)

Ordinary importance-weighted estimates satisfy the translated conjugate domain.

theorem importanceWeightedLoss_sub_selectedLoss_conjugate_domain {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (probability loss : Action -> Real) (heta : 0 < eta) (heta_le : eta <= 1 / 2) (hprobability : FTRL.finiteSimplex arms probability) (hprobabilityPos : forall action, action ∈ arms -> 0 < probability action) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) {chosen action : Action} (hchosen : chosen ∈ arms) (haction : action ∈ arms) : -1 <= 2 * eta * (Exp3.importanceWeightedLoss probability loss chosen action - loss chosen) * Real.sqrt (probability action)

No declaration docstring is present; use the chapter context and exact statement below.

theorem linearLoss_sub_linearLoss_eq_sum_sub_mul {Action : Type u} (arms : Finset Action) (p q score : Action -> Real) : FTRL.linearLoss arms p score - FTRL.linearLoss arms q score = arms.sum (fun action => (p action - q action) * score action)

No declaration docstring is present; use the chapter context and exact statement below.

theorem sum_sub_mul_sub_baseline_eq_sum_sub_mul {Action : Type u} (arms : Finset Action) (p q value : Action -> Real) (baseline : Real) (hp : arms.sum p = 1) (hq : arms.sum q = 1) : arms.sum (fun action => (p action - q action) * (value action - baseline)) = arms.sum (fun action => (p action - q action) * value action)

Stationarity removes the score and its common simplex multiplier.

theorem linearLoss_sub_linearLoss_score_eq_sum_div_sqrt_of_stationary {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score p q : Action -> Real) (multiplier : Real) (heta : 0 < eta) (hp : FTRL.finiteSimplex arms p) (hq : FTRL.finiteSimplex arms q) (hpPos : forall action, action ∈ arms -> 0 < p action) (hstationary : HalfTsallisInteriorStationary arms eta score p multiplier) : FTRL.linearLoss arms p score - FTRL.linearLoss arms q score = arms.sum (fun action => (p action - q action) / (eta * Real.sqrt (p action)))

The feasible-next candidate-potential expression is bounded by the explicit unconstrained conjugate sum. Only the current point needs stationarity. This is an algebraic bridge, not an actual constrained-potential theorem unless the caller separately certifies that `next` minimizes the updated objective.

theorem halfTsallisPotentialStability_le_conjugatePotentialUpper_of_feasible {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score probability estimate next : Action -> Real) (baseline multiplier : Real) (heta : 0 < eta) (hprobability : FTRL.finiteSimplex arms probability) (hnext : FTRL.finiteSimplex arms next) (hprobabilityPos : forall action, action ∈ arms -> 0 < probability action) (hstationary : HalfTsallisInteriorStationary arms eta score probability multiplier) (hdomain : forall action, action ∈ arms -> -1 <= 2 * eta * (estimate action - baseline) * Real.sqrt (probability action)) : halfTsallisPotentialStability arms eta score probability estimate next <= halfTsallisConjugatePotentialUpper arms eta probability estimate baseline

Paper-faithful one-step conjugate-potential stability for an ordinary importance-weighted sampled update.

theorem halfTsallisPotentialStability_importanceWeightedLoss_le_shiftedMoments_of_minimizers {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score probability loss next : Action -> Real) (chosen : Action) (hchosen : chosen ∈ arms) (heta : 0 < eta) (heta_le : eta <= 1 / 2) (hprobabilityMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score probability) (hnextMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun action => score action + Exp3.importanceWeightedLoss probability loss chosen action) next) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) : halfTsallisPotentialStability arms eta score probability (Exp3.importanceWeightedLoss probability loss chosen) next <= eta * shiftedHalfPowerImportanceWeightedMoment arms probability loss chosen + 2 * eta ^ 2 * shiftedPositiveCubicImportanceWeightedMoment arms probability loss chosen

Sampled-action averaged ordinary-IW conjugate-potential stability. This is the deterministic finite-action form of the refined coefficient used downstream by the self-bounding route.

theorem sum_prob_mul_halfTsallisPotentialStability_importanceWeightedLoss_le_refined_of_minimizers {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score probability loss : Action -> Real) (next : Action -> Action -> Real) (heta : 0 < eta) (heta_le : eta <= 1 / 2) (hprobabilityMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score probability) (hnextMin : forall chosen, chosen ∈ arms -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun action => score action + Exp3.importanceWeightedLoss probability loss chosen action) (next chosen)) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) : arms.sum (fun chosen => probability chosen * halfTsallisPotentialStability arms eta score probability (Exp3.importanceWeightedLoss probability loss chosen) (next chosen)) <= eta * arms.sum (fun action => Real.sqrt (probability action) * (1 - probability action)) + 2 * eta ^ 2

Canonical-selector wrapper with all minimizer certificates discharged.

theorem sum_halfTsallisMinimizer_mul_potentialStability_le_refined {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score loss : Action -> Real) (heta : 0 < eta) (heta_le : eta <= 1 / 2) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) : let probability := halfTsallisMinimizer arms harms eta score let next := fun chosen => halfTsallisUpdatedMinimizer arms harms eta score loss chosen arms.sum (fun chosen => probability chosen * halfTsallisPotentialStability arms eta score probability (Exp3.importanceWeightedLoss probability loss chosen) (next chosen)) <= eta * arms.sum (fun action => Real.sqrt (probability action) * (1 - probability action)) + 2 * eta ^ 2