BanditRLProof.TsallisScheduledRefinedStabilityPenalty

Sum of square roots of expected probabilities over suboptimal arms.

noncomputable def sampledScheduledHalfTsallisExpectedSuboptimalSqrtMassAt {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) (best : Action) (t : Nat) : Real

Dropping the nonpositive linear correction weakens the expected refined mass to the square-root mass used by completion of squares.

theorem sampledScheduledHalfTsallisExpectedRefinedSuboptimalMassAt_le_sqrtMass {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} (t : Nat) : sampledScheduledHalfTsallisExpectedRefinedSuboptimalMassAt mu arms harms eta best t <= sampledScheduledHalfTsallisExpectedSuboptimalSqrtMassAt mu arms harms eta best t

Combined coefficient multiplying `sqrt (E[p_t(a)])` after adding refined stability and reciprocal-rate penalty terms.

noncomputable def sampledScheduledHalfTsallisRefinedCoefficient (eta : Nat -> Real) : Nat -> Real | 0 => 2 * eta 0 + 2 / eta 0 | t + 1 => 2 * eta (t + 1) + 2 * (1 / eta (t + 1) - 1 / eta t) /-- Generated predictable environment regret is bounded by the deterministic quadratic-rate budget plus one refined square-root mass per actual time. -/ theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_refinedStabilityPenalty {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) : 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 => 2 * (eta t) ^ 2) + (Finset.range (horizon + 1)).sum (fun t => sampledScheduledHalfTsallisRefinedCoefficient eta t * sampledScheduledHalfTsallisExpectedSuboptimalSqrtMassAt mu arms harms eta best t)

Generated predictable environment regret is bounded by the deterministic quadratic-rate budget plus one refined square-root mass per actual time.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_refinedStabilityPenalty {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) : 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 => 2 * (eta t) ^ 2) + (Finset.range (horizon + 1)).sum (fun t => sampledScheduledHalfTsallisRefinedCoefficient eta t * sampledScheduledHalfTsallisExpectedSuboptimalSqrtMassAt mu arms harms eta best t)

The combined refined scheduled upper bound consumes any matching expected self-bounding law and yields a squared-coefficient-over-gap theorem.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_refinedStabilityPenalty_of_selfBounding {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) (corruption : Real) (hselfBounding : 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)) : 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) + ((Finset.range (horizon + 1)).product (arms.erase best)).sum (fun index => (sampledScheduledHalfTsallisRefinedCoefficient eta index.1) ^ 2 / gap index.2) + corruption

Under an exact predictable fixed-gap law, the combined refined scheduled upper bound automatically yields a squared-coefficient-over-gap theorem.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_refinedStabilityPenalty_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) + ((Finset.range (horizon + 1)).product (arms.erase best)).sum (fun index => (sampledScheduledHalfTsallisRefinedCoefficient eta index.1) ^ 2 / gap index.2) + corruption

A coordinatewise expected-gap law supplies the refined scheduled squared-coefficient-over-gap theorem without a samplewise fixed-gap premise.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_refinedStabilityPenalty_of_expectedGapLaw {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 : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment HasScheduledExpectedGapLaw mu arms harms eta loss best gap horizon) (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) + ((Finset.range (horizon + 1)).product (arms.erase best)).sum (fun index => (sampledScheduledHalfTsallisRefinedCoefficient eta index.1) ^ 2 / gap index.2) + corruption