BanditRLProof.TsallisOracleRestartDynamicRegret

Included rounds assigned to one epoch.

def oracleRestartEpochRounds {Epoch : Type w} [DecidableEq Epoch] (epochOf : Nat -> Epoch) (horizon : Nat) (epoch : Epoch) : Finset Nat

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

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)

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))

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))

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))