BanditRLProof.TsallisOracleRestartScoreAlignment

Shift a generated trajectory so that `start` becomes local time zero.

def oracleRestartShiftedTrajectory {Env : Type u} {Action : Type v} (start : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Env × ((k : Nat) -> Action × Real)

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

theorem oracleRestartShiftedTrajectory_fst {Env : Type u} {Action : Type v} (start : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : (oracleRestartShiftedTrajectory start sample).1 = sample.1

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

theorem oracleRestartShiftedTrajectory_snd_apply {Env : Type u} {Action : Type v} (start : Nat) (sample : Env × ((k : Nat) -> Action × Real)) (localTime : Nat) : (oracleRestartShiftedTrajectory start sample).2 localTime = sample.2 (start + localTime)

Restart epoch starts are monotone in actual time.

theorem OracleRestartSchedule.monotone_start (schedule : OracleRestartSchedule) : Monotone schedule.start

Every epoch identifier visited by the schedule is a fixed point of `schedule.start`.

theorem OracleRestartSchedule.start_start (schedule : OracleRestartSchedule) (t : Nat) : schedule.start (schedule.start t) = schedule.start t

A restart schedule cannot leave an epoch and later return to it.

theorem OracleRestartSchedule.start_eq_of_between (schedule : OracleRestartSchedule) {epoch localTime t : Nat} (ht : schedule.start t = epoch) (hepoch : epoch <= localTime) (hlocalTime : localTime <= t) : schedule.start localTime = epoch

At every actual time, the restarted probability is exactly the scheduled probability at local time `t - schedule.start t` on the shifted trajectory.

theorem sampledOracleRestartHalfTsallisProbabilityAtTime_eq_scheduled_shift {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledOracleRestartHalfTsallisProbabilityAtTime arms harms eta schedule t sample = sampledScheduledHalfTsallisProbabilityAtTime arms harms eta (t - schedule.start t) (oracleRestartShiftedTrajectory (schedule.start t) sample)

The stored-reward restart estimator is the scheduled stored-reward estimator at the current epoch's local time.

theorem sampledOracleRestartHalfTsallisObservedEstimatedLossAt_eq_scheduled_shift {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledOracleRestartHalfTsallisObservedEstimatedLossAt arms harms eta schedule t sample = sampledScheduledHalfTsallisObservedEstimatedLossAt arms harms eta (t - schedule.start t) (oracleRestartShiftedTrajectory (schedule.start t) sample)

On a fixed epoch fiber, the restarted probability is the scheduled local probability on the trajectory shifted by that epoch.

theorem sampledOracleRestartHalfTsallisProbabilityAtTime_add_eq_scheduled_of_start_eq {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (epoch localTime : Nat) (sample : Env × ((k : Nat) -> Action × Real)) (hstart : schedule.start (epoch + localTime) = epoch) : sampledOracleRestartHalfTsallisProbabilityAtTime arms harms eta schedule (epoch + localTime) sample = sampledScheduledHalfTsallisProbabilityAtTime arms harms eta localTime (oracleRestartShiftedTrajectory epoch sample)

On a fixed epoch fiber, the stored-reward restarted estimator is the scheduled local estimator on the shifted trajectory.

theorem sampledOracleRestartHalfTsallisObservedEstimatedLossAt_add_eq_scheduled_of_start_eq {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (epoch localTime : Nat) (sample : Env × ((k : Nat) -> Action × Real)) (hstart : schedule.start (epoch + localTime) = epoch) : sampledOracleRestartHalfTsallisObservedEstimatedLossAt arms harms eta schedule (epoch + localTime) sample = sampledScheduledHalfTsallisObservedEstimatedLossAt arms harms eta localTime (oracleRestartShiftedTrajectory epoch sample)

Stored-reward estimated regret on an explicit inclusive prefix of one restart epoch, indexed by local times `0, ..., localHorizon`.

noncomputable def sampledOracleRestartHalfTsallisLocalPrefixObservedEstimatedRegret {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (q : Action -> Real) (epoch localHorizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

A contiguous restart-epoch prefix is definitionally the existing scheduled estimated regret on the shifted trajectory.

theorem sampledOracleRestartHalfTsallisLocalPrefixObservedEstimatedRegret_eq_scheduled {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (q : Action -> Real) (epoch localHorizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) (hstart : forall localTime, localTime <= localHorizon -> schedule.start (epoch + localTime) = epoch) : sampledOracleRestartHalfTsallisLocalPrefixObservedEstimatedRegret arms harms eta schedule q epoch localHorizon sample = sampledScheduledHalfTsallisEstimatedRegret arms harms eta q localHorizon (oracleRestartShiftedTrajectory epoch sample)

Pathwise FTRL certificate for any explicit contiguous prefix of one restart epoch.

theorem sampledOracleRestartHalfTsallisLocalPrefixObservedEstimatedRegret_pointMass_le_stability_add_penalty {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (epoch localHorizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) {best : Action} (hbest : best ∈ arms) (hstart : forall localTime, localTime <= localHorizon -> schedule.start (epoch + localTime) = epoch) (heta : forall localTime, localTime <= localHorizon -> 0 < eta localTime) (hetaMono : forall localTime, localTime < localHorizon -> eta (localTime + 1) <= eta localTime) : sampledOracleRestartHalfTsallisLocalPrefixObservedEstimatedRegret arms harms eta schedule (pointMass best) epoch localHorizon sample <= (Finset.range (localHorizon + 1)).sum (fun localTime => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta (oracleRestartShiftedTrajectory epoch sample) localTime) + halfTsallisPotentialMass arms (sampledScheduledHalfTsallisProbabilityAtTime arms harms eta 0 (oracleRestartShiftedTrajectory epoch sample)) / eta localHorizon - 1 / eta localHorizon

Every visited restart epoch fiber is a nonempty contiguous range starting at its epoch identifier.

theorem exists_oracleRestartEpochRounds_eq_image_range (schedule : OracleRestartSchedule) (horizon epoch : Nat) (hepoch : epoch ∈ oracleRestartScheduleEpochs schedule horizon) : ∃ localHorizon, oracleRestartEpochRounds schedule.start horizon epoch = (Finset.range (localHorizon + 1)).image (fun localTime => epoch + localTime)

An explicit range representation of an actual epoch fiber identifies its stored-reward regret with the local-prefix surface.

theorem sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret_eq_localPrefix_of_epochRounds_eq {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (q : Action -> Real) (horizon epoch localHorizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) (hRounds : oracleRestartEpochRounds schedule.start horizon epoch = (Finset.range (localHorizon + 1)).image (fun localTime => epoch + localTime)) : sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret arms harms eta schedule q horizon epoch sample = sampledOracleRestartHalfTsallisLocalPrefixObservedEstimatedRegret arms harms eta schedule q epoch localHorizon sample

Pathwise FTRL certificate for an actual epoch once its finite fiber is presented as a contiguous local-time range.

theorem sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret_pointMass_le_stability_add_penalty_of_epochRounds_eq {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (horizon epoch localHorizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) {best : Action} (hbest : best ∈ arms) (hRounds : oracleRestartEpochRounds schedule.start horizon epoch = (Finset.range (localHorizon + 1)).image (fun localTime => epoch + localTime)) (heta : forall localTime, localTime <= localHorizon -> 0 < eta localTime) (hetaMono : forall localTime, localTime < localHorizon -> eta (localTime + 1) <= eta localTime) : sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret arms harms eta schedule (pointMass best) horizon epoch sample <= (Finset.range (localHorizon + 1)).sum (fun localTime => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta (oracleRestartShiftedTrajectory epoch sample) localTime) + halfTsallisPotentialMass arms (sampledScheduledHalfTsallisProbabilityAtTime arms harms eta 0 (oracleRestartShiftedTrajectory epoch sample)) / eta localHorizon - 1 / eta localHorizon

Every visited epoch admits a local horizon whose cardinality is the actual fiber cardinality and whose stored-reward regret satisfies the pathwise FTRL stability-plus-penalty certificate.

theorem exists_sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret_pointMass_le_stability_add_penalty {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (horizon epoch : Nat) (hepoch : epoch ∈ oracleRestartScheduleEpochs schedule horizon) (sample : Env × ((k : Nat) -> Action × Real)) {best : Action} (hbest : best ∈ arms) (heta : forall localTime, 0 < eta localTime) (hetaMono : forall localTime, eta (localTime + 1) <= eta localTime) : ∃ localHorizon, oracleRestartEpochRounds schedule.start horizon epoch = (Finset.range (localHorizon + 1)).image (fun localTime => epoch + localTime) ∧ (oracleRestartEpochRounds schedule.start horizon epoch).card = localHorizon + 1 ∧ sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret arms harms eta schedule (pointMass best) horizon epoch sample <= (Finset.range (localHorizon + 1)).sum (fun localTime => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta (oracleRestartShiftedTrajectory epoch sample) localTime) + halfTsallisPotentialMass arms (sampledScheduledHalfTsallisProbabilityAtTime arms harms eta 0 (oracleRestartShiftedTrajectory epoch sample)) / eta localHorizon - 1 / eta localHorizon