BanditRLProof.TsallisScheduledAllRateExpectedStability

Comparing the old objective at its minimizer with the updated minimizer reduces conjugate-potential stability to a difference of linear losses.

theorem halfTsallisPotentialStability_le_linearLoss_sub_of_minimizers {Action : Type u} (arms : Finset Action) (eta : Real) (score probability estimate next : Action -> Real) (heta : 0 < eta) (hprobabilityMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score probability) (hnextMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun action => score action + estimate action) next) : halfTsallisPotentialStability arms eta score probability estimate next <= FTRL.linearLoss arms probability estimate - FTRL.linearLoss arms next estimate

An ordinary importance-weighted minimizer step is at most one, with no upper bound on the positive learning rate.

theorem halfTsallisPotentialStability_importanceWeightedLoss_le_one_of_minimizers {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score probability loss next : Action -> Real) (chosen : Action) (hchosen : chosen ∈ arms) (heta : 0 < eta) (hprobabilityMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score probability) (hnextMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun action => score action + Exp3.importanceWeightedLoss probability loss chosen action) next) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) : halfTsallisPotentialStability arms eta score probability (Exp3.importanceWeightedLoss probability loss chosen) next <= 1

Averaging the arbitrary-rate pointwise bound under the current simplex keeps the coarse one-round budget equal to one.

theorem sum_prob_mul_halfTsallisPotentialStability_importanceWeightedLoss_le_one_of_minimizers {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (score probability loss : Action -> Real) (next : Action -> Action -> Real) (heta : 0 < eta) (hprobabilityMin : FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) score probability) (hnextMin : forall chosen, chosen ∈ arms -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun action => score action + Exp3.importanceWeightedLoss probability loss chosen action) (next chosen)) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) : arms.sum (fun chosen => probability chosen * halfTsallisPotentialStability arms eta score probability (Exp3.importanceWeightedLoss probability loss chosen) (next chosen)) <= 1

The finite-action product-law score is integrable for every positive rate. The absolute-value argument uses nonnegativity of true minimizer steps and the coarse averaged bound, so no probability floor or upper rate bound appears.

theorem integrable_importanceWeightedPotentialStabilityScore_finiteActionKernel_coarse {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (eta : Real) (score prob loss : History -> Action -> Real) (next : History -> Action -> Action -> Real) (source : Exp3.MeasurableFiniteActionDistribution arms prob) (heta : 0 < eta) (hprobMin : forall history, FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (score history) (prob history)) (hnextMin : forall history chosen, chosen ∈ arms -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun candidate => score history candidate + Exp3.importanceWeightedLoss (prob history) (loss history) chosen candidate) (next history chosen)) (hloss : forall history action, action ∈ arms -> 0 <= loss history action ∧ loss history action <= 1) (hscore : Measurable (importanceWeightedPotentialStabilityScore arms eta score prob loss next)) : Integrable (importanceWeightedPotentialStabilityScore arms eta score prob loss next) (historyMu ⊗ₘ Exp3.finiteActionKernel arms prob source)

An identified finite conditional action law transports the arbitrary-rate ordinary-IW bound to a one-round integral inequality with constant budget.

theorem integral_importanceWeightedPotentialStabilityScore_le_integral_one_of_condDistrib_of_minimizers {Omega : Type u} {History : Type v} {Action : Type w} [MeasurableSpace Omega] [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (mu : Measure Omega) [IsFiniteMeasure mu] (history : Omega -> History) (hhistory : Measurable history) (action : Omega -> Action) (haction : Measurable action) (arms : Finset Action) (eta : Real) (score prob loss : History -> Action -> Real) (next : History -> Action -> Action -> Real) (policy : Kernel History Action) [IsMarkovKernel policy] (hpolicy : policy =ᵐ[mu.map history] fun h => Exp3.finiteActionMeasure arms (prob h)) (hcond : condDistrib action history mu =ᵐ[mu.map history] policy) (heta : 0 < eta) (hprobMin : forall h, FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (score h) (prob h)) (hnextMin : forall h chosen, chosen ∈ arms -> FTRL.IsRegularizedMinimizer (FTRL.finiteSimplex arms) arms eta (negEntropyRegularizer arms (1 / 2 : Real)) (fun candidate => score h candidate + Exp3.importanceWeightedLoss (prob h) (loss h) chosen candidate) (next h chosen)) (hloss : forall h candidate, candidate ∈ arms -> 0 <= loss h candidate ∧ loss h candidate <= 1) (hscore : Measurable (importanceWeightedPotentialStabilityScore arms eta score prob loss next)) (hIntegrable : Integrable (importanceWeightedPotentialStabilityScore arms eta score prob loss next) (mu.map history ⊗ₘ policy)) : integral mu (fun omega => importanceWeightedPotentialStabilityScore arms eta score prob loss next (history omega, action omega)) <= integral (mu.map history) (fun _ => (1 : Real))

A generated scheduled successor term is integrable and has coarse expected budget one at every positive local rate.

theorem integral_sampledScheduledHalfTsallisSuccessorPotentialStabilityAtTime_le_one {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (heta : 0 < eta (n + 1)) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample (n + 1)) mu ∧ integral mu (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample (n + 1)) <= integral mu (fun _sample => (1 : Real))

One generated successor round exposes the refined budget directly, rather than only through a sum whose rates are all assumed small.

theorem integral_sampledScheduledHalfTsallisSuccessorPotentialStabilityAtTime_le_refined {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (heta : 0 < eta (n + 1)) (heta_le : eta (n + 1) <= 1 / 2) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample (n + 1)) mu ∧ Integrable (fun sample => sampledScheduledHalfTsallisRefinedPotentialStabilityBoundAt (Env

The generated scheduled time-zero term has the same arbitrary-rate coarse budget as successor terms.

theorem integral_sampledScheduledHalfTsallisInitialPotentialStabilityAtTime_le_one {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (heta : 0 < eta 0) (loss : Exp3.PredictableLossVector Env Action) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample 0) mu ∧ integral mu (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample 0) <= integral mu (fun _sample => (1 : Real))

Piecewise successor budget: use the refined expression at small local rates and the coarse constant otherwise.

noncomputable def sampledScheduledHalfTsallisSuccessorAllRatePotentialStabilityBoundAt {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (n : Nat) (input : Env × History.FinitePairHistory Action Real n) : Real

Piecewise initial budget with the same local-rate threshold.

noncomputable def sampledScheduledHalfTsallisInitialAllRatePotentialStabilityBound {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (env : Env) : Real

Piecewise budget indexed by the actual scheduled time.

noncomputable def sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (sample : Env × ((k : Nat) -> Action × Real)) : Nat -> Real | 0 => sampledScheduledHalfTsallisInitialAllRatePotentialStabilityBound arms harms eta sample.1 | n + 1 => sampledScheduledHalfTsallisSuccessorAllRatePotentialStabilityBoundAt arms harms eta n (sampledScheduledHalfTsallisHistoryAt n sample) /-- A successor term and its piecewise all-rate budget are integrable, and the expected term is bounded by that budget. -/ theorem integral_sampledScheduledHalfTsallisSuccessorPotentialStabilityAtTime_le_allRateBound {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (heta : 0 < eta (n + 1)) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample (n + 1)) mu ∧ Integrable (fun sample => sampledScheduledHalfTsallisSuccessorAllRatePotentialStabilityBoundAt arms harms eta n (sampledScheduledHalfTsallisHistoryAt n sample)) mu ∧ integral mu (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample (n + 1)) <= integral mu (fun sample => sampledScheduledHalfTsallisSuccessorAllRatePotentialStabilityBoundAt arms harms eta n (sampledScheduledHalfTsallisHistoryAt n sample))

A successor term and its piecewise all-rate budget are integrable, and the expected term is bounded by that budget.

theorem integral_sampledScheduledHalfTsallisSuccessorPotentialStabilityAtTime_le_allRateBound {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (heta : 0 < eta (n + 1)) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample (n + 1)) mu ∧ Integrable (fun sample => sampledScheduledHalfTsallisSuccessorAllRatePotentialStabilityBoundAt arms harms eta n (sampledScheduledHalfTsallisHistoryAt n sample)) mu ∧ integral mu (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample (n + 1)) <= integral mu (fun sample => sampledScheduledHalfTsallisSuccessorAllRatePotentialStabilityBoundAt arms harms eta n (sampledScheduledHalfTsallisHistoryAt n sample))

The initial term and its piecewise all-rate budget satisfy the analogous integrability and expectation contract.

theorem integral_sampledScheduledHalfTsallisInitialPotentialStabilityAtTime_le_allRateBound {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (heta : 0 < eta 0) (loss : Exp3.PredictableLossVector Env Action) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample 0) mu ∧ Integrable (fun sample => sampledScheduledHalfTsallisInitialAllRatePotentialStabilityBound arms harms eta sample.1) mu ∧ integral mu (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample 0) <= integral mu (fun sample => sampledScheduledHalfTsallisInitialAllRatePotentialStabilityBound arms harms eta sample.1)

Every actual scheduled time has an integrable stability term and an integrable piecewise all-rate budget, with the corresponding expectation inequality.

theorem integral_sampledScheduledHalfTsallisPotentialStabilityAtTime_le_allRateBound {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (t : Nat) (heta : 0 < eta t) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample t) mu ∧ Integrable (fun sample => sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime arms harms eta sample t) mu ∧ integral mu (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample t) <= integral mu (fun sample => sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime arms harms eta sample t)

Under positivity of every included local rate, both the exact full scheduled stability sum and its piecewise all-rate budget are integrable.

theorem integrable_sum_sampledScheduledHalfTsallisPotentialStabilityAtTime_allRate {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (horizon : Nat) (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (heta : forall t, t <= horizon -> 0 < eta t) (loss : Exp3.PredictableLossVector Env Action) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (fun sample => (Finset.range (horizon + 1)).sum (fun t => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample t)) mu ∧ Integrable (fun sample => (Finset.range (horizon + 1)).sum (fun t => sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime arms harms eta sample t)) mu

Under positivity of every included local rate, both the exact full scheduled stability sum and its piecewise all-rate budget are integrable. -/ theorem integrable_sum_sampledScheduledHalfTsallisPotentialStabilityAtTime_allRate {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (horizon : Nat) (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (heta : forall t, t <= horizon -> 0 < eta t) (loss : Exp3.PredictableLossVector Env Action) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment Integrable (fun sample => (Finset.range (horizon + 1)).sum (fun t => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample t)) mu ∧ Integrable (fun sample => (Finset.range (horizon + 1)).sum (fun t => sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime arms harms eta sample t)) mu := by dsimp only let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment have hround (t : Nat) (ht : t ∈ Finset.range (horizon + 1)) := integral_sampledScheduledHalfTsallisPotentialStabilityAtTime_le_allRateBound prior arms harms eta loss t (heta t (by have ht' := Finset.mem_range.mp ht omega)) dsimp only at hround exact ⟨ IntegrabilitySums.integrable_finset_sum mu (Finset.range (horizon + 1)) (fun t sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample t) (fun t ht => (hround t ht).1), IntegrabilitySums.integrable_finset_sum mu (Finset.range (horizon + 1)) (fun t sample => sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime arms harms eta sample t) (fun t ht => (hround t ht).2.1)⟩ /-! Full all-rate expected scheduled stability. Each actual time independently uses the refined budget when `eta t <= 1 / 2`, and otherwise uses the coarse constant one. Unlike the refined-only predecessor, this theorem imposes no uniform upper bound on the included positive rates.

theorem integral_sum_sampledScheduledHalfTsallisPotentialStabilityAtTime_le_allRateBound {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsFiniteMeasure prior] (horizon : Nat) (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (heta : forall t, t <= horizon -> 0 < eta t) (loss : Exp3.PredictableLossVector Env Action) : 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 => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample t)) <= integral mu (fun sample => (Finset.range (horizon + 1)).sum (fun t => sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime arms harms eta sample t))