BanditRLProof.TsallisOracleRestartExpectedRegret

Predictable importance-weighted loss using the generated restart probability at the same actual trajectory time.

noncomputable def sampledOracleRestartHalfTsallisPredictableEstimatedLossAt {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) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Action -> Real

Stored-reward importance-weighted loss under the generated restart probability at the same actual trajectory time.

noncomputable def sampledOracleRestartHalfTsallisObservedEstimatedLossAt {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)) : Action -> Real

Restarted successor probability on an environment/global-prefix state.

noncomputable def sampledOracleRestartHalfTsallisProbabilityAt {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

Environment-lifted measurable source for one restarted successor law.

noncomputable def sampledOracleRestartHalfTsallisEnvironmentHistoryDistributionSource {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) : Exp3.MeasurableFiniteActionDistribution arms (sampledOracleRestartHalfTsallisProbabilityAt (Env

The restarted policy comapped to the environment/global-prefix state.

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

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

theorem sampledOracleRestartHalfTsallisPolicyAt_eq_finiteActionKernel {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) : sampledOracleRestartHalfTsallisPolicyAt (Env

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

theorem measurable_sampledOracleRestartHalfTsallisProbabilityAtTime {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) (t : Nat) (candidate : Action) (hcandidate : candidate ∈ arms) : Measurable (fun sample : Env × ((k : Nat) -> Action × Real) => sampledOracleRestartHalfTsallisProbabilityAtTime arms harms eta schedule t sample candidate)

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

theorem measurable_sampledOracleRestartHalfTsallisPredictableEstimatedLossAt {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) (t : Nat) (candidate : Action) (hcandidate : candidate ∈ arms) : Measurable (fun sample : Env × ((k : Nat) -> Action × Real) => sampledOracleRestartHalfTsallisPredictableEstimatedLossAt arms harms eta schedule loss t sample candidate)

Deterministic predictable feedback identifies each stored-reward restart estimator with its predictable counterpart almost surely.

theorem sampledOracleRestartHalfTsallisObservedEstimatedLossAt_eq_predictable_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) (t : Nat) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment (fun sample => sampledOracleRestartHalfTsallisObservedEstimatedLossAt arms harms eta schedule t sample) =ᵐ[mu] (fun sample => sampledOracleRestartHalfTsallisPredictableEstimatedLossAt arms harms eta schedule loss t sample)

At each generated restart time, mixed and comparator-weighted importance-weighted estimators are integrable and have the corresponding predictable environment first moments.

theorem sampledOracleRestartHalfTsallisPredictableEstimatedLossAt_first_moments {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) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (t : Nat) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment (Integrable (fun sample => FTRL.linearLoss arms (sampledOracleRestartHalfTsallisProbabilityAtTime arms harms eta schedule t sample) (sampledOracleRestartHalfTsallisPredictableEstimatedLossAt arms harms eta schedule loss t sample)) mu ∧ Integrable (fun sample => FTRL.linearLoss arms q (sampledOracleRestartHalfTsallisPredictableEstimatedLossAt arms harms eta schedule loss t sample)) mu) ∧ ((integral mu (fun sample => FTRL.linearLoss arms (sampledOracleRestartHalfTsallisProbabilityAtTime arms harms eta schedule t sample) (sampledOracleRestartHalfTsallisPredictableEstimatedLossAt arms harms eta schedule loss t sample)) = integral mu (fun sample => FTRL.linearLoss arms (sampledOracleRestartHalfTsallisProbabilityAtTime arms harms eta schedule t sample) (Exp3.predictableLossAt loss t sample))) ∧ (integral mu (fun sample => FTRL.linearLoss arms q (sampledOracleRestartHalfTsallisPredictableEstimatedLossAt arms harms eta schedule loss t sample)) = integral mu (fun sample => FTRL.linearLoss arms q (Exp3.predictableLossAt loss t sample))))

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

theorem finiteSimplex_sampledOracleRestartHalfTsallisProbabilityAtTime {Env : Type u} {Action : Type v} [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : FTRL.finiteSimplex arms (sampledOracleRestartHalfTsallisProbabilityAtTime arms harms eta schedule t sample)

Generated restart mixed predictable loss and any fixed simplex comparator loss are integrable at every actual time.

theorem integrable_sampledOracleRestartHalfTsallisPredictableLinearLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) [IsFiniteMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (schedule : OracleRestartSchedule) (loss : Exp3.PredictableLossVector Env Action) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (t : Nat) : Integrable (fun sample => FTRL.linearLoss arms (sampledOracleRestartHalfTsallisProbabilityAtTime arms harms eta schedule t sample) (Exp3.predictableLossAt loss t sample)) mu ∧ Integrable (fun sample => FTRL.linearLoss arms q (Exp3.predictableLossAt loss t sample)) mu

Estimated regret contributed by one actual schedule epoch.

noncomputable def sampledOracleRestartHalfTsallisPredictableScheduleEpochEstimatedRegret {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 epoch : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

Stored-reward estimated regret contributed by one actual schedule epoch.

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

Environment regret against a fixed comparator distribution on one actual schedule epoch.

noncomputable def sampledOracleRestartHalfTsallisPredictableScheduleEpochEnvironmentRegret {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 epoch : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

Epoch-local estimated regret is integrable and has exactly the same integral as fixed-comparator environment regret on the actual generated restart law.

theorem integral_sampledOracleRestartHalfTsallisPredictableScheduleEpochEstimatedRegret_eq_environmentRegret {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) (q : Action -> Real) (hq : FTRL.finiteSimplex arms q) (horizon epoch : Nat) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment Integrable (sampledOracleRestartHalfTsallisPredictableScheduleEpochEstimatedRegret arms harms eta schedule loss q horizon epoch) mu ∧ Integrable (sampledOracleRestartHalfTsallisPredictableScheduleEpochEnvironmentRegret arms harms eta schedule loss q horizon epoch) mu ∧ integral mu (sampledOracleRestartHalfTsallisPredictableScheduleEpochEstimatedRegret arms harms eta schedule loss q horizon epoch) = integral mu (sampledOracleRestartHalfTsallisPredictableScheduleEpochEnvironmentRegret arms harms eta schedule loss q horizon epoch)

Stored-reward and predictable-estimator regret agree almost surely on every actual schedule epoch fiber.

theorem sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret_eq_predictable_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) (q : Action -> Real) (horizon epoch : Nat) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret arms harms eta schedule q horizon epoch =ᵐ[mu] sampledOracleRestartHalfTsallisPredictableScheduleEpochEstimatedRegret arms harms eta schedule loss q horizon epoch

A point-mass comparator on one schedule fiber is the existing epoch-comparator environment-regret surface.

theorem sampledOracleRestartHalfTsallisPredictableScheduleEpochEnvironmentRegret_pointMass_eq {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) (epoch : Nat) (hcomparator : epochComparator epoch ∈ arms) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledOracleRestartHalfTsallisPredictableScheduleEpochEnvironmentRegret arms harms eta schedule loss (pointMass (epochComparator epoch)) horizon epoch sample = sampledOracleRestartHalfTsallisPredictableScheduleEpochRegret arms harms eta schedule loss epochComparator horizon epoch sample

Fixed-arm epoch estimated regret transports exactly to the existing epoch environment-regret integral on the generated restart law.

theorem integral_sampledOracleRestartHalfTsallisPredictableScheduleEpochEstimatedRegret_pointMass_eq_epochRegret {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) (epochComparator : Nat -> Action) (epoch : Nat) (hcomparator : epochComparator epoch ∈ arms) (horizon : Nat) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment Integrable (sampledOracleRestartHalfTsallisPredictableScheduleEpochEstimatedRegret arms harms eta schedule loss (pointMass (epochComparator epoch)) horizon epoch) mu ∧ Integrable (sampledOracleRestartHalfTsallisPredictableScheduleEpochRegret arms harms eta schedule loss epochComparator horizon epoch) mu ∧ integral mu (sampledOracleRestartHalfTsallisPredictableScheduleEpochEstimatedRegret arms harms eta schedule loss (pointMass (epochComparator epoch)) horizon epoch) = integral mu (sampledOracleRestartHalfTsallisPredictableScheduleEpochRegret arms harms eta schedule loss epochComparator horizon epoch)

Stored-reward fixed-arm epoch estimated regret is integrable and has exactly the existing epoch environment-regret integral.

theorem integral_sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret_pointMass_eq_epochRegret {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) (epochComparator : Nat -> Action) (epoch : Nat) (hcomparator : epochComparator epoch ∈ arms) (horizon : Nat) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment Integrable (sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret arms harms eta schedule (pointMass (epochComparator epoch)) horizon epoch) mu ∧ Integrable (sampledOracleRestartHalfTsallisPredictableScheduleEpochRegret arms harms eta schedule loss epochComparator horizon epoch) mu ∧ integral mu (sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret arms harms eta schedule (pointMass (epochComparator epoch)) horizon epoch) = integral mu (sampledOracleRestartHalfTsallisPredictableScheduleEpochRegret arms harms eta schedule loss epochComparator horizon epoch)

Any expected estimated-regret certificate on an actual schedule epoch transports to the corresponding fixed-arm environment-regret certificate.

theorem integral_sampledOracleRestartHalfTsallisPredictableScheduleEpochRegret_le_of_estimatedRegret_le {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) (epochComparator : Nat -> Action) (epoch : Nat) (hcomparator : epochComparator epoch ∈ arms) (horizon : Nat) (bound : Real) (hEstimated : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment integral mu (sampledOracleRestartHalfTsallisPredictableScheduleEpochEstimatedRegret arms harms eta schedule loss (pointMass (epochComparator epoch)) horizon epoch) <= bound) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment integral mu (sampledOracleRestartHalfTsallisPredictableScheduleEpochRegret arms harms eta schedule loss epochComparator horizon epoch) <= bound

Epoch-local expected estimated-regret certificates assemble into an expected moving-comparator square-root bound on the actual generated restart trajectory.

theorem integral_sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_scheduleSqrt_of_epochEstimatedRegret {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) (epochComparator : Nat -> Action) (horizon : Nat) (hcomparator : ∀ epoch ∈ oracleRestartScheduleEpochs schedule horizon, epochComparator epoch ∈ arms) (coefficient : Real) (hcoefficient : 0 <= coefficient) (hEstimated : ∀ epoch ∈ oracleRestartScheduleEpochs schedule horizon, integral (prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment) (sampledOracleRestartHalfTsallisPredictableScheduleEpochEstimatedRegret arms harms eta schedule loss (pointMass (epochComparator epoch)) horizon epoch) <= coefficient * Real.sqrt ((oracleRestartEpochRounds schedule.start horizon epoch).card : Real)) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment Integrable (sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta schedule loss (fun t => epochComparator (schedule.start t)) horizon) mu ∧ integral mu (sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta schedule loss (fun t => epochComparator (schedule.start t)) horizon) <= coefficient * Real.sqrt ((oracleRestartScheduleEpochs schedule horizon).card : Real) * Real.sqrt (((horizon + 1 : Nat) : Real))

Switch-count-facing expected restart bound under an explicit cardinality contract and epoch-local estimated-regret certificates.

theorem integral_sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_scheduleSwitchCountSqrt_of_epochEstimatedRegret {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) (epochComparator : Nat -> Action) (horizon switches : Nat) (hcomparator : ∀ epoch ∈ oracleRestartScheduleEpochs schedule horizon, epochComparator epoch ∈ arms) (hEpochCard : (oracleRestartScheduleEpochs schedule horizon).card <= switches + 1) (coefficient : Real) (hcoefficient : 0 <= coefficient) (hEstimated : ∀ epoch ∈ oracleRestartScheduleEpochs schedule horizon, integral (prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment) (sampledOracleRestartHalfTsallisPredictableScheduleEpochEstimatedRegret arms harms eta schedule loss (pointMass (epochComparator epoch)) horizon epoch) <= coefficient * Real.sqrt ((oracleRestartEpochRounds schedule.start horizon epoch).card : Real)) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment Integrable (sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta schedule loss (fun t => epochComparator (schedule.start t)) horizon) mu ∧ integral mu (sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta schedule loss (fun t => epochComparator (schedule.start t)) horizon) <= coefficient * Real.sqrt (((switches + 1 : Nat) : Real)) * Real.sqrt (((horizon + 1 : Nat) : Real))

Stored-reward epoch certificates assemble into the same expected moving-comparator square-root bound on the actual generated restart trajectory.

theorem integral_sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_scheduleSqrt_of_epochObservedEstimatedRegret {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) (epochComparator : Nat -> Action) (horizon : Nat) (hcomparator : ∀ epoch ∈ oracleRestartScheduleEpochs schedule horizon, epochComparator epoch ∈ arms) (coefficient : Real) (hcoefficient : 0 <= coefficient) (hObserved : ∀ epoch ∈ oracleRestartScheduleEpochs schedule horizon, integral (prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment) (sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret arms harms eta schedule (pointMass (epochComparator epoch)) horizon epoch) <= coefficient * Real.sqrt ((oracleRestartEpochRounds schedule.start horizon epoch).card : Real)) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment Integrable (sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta schedule loss (fun t => epochComparator (schedule.start t)) horizon) mu ∧ integral mu (sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta schedule loss (fun t => epochComparator (schedule.start t)) horizon) <= coefficient * Real.sqrt ((oracleRestartScheduleEpochs schedule horizon).card : Real) * Real.sqrt (((horizon + 1 : Nat) : Real))

Stored-reward epoch certificates imply the switch-count-facing expected restart bound under the explicit schedule-cardinality contract.

theorem integral_sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_le_scheduleSwitchCountSqrt_of_epochObservedEstimatedRegret {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) (epochComparator : Nat -> Action) (horizon switches : Nat) (hcomparator : ∀ epoch ∈ oracleRestartScheduleEpochs schedule horizon, epochComparator epoch ∈ arms) (hEpochCard : (oracleRestartScheduleEpochs schedule horizon).card <= switches + 1) (coefficient : Real) (hcoefficient : 0 <= coefficient) (hObserved : ∀ epoch ∈ oracleRestartScheduleEpochs schedule horizon, integral (prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment) (sampledOracleRestartHalfTsallisObservedScheduleEpochEstimatedRegret arms harms eta schedule (pointMass (epochComparator epoch)) horizon epoch) <= coefficient * Real.sqrt ((oracleRestartEpochRounds schedule.start horizon epoch).card : Real)) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms eta schedule loss.environment Integrable (sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta schedule loss (fun t => epochComparator (schedule.start t)) horizon) mu ∧ integral mu (sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms eta schedule loss (fun t => epochComparator (schedule.start t)) horizon) <= coefficient * Real.sqrt (((switches + 1 : Nat) : Real)) * Real.sqrt (((horizon + 1 : Nat) : Real))