BanditRLProof.TsallisScheduledTimeVaryingExpectedGap

Per-time first-moment law for probability-weighted predictable loss gaps.

def HasScheduledTimeVaryingExpectedGapLaw {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 : Nat -> Action -> Real) (horizon : Nat) : Prop

Per-time conditional mean law relative to the information available before the scheduled action.

def HasScheduledTimeVaryingConditionalMeanGapLaw {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 : Nat -> Action -> Real) (horizon : Nat) : Prop

Per-time independence and global-mean law for predictable loss gaps.

def HasScheduledTimeVaryingIndependentMeanGapLaw {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 : Nat -> Action -> Real) (horizon : Nat) : Prop

Independence from the scheduled past identifies each time-varying conditional mean.

theorem hasScheduledTimeVaryingConditionalMeanGapLaw_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 : Nat -> Action -> Real) (horizon : Nat) (hgap : HasScheduledTimeVaryingIndependentMeanGapLaw mu arms loss best gap horizon) : HasScheduledTimeVaryingConditionalMeanGapLaw mu arms loss best gap horizon

A time-varying conditional mean law yields the corresponding weighted expected-gap law by pulling the scheduled probability through `condExp`.

theorem hasScheduledTimeVaryingExpectedGapLaw_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 : Nat -> Action -> Real) (horizon : Nat) (hgap : HasScheduledTimeVaryingConditionalMeanGapLaw mu arms loss best gap horizon) : HasScheduledTimeVaryingExpectedGapLaw mu arms harms eta loss best gap horizon

The independent time-varying mean contract directly feeds the weighted expected-gap law.

theorem hasScheduledTimeVaryingExpectedGapLaw_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 : Nat -> Action -> Real) (horizon : Nat) (hgap : HasScheduledTimeVaryingIndependentMeanGapLaw mu arms loss best gap horizon) : HasScheduledTimeVaryingExpectedGapLaw mu arms harms eta loss best gap horizon

A time-varying expected-gap law identifies integrated regret with the time-by-arm actual gap mass.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_eq_suboptimalTimeVaryingExpectedGapMass {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 : Nat -> Action -> Real) (horizon : Nat) (hgapLaw : HasScheduledTimeVaryingExpectedGapLaw 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 t action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action))

Accumulated coordinatewise deviation from fixed baseline gaps.

noncomputable def scheduledTimeVaryingGapDeviationBudget {Action : Type*} [DecidableEq Action] (arms : Finset Action) (best : Action) (horizon : Nat) (deviation : Nat -> Action -> Real) : Real

A time-varying actual-gap law within a known coordinatewise distance of fixed baseline gaps yields the self-bound consumed by schedule tuning.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_hasSelfBounding_of_timeVaryingPerturbedExpectedGapLaw {Env Action : Type*} [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) (horizon : Nat) (baseGap : Action -> Real) (actualGap deviation : Nat -> Action -> Real) (hactualGapLaw : HasScheduledTimeVaryingExpectedGapLaw mu arms harms eta loss best actualGap horizon) (hdeviation : ∀ t, t <= horizon -> ∀ action, action ∈ arms.erase best -> |actualGap t action - baseGap action| <= 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 loss (pointMass best) horizon)