Lean module · Tsallis-FTRL
BanditRLProof.TsallisScheduledReferenceGapExpectedDeviationSelfBounding
# Expected-deviation self-bounding for predictable perturbations This variant retains the scheduled action probability inside the corruption allowance. A sample-dependent predictable deviation therefore contributes its actual probability-weighted expectation instead of a deterministic pointwise envelope.
Module map
Imports
BanditRLProof.TsallisScheduledReferenceGapSelfBounding
Imported by
BanditRLProof.TsallisFiniteArmIIDHistoryAdaptiveExpectedCorruptedRewardLaw
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_of_expectedDeviation
Compiled
A reference expected-gap law plus an integrable sample-dependent predictable perturbation yields a self-bound with the exact expected weighted deviation allowance.
theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_hasSelfBounding_of_referenceExpectedGapLaw_of_expectedDeviation {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 -> (Env × ((k : Nat) -> Action × Real)) -> Action -> Real) (horizon : Nat) (hreferenceGapLaw : HasScheduledExpectedGapLaw mu arms harms eta referenceLoss best baseGap horizon) (hdeviation_integrable : forall t, t <= horizon -> forall action, action ∈ arms.erase best -> Integrable (fun sample => sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample action * deviation t sample action) mu) (hdeviation : forall t, t <= horizon -> forall 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 sample action) : (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => baseGap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)) - (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => integral mu (fun sample => sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample action * deviation t sample action))) <= integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta actualLoss (pointMass best) horizon)