Lean module · Tsallis-FTRL
BanditRLProof.TsallisScheduledIndependentMeanGap
# Independent-mean producer for scheduled half-Tsallis expected gaps This module turns an independence-plus-global-mean contract for every predictable loss difference into the conditional-mean law used by scheduled self-bounding. It also exposes the resulting logarithmic square-root-schedule regret theorem on the generated trajectory law.
Module map
Imports
BanditRLProof.TsallisScheduledConditionalMeanGap, BanditRLProof.TsallisSqrtScheduleFixedGap
Imported by
BanditRLProof, BanditRLProof.TsallisFiniteArmIndependentRewardLaw, BanditRLProof.TsallisScheduledIIDMeanGap
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.HasScheduledIndependentMeanGapLaw
Compiled
For every included time and suboptimal arm, the predictable loss difference is independent of the pre-action trace sigma-algebra and has global mean equal to the arm gap.
def HasScheduledIndependentMeanGapLaw {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) (arms : Finset Action) (loss : Exp3.PredictableLossVector Env Action) (best : Action) (gap : Action -> Real) (horizon : Nat) : Prop
theorem
BanditRLProof.Tsallis.hasScheduledConditionalMeanGapLaw_of_independentMeanGapLaw
Compiled
Independence from the pre-action trace and the correct global mean imply the scheduled conditional-mean gap law.
theorem hasScheduledConditionalMeanGapLaw_of_independentMeanGapLaw {Env : Type u} {Action : Type v} [mEnv : MeasurableSpace Env] [mAction : MeasurableSpace Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) [IsProbabilityMeasure mu] (arms : Finset Action) (loss : Exp3.PredictableLossVector Env Action) (best : Action) (gap : Action -> Real) (horizon : Nat) (hgap : HasScheduledIndependentMeanGapLaw mu arms loss best gap horizon) : HasScheduledConditionalMeanGapLaw mu arms loss best gap horizon
theorem
BanditRLProof.Tsallis.hasScheduledExpectedGapLaw_of_independentMeanGapLaw
Compiled
The independence-plus-mean contract also directly produces the coordinatewise first-moment law used by scheduled self-bounding.
theorem hasScheduledExpectedGapLaw_of_independentMeanGapLaw {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) [IsProbabilityMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (best : Action) (gap : Action -> Real) (horizon : Nat) (hgap : HasScheduledIndependentMeanGapLaw mu arms loss best gap horizon) : HasScheduledExpectedGapLaw mu arms harms eta loss best gap horizon
theorem
BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_log_independentMeanGap
Compiled
Under coordinatewise independence from the pre-action trace and the correct global loss-gap means, the generated square-root schedule satisfies the explicit logarithmic regret bound.
theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_log_independentMeanGap {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) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon : Nat) (gap : Action -> Real) (hgapPos : ∀ action, action ∈ arms.erase best -> 0 < gap action) (hgapLaw : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment HasScheduledIndependentMeanGapLaw mu arms loss best gap horizon) (corruption : Real) (hcorruption : 0 <= corruption) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= (1 + Real.log (((horizon + 1 : Nat) : Real))) * (1 + 25 * (arms.erase best).sum (fun action => 1 / gap action)) + corruption