BanditRLProof.TsallisSqrtScheduleSelfBoundingOptimization

Integral-comparison bound for the shifted inverse-square-root prefix.

theorem sum_range_one_div_sqrt_natSucc_le_two_sqrt (n : Nat) : (Finset.range n).sum (fun t => 1 / Real.sqrt (((t + 1 : Nat) : Real))) ≤ 2 * Real.sqrt (n : Real)

Harmonic tail bound with the exact logarithmic ratio needed by the self-bounding threshold split.

theorem sum_Ico_one_div_natSucc_le_log_div (m n : Nat) (hm : 0 < m) (hmn : m ≤ n) : (Finset.Ico m n).sum (fun t => 1 / (((t + 1 : Nat) : Real))) ≤ Real.log ((n : Real) / (m : Real))

The active-prefix branch of the square-root schedule has a closed-form inverse-square-root bound.

theorem sum_range_sqrtSchedule_activeBranch_le_closedForm (cutoff : Nat) (amplitude sqrtCard card reciprocalGap : Real) (hamplitude : 0 <= amplitude) (hsqrtCard : 0 <= sqrtCard) : (Finset.range cutoff).sum (fun t => amplitude / Real.sqrt (((t + 1 : Nat) : Real)) * sqrtCard - card / reciprocalGap) <= 2 * amplitude * sqrtCard * Real.sqrt (cutoff : Real) - (cutoff : Real) * card / reciprocalGap

The unconstrained tail branch of the square-root schedule is controlled by the logarithmic harmonic tail.

theorem sum_Ico_sqrtSchedule_unconstrainedBranch_le_log (m n : Nat) (hm : 0 < m) (hmn : m <= n) (amplitude reciprocalGap : Real) (hreciprocalGap : 0 <= reciprocalGap) : (Finset.Ico m n).sum (fun t => (amplitude / Real.sqrt (((t + 1 : Nat) : Real))) ^ 2 / 4 * reciprocalGap) <= (amplitude ^ 2 / 4 * reciprocalGap) * Real.log ((n : Real) / (m : Real))

The refined terminal self-bounding route under the concrete square-root schedule, reduced to two explicit filtered scalar sums.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_refinedSelfBoundingQuadraticSplit {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) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon : Nat) (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 sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms sampledScheduledHalfTsallisSqrtSchedule t action)) - corruption ≤ integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon)) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule 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 => (1 + lambda) * (5 / Real.sqrt (((t + 1 : Nat) : Real))) let active := fun t => 2 * Real.sqrt ((arms.erase best).card : Real) ≤ b t * reciprocalGap integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) ≤ (1 + lambda) * (sampledScheduledHalfTsallisHarmonicBudget horizon / 2) + 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)

Prefix/suffix specialization with a single scalar cutoff certificate.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_refinedSelfBoundingQuadraticPrefixSplit {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) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon cutoff : Nat) (hcutoff : cutoff ≤ horizon + 1) (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) (hcutoffThreshold : 2 * Real.sqrt ((arms.erase best).card : Real) * Real.sqrt (cutoff : Real) ≤ 5 * (1 + lambda) * (arms.erase best).sum (fun action => 1 / (lambda * gap action))) (hselfBounding : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms sampledScheduledHalfTsallisSqrtSchedule t action)) - corruption ≤ integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon)) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment let reciprocalGap := (arms.erase best).sum (fun action => 1 / (lambda * gap action)) let b := fun t => (1 + lambda) * (5 / Real.sqrt (((t + 1 : Nat) : Real))) integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) ≤ (1 + lambda) * (sampledScheduledHalfTsallisHarmonicBudget horizon / 2) + lambda * corruption + (Finset.range cutoff).sum (fun t => b t * Real.sqrt ((arms.erase best).card : Real) - (arms.erase best).card / reciprocalGap) + (Finset.Ico cutoff (horizon + 1)).sum (fun t => (b t) ^ 2 / 4 * reciprocalGap)

Closed-form generated-regret endpoint after choosing a positive cutoff. The only remaining scalar optimization is the choice of `cutoff` and `lambda`.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_refinedSelfBoundingQuadraticClosedForm {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) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon cutoff : Nat) (hcutoffPos : 0 < cutoff) (hcutoff : cutoff <= horizon + 1) (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) (hcutoffThreshold : 2 * Real.sqrt ((arms.erase best).card : Real) * Real.sqrt (cutoff : Real) <= 5 * (1 + lambda) * (arms.erase best).sum (fun action => 1 / (lambda * gap action))) (hselfBounding : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment (Finset.range (horizon + 1)).sum (fun t => (arms.erase best).sum (fun action => gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms sampledScheduledHalfTsallisSqrtSchedule t action)) - corruption <= integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon)) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment let reciprocalGap := (arms.erase best).sum (fun action => 1 / (lambda * gap action)) let amplitude := 5 * (1 + lambda) integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= (1 + lambda) * (sampledScheduledHalfTsallisHarmonicBudget horizon / 2) + lambda * corruption + 2 * amplitude * Real.sqrt ((arms.erase best).card : Real) * Real.sqrt (cutoff : Real) - (cutoff : Real) * (arms.erase best).card / reciprocalGap + (amplitude ^ 2 / 4 * reciprocalGap) * Real.log (((horizon + 1 : Nat) : Real) / (cutoff : Real))