BanditRLProof.TsallisFTRLConditionalStability

The one-round FTRL stability score generated by an importance-weighted loss estimate.

noncomputable def importanceWeightedStabilityScore {History : Type u} {Action : Type v} (arms : Finset Action) (prob loss : History -> Action -> Real) (next : History -> Action -> Action -> Real) (sample : History × Action) : Real

The pointwise half-Tsallis upper bound for the sampling-law averaged one-round stability score.

noncomputable def halfPowerStabilityBound {History : Type u} {Action : Type v} (arms : Finset Action) (eta : Real) (prob : History -> Action -> Real) (history : History) : Real

An identified finite conditional action law transports the pointwise half-Tsallis minimizer stability theorem to a one-round integral inequality. The score and bound integrability hypotheses are the exact analytic boundary needed by Bochner integral monotonicity. No measurability of a particular minimizer selector is inferred here.

theorem integral_importanceWeightedStabilityScore_le_integral_halfPowerStabilityBound_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 (importanceWeightedStabilityScore arms prob loss next)) (hIntegrable : Integrable (importanceWeightedStabilityScore arms prob loss next) (mu.map history ⊗ₘ policy)) (hboundIntegrable : Integrable (halfPowerStabilityBound arms eta prob) (mu.map history)) : integral mu (fun omega => importanceWeightedStabilityScore arms prob loss next (history omega, action omega)) <= integral (mu.map history) (halfPowerStabilityBound arms eta prob)

Generated finite-action process specialization of the conditional half-Tsallis stability transport.

theorem actionProcess_integral_importanceWeightedStabilityScore_le_integral_halfPowerStabilityBound_of_minimizers {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty 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 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 (importanceWeightedStabilityScore arms prob loss next)) (hIntegrable : Integrable (importanceWeightedStabilityScore arms prob loss next) (historyMu ⊗ₘ Exp3.finiteActionKernel arms prob source)) (hboundIntegrable : Integrable (halfPowerStabilityBound arms eta prob) historyMu) : integral (Exp3.actionProcessMeasure historyMu arms prob source) (importanceWeightedStabilityScore arms prob loss next) <= integral historyMu (halfPowerStabilityBound arms eta prob)

The fixed half-Tsallis minimizer viewed as a history-indexed action distribution.

noncomputable def halfTsallisHistoryMinimizer {History : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : History -> Action -> Real) : History -> Action -> Real

The fixed importance-weighted half-Tsallis update viewed as a history/action-indexed family.

noncomputable def halfTsallisHistoryUpdatedMinimizer {History : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score loss : History -> Action -> Real) : History -> Action -> Action -> Real

Coordinate measurability is the only missing contract for turning the fixed history-indexed minimizer into the project's finite-action kernel source. Distribution feasibility follows from the minimizer certificate.

noncomputable def measurableFiniteActionDistribution_halfTsallisHistoryMinimizer {History : Type u} {Action : Type v} [MeasurableSpace History] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score : History -> Action -> Real) (hmeasurable : forall action, action ∈ arms -> Measurable (fun history => halfTsallisHistoryMinimizer arms harms eta score history action)) : Exp3.MeasurableFiniteActionDistribution arms (halfTsallisHistoryMinimizer arms harms eta score) where

Canonical generated-action one-round stability endpoint. The minimizer certificates and finite-distribution laws are internal. The remaining caller contracts expose exactly what is not yet proved for the `Classical.choose` selector: coordinate measurability and regularity of the updated stability score.

theorem actionProcess_integral_halfTsallisHistoryStability_le_integral_halfPowerStabilityBound {History : Type u} {Action : Type v} [MeasurableSpace History] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (historyMu : Measure History) [IsFiniteMeasure historyMu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (score loss : History -> Action -> Real) (hmeasurable : forall action, action ∈ arms -> Measurable (fun history => halfTsallisHistoryMinimizer arms harms eta score history action)) (heta : 0 < eta) (hloss : forall history candidate, candidate ∈ arms -> 0 <= loss history candidate ∧ loss history candidate <= 1) (hscore : Measurable (importanceWeightedStabilityScore arms (halfTsallisHistoryMinimizer arms harms eta score) loss (halfTsallisHistoryUpdatedMinimizer arms harms eta score loss))) (hIntegrable : Integrable (importanceWeightedStabilityScore arms (halfTsallisHistoryMinimizer arms harms eta score) loss (halfTsallisHistoryUpdatedMinimizer arms harms eta score loss)) (historyMu ⊗ₘ Exp3.finiteActionKernel arms (halfTsallisHistoryMinimizer arms harms eta score) (measurableFiniteActionDistribution_halfTsallisHistoryMinimizer arms harms eta score hmeasurable))) (hboundIntegrable : Integrable (halfPowerStabilityBound arms eta (halfTsallisHistoryMinimizer arms harms eta score)) historyMu) : integral (Exp3.actionProcessMeasure historyMu arms (halfTsallisHistoryMinimizer arms harms eta score) (measurableFiniteActionDistribution_halfTsallisHistoryMinimizer arms harms eta score hmeasurable)) (importanceWeightedStabilityScore arms (halfTsallisHistoryMinimizer arms harms eta score) loss (halfTsallisHistoryUpdatedMinimizer arms harms eta score loss)) <= integral historyMu (halfPowerStabilityBound arms eta (halfTsallisHistoryMinimizer arms harms eta score))