BanditRLProof.TsallisScheduledSelfBoundingOptimization

Split a finite collection of generated expected-probability quadratic terms at the exact active-mass threshold. The active times use the simplex mass constraint; all other times use coordinatewise completion of squares.

theorem sum_sampledScheduledHalfTsallisExpectedProbability_le_quadraticFilterSplit {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) → Action × Real))) [IsProbabilityMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat → Real) (times : Finset Nat) {best : Action} (hbest : best ∈ arms) (gap : Action → Real) (hsuboptimal : (arms.erase best).Nonempty) (hgap : ∀ action ∈ arms.erase best, 0 < gap action) (b : Nat → Real) (lambda : Real) (hlambda : 0 < lambda) : times.sum (fun t => (arms.erase best).sum (fun action => b t * Real.sqrt (sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action) - lambda * gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)) ≤ (times.filter fun t => 2 * Real.sqrt ((arms.erase best).card : Real) ≤ b t * (arms.erase best).sum (fun action => 1 / (lambda * gap action))).sum (fun t => b t * Real.sqrt ((arms.erase best).card : Real) - (arms.erase best).card / (arms.erase best).sum (fun action => 1 / (lambda * gap action))) + (times.filter fun t => ¬ 2 * Real.sqrt ((arms.erase best).card : Real) ≤ b t * (arms.erase best).sum (fun action => 1 / (lambda * gap action))).sum (fun t => (b t) ^ 2 / 4 * (arms.erase best).sum (fun action => 1 / (lambda * gap action)))

Prefix/suffix form of the one-round split. A caller supplies a cutoff and proves the active threshold only on its prefix; the suffix always admits the unconstrained branch.

theorem sum_range_sampledScheduledHalfTsallisExpectedProbability_le_quadraticPrefixSplit {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) → Action × Real))) [IsProbabilityMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat → Real) (n cutoff : Nat) (hcutoff : cutoff ≤ n) {best : Action} (hbest : best ∈ arms) (gap : Action → Real) (hsuboptimal : (arms.erase best).Nonempty) (hgap : ∀ action ∈ arms.erase best, 0 < gap action) (b : Nat → Real) (lambda : Real) (hlambda : 0 < lambda) (hthreshold : ∀ t < cutoff, 2 * Real.sqrt ((arms.erase best).card : Real) ≤ b t * (arms.erase best).sum (fun action => 1 / (lambda * gap action))) : (Finset.range n).sum (fun t => (arms.erase best).sum (fun action => b t * Real.sqrt (sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action) - lambda * gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)) ≤ (Finset.range cutoff).sum (fun t => b t * Real.sqrt ((arms.erase best).card : Real) - (arms.erase best).card / (arms.erase best).sum (fun action => 1 / (lambda * gap action))) + (Finset.Ico cutoff n).sum (fun t => (b t) ^ 2 / 4 * (arms.erase best).sum (fun action => 1 / (lambda * gap action)))

The generated scheduled regret theorem after terminal self-bounding and the exact finite-time quadratic branch split. All probabilistic, conditional law, Jensen, and finite-simplex obligations have been discharged; the remaining right-hand side is deterministic schedule algebra.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_selfBoundingQuadraticSplit {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat → Real) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon : Nat) (heta : ∀ t, t ≤ horizon → 0 < eta t) (heta_le : ∀ t, t ≤ horizon → eta t ≤ 1 / 2) (hetaMono : ∀ t, t < horizon → eta (t + 1) ≤ eta t) (gap : Action → Real) (hsuboptimal : (arms.erase best).Nonempty) (hgap : ∀ action ∈ arms.erase best, 0 < gap action) (corruption lambda : Real) (hlambda : lambda ∈ Set.Ioc (0 : Real) 1) (hselfBounding : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)) - corruption ≤ integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon)) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment let times := Finset.range (horizon + 1) let reciprocalGap := (arms.erase best).sum (fun action => 1 / (lambda * gap action)) let b := fun t => 2 * (1 + lambda) * eta t let active := fun t => 2 * Real.sqrt ((arms.erase best).card : Real) ≤ b t * reciprocalGap let base := times.sum (fun t => 2 * (eta t) ^ 2) + (halfTsallisPotentialMass arms (initialHalfTsallisDistribution arms harms (eta 0)) / eta horizon - 1 / eta horizon) integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon) ≤ (1 + lambda) * base + lambda * corruption + (times.filter active).sum (fun t => b t * Real.sqrt ((arms.erase best).card : Real) - (arms.erase best).card / reciprocalGap) + (times.filter fun t => ¬ active t).sum (fun t => (b t) ^ 2 / 4 * reciprocalGap)

Refined generated interpolation with any deterministic coefficient envelope `b`. This is the common pre-split surface for filter and prefix quadratic consumers.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_refinedSelfBoundingQuadraticSum_of_refinedCoefficient_le {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat → Real) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon : Nat) (heta : ∀ t, t ≤ horizon → 0 < eta t) (heta_le : ∀ t, t ≤ horizon → eta t ≤ 1 / 2) (hetaMono : ∀ t, t < horizon → eta (t + 1) ≤ eta t) (gap : Action → Real) (corruption lambda : Real) (hlambda : lambda ∈ Set.Ioc (0 : Real) 1) (b : Nat → Real) (hb : ∀ t, t ≤ horizon → (1 + lambda) * sampledScheduledHalfTsallisRefinedCoefficient eta t ≤ b t) (hselfBounding : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)) - corruption ≤ integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon)) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment let times := Finset.range (horizon + 1) let base := times.sum (fun t => 2 * (eta t) ^ 2) integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon) ≤ (1 + lambda) * base + lambda * corruption + times.sum (fun t => (arms.erase best).sum (fun action => b t * Real.sqrt (sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action) - lambda * gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action))

Refined generated quadratic split for the theorem route. Unlike the coarse scheduled interpolation above, this theorem consumes the uncollapsed stability-penalty coefficient, so its deterministic base contains only `sum_t 2 * eta_t^2` and no terminal `1 / eta_T` potential term.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_refinedSelfBoundingQuadraticSplit_of_refinedCoefficient_le {Env : Type u} {Action : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [StandardBorelSpace Action] [Nonempty Action] [DecidableEq Action] (prior : Measure Env) [IsProbabilityMeasure prior] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat → Real) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon : Nat) (heta : ∀ t, t ≤ horizon → 0 < eta t) (heta_le : ∀ t, t ≤ horizon → eta t ≤ 1 / 2) (hetaMono : ∀ t, t < horizon → eta (t + 1) ≤ eta t) (gap : Action → Real) (hsuboptimal : (arms.erase best).Nonempty) (hgap : ∀ action ∈ arms.erase best, 0 < gap action) (corruption lambda : Real) (hlambda : lambda ∈ Set.Ioc (0 : Real) 1) (b : Nat → Real) (hb : ∀ t, t ≤ horizon → (1 + lambda) * sampledScheduledHalfTsallisRefinedCoefficient eta t ≤ b t) (hselfBounding : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action)) - corruption ≤ integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon)) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment let times := Finset.range (horizon + 1) let reciprocalGap := (arms.erase best).sum (fun action => 1 / (lambda * gap action)) let active := fun t => 2 * Real.sqrt ((arms.erase best).card : Real) ≤ b t * reciprocalGap let base := times.sum (fun t => 2 * (eta t) ^ 2) integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon) ≤ (1 + lambda) * base + lambda * corruption + (times.filter active).sum (fun t => b t * Real.sqrt ((arms.erase best).card : Real) - (arms.erase best).card / reciprocalGap) + (times.filter fun t => ¬ active t).sum (fun t => (b t) ^ 2 / 4 * reciprocalGap)