BanditRLProof.TsallisScheduledSuboptimalExpectedBound

Expected probability of one action under an arbitrary trajectory law.

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

No declaration docstring is present; use the chapter context and exact statement below.

theorem integrable_sampledScheduledHalfTsallisProbabilityAtTime {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) (t : Nat) (action : Action) (haction : action ∈ arms) : Integrable (fun sample => sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample action) mu

No declaration docstring is present; use the chapter context and exact statement below.

theorem integrable_sqrt_sampledScheduledHalfTsallisProbabilityAtTime {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) (t : Nat) (action : Action) (haction : action ∈ arms) : Integrable (fun sample => Real.sqrt (sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample action)) mu

Integrating a generated finite-simplex law under a probability measure again gives a finite-simplex law.

theorem finiteSimplex_sampledScheduledHalfTsallisExpectedProbabilityAt {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) (t : Nat) : FTRL.finiteSimplex arms (sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t)

Jensen transport for one scheduled action coordinate.

theorem integral_sqrt_sampledScheduledHalfTsallisProbabilityAtTime_le_sqrt_expected {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) (t : Nat) (action : Action) (haction : action ∈ arms) : integral mu (fun sample => Real.sqrt (sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample action)) <= Real.sqrt (sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)

On the small-rate branch, the all-rate actual-time budget is the refined half-power budget of the actual scheduled probability.

theorem sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime_eq_refined {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (sample : Env × ((k : Nat) -> Action × Real)) (t : Nat) (heta_le : eta t <= 1 / 2) : sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime arms harms eta sample t = refinedPotentialStabilityBound arms (eta t) (fun sample action => sampledScheduledHalfTsallisProbabilityAtTime arms harms eta t sample action) sample

One integrated small-rate budget is bounded by suboptimal-arm square roots of expected scheduled probabilities.

theorem integral_sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime_le_suboptimalExpectedSqrt {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) (t : Nat) (heta : 0 < eta t) (heta_le : eta t <= 1 / 2) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment integral mu (fun sample => sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime arms harms eta sample t) <= 2 * eta t * (arms.erase best).sum (fun action => Real.sqrt (sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)) + 2 * (eta t) ^ 2

The complete integrated all-rate budget, on its small-rate branch, is bounded by a deterministic time/suboptimal-arm sum of square roots of expected scheduled probabilities.

theorem integral_sum_sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime_le_suboptimalExpectedSqrt {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] (horizon : Nat) (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (heta : forall t, t <= horizon -> 0 < eta t) (heta_le : forall t, t <= horizon -> eta t <= 1 / 2) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment integral mu (fun sample => (Finset.range (horizon + 1)).sum (fun t => sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime arms harms eta sample t)) <= (Finset.range (horizon + 1)).sum (fun t => 2 * eta t * (arms.erase best).sum (fun action => Real.sqrt (sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)) + 2 * (eta t) ^ 2)

Generated scheduled predictable environment regret against the best-arm point mass has the deterministic suboptimal-arm upper needed by the self-bounding completion-of-squares step.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_suboptimalExpectedSqrt {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 * (arms.erase best).sum (fun action => Real.sqrt (sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)) + 2 * (eta t) ^ 2) + halfTsallisPotentialMass arms (initialHalfTsallisDistribution arms harms (eta 0)) / eta horizon - 1 / eta horizon

The generated scheduled upper bound feeds the abstract self-bounding completion-of-squares theorem without any remaining pathwise or Jensen obligation.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_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) (hgap : forall action, action ∈ arms.erase best -> 0 < gap action) (corruption : Real) (hselfBounding : (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => gap action * sampledScheduledHalfTsallisExpectedProbabilityAt (prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta (canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss).finiteHistory loss.environment) arms harms eta t action)) - corruption <= integral (prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta (canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss).finiteHistory loss.environment) (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) + (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