BanditRLProof.TsallisOracleRestartRefinedStabilityTuning

The refined all-arm half-Tsallis budget is bounded by the square-root mass of the arms other than any distinguished supported arm.

theorem refinedPotentialStabilityBound_le_two_mul_eta_mul_sqrt_erase_card {History : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) {best : Action} (hbest : best ∈ arms) (eta : Real) (heta : 0 <= eta) (probability : History -> Action -> Real) (history : History) (hprobability : FTRL.finiteSimplex arms (probability history)) : refinedPotentialStabilityBound arms eta probability history <= 2 * eta * Real.sqrt ((arms.erase best).card : Real) + 2 * eta ^ 2

One actual restart-local successor has the deterministic refined square-root-cardinality budget under the single global generated law.

theorem integral_sampledOracleRestartHalfTsallisShiftedPotentialStabilityAtSuccessor_le_two_mul_eta_mul_sqrt_erase_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) (n : Nat) {best : Action} (hbest : best ∈ arms) (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)) Integrable term mu ∧ integral mu term <= 2 * eta (oracleRestartLocalTime schedule (n + 1)) * Real.sqrt ((arms.erase best).card : Real) + 2 * eta (oracleRestartLocalTime schedule (n + 1)) ^ 2

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

theorem one_div_natSucc_le_one_div_sqrt_natSucc (t : Nat) : 1 / (((t + 1 : Nat) : Real)) <= 1 / Real.sqrt (((t + 1 : Nat) : Real))

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

theorem sampledScheduledHalfTsallisSqrtSchedule_two_mul (t : Nat) : 2 * sampledScheduledHalfTsallisSqrtSchedule t = 1 / Real.sqrt (((t + 1 : Nat) : Real))

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

theorem sampledScheduledHalfTsallisSqrtSchedule_two_mul_sq (t : Nat) : 2 * sampledScheduledHalfTsallisSqrtSchedule t ^ 2 = (1 / 2 : Real) * (1 / (((t + 1 : Nat) : Real)))

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

theorem one_div_sampledScheduledHalfTsallisSqrtSchedule (t : Nat) : 1 / sampledScheduledHalfTsallisSqrtSchedule t = 2 * Real.sqrt (((t + 1 : Nat) : Real))

The deterministic refined budgets of the square-root schedule have an inclusive prefix bound of order `sqrt(card * time)`.

theorem sum_range_sampledScheduledHalfTsallisSqrtSchedule_refinedBudget_le_three_mul_sqrt {Action : Type u} (arms : Finset Action) (harms : arms.Nonempty) (n : Nat) : (Finset.range n).sum (fun t => 2 * sampledScheduledHalfTsallisSqrtSchedule t * Real.sqrt (arms.card : Real) + 2 * sampledScheduledHalfTsallisSqrtSchedule t ^ 2) <= 3 * Real.sqrt (arms.card : Real) * Real.sqrt (n : Real)

A deterministic contiguous restart epoch has an expected shifted stability prefix bounded by `4 * sqrt(K) * sqrt(epoch length)`.

theorem integral_sum_sampledOracleRestartHalfTsallisShiftedPotentialStabilityAtLocalPrefix_sqrtSchedule_le_four_mul_sqrt {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) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (epoch localHorizon : Nat) {best : Action} (hbest : best ∈ arms) (hstart : ∀ localTime, localTime <= localHorizon -> schedule.start (epoch + localTime) = epoch) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule schedule loss.environment let stabilitySum := fun sample => (Finset.range (localHorizon + 1)).sum (fun localTime => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms sampledScheduledHalfTsallisSqrtSchedule (oracleRestartShiftedTrajectory epoch sample) localTime) Integrable stabilitySum mu ∧ integral mu stabilitySum <= 4 * Real.sqrt (arms.card : Real) * Real.sqrt ((localHorizon + 1 : Nat) : Real)

The terminal point-mass penalty of one square-root-scheduled epoch is bounded by `4 * sqrt(K) * sqrt(epoch length)`.

theorem initialHalfTsallisPotentialMass_sqrtSchedule_pointMassPenalty_le_four_mul_sqrt {Action : Type u} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) {best : Action} (hbest : best ∈ arms) (localHorizon : Nat) : halfTsallisPotentialMass arms (initialHalfTsallisDistribution arms harms (sampledScheduledHalfTsallisSqrtSchedule 0)) / sampledScheduledHalfTsallisSqrtSchedule localHorizon - 1 / sampledScheduledHalfTsallisSqrtSchedule localHorizon <= 4 * Real.sqrt (arms.card : Real) * Real.sqrt ((localHorizon + 1 : Nat) : Real)

An actual contiguous restart epoch run with the square-root schedule has the `C * sqrt(epoch length)` observed estimated-regret certificate required by the restart dynamic-regret assembly, with `C = 8 * sqrt(K)`.

theorem integral_sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret_pointMass_sqrtSchedule_le_eight_mul_sqrt {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) (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)) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule schedule loss.environment let observed := sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret (Env

Cardinality-shaped form of the tuned epoch certificate.

theorem integral_sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret_pointMass_sqrtSchedule_le_eight_mul_sqrt_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) (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)) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule schedule loss.environment let observed := sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret (Env

Every actual epoch of the restart schedule exposes the cardinality-shaped certificate directly, with no caller-supplied local-horizon witness.

theorem integral_sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret_pointMass_sqrtSchedule_le_eight_mul_sqrt_card_of_mem {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) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (horizon epoch : Nat) {best : Action} (hbest : best ∈ arms) (hepoch : epoch ∈ oracleRestartScheduleEpochs schedule horizon) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule schedule loss.environment let observed := sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret (Env