BanditRLProof.TsallisScheduledExpectedStability

Visible environment/pair-history state before scheduled action `n + 1`.

def sampledScheduledHalfTsallisHistoryAt {Env : Type u} {Action : Type v} (n : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Env × History.FinitePairHistory Action Real n

Scheduled successor action after the visible prefix through `n`.

def sampledScheduledHalfTsallisActionAt {Env : Type u} {Action : Type v} (n : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Action

Scheduled recursive score on an environment/prefix state.

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

Predictable successor loss on a scheduled environment/prefix state.

def sampledScheduledHalfTsallisPredictableLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : Env × History.FinitePairHistory Action Real n -> Action -> Real

Scheduled successor probability on an environment/prefix state.

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

Same-rate canonical update after sampling scheduled action `n + 1`.

noncomputable def sampledScheduledHalfTsallisUpdatedAt {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) (n : Nat) : Env × History.FinitePairHistory Action Real n -> Action -> Action -> Real

Environment-lifted measurable scheduled probability source.

noncomputable def sampledScheduledHalfTsallisEnvironmentHistoryDistributionSource {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) (n : Nat) : Exp3.MeasurableFiniteActionDistribution arms (sampledScheduledHalfTsallisProbabilityAt (Env

The scheduled policy comapped to the environment/prefix state.

noncomputable def sampledScheduledHalfTsallisPolicyAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) (n : Nat) : Kernel (Env × History.FinitePairHistory Action Real n) Action

The environment-lifted scheduled policy is the corresponding finite action kernel.

theorem sampledScheduledHalfTsallisPolicyAt_eq_finiteActionKernel {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) (n : Nat) : sampledScheduledHalfTsallisPolicyAt (Env

Coordinate regularity for the scheduled current and same-rate updated selectors.

structure HalfTsallisScheduleGeneratedSelectorMeasurability {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) : Prop where

Every supported coordinate of the scheduled same-rate update is measurable.

theorem measurable_sampledScheduledHalfTsallisUpdatedAt_canonical {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (candidate : Action) (hcandidate : candidate ∈ arms) : Measurable (fun sample : (Env × History.FinitePairHistory Action Real n) × Action => sampledScheduledHalfTsallisUpdatedAt arms harms eta loss n sample.1 sample.2 candidate)

The canonical scheduled selector satisfies current and updated coordinate measurability at every successor round.

noncomputable def canonicalHalfTsallisScheduleGeneratedSelectorMeasurability {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) : HalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss where

Scheduled one-round conjugate-potential score on a visible prefix and sampled successor action.

noncomputable def sampledScheduledHalfTsallisHistoryActionPotentialStabilityAt {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) (n : Nat) : (Env × History.FinitePairHistory Action Real n) × Action -> Real

Refined one-round budget for scheduled successor action `n + 1`.

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

The canonical scheduled successor potential score is measurable.

theorem measurable_sampledScheduledHalfTsallisHistoryActionPotentialStabilityAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : Measurable (sampledScheduledHalfTsallisHistoryActionPotentialStabilityAt arms harms eta loss n)

The scheduled refined budget is automatically integrable under any finite visible-history law when its local rate is positive.

theorem integrable_sampledScheduledHalfTsallisRefinedPotentialStabilityBoundAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (n : Nat) (historyMu : Measure (Env × History.FinitePairHistory Action Real n)) [IsFiniteMeasure historyMu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (heta : 0 < eta (n + 1)) (selector : HalfTsallisScheduleFiniteHistorySelectorMeasurability arms harms eta) : Integrable (sampledScheduledHalfTsallisRefinedPotentialStabilityBoundAt (Env

The canonical scheduled successor potential score is automatically integrable under its visible-history/action product law.

theorem integrable_sampledScheduledHalfTsallisHistoryActionPotentialStabilityAt {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 (sampledScheduledHalfTsallisHistoryActionPotentialStabilityAt arms harms eta loss n) (mu.map (sampledScheduledHalfTsallisHistoryAt n) ⊗ₘ sampledScheduledHalfTsallisPolicyAt (Env

The actual scheduled successor potential term agrees almost surely with the canonical visible-history/action potential score.

theorem sampledScheduledHalfTsallisPotentialStabilityAtTime_succ_eq_historyAction_ae {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) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment (fun sample => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample (n + 1)) =ᵐ[mu] (fun sample => sampledScheduledHalfTsallisHistoryActionPotentialStabilityAt arms harms eta loss n (sampledScheduledHalfTsallisHistoryAt n sample, sampledScheduledHalfTsallisActionAt n sample))

Expected finite-horizon refined stability for all generated successor rounds. The left side is exactly the same-rate stability sum consumed by the pathwise scheduled score/penalty decomposition, restricted to actual times `n + 1`. Time zero and rates above `1 / 2` are deliberately not claimed.

theorem integral_sum_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] (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 integral mu (fun sample => (Finset.range horizon).sum (fun n => sampledScheduledHalfTsallisPotentialStabilityAtTime arms harms eta sample (n + 1))) <= integral mu (fun sample => (Finset.range horizon).sum (fun n => sampledScheduledHalfTsallisRefinedPotentialStabilityBoundAt (Env