Lean module · Tsallis-FTRL

BanditRLProof.TsallisRefinedAveragedStabilityObstruction

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.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.CounterAction

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterArms

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterEta

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterProb

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterScore

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterLoss

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterNext

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterNextMultiplier

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.sqrt_49

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.sqrt_576

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.sqrt_625

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.sqrt_24778200568643041

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.sqrt_1813828968643041

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.sqrt_22964371600000000

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.sqrt_1524122302720081

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.sqrt_120121402720081

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.sqrt_1404000900000000

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterEta_pos

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterEta_le_one

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterProb_simplex

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterProb_pos

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterLoss_mem_Icc

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterNext_simplex

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterNext_pos

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.rpow_neg_half_eq_inv_sqrt

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterProb_stationary

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterNext_stationary

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterProb_minimizer

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.counterNext_minimizer

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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`.

Used in these reading views: Bandit Book · Online Learning Book

8. Tsallis-FTRL, corruption, and nonstationarity

Canonical node identity

declaration:BanditRLProof.Tsallis.exists_minimizer_counterexample_to_refinedAveragedStability

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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