BanditRLProof.TsallisFTRLGeneratedMeasurability

Coordinate regularity for the generated current and sampled-action updated half-Tsallis selectors. The finite-history component constructs the policy; the second component covers the environment/prefix/action parameter space of the updated canonical minimizer.

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

The canonical half-Tsallis selector itself satisfies the finite-history coordinate measurability contract.

noncomputable def canonicalHalfTsallisFiniteHistorySelectorMeasurability {Action : Type v} [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) : HalfTsallisFiniteHistorySelectorMeasurability arms harms eta where

A finite sum of current-minus-updated importance-weighted linear losses is measurable once all current, loss, and updated coordinates are measurable.

theorem measurable_importanceWeightedStabilityScore {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (prob loss : History -> Action -> Real) (next : History -> Action -> Action -> Real) (hprob : forall candidate, candidate ∈ arms -> Measurable (fun history => prob history candidate)) (hloss : forall candidate, candidate ∈ arms -> Measurable (fun history => loss history candidate)) (hnext : forall candidate, candidate ∈ arms -> Measurable (fun sample : History × Action => next sample.1 sample.2 candidate)) : Measurable (importanceWeightedStabilityScore arms prob loss next)

Every supported coordinate of the generated predictable loss vector is measurable on the environment/prefix parameter space.

theorem measurable_sampledHalfTsallisPredictableLossAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] (loss : Exp3.PredictableLossVector Env Action) (n : Nat) (candidate : Action) : Measurable (fun input : Env × History.FinitePairHistory Action Real n => sampledHalfTsallisPredictableLossAt loss n input candidate)

Every supported coordinate of the canonical sampled-action update is measurable without an external selector assumption.

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

The canonical current and one-step updated minimizers satisfy the full generated-selector regularity contract; callers no longer need to assume measurability of either `Classical.choose` surface.

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

The generated one-round current-minus-updated stability score is measurable under the generated selector coordinate contract.

theorem measurable_sampledHalfTsallisHistoryActionStabilityAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Exp3.PredictableLossVector Env Action) (selector : HalfTsallisGeneratedSelectorMeasurability arms harms eta loss) (n : Nat) : Measurable (sampledHalfTsallisHistoryActionStabilityAt arms harms eta loss n)

Generated finite-horizon actual-successor stability with all score and integrability regularity derived from one generated-selector contract.

theorem integral_sum_sampledHalfTsallisSuccessorStability_le_integral_sum_halfPowerStabilityBound_of_selector {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) (loss : Exp3.PredictableLossVector Env Action) (selector : HalfTsallisGeneratedSelectorMeasurability arms harms eta loss) : let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory 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 := Env) arms harms eta n (sampledHalfTsallisHistoryAt n sample)))

Generated finite-horizon actual-successor stability for the canonical half-Tsallis policy, with selector measurability proved internally.

theorem integral_sum_sampledHalfTsallisSuccessorStability_le_integral_sum_halfPowerStabilityBound_canonical {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) (loss : Exp3.PredictableLossVector Env Action) : let selector := canonicalHalfTsallisGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory 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 := Env) arms harms eta n (sampledHalfTsallisHistoryAt n sample)))