Lean module · Tsallis-FTRL
BanditRLProof.TsallisScheduledReferenceGapSelfBounding
# Reference-gap self-bounding for predictable perturbations The action probabilities and regret are generated by `actualLoss`, while a second predictable loss vector on the same trajectory supplies the stochastic baseline gap law. A pointwise bound between the two loss differences then converts the reference expected-gap law into a self-bound for the actual regret. This is the generic bridge needed by history-adaptive corruption.
Module map
Imports
BanditRLProof.TsallisScheduledTimeVaryingExpectedGap
Imported by
BanditRLProof.TsallisFiniteArmIIDHistoryAdaptiveCorruptedRewardLaw, BanditRLProof.TsallisScheduledReferenceGapExpectedDeviationSelfBounding
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_hasSelfBounding_of_referenceExpectedGapLaw
Compiled
A reference expected-gap law plus a pointwise predictable perturbation bound yields the fixed-baseline self-bound for the actual generated regret.
theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_hasSelfBounding_of_referenceExpectedGapLaw {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) (actualLoss referenceLoss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (baseGap : Action -> Real) (deviation : Nat -> Action -> Real) (horizon : Nat) (hreferenceGapLaw : HasScheduledExpectedGapLaw mu arms harms eta referenceLoss best baseGap horizon) (hdeviation : ∀ t, t <= horizon -> ∀ sample action, action ∈ arms.erase best -> |(Exp3.predictableLossAt actualLoss t sample action - Exp3.predictableLossAt actualLoss t sample best) - (Exp3.predictableLossAt referenceLoss t sample action - Exp3.predictableLossAt referenceLoss t sample best)| <= deviation t action) : (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => baseGap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)) - scheduledTimeVaryingGapDeviationBudget arms best horizon deviation <= integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta actualLoss (pointMass best) horizon)