Lean module · Tsallis-FTRL
BanditRLProof.TsallisScheduledExpectedGapSelfBounding
# Expected-gap self-bounding for scheduled half-Tsallis FTRL This module replaces the samplewise fixed-gap premise by the stochastic first-moment law actually needed by self-bounding. For every time and suboptimal arm, the probability-weighted predictable loss difference has expectation `gap action * E[p_t(action)]`.
Module map
Imports
BanditRLProof.TsallisScheduledFixedGapSelfBounding
Imported by
BanditRLProof, BanditRLProof.TsallisScheduledConditionalMeanGap, BanditRLProof.TsallisScheduledRefinedStabilityPenalty
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.HasScheduledExpectedGapLaw
Compiled
The per-time, per-suboptimal-arm first-moment law needed by stochastic self-bounding. It is deliberately finer than the final summed regret law so that later conditional-expectation producers can discharge it one coordinate at a time.
def HasScheduledExpectedGapLaw {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (best : Action) (gap : Action -> Real) (horizon : Nat) : Prop
theorem
BanditRLProof.Tsallis.integrable_sampledScheduledHalfTsallisProbability_mul_predictableLossDiffAt
Compiled
One probability-weighted predictable loss difference is integrable.
theorem integrable_sampledScheduledHalfTsallisProbability_mul_predictableLossDiffAt {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) (loss : Exp3.PredictableLossVector Env Action) (best action : Action) (haction : action ∈ arms) (t : Nat) : Integrable (fun sample => sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample action * (Exp3.predictableLossAt loss t sample action - Exp3.predictableLossAt loss t sample best)) mu
theorem
BanditRLProof.Tsallis.sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_eq_weightedLossGapMass
Compiled
Pathwise scheduled regret against a best-arm point mass is the finite sum of probability-weighted predictable loss differences over suboptimal arms.
theorem sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_eq_weightedLossGapMass {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon sample = (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample action * (Exp3.predictableLossAt loss t sample action - Exp3.predictableLossAt loss t sample best)))
theorem
BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_eq_suboptimalExpectedGapMass_of_expectedGapLaw
Compiled
A coordinatewise expected-gap law identifies integrated scheduled regret with the expected suboptimal-arm gap mass.
theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_eq_suboptimalExpectedGapMass_of_expectedGapLaw {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} (hbest : best ∈ arms) (gap : Action -> Real) (horizon : Nat) (hgapLaw : HasScheduledExpectedGapLaw mu arms harms eta loss best gap horizon) : integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon) = (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action))
theorem
BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_hasSelfBounding_of_expectedGapLaw
Compiled
A nonnegative corruption allowance turns the expected-gap identity into the self-bounding premise consumed by completion of squares.
theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_hasSelfBounding_of_expectedGapLaw {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} (hbest : best ∈ arms) (gap : Action -> Real) (horizon : Nat) (hgapLaw : HasScheduledExpectedGapLaw mu arms harms eta loss best gap horizon) (corruption : Real) (hcorruption : 0 <= corruption) : (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)) - corruption <= integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon)