BanditRLProof.TsallisFTRLMinimizerExistence

Extend finite-subtype weights by zero outside the explicit arm set.

def extendFiniteWeights {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p : ↥arms -> Real) : Action -> Real

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

theorem extendFiniteWeights_apply_of_mem {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p : ↥arms -> Real) {action : Action} (haction : action ∈ arms) : extendFiniteWeights arms p action = p ⟨action, haction⟩

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

theorem extendFiniteWeights_apply_of_not_mem {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p : ↥arms -> Real) {action : Action} (haction : action ∉ arms) : extendFiniteWeights arms p action = 0

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

theorem sum_extendFiniteWeights {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p : ↥arms -> Real) : arms.sum (extendFiniteWeights arms p) = ∑ action : ↥arms, p action

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

theorem finiteSimplex_extendFiniteWeights {Action : Type u} [DecidableEq Action] (arms : Finset Action) {p : ↥arms -> Real} (hp : p ∈ stdSimplex Real ↥arms) : FTRL.finiteSimplex arms (extendFiniteWeights arms p)

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

theorem restrict_mem_stdSimplex_of_finiteSimplex {Action : Type u} [DecidableEq Action] (arms : Finset Action) {p : Action -> Real} (hp : FTRL.finiteSimplex arms p) : Finset.restrict arms p ∈ stdSimplex Real ↥arms

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

theorem linearLoss_extendFiniteWeights_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p : ↥arms -> Real) (score : Action -> Real) : FTRL.linearLoss arms (extendFiniteWeights arms p) score = FTRL.linearLoss Finset.univ p (fun action => score action)

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

theorem linearLoss_restrict_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p score : Action -> Real) : FTRL.linearLoss Finset.univ (Finset.restrict arms p) (fun action => score action) = FTRL.linearLoss arms p score

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

theorem sum_sqrt_extendFiniteWeights_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p : ↥arms -> Real) : arms.sum (fun action => Real.sqrt (extendFiniteWeights arms p action)) = ∑ action : ↥arms, Real.sqrt (p action)

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

theorem sum_sqrt_restrict_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (p : Action -> Real) : (Finset.univ : Finset ↥arms).sum (fun action => Real.sqrt (Finset.restrict arms p action)) = arms.sum (fun action => Real.sqrt (p action))

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

theorem regularizedObjective_half_extendFiniteWeights_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score : Action -> Real) (p : ↥arms -> Real) : FTRL.regularizedObjective arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score (extendFiniteWeights arms p) = FTRL.regularizedObjective arms.attach eta (negEntropyRegularizer arms.attach (1 / 2 : Real)) (fun action : ↥arms => score action) p

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

theorem regularizedObjective_half_restrict_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score p : Action -> Real) : FTRL.regularizedObjective arms.attach eta (negEntropyRegularizer arms.attach (1 / 2 : Real)) (fun action : ↥arms => score action) (Finset.restrict arms p) = FTRL.regularizedObjective arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score p

The half-Tsallis objective is continuous on the finite subtype function space.

theorem continuous_regularizedObjective_half_univ {Action : Type u} [Fintype Action] (eta : Real) (score : Action -> Real) : Continuous (fun p : Action -> Real => FTRL.regularizedObjective Finset.univ eta (negEntropyRegularizer Finset.univ (1 / 2 : Real)) score p)

Every nonempty explicit finite arm set admits a half-Tsallis regularized minimizer. The learning rate and finite score coordinates may be arbitrary real numbers.

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

A fixed choice of half-Tsallis minimizer on a nonempty explicit arm set.

noncomputable def halfTsallisMinimizer {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : Action -> Real) : Action -> Real

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

theorem halfTsallisMinimizer_isRegularizedMinimizer {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : Action -> Real) : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score (halfTsallisMinimizer arms harms eta score)

Canonical half-Tsallis update after observing one importance-weighted loss.

noncomputable def halfTsallisUpdatedMinimizer {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score loss : Action -> Real) (chosen : Action) : Action -> Real

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

theorem halfTsallisUpdatedMinimizer_isRegularizedMinimizer {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score loss : Action -> Real) (chosen : Action) : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun action => score action + Exp3.importanceWeightedLoss (halfTsallisMinimizer arms harms eta score) loss chosen action) (halfTsallisUpdatedMinimizer arms harms eta score loss chosen)

The sampling-law one-step stability endpoint with both current and updated minimizers selected internally.

theorem sum_halfTsallisMinimizer_mul_linearLoss_sub_updated_le_powerSum_half {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score loss : Action -> Real) (heta : 0 < eta) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) : let prob := halfTsallisMinimizer arms harms eta score let next := fun chosen => halfTsallisUpdatedMinimizer arms harms eta score loss 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

A nonempty finite arm set admits a strictly positive half-Tsallis minimizer together with its common stationarity multiplier.

theorem exists_halfTsallisInteriorStationary_minimizer {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : Action -> Real) : exists p multiplier, FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score p ∧ (forall action, action ∈ arms -> 0 < p action) ∧ HalfTsallisInteriorStationary arms eta score p multiplier