BanditRLProof.TsallisOracleRestartPredictableRegret

Predictable environment regret of the generated restart probabilities against a fixed comparator distribution through the inclusive horizon.

noncomputable def sampledOracleRestartHalfTsallisPredictableEnvironmentRegret {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

Predictable environment regret of the generated restart probabilities against a deterministic comparator arm that may change with the round.

noncomputable def sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (comparator : Nat -> Action) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem sampledOracleRestartHalfTsallisPredictableEnvironmentRegret_neverRestart {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledOracleRestartHalfTsallisPredictableEnvironmentRegret arms harms eta oracleNeverRestartSchedule loss q horizon sample = sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss q horizon sample

No declaration docstring is present; use the chapter context and exact statement below.

theorem sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_neverRestart {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (comparator : Nat -> Action) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta oracleNeverRestartSchedule loss comparator horizon sample = sampledScheduledHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta loss comparator horizon sample

Restarted moving-comparator regret is fixed point-mass regret plus the cumulative advantage of the moving comparator over the fixed arm.

theorem sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_eq_fixed_add {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (comparator : Nat -> Action) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta schedule loss comparator horizon sample = sampledOracleRestartHalfTsallisPredictableEnvironmentRegret arms harms eta schedule loss (pointMass best) horizon sample + (Finset.range (horizon + 1)).sum (fun t => Exp3.predictableLossAt loss t sample best - Exp3.predictableLossAt loss t sample (comparator t))

Epoch ids actually visited by the restart schedule through the inclusive horizon. The epoch assignment is exactly `schedule.start`.

def oracleRestartScheduleEpochs (schedule : OracleRestartSchedule) (horizon : Nat) : Finset Nat

No declaration docstring is present; use the chapter context and exact statement below.

theorem oracleRestartSchedule_start_mem_epochs (schedule : OracleRestartSchedule) (horizon t : Nat) (ht : t ∈ Finset.range (horizon + 1)) : schedule.start t ∈ oracleRestartScheduleEpochs schedule horizon

Restart-specific predictable regret contributed by one schedule epoch.

noncomputable def sampledOracleRestartHalfTsallisPredictableScheduleEpochRegret {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (epochComparator : Nat -> Action) (horizon epoch : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

Schedule-aligned moving regret is exactly the sum of its epoch-fiber regrets, with no independent `epochOf` compatibility premise.

theorem sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_eq_sum_scheduleEpochRegret {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (epochComparator : Nat -> Action) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta schedule loss (fun t => epochComparator (schedule.start t)) horizon sample = (oracleRestartScheduleEpochs schedule horizon).sum (fun epoch => sampledOracleRestartHalfTsallisPredictableScheduleEpochRegret arms harms eta schedule loss epochComparator horizon epoch sample)

Schedule-aligned epoch certificates assemble into a global square-root bound for the generated restart regret surface.

theorem sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_scheduleSqrt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (epochComparator : Nat -> Action) (horizon : Nat) (coefficient : Real) (hcoefficient : 0 <= coefficient) (sample : Env × ((k : Nat) -> Action × Real)) (hEpochRegret : ∀ epoch ∈ oracleRestartScheduleEpochs schedule horizon, sampledOracleRestartHalfTsallisPredictableScheduleEpochRegret arms harms eta schedule loss epochComparator horizon epoch sample <= coefficient * Real.sqrt ((oracleRestartEpochRounds schedule.start horizon epoch).card : Real)) : sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta schedule loss (fun t => epochComparator (schedule.start t)) horizon sample <= coefficient * Real.sqrt ((oracleRestartScheduleEpochs schedule horizon).card : Real) * Real.sqrt (((horizon + 1 : Nat) : Real))

Switch-count-facing schedule assembly under an explicit cardinality contract on the epochs actually visited by `schedule.start`.

theorem sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_scheduleSwitchCountSqrt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (epochComparator : Nat -> Action) (horizon switches : Nat) (hEpochCard : (oracleRestartScheduleEpochs schedule horizon).card <= switches + 1) (coefficient : Real) (hcoefficient : 0 <= coefficient) (sample : Env × ((k : Nat) -> Action × Real)) (hEpochRegret : ∀ epoch ∈ oracleRestartScheduleEpochs schedule horizon, sampledOracleRestartHalfTsallisPredictableScheduleEpochRegret arms harms eta schedule loss epochComparator horizon epoch sample <= coefficient * Real.sqrt ((oracleRestartEpochRounds schedule.start horizon epoch).card : Real)) : sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta schedule loss (fun t => epochComparator (schedule.start t)) horizon sample <= coefficient * Real.sqrt (((switches + 1 : Nat) : Real)) * Real.sqrt (((horizon + 1 : Nat) : Real))