BanditRLProof.TsallisOracleRestartGlobalMeanSwitchCount

Start of the most recent epoch when a restart occurs after every `change` boundary. A true value at `s` starts the new epoch at `s + 1`.

def oracleChangePointRestartStart (change : Nat -> Prop) [DecidablePred change] : Nat -> Nat | 0 => 0 | n + 1 => if change n then n + 1 else oracleChangePointRestartStart change n /-- A valid restart schedule generated by an arbitrary decidable boundary predicate. -/ def oracleChangePointRestartSchedule (change : Nat -> Prop) [DecidablePred change] : OracleRestartSchedule where

A valid restart schedule generated by an arbitrary decidable boundary predicate.

def oracleChangePointRestartSchedule (change : Nat -> Prop) [DecidablePred change] : OracleRestartSchedule where

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

theorem oracleChangePointRestartSchedule_start_zero (change : Nat -> Prop) [DecidablePred change] : (oracleChangePointRestartSchedule change).start 0 = 0

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

theorem oracleChangePointRestartSchedule_start_succ (change : Nat -> Prop) [DecidablePred change] (n : Nat) : (oracleChangePointRestartSchedule change).start (n + 1) = if change n then n + 1 else (oracleChangePointRestartSchedule change).start n

The registered epochs are zero together with every successor of a change point before the inclusive horizon.

theorem oracleRestartScheduleEpochs_oracleChangePointRestartSchedule (change : Nat -> Prop) [DecidablePred change] (horizon : Nat) : oracleRestartScheduleEpochs (oracleChangePointRestartSchedule change) horizon = insert 0 (((Finset.range horizon).filter change).image (fun s => s + 1))

A change-point restart schedule has exactly one more visited epoch than the number of change boundaries before the inclusive horizon.

theorem oracleRestartScheduleEpochs_card_oracleChangePointRestartSchedule (change : Nat -> Prop) [DecidablePred change] (horizon : Nat) : (oracleRestartScheduleEpochs (oracleChangePointRestartSchedule change) horizon).card = ((Finset.range horizon).filter change).card + 1

A boundary has a global population-mean change when at least one arm changes mean between its two adjacent reward laws.

def finiteArmIndependentGlobalMeanChangeAt {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (s : Nat) : Prop

Global population-mean change boundaries strictly before `horizon`.

noncomputable def finiteArmIndependentGlobalMeanChangeTimes {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (horizon : Nat) : Finset Nat

Population-mean oracle schedule: restart immediately after every global mean-change boundary.

noncomputable def finiteArmIndependentGlobalMeanChangeRestartSchedule {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) : OracleRestartSchedule

The population-mean restart schedule has exactly one initial epoch plus one epoch for every global mean-change boundary.

theorem oracleRestartScheduleEpochs_card_finiteArmIndependentGlobalMeanChangeRestartSchedule {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (horizon : Nat) : (oracleRestartScheduleEpochs (finiteArmIndependentGlobalMeanChangeRestartSchedule armLaw) horizon).card = (finiteArmIndependentGlobalMeanChangeTimes armLaw horizon).card + 1

The existing real-valued global switch count is the coercion of the named change-time finset cardinality.

theorem finiteArmIndependentCumulativeGlobalMeanSwitchCount_eq_changeTimes_card {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (horizon : Nat) : finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw horizon = ((finiteArmIndependentGlobalMeanChangeTimes armLaw horizon).card : Real)

In real-valued form, the exact epoch count is the existing cumulative global population-mean switch count plus one.

theorem oracleRestartScheduleEpochs_card_cast_finiteArmIndependentGlobalMeanChangeRestartSchedule {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (horizon : Nat) : ((oracleRestartScheduleEpochs (finiteArmIndependentGlobalMeanChangeRestartSchedule armLaw) horizon).card : Real) = finiteArmIndependentCumulativeGlobalMeanSwitchCount armLaw horizon + 1

Since every global mean change starts a new epoch, each arm's population mean is constant from the current epoch start through the current round.

theorem finiteArmIndependentRewardMean_eq_globalMeanChangeRestartStart {K : Nat} (armLaw : Nat -> Fin K -> Measure Rat) (t : Nat) (arm : Fin K) : finiteArmIndependentRewardMean armLaw t arm = finiteArmIndependentRewardMean armLaw ((finiteArmIndependentGlobalMeanChangeRestartSchedule armLaw).start t) arm

The arm maximizing population mean at the current epoch start remains a population-mean maximizer at every round in that epoch.

theorem finiteArmIndependentRewardMean_le_globalMeanChangeRestartBestArm {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (t : Nat) (arm : Fin K) : finiteArmIndependentRewardMean armLaw t arm <= finiteArmIndependentRewardMean armLaw t (finiteArmIndependentBestArmAt model armLaw ((finiteArmIndependentGlobalMeanChangeRestartSchedule armLaw).start t))

Under unit support, the raw-population-mean oracle comparator is also optimal for the clipped loss used by the generated trajectory.

theorem independentLossStateTimeVaryingMeanGap_globalMeanChangeRestartBestArm_nonneg {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (hprob : forall t arm, IsProbabilityMeasure (armLaw t arm)) (hbound : forall t arm, ∀ᵐ reward ∂armLaw t arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (t : Nat) (arm : Fin K) : 0 <= independentLossStateTimeVaryingMeanGap (finiteArmIndependentRewardVectorLaw armLaw) (fun _ => finiteArmIIDRewardVectorLoss) t (finiteArmIndependentBestArmAt model armLaw ((finiteArmIndependentGlobalMeanChangeRestartSchedule armLaw).start t)) arm

The concrete independent reward law, restarted at every global population-mean change, has generated expected dynamic regret bounded by the square root of its exact population-mean switch count. The comparator selected at each epoch start remains optimal for the clipped loss throughout that epoch under the almost-sure unit-support contract.

theorem integral_sampledOracleRestartHalfTsallisFiniteArmIndependentGlobalMeanChangeDynamicRegret_le {K : Nat} (model : FiniteBanditModel K) (armLaw : Nat -> Fin K -> Measure Rat) (hprob : ∀ t arm, IsProbabilityMeasure (armLaw t arm)) (hbound : ∀ t arm, ∀ᵐ reward ∂armLaw t arm, ((reward : Rat) : Real) ∈ Set.Icc (0 : Real) 1) (horizon : Nat) : letI : Nonempty (Fin K)