Lean module · Tsallis-FTRL
BanditRLProof.TsallisOracleRestartGeneratedDynamicRegret
# Generated oracle-restart dynamic regret This module feeds the generated, observed epoch certificate for the square-root half-Tsallis schedule into the predictable moving-comparator assembly. The switch-count-facing theorem keeps schedule cardinality as an explicit contract; deriving that contract from a concrete restart law is a separate obligation.
Module map
Imports
BanditRLProof.TsallisOracleRestartRefinedStabilityTuning
Imported by
BanditRLProof, BanditRLProof.TsallisOracleRestartGlobalMeanSwitchCount
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Tsallis.integral_sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_sqrtSchedule_le_scheduleSqrt
Compiled
The generated square-root-schedule epoch certificate assembles into the schedule-cardinality-facing expected moving-comparator regret bound.
theorem integral_sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_sqrtSchedule_le_scheduleSqrt {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) (epochComparator : Nat -> Action) (horizon : Nat) (hcomparator : ∀ epoch ∈ oracleRestartScheduleEpochs schedule horizon, epochComparator epoch ∈ arms) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule schedule loss.environment Integrable (sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule schedule loss (fun t => epochComparator (schedule.start t)) horizon) mu ∧ integral mu (sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule schedule loss (fun t => epochComparator (schedule.start t)) horizon) <= (8 * Real.sqrt (arms.card : Real)) * Real.sqrt ((oracleRestartScheduleEpochs schedule horizon).card : Real) * Real.sqrt (((horizon + 1 : Nat) : Real))
theorem
BanditRLProof.Tsallis.integral_sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_sqrtSchedule_le_scheduleSwitchCountSqrt
Compiled
Under an explicit schedule-epoch count contract, the same generated certificate yields the switch-count-facing expected dynamic-regret bound.
theorem integral_sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret_sqrtSchedule_le_scheduleSwitchCountSqrt {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) (epochComparator : Nat -> Action) (horizon switches : Nat) (hcomparator : ∀ epoch ∈ oracleRestartScheduleEpochs schedule horizon, epochComparator epoch ∈ arms) (hEpochCard : (oracleRestartScheduleEpochs schedule horizon).card <= switches + 1) : let mu := prior ⊗ₘ sampledOracleRestartHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule schedule loss.environment Integrable (sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule schedule loss (fun t => epochComparator (schedule.start t)) horizon) mu ∧ integral mu (sampledOracleRestartHalfTsallisPredictableMovingComparatorEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule schedule loss (fun t => epochComparator (schedule.start t)) horizon) <= (8 * Real.sqrt (arms.card : Real)) * Real.sqrt (((switches + 1 : Nat) : Real)) * Real.sqrt (((horizon + 1 : Nat) : Real))