Lean module · Tsallis-FTRL
BanditRLProof.TsallisFTRLMinimizerExistence
# Existence of half-Tsallis finite-simplex minimizers The project simplex only constrains coordinates in an explicit `Finset`, so it is not compact as a subset of the full function space when the ambient action type is infinite. We minimize instead on Mathlib's compact standard simplex over the finite subtype `↥arms`, then extend the minimizer by zero.
Module map
Imports
BanditRLProof.TsallisFTRLInteriority
Imported by
BanditRLProof.TsallisFTRLFiniteHorizonSelection, BanditRLProof.TsallisFTRLMinimizerUniqueness
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.extendFiniteWeights
Compiled
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
theorem
BanditRLProof.Tsallis.extendFiniteWeights_apply_of_mem
Compiled
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⟩
theorem
BanditRLProof.Tsallis.extendFiniteWeights_apply_of_not_mem
Compiled
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
theorem
BanditRLProof.Tsallis.sum_extendFiniteWeights
Compiled
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
theorem
BanditRLProof.Tsallis.finiteSimplex_extendFiniteWeights
Compiled
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)
theorem
BanditRLProof.Tsallis.restrict_mem_stdSimplex_of_finiteSimplex
Compiled
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
theorem
BanditRLProof.Tsallis.linearLoss_extendFiniteWeights_eq
Compiled
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)
theorem
BanditRLProof.Tsallis.linearLoss_restrict_eq
Compiled
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
theorem
BanditRLProof.Tsallis.sum_sqrt_extendFiniteWeights_eq
Compiled
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)
theorem
BanditRLProof.Tsallis.sum_sqrt_restrict_eq
Compiled
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))
theorem
BanditRLProof.Tsallis.regularizedObjective_half_extendFiniteWeights_eq
Compiled
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
theorem
BanditRLProof.Tsallis.regularizedObjective_half_restrict_eq
Compiled
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
theorem
BanditRLProof.Tsallis.continuous_regularizedObjective_half_univ
Compiled
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)
theorem
BanditRLProof.Tsallis.exists_isRegularizedMinimizer_half
Compiled
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
def
BanditRLProof.Tsallis.halfTsallisMinimizer
Compiled
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
theorem
BanditRLProof.Tsallis.halfTsallisMinimizer_isRegularizedMinimizer
Compiled
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)
def
BanditRLProof.Tsallis.halfTsallisUpdatedMinimizer
Compiled
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
theorem
BanditRLProof.Tsallis.halfTsallisUpdatedMinimizer_isRegularizedMinimizer
Compiled
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)
theorem
BanditRLProof.Tsallis.sum_halfTsallisMinimizer_mul_linearLoss_sub_updated_le_powerSum_half
Compiled
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
theorem
BanditRLProof.Tsallis.exists_halfTsallisInteriorStationary_minimizer
Compiled
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