BanditRLProof.TsallisScheduledAllTimesExpectedStability

One actual scheduled successor potential term is integrable under the canonical generated trajectory.

theorem integrable_sampledScheduledHalfTsallisSuccessorPotentialStabilityAtTime {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

The complete scheduled successor stability sum is integrable.

theorem integrable_sum_sampledScheduledHalfTsallisSuccessorPotentialStabilityAtTime {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 n, n < horizon -> 0 < eta (n + 1)) (heta_le : forall n, n < horizon -> eta (n + 1) <= 1 / 2) (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).sum (fun n => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample (n + 1))) mu

The full scheduled stability sum from time zero through `horizon` is integrable under the canonical generated trajectory.

theorem integrable_sum_sampledScheduledHalfTsallisPotentialStabilityAtTime {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) (heta_le : forall t, t <= horizon -> eta t <= 1 / 2) (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

The full scheduled stability sum from time zero through `horizon` is integrable under the canonical generated trajectory. -/ theorem integrable_sum_sampledScheduledHalfTsallisPotentialStabilityAtTime {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) (heta_le : forall t, t <= horizon -> eta t <= 1 / 2) (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 := by dsimp only let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment have hinitial := integral_sampledScheduledHalfTsallisInitialPotentialStabilityAtTime_le_refined prior arms harms eta (heta 0 (Nat.zero_le horizon)) (heta_le 0 (Nat.zero_le horizon)) loss dsimp only at hinitial have hsuccessor := integrable_sum_sampledScheduledHalfTsallisSuccessorPotentialStabilityAtTime prior horizon arms harms eta (fun n hn => heta (n + 1) (Nat.succ_le_iff.mpr hn)) (fun n hn => heta_le (n + 1) (Nat.succ_le_iff.mpr hn)) loss dsimp only at hsuccessor have hadd := hinitial.1.add hsuccessor simpa [Finset.sum_range_succ', add_comm] using hadd /-! Expected refined stability for every actual time from zero through `horizon`. The left side is exactly the stability sum in `sampledScheduledHalfTsallisEstimatedRegret_eq_stability_add_penalty`.

theorem integral_sum_sampledScheduledHalfTsallisPotentialStabilityAtTime_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] (horizon : Nat) (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (heta : forall t, t <= horizon -> 0 < eta t) (heta_le : forall t, t <= horizon -> eta t <= 1 / 2) (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 => sampledScheduledHalfTsallisInitialRefinedPotentialStabilityBound (Env