Lean module · Tsallis-FTRL
BanditRLProof.TsallisFiniteBanditMeanLoss
# Finite-bandit mean losses for scheduled half-Tsallis FTRL 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. The generated feedback remains the deterministic mean-loss environment of `Exp3.PredictableLossVector`; this module does not identify it with a stochastic reward-kernel trajectory.
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.
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.
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
theorem
BanditRLProof.Exp3.finiteBanditMeanLoss_successor
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
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
theorem
BanditRLProof.Exp3.predictableLossAt_finiteBanditMeanLoss
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
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
theorem
BanditRLProof.Exp3.predictableLossAt_finiteBanditMeanLoss_sub_bestArm_eq_gap
Compiled
Mean-loss differences against the selected best arm are model gaps.
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
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.
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)