Lean module · Tsallis-FTRL
BanditRLProof.TsallisFiniteBanditMeanLoss
This module turns a bounded finite-bandit mean-reward model into the history-independent predictable loss family 1 - mean. Its loss differences are exactly the model gaps, so the compiled square-root-schedule fixed-gap theorem applies without a caller-supplied predictable gap law.
Module map
Imports
BanditRLProof.FiniteBanditModelInvariants, BanditRLProof.TsallisSqrtScheduleFixedGap
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Exp3.finiteBanditMeanLoss
Compiled
The stationary predictable loss family obtained from bounded arm means.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Exp3.finiteBanditMeanLossReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def finiteBanditMeanLoss {K : Nat} {Env : Type u} [MeasurableSpace Env] (model : FiniteBanditModel K) (hmean : forall arm, ((model.mean arm : Rat) : Real) ∈ Set.Icc (0 : Real) 1) : PredictableLossVector Env (Fin K) where
theorem
BanditRLProof.Exp3.finiteBanditMeanLoss_initial
Compiled
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.Exp3.finiteBanditMeanLoss_initialReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem finiteBanditMeanLoss_initial {K : Nat} {Env : Type u} [MeasurableSpace Env] (model : FiniteBanditModel K) (hmean : forall arm, ((model.mean arm : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (env : Env) (arm : Fin K) : (finiteBanditMeanLoss (Env := Env) model hmean).initial env arm = 1 - ((model.mean arm : Rat) : Real)
theorem
BanditRLProof.Exp3.finiteBanditMeanLoss_successor
Compiled
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.Exp3.finiteBanditMeanLoss_successorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem finiteBanditMeanLoss_successor {K : Nat} {Env : Type u} [MeasurableSpace Env] (model : FiniteBanditModel K) (hmean : forall arm, ((model.mean arm : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (n : Nat) (env : Env) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : (finiteBanditMeanLoss (Env := Env) model hmean).successor n env history arm = 1 - ((model.mean arm : Rat) : Real)
theorem
BanditRLProof.Exp3.predictableLossAt_finiteBanditMeanLoss
Compiled
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.Exp3.predictableLossAt_finiteBanditMeanLossReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem predictableLossAt_finiteBanditMeanLoss {K : Nat} {Env : Type u} [MeasurableSpace Env] (model : FiniteBanditModel K) (hmean : forall arm, ((model.mean arm : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (t : Nat) (sample : Env × ((k : Nat) -> Fin K × Real)) (arm : Fin K) : predictableLossAt (finiteBanditMeanLoss (Env := Env) model hmean) t sample arm = 1 - ((model.mean arm : Rat) : Real)
theorem
BanditRLProof.Exp3.predictableLossAt_finiteBanditMeanLoss_sub_bestArm_eq_gap
Compiled
Mean-loss differences against the selected best arm are model gaps.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Exp3.predictableLossAt_finiteBanditMeanLoss_sub_bestArm_eq_gapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem predictableLossAt_finiteBanditMeanLoss_sub_bestArm_eq_gap {K : Nat} {Env : Type u} [MeasurableSpace Env] (model : FiniteBanditModel K) (hmean : forall arm, ((model.mean arm : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (t : Nat) (sample : Env × ((k : Nat) -> Fin K × Real)) (arm : Fin K) : predictableLossAt (finiteBanditMeanLoss (Env := Env) model hmean) t sample arm - predictableLossAt (finiteBanditMeanLoss (Env := Env) model hmean) t sample model.bestArm = ((model.gap arm : Rat) : Real)
theorem
BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteBanditMeanLossRegret_le_log_fixedGap
Compiled
The square-root scheduled half-Tsallis algorithm has logarithmic fixed-gap regret on the deterministic mean-loss environment of a bounded finite-bandit model with strictly positive non-best gaps.
Used in these reading views: Bandit Book · Online Learning Book
8. Tsallis-FTRL, corruption, and nonstationarity
Canonical node identity
declaration:BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteBanditMeanLossRegret_le_log_fixedGapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_sampledScheduledHalfTsallisFiniteBanditMeanLossRegret_le_log_fixedGap {K : Nat} {Env : Type u} [MeasurableSpace Env] [StandardBorelSpace Env] (prior : Measure Env) [IsProbabilityMeasure prior] (model : FiniteBanditModel K) (hmean : forall arm, ((model.mean arm : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (hgapPos : forall arm, arm ≠ model.bestArm -> 0 < ((model.gap arm : Rat) : Real)) (horizon : Nat) (corruption : Real) (hcorruption : 0 <= corruption) : letI : Nonempty (Fin K)