BanditRLlib

Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Tsallis-FTRL

BanditRLProof.TsallisRefinedAveragedStabilityObstruction

# Obstruction to refining the current symmetrized half-Tsallis stability term The shifted ordinary-importance-weighted moments have the paper-shaped sampled-action average, but the current local stability quantity `<p - p_next, hatLoss>` is not the conjugate-potential stability used in the Tsallis-INF proof. This module gives a fully rational two-arm counterexample: the current and sampled-update distributions are strict simplex minimizers and the losses lie in `[0,1]`, yet the proposed refined averaged upper bound fails. The counterexample closes the direct averaged-stability diagnostic. It does not obstruct the paper's conjugate-potential route.

Module map

Source: BanditRLProof/TsallisRefinedAveragedStabilityObstruction.lean
Teaching chapter: 8. Tsallis-FTRL, corruption, and nonstationarity
Declarations: 30
Placeholders: 0

Imports

BanditRLProof.TsallisRefinedImportanceWeightedMoment

Imported by

BanditRLProof

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

abbrev BanditRLProof.Tsallis.CounterAction Compiled Internal helper

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

private abbrev CounterAction

Source line 22 Chapter context: Tsallis-FTRL

def BanditRLProof.Tsallis.counterArms Compiled Internal helper

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

private noncomputable def counterArms : Finset CounterAction

Source line 24 Chapter context: Tsallis-FTRL

def BanditRLProof.Tsallis.counterEta Compiled Internal helper

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

private noncomputable def counterEta : Real

Source line 26 Chapter context: Tsallis-FTRL

def BanditRLProof.Tsallis.counterProb Compiled Internal helper

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

private noncomputable def counterProb : CounterAction -> Real

Source line 28 Chapter context: Tsallis-FTRL

def BanditRLProof.Tsallis.counterScore Compiled Internal helper

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

private noncomputable def counterScore : CounterAction -> Real

Source line 31 Chapter context: Tsallis-FTRL

def BanditRLProof.Tsallis.counterLoss Compiled Internal helper

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

private noncomputable def counterLoss : CounterAction -> Real

Source line 34 Chapter context: Tsallis-FTRL

def BanditRLProof.Tsallis.counterNext Compiled Internal helper

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

private noncomputable def counterNext (chosen action : CounterAction) : Real

Source line 38 Chapter context: Tsallis-FTRL

def BanditRLProof.Tsallis.counterNextMultiplier Compiled Internal helper

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

private noncomputable def counterNextMultiplier (chosen : CounterAction) : Real

Source line 47 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.sqrt_49 Compiled Internal helper

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

private theorem sqrt_49 : Real.sqrt (49 : Real) = 7

Source line 51 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.sqrt_576 Compiled Internal helper

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

private theorem sqrt_576 : Real.sqrt (576 : Real) = 24

Source line 54 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.sqrt_625 Compiled Internal helper

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

private theorem sqrt_625 : Real.sqrt (625 : Real) = 25

Source line 57 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.sqrt_24778200568643041 Compiled Internal helper

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

private theorem sqrt_24778200568643041 : Real.sqrt (24778200568643041 : Real) = 157410929

Source line 60 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.sqrt_1813828968643041 Compiled Internal helper

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

private theorem sqrt_1813828968643041 : Real.sqrt (1813828968643041 : Real) = 42589071

Source line 65 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.sqrt_22964371600000000 Compiled Internal helper

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

private theorem sqrt_22964371600000000 : Real.sqrt (22964371600000000 : Real) = 151540000

Source line 70 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.sqrt_1524122302720081 Compiled Internal helper

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

private theorem sqrt_1524122302720081 : Real.sqrt (1524122302720081 : Real) = 39040009

Source line 75 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.sqrt_120121402720081 Compiled Internal helper

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

private theorem sqrt_120121402720081 : Real.sqrt (120121402720081 : Real) = 10959991

Source line 80 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.sqrt_1404000900000000 Compiled Internal helper

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

private theorem sqrt_1404000900000000 : Real.sqrt (1404000900000000 : Real) = 37470000

Source line 85 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.counterEta_pos Compiled Internal helper

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

private theorem counterEta_pos : 0 < counterEta

Source line 90 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.counterEta_le_one Compiled Internal helper

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

private theorem counterEta_le_one : counterEta <= 1

Source line 93 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.counterProb_simplex Compiled Internal helper

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

private theorem counterProb_simplex : FTRL.finiteSimplex counterArms counterProb

Source line 96 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.counterProb_pos Compiled Internal helper

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

private theorem counterProb_pos (action : CounterAction) (haction : action ∈ counterArms) : 0 < counterProb action

Source line 103 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.counterLoss_mem_Icc Compiled Internal helper

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

private theorem counterLoss_mem_Icc (action : CounterAction) (haction : action ∈ counterArms) : 0 <= counterLoss action ∧ counterLoss action <= 1

Source line 108 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.counterNext_simplex Compiled Internal helper

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

private theorem counterNext_simplex (chosen : CounterAction) (hchosen : chosen ∈ counterArms) : FTRL.finiteSimplex counterArms (counterNext chosen)

Source line 113 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.counterNext_pos Compiled Internal helper

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

private theorem counterNext_pos (chosen : CounterAction) (hchosen : chosen ∈ counterArms) (action : CounterAction) (haction : action ∈ counterArms) : 0 < counterNext chosen action

Source line 122 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.rpow_neg_half_eq_inv_sqrt Compiled Internal helper

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

private theorem rpow_neg_half_eq_inv_sqrt {x : Real} (hx : 0 < x) : x ^ (-(1 / 2 : Real)) = 1 / Real.sqrt x

Source line 128 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.counterProb_stationary Compiled Internal helper

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

private theorem counterProb_stationary : HalfTsallisInteriorStationary counterArms counterEta counterScore counterProb 0

Source line 133 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.counterNext_stationary Compiled Internal helper

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

private theorem counterNext_stationary (chosen : CounterAction) (hchosen : chosen ∈ counterArms) : HalfTsallisInteriorStationary counterArms counterEta (fun action => counterScore action + Exp3.importanceWeightedLoss counterProb counterLoss chosen action) (counterNext chosen) (counterNextMultiplier chosen)

Source line 142 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.counterProb_minimizer Compiled Internal helper

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

private theorem counterProb_minimizer : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex counterArms) counterArms counterEta (negEntropyRegularizer counterArms (1 / 2 : Real)) counterScore counterProb

Source line 159 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.counterNext_minimizer Compiled Internal helper

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

private theorem counterNext_minimizer (chosen : CounterAction) (hchosen : chosen ∈ counterArms) : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex counterArms) counterArms counterEta (negEntropyRegularizer counterArms (1 / 2 : Real)) (fun action => counterScore action + Exp3.importanceWeightedLoss counterProb counterLoss chosen action) (counterNext chosen)

Source line 167 Chapter context: Tsallis-FTRL

theorem BanditRLProof.Tsallis.exists_minimizer_counterexample_to_refinedAveragedStability Compiled

Even with strict positive simplex minimizers and `[0,1]` losses, the current sampled-action average of `<p - p_next, hatLoss>` can exceed the locally scaled paper coefficient `eta * sum sqrt(p) * (1-p) + 2 * eta^2`.

theorem exists_minimizer_counterexample_to_refinedAveragedStability : ∃ (eta : Real) (score prob loss : Fin 2 -> Real) (next : Fin 2 -> Fin 2 -> Real), 0 < eta ∧ eta <= 1 ∧ FTRL.finiteSimplex Finset.univ prob ∧ (∀ action ∈ (Finset.univ : Finset (Fin 2)), 0 < prob action) ∧ (∀ action ∈ (Finset.univ : Finset (Fin 2)), 0 <= loss action ∧ loss action <= 1) ∧ FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex Finset.univ) Finset.univ eta (negEntropyRegularizer Finset.univ (1 / 2 : Real)) score prob ∧ (∀ chosen ∈ (Finset.univ : Finset (Fin 2)), ∀ action ∈ (Finset.univ : Finset (Fin 2)), 0 < next chosen action) ∧ (∀ chosen ∈ (Finset.univ : Finset (Fin 2)), FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex Finset.univ) Finset.univ eta (negEntropyRegularizer Finset.univ (1 / 2 : Real)) (fun action => score action + Exp3.importanceWeightedLoss prob loss chosen action) (next chosen)) ∧ eta * (Finset.univ : Finset (Fin 2)).sum (fun action => Real.sqrt (prob action) * (1 - prob action)) + 2 * eta ^ 2 < (Finset.univ : Finset (Fin 2)).sum (fun chosen => prob chosen * (FTRL.linearLoss Finset.univ prob (Exp3.importanceWeightedLoss prob loss chosen) - FTRL.linearLoss Finset.univ (next chosen) (Exp3.importanceWeightedLoss prob loss chosen)))

Source line 188 Chapter context: Tsallis-FTRL