BanditRLProof.TsallisScheduledFixedGapSelfBounding

Pathwise suboptimal-arm gap mass of the scheduled generated laws.

noncomputable def sampledScheduledHalfTsallisPredictableSuboptimalGapMass {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (best : Action) (gap : Action -> Real) (horizon : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

An exact predictable fixed-gap law identifies scheduled environment regret against the best-arm point mass with suboptimal-arm gap mass pathwise.

theorem sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_eq_suboptimalGapMass {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) (gap : Action -> Real) (horizon : Nat) (hgapLaw : ∀ t sample action, action ∈ arms -> Exp3.predictableLossAt loss t sample action - Exp3.predictableLossAt loss t sample best = gap action) (sample : Env × ((k : Nat) -> Action × Real)) : sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon sample = sampledScheduledHalfTsallisPredictableSuboptimalGapMass arms harms eta best gap horizon sample

Integrating scheduled pathwise suboptimal gap mass gives the deterministic time-by-arm sum of gaps times expected scheduled action probabilities.

theorem integral_sampledScheduledHalfTsallisPredictableSuboptimalGapMass_eq {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) (best : Action) (gap : Action -> Real) (horizon : Nat) : integral mu (sampledScheduledHalfTsallisPredictableSuboptimalGapMass arms harms eta best gap horizon) = (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action))

The exact predictable fixed-gap law identifies the integrated scheduled environment regret with the expected suboptimal-arm gap mass.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_eq_suboptimalExpectedGapMass {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (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 : ∀ t sample action, action ∈ arms -> Exp3.predictableLossAt loss t sample action - Exp3.predictableLossAt loss t sample best = gap action) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment 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))

Any nonnegative corruption allowance turns the exact fixed-gap identity into the explicit self-bounding inequality required by completion of squares.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_hasSelfBounding_of_fixedGap {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (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 : ∀ t sample action, action ∈ arms -> Exp3.predictableLossAt loss t sample action - Exp3.predictableLossAt loss t sample best = gap action) (corruption : Real) (hcorruption : 0 <= corruption) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment (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)

The generated scheduled regret bound with an explicit self-bounding premise becomes automatic under an exact predictable fixed-gap law.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_of_fixedGap {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon : Nat) (heta : forall t, t <= horizon -> 0 < eta t) (heta_le : forall t, t <= horizon -> eta t <= 1 / 2) (hetaMono : forall t, t < horizon -> eta (t + 1) <= eta t) (gap : Action -> Real) (hgapPos : forall action, action ∈ arms.erase best -> 0 < gap action) (hgapLaw : ∀ t sample action, action ∈ arms -> Exp3.predictableLossAt loss t sample action - Exp3.predictableLossAt loss t sample best = gap action) (corruption : Real) (hcorruption : 0 <= corruption) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon) <= 2 * ((Finset.range (horizon + 1)).sum (fun t => 2 * (eta t) ^ 2) + (halfTsallisPotentialMass arms (initialHalfTsallisDistribution arms harms (eta 0)) / eta horizon - 1 / eta horizon)) + ((Finset.range (horizon + 1)).product (arms.erase best)).sum (fun index => (2 * eta index.1) ^ 2 / gap index.2) + corruption