Lean module · Tsallis-FTRL
BanditRLProof.TsallisOracleRestartDynamicRegret
# Oracle-restart dynamic-regret assembly This module proves the finite-sum assembly behind a switch-aligned restart route. It does not construct a restarted selector or trajectory kernel: epoch-local fixed-comparator regret certificates remain explicit inputs.
Module map
Imports
BanditRLProof.TsallisFiniteArmIndependentDriftingMeanDynamicRegret
Imported by
BanditRLProof, BanditRLProof.TsallisOracleRestartPredictableRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.oracleRestartEpochRounds
Compiled
Included rounds assigned to one epoch.
def oracleRestartEpochRounds {Epoch : Type w} [DecidableEq Epoch] (epochOf : Nat -> Epoch) (horizon : Nat) (epoch : Epoch) : Finset Nat
def
BanditRLProof.Tsallis.sampledScheduledHalfTsallisPredictableOracleRestartEpochRegret
Compiled
Predictable fixed-comparator regret contributed by one epoch fiber.
noncomputable def sampledScheduledHalfTsallisPredictableOracleRestartEpochRegret {Env : Type u} {Action : Type v} {Epoch : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] [DecidableEq Epoch] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (epochOf : Nat -> Epoch) (epochComparator : Epoch -> Action) (horizon : Nat) (epoch : Epoch) (sample : Env × ((k : Nat) -> Action × Real)) : Real
theorem
BanditRLProof.Tsallis.sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret_eq_sum_oracleRestartEpochRegret
Compiled
Moving-comparator regret against an epochwise constant comparator is exactly the sum of its epoch-fiber fixed-comparator regrets.
theorem sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret_eq_sum_oracleRestartEpochRegret {Env : Type u} {Action : Type v} {Epoch : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] [DecidableEq Epoch] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (epochs : Finset Epoch) (epochOf : Nat -> Epoch) (epochComparator : Epoch -> Action) (horizon : Nat) (hEpochOf : ∀ t ∈ Finset.range (horizon + 1), epochOf t ∈ epochs) (sample : Env × ((k : Nat) -> Action × Real)) : sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta loss (fun t => epochComparator (epochOf t)) horizon sample = epochs.sum (fun epoch => sampledScheduledHalfTsallisPredictableOracleRestartEpochRegret arms harms eta loss epochOf epochComparator horizon epoch sample)
theorem
BanditRLProof.Tsallis.sum_sqrt_oracleRestartEpochRounds_card_le
Compiled
Cauchy--Schwarz bound for the square roots of epoch-fiber lengths.
theorem sum_sqrt_oracleRestartEpochRounds_card_le {Epoch : Type w} [DecidableEq Epoch] (epochs : Finset Epoch) (epochOf : Nat -> Epoch) (horizon : Nat) (hEpochOf : ∀ t ∈ Finset.range (horizon + 1), epochOf t ∈ epochs) : epochs.sum (fun epoch => Real.sqrt ((oracleRestartEpochRounds epochOf horizon epoch).card : Real)) <= Real.sqrt (epochs.card : Real) * Real.sqrt (((horizon + 1 : Nat) : Real))
theorem
BanditRLProof.Tsallis.sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_oracleRestartSqrt
Compiled
Oracle-restart assembly: epoch-local square-root fixed-comparator certificates yield a global square-root moving-comparator bound.
theorem sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_oracleRestartSqrt {Env : Type u} {Action : Type v} {Epoch : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] [DecidableEq Epoch] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (epochs : Finset Epoch) (epochOf : Nat -> Epoch) (epochComparator : Epoch -> Action) (horizon : Nat) (hEpochOf : ∀ t ∈ Finset.range (horizon + 1), epochOf t ∈ epochs) (coefficient : Real) (hcoefficient : 0 <= coefficient) (sample : Env × ((k : Nat) -> Action × Real)) (hEpochRegret : ∀ epoch ∈ epochs, sampledScheduledHalfTsallisPredictableOracleRestartEpochRegret arms harms eta loss epochOf epochComparator horizon epoch sample <= coefficient * Real.sqrt ((oracleRestartEpochRounds epochOf horizon epoch).card : Real)) : sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta loss (fun t => epochComparator (epochOf t)) horizon sample <= coefficient * Real.sqrt (epochs.card : Real) * Real.sqrt (((horizon + 1 : Nat) : Real))
theorem
BanditRLProof.Tsallis.sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_oracleRestartSwitchCountSqrt
Compiled
Switch-count-facing oracle-restart assembly. When the epoch partition has at most one more epoch than switches, the global moving-comparator bound has the standard `sqrt((switches + 1) * (horizon + 1))` product form.
theorem sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_oracleRestartSwitchCountSqrt {Env : Type u} {Action : Type v} {Epoch : Type w} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] [DecidableEq Epoch] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (epochs : Finset Epoch) (epochOf : Nat -> Epoch) (epochComparator : Epoch -> Action) (horizon switches : Nat) (hEpochOf : ∀ t ∈ Finset.range (horizon + 1), epochOf t ∈ epochs) (hEpochCard : epochs.card <= switches + 1) (coefficient : Real) (hcoefficient : 0 <= coefficient) (sample : Env × ((k : Nat) -> Action × Real)) (hEpochRegret : ∀ epoch ∈ epochs, sampledScheduledHalfTsallisPredictableOracleRestartEpochRegret arms harms eta loss epochOf epochComparator horizon epoch sample <= coefficient * Real.sqrt ((oracleRestartEpochRounds epochOf horizon epoch).card : Real)) : sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta loss (fun t => epochComparator (epochOf t)) horizon sample <= coefficient * Real.sqrt (((switches + 1 : Nat) : Real)) * Real.sqrt (((horizon + 1 : Nat) : Real))