BanditRLProof.TsallisOracleRestartExpectedStability

Local time of an actual round in its restart epoch.

def oracleRestartLocalTime (schedule : OracleRestartSchedule) (t : Nat) : Nat

Environment and visible global prefix before actual action `n + 1`.

def sampledOracleRestartHalfTsallisHistoryAt {Env : Type u} {Action : Type v} (n : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Env × History.FinitePairHistory Action Real n

Actual successor action after the visible global prefix through `n`.

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

Restricting a shifted trajectory to its local predecessor prefix is the same finite history as reindexing the corresponding global prefix.

theorem frestrictLe_oracleRestartShiftedTrajectory_eq_localPairHistory {Env : Type u} {Action : Type v} (start n : Nat) (hstart : start <= n) (sample : Env × ((k : Nat) -> Action × Real)) : Preorder.frestrictLe (n - start) (oracleRestartShiftedTrajectory start sample).2 = oracleRestartLocalPairHistory start n hstart (Preorder.frestrictLe n sample.2)

Restart-local cumulative score before actual action `n + 1`.

noncomputable def sampledOracleRestartHalfTsallisScoreAt {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (n : Nat) : Env × History.FinitePairHistory Action Real n -> Action -> Real

Predictable loss at actual successor time `n + 1`.

def sampledOracleRestartHalfTsallisPredictableLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : Env × History.FinitePairHistory Action Real n -> Action -> Real

Same-local-rate update after actual action `n + 1`.

noncomputable def sampledOracleRestartHalfTsallisUpdatedAt {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) (n : Nat) : Env × History.FinitePairHistory Action Real n -> Action -> Action -> Real

Restart-local predictable history/action potential-stability score.

noncomputable def sampledOracleRestartHalfTsallisHistoryActionPotentialStabilityAt {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) (n : Nat) : (Env × History.FinitePairHistory Action Real n) × Action -> Real

Refined restart-local one-round stability budget.

noncomputable def sampledOracleRestartHalfTsallisRefinedPotentialStabilityBoundAt {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (n : Nat) : Env × History.FinitePairHistory Action Real n -> Real

Restart-local potential stability at actual successor time `n + 1`, written with the stored reward before the predictable-law rewrite.

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

The stored-reward restart-local potential term is exactly the scheduled potential term on the path shifted to the current epoch.

theorem sampledOracleRestartHalfTsallisObservedPotentialStabilityAtSuccessor_eq_shifted {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (n : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledOracleRestartHalfTsallisObservedPotentialStabilityAtSuccessor arms harms eta schedule n sample = sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta (oracleRestartShiftedTrajectory (schedule.start (n + 1)) sample) (oracleRestartLocalTime schedule (n + 1))

On the global generated restart law, the shifted stored-reward local stability term agrees almost surely with the predictable restart-local history/action score.

theorem sampledOracleRestartHalfTsallisShiftedPotentialStabilityAtSuccessor_eq_historyAction_ae {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta (oracleRestartShiftedTrajectory (schedule.start (n + 1)) sample) (oracleRestartLocalTime schedule (n + 1))) =ᵐ[mu] (fun sample => sampledOracleRestartHalfTsallisHistoryActionPotentialStabilityAt arms harms eta schedule loss n (sampledOracleRestartHalfTsallisHistoryAt n sample, sampledOracleRestartHalfTsallisActionAt n sample))

Supported coordinates of the restart-local cumulative score are measurable on the visible global prefix.

theorem measurable_sampledOracleRestartHalfTsallisScoreAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (n : Nat) (candidate : Action) (hcandidate : candidate ∈ arms) : Measurable (fun input : Env × History.FinitePairHistory Action Real n => sampledOracleRestartHalfTsallisScoreAt arms harms eta schedule n input candidate)

Supported coordinates of the restart-local same-rate update are measurable.

theorem measurable_sampledOracleRestartHalfTsallisUpdatedAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (candidate : Action) (hcandidate : candidate ∈ arms) : Measurable (fun sample : (Env × History.FinitePairHistory Action Real n) × Action => sampledOracleRestartHalfTsallisUpdatedAt arms harms eta schedule loss n sample.1 sample.2 candidate)

The restart-local predictable history/action potential score is measurable.

theorem measurable_sampledOracleRestartHalfTsallisHistoryActionPotentialStabilityAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : Measurable (sampledOracleRestartHalfTsallisHistoryActionPotentialStabilityAt arms harms eta schedule loss n)

The refined restart-local budget is integrable under every finite visible history law when the local rate is positive.

theorem integrable_sampledOracleRestartHalfTsallisRefinedPotentialStabilityBoundAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (n : Nat) (historyMu : Measure (Env × History.FinitePairHistory Action Real n)) [IsFiniteMeasure historyMu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (heta : 0 < eta (oracleRestartLocalTime schedule (n + 1))) : Integrable (sampledOracleRestartHalfTsallisRefinedPotentialStabilityBoundAt (Env := Env) arms harms eta schedule n) historyMu

The actual restart probability is the regularized minimizer of the restart-local pre-action score at the local learning rate.

theorem sampledOracleRestartHalfTsallisProbabilityAt_isRegularizedMinimizer {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (n : Nat) (input : Env × History.FinitePairHistory Action Real n) : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms (eta (oracleRestartLocalTime schedule (n + 1))) (negEntropyRegularizer arms (1 / 2 : Real)) (sampledOracleRestartHalfTsallisScoreAt arms harms eta schedule n input) (sampledOracleRestartHalfTsallisProbabilityAt arms harms eta schedule n input)

The same-local-rate restart update is the regularized minimizer after the predictable ordinary-IW increment.

theorem sampledOracleRestartHalfTsallisUpdatedAt_isRegularizedMinimizer {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) (n : Nat) (input : Env × History.FinitePairHistory Action Real n) (chosen : Action) : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms (eta (oracleRestartLocalTime schedule (n + 1))) (negEntropyRegularizer arms (1 / 2 : Real)) (fun candidate => sampledOracleRestartHalfTsallisScoreAt arms harms eta schedule n input candidate + Exp3.importanceWeightedLoss (sampledOracleRestartHalfTsallisProbabilityAt arms harms eta schedule n input) (sampledOracleRestartHalfTsallisPredictableLossAt loss n input) chosen candidate) (sampledOracleRestartHalfTsallisUpdatedAt arms harms eta schedule loss n input chosen)

The restart-local predictable potential score is automatically integrable under its visible-history/action finite kernel.

theorem integrable_sampledOracleRestartHalfTsallisHistoryActionPotentialStabilityAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (heta : 0 < eta (oracleRestartLocalTime schedule (n + 1))) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment Integrable (sampledOracleRestartHalfTsallisHistoryActionPotentialStabilityAt arms harms eta schedule loss n) (mu.map (sampledOracleRestartHalfTsallisHistoryAt n) ⊗ₘ sampledOracleRestartHalfTsallisPolicyAt (Env := Env) arms harms eta schedule n)

Under the single generated restart law, the predictable restart-local successor stability score is integrable and has coarse expected budget one.

theorem integral_sampledOracleRestartHalfTsallisHistoryActionPotentialStabilityAt_le_one {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (heta : 0 < eta (oracleRestartLocalTime schedule (n + 1))) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment let term := fun sample => sampledOracleRestartHalfTsallisHistoryActionPotentialStabilityAt arms harms eta schedule loss n (sampledOracleRestartHalfTsallisHistoryAt n sample, sampledOracleRestartHalfTsallisActionAt n sample) Integrable term mu ∧ integral mu term <= integral mu (fun _sample => (1 : Real))

The actual shifted restart-local successor stability term is integrable and has coarse expected budget one under the single global restart law.

theorem integral_sampledOracleRestartHalfTsallisShiftedPotentialStabilityAtSuccessor_le_one {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (heta : 0 < eta (oracleRestartLocalTime schedule (n + 1))) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment let term := fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta (oracleRestartShiftedTrajectory (schedule.start (n + 1)) sample) (oracleRestartLocalTime schedule (n + 1)) Integrable term mu ∧ integral mu term <= integral mu (fun _sample => (1 : Real))

At local rates at most one half, the actual shifted restart-local successor stability term has the refined expected conjugate-potential bound under the single global restart law.

theorem integral_sampledOracleRestartHalfTsallisShiftedPotentialStabilityAtSuccessor_le_refined {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (heta : 0 < eta (oracleRestartLocalTime schedule (n + 1))) (heta_le : eta (oracleRestartLocalTime schedule (n + 1)) <= 1 / 2) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment let term := fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta (oracleRestartShiftedTrajectory (schedule.start (n + 1)) sample) (oracleRestartLocalTime schedule (n + 1)) let bound := fun sample => sampledOracleRestartHalfTsallisRefinedPotentialStabilityBoundAt (Env := Env) arms harms eta schedule n (sampledOracleRestartHalfTsallisHistoryAt n sample) Integrable term mu ∧ Integrable bound mu ∧ integral mu term <= integral mu bound

At global time zero, the restart process has the canonical initial half-Tsallis action law and the usual coarse expected stability budget.

theorem integral_sampledOracleRestartHalfTsallisInitialPotentialStabilityAtTime_le_one {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (heta : 0 < eta 0) (loss : Exp3.PredictableLossVector Env Action) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment Integrable (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta (oracleRestartShiftedTrajectory 0 sample) 0) mu ∧ integral mu (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta (oracleRestartShiftedTrajectory 0 sample) 0) <= integral mu (fun _sample => (1 : Real))

Every actual restart time, including global time zero and later restart boundaries, has the mass-scaled coarse local stability budget under the one global generated law.

theorem integral_sampledOracleRestartHalfTsallisShiftedPotentialStabilityAtTime_le_integral_one {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (t : Nat) (heta : 0 < eta (oracleRestartLocalTime schedule t)) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment let term := fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta (oracleRestartShiftedTrajectory (schedule.start t) sample) (oracleRestartLocalTime schedule t) Integrable term mu ∧ integral mu term <= integral mu (fun _sample => (1 : Real))

On a deterministic contiguous restart epoch, the complete shifted local stability prefix is integrable and its expectation is at most the prefix cardinality. The probability assumption turns the finite-measure one-round budget into the literal constant `1`.

theorem integral_sum_sampledOracleRestartHalfTsallisShiftedPotentialStabilityAtLocalPrefix_le_card {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (epoch localHorizon : Nat) (hstart : ∀ localTime, localTime ≤ localHorizon -> schedule.start (epoch + localTime) = epoch) (heta : ∀ localTime, localTime ≤ localHorizon -> 0 < eta localTime) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment let stabilitySum := fun sample => (Finset.range (localHorizon + 1)).sum (fun localTime => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta (oracleRestartShiftedTrajectory epoch sample) localTime) Integrable stabilitySum mu ∧ integral mu stabilitySum ≤ (localHorizon + 1 : Nat)

A contiguous actual restart epoch inherits an expected observed estimated-regret certificate from the one global generated law. This coarse endpoint is linear in the epoch cardinality; obtaining the target square-root certificate still requires summing and tuning the refined one-round bounds.

theorem integral_sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret_pointMass_le_card_add_penalty_of_epochRounds_eq {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (horizon epoch localHorizon : Nat) {best : Action} (hbest : best ∈ arms) (hRounds : oracleRestartEpochRounds schedule.start horizon epoch = (Finset.range (localHorizon + 1)).image (fun localTime => epoch + localTime)) (heta : ∀ localTime, localTime ≤ localHorizon -> 0 < eta localTime) (hetaMono : ∀ localTime, localTime < localHorizon -> eta (localTime + 1) ≤ eta localTime) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment let observed := sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret (Env := Env) arms harms eta schedule (pointMass best) horizon epoch Integrable observed mu ∧ integral mu observed ≤ (localHorizon + 1 : Nat) + halfTsallisPotentialMass arms (initialHalfTsallisDistribution arms harms (eta 0)) / eta localHorizon - 1 / eta localHorizon