BanditRLProof.TsallisFTRLGeneratedRegularity

Every supported coordinate of a finite simplex point is at most one.

theorem finiteSimplex_apply_le_one {Action : Type u} {arms : Finset Action} {p : Action -> Real} (hp : FTRL.finiteSimplex arms p) {action : Action} (haction : action ∈ arms) : p action <= 1

Sampling mass cancels the inverse probability in one realized stability score, leaving a bound by the current and updated selected coordinates.

theorem prob_mul_abs_importanceWeightedStabilityScore_le {History : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (next : History -> Action -> Action -> Real) (history : History) (chosen : Action) (hchosen : chosen ∈ arms) (hnextSimplex : FTRL.finiteSimplex arms (next history chosen)) (hprobPos : 0 < prob history chosen) (hloss : 0 <= loss history chosen ∧ loss history chosen <= 1) : prob history chosen * |importanceWeightedStabilityScore arms prob loss next (history, chosen)| <= prob history chosen + next history chosen chosen

Every real-valued function is integrable under a finite action law.

theorem integrable_finiteActionMeasure {Action : Type u} [MeasurableSpace Action] [MeasurableSingletonClass Action] (arms : Finset Action) (prob : Action -> Real) (f : Action -> Real) : Integrable f (Exp3.finiteActionMeasure arms prob)

A measurable one-round stability score is automatically integrable under its finite sampling kernel. No uniform lower probability floor is needed.

theorem integrable_importanceWeightedStabilityScore_finiteActionKernel {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (prob loss : History -> Action -> Real) (next : History -> Action -> Action -> Real) (source : Exp3.MeasurableFiniteActionDistribution arms prob) (hprobPos : forall history action, action ∈ arms -> 0 < prob history action) (hnextSimplex : forall history chosen, chosen ∈ arms -> FTRL.finiteSimplex arms (next history chosen)) (hloss : forall history action, action ∈ arms -> 0 <= loss history action ∧ loss history action <= 1) (hscore : Measurable (importanceWeightedStabilityScore arms prob loss next)) : Integrable (importanceWeightedStabilityScore arms prob loss next) (historyMu ⊗ₘ Exp3.finiteActionKernel arms prob source)

The half-power stability budget is uniformly bounded and hence integrable under every finite history measure.

theorem integrable_halfPowerStabilityBound_of_finiteSimplex {History : Type u} {Action : Type v} [MeasurableSpace History] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (eta : Real) (prob : History -> Action -> Real) (source : Exp3.MeasurableFiniteActionDistribution arms prob) : Integrable (halfPowerStabilityBound arms eta prob) historyMu

The environment-lifted generated policy is exactly the finite-action kernel carried by its measurable distribution source.

theorem sampledHalfTsallisPolicyAt_eq_finiteActionKernel {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (n : Nat) : sampledHalfTsallisPolicyAt (Env

Measurability of the generated stability score now suffices for its integrability under the generated history/action product law.

theorem integrable_sampledHalfTsallisHistoryActionStabilityAt {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 : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (hscore : Measurable (sampledHalfTsallisHistoryActionStabilityAt arms harms eta loss n)) : Integrable (sampledHalfTsallisHistoryActionStabilityAt arms harms eta loss n) (((prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment).map (sampledHalfTsallisHistoryAt n)) ⊗ₘ sampledHalfTsallisPolicyAt (Env

The generated half-power budget is automatically integrable under every generated history marginal.

theorem integrable_sampledHalfTsallisHalfPowerBoundAt {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 : Real) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (loss : Exp3.PredictableLossVector Env Action) (n : Nat) : Integrable (sampledHalfTsallisHalfPowerBoundAt (Env

Generated finite-horizon actual-successor stability with both integrability contracts discharged. Stability-score measurability remains the exact selector/update regularity boundary.

theorem integral_sum_sampledHalfTsallisSuccessorStability_le_integral_sum_halfPowerStabilityBound_of_measurable {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 : Real) (heta : 0 < eta) (selector : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta) (loss : Exp3.PredictableLossVector Env Action) (hscore : forall n, Measurable (sampledHalfTsallisHistoryActionStabilityAt arms harms eta loss n)) : let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment integral mu (fun sample => (Finset.range horizon).sum (fun n => sampledHalfTsallisSuccessorStabilityAt arms harms eta loss n sample)) <= integral mu (fun sample => (Finset.range horizon).sum (fun n => sampledHalfTsallisHalfPowerBoundAt (Env