Lean module · Tsallis-FTRL
BanditRLProof.TsallisScheduledConditionalMeanGap
# Conditional-mean producer for scheduled half-Tsallis expected gaps This module exposes the sampling-before-action sigma-algebra at each scheduled time. The scheduled action probability is measurable with respect to that sigma-algebra, so Mathlib's conditional-expectation pull-out theorem turns a constant conditional loss-gap law into `HasScheduledExpectedGapLaw`.
Module map
Imports
BanditRLProof.TsallisScheduledExpectedGapSelfBounding
Imported by
BanditRLProof, BanditRLProof.TsallisScheduledIndependentMeanGap, BanditRLProof.TsallisScheduledTimeVaryingExpectedGap
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.sampledScheduledHalfTsallisPastSigma
Compiled
Information in the generated action/reward trace strictly before the scheduled action at time `t`. At time zero there is no trace information; at time `n + 1` this is the sigma-algebra generated by the prefix through `n`.
@[reducible] def sampledScheduledHalfTsallisPastSigma {Env : Type u} {Action : Type v} [MeasurableSpace Action] (t : Nat) : MeasurableSpace (Env × ((k : Nat) -> Action × Real))
theorem
BanditRLProof.Tsallis.sampledScheduledHalfTsallisPastSigma_le
Compiled
The scheduled past sigma-algebra is a sub-sigma-algebra of the ambient trajectory sigma-algebra.
theorem sampledScheduledHalfTsallisPastSigma_le {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (t : Nat) : sampledScheduledHalfTsallisPastSigma (Env
theorem
BanditRLProof.Tsallis.measurable_sampledScheduledHalfTsallisProbabilityAtTime_pastSigma
Compiled
Every scheduled action-probability coordinate is measurable using only the trace prefix available before that action is sampled.
theorem measurable_sampledScheduledHalfTsallisProbabilityAtTime_pastSigma {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (t : Nat) (candidate : Action) (hcandidate : candidate ∈ arms) : @Measurable (Env × ((k : Nat) -> Action × Real)) Real (sampledScheduledHalfTsallisPastSigma (Env
def
BanditRLProof.Tsallis.HasScheduledConditionalMeanGapLaw
Compiled
Coordinatewise conditional-mean gap law relative to the information available before the scheduled action at each time.
def HasScheduledConditionalMeanGapLaw {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.hasScheduledExpectedGapLaw_of_conditionalMeanGapLaw
Compiled
A constant conditional loss-gap law implies the expected-gap law consumed by scheduled stochastic self-bounding. The proof uses only Mathlib's pull-out property and preservation of the integral by conditional expectation.
theorem hasScheduledExpectedGapLaw_of_conditionalMeanGapLaw {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 : HasScheduledConditionalMeanGapLaw mu arms loss best gap horizon) : HasScheduledExpectedGapLaw mu arms harms eta loss best gap horizon