BanditRLProof.TsallisSqrtScheduleSelfBoundingTuning

A positive real threshold and its natural floor differ by at most a factor of two once the threshold is at least one.

theorem natFloor_positive_and_half_le (q : Real) (hq : 1 <= q) : 0 < ⌊q⌋₊ ∧ ((⌊q⌋₊ : Nat) : Real) <= q ∧ q <= 2 * ((⌊q⌋₊ : Nat) : Real)

The continuous threshold whose floor is used for the active-prefix split.

noncomputable def sampledScheduledHalfTsallisSelfBoundingThreshold {Action : Type u} [DecidableEq Action] (arms : Finset Action) (best : Action) (gap : Action -> Real) (lambda : Real) : Real

In the large-horizon branch, flooring the continuous threshold removes the explicit cutoff from the refined generated-regret theorem.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_refinedSelfBoundingFloorCutoff {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) (hthresholdOne : 1 <= sampledScheduledHalfTsallisSelfBoundingThreshold arms best gap lambda) (hthresholdHorizon : sampledScheduledHalfTsallisSelfBoundingThreshold arms best gap lambda <= ((horizon + 1 : Nat) : Real)) (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) let threshold := sampledScheduledHalfTsallisSelfBoundingThreshold arms best gap lambda integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= (1 + lambda) * ((1 + Real.log (((horizon + 1 : Nat) : Real))) / 2) + lambda * corruption + amplitude ^ 2 * reciprocalGap + (amplitude ^ 2 / 4 * reciprocalGap) * Real.log ((2 * (((horizon + 1 : Nat) : Real))) / threshold)

The `lambda = 1` continuous threshold, written with the ordinary reciprocal-gap mass.

noncomputable def sampledScheduledHalfTsallisSelfBoundingOneThreshold {Action : Type u} [DecidableEq Action] (arms : Finset Action) (best : Action) (gap : Action -> Real) : Real

The `lambda = 1` threshold has the expected reciprocal-gap/card form.

theorem sampledScheduledHalfTsallisSelfBoundingOneThreshold_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (best : Action) (gap : Action -> Real) (hsuboptimal : (arms.erase best).Nonempty) : sampledScheduledHalfTsallisSelfBoundingOneThreshold arms best gap = 25 * ((arms.erase best).sum (fun action => 1 / gap action)) ^ 2 / ((arms.erase best).card : Real)

A concrete large-horizon self-bounding theorem with `lambda = 1`. Unlike the refined corruption endpoint, this theorem needs no scalar optimization beyond checking that its continuous threshold lies in the horizon.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_selfBoundingOne {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 : Real) (hthresholdOne : 1 <= sampledScheduledHalfTsallisSelfBoundingOneThreshold arms best gap) (hthresholdHorizon : sampledScheduledHalfTsallisSelfBoundingOneThreshold arms best gap <= ((horizon + 1 : Nat) : Real)) (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 / gap action) let threshold := sampledScheduledHalfTsallisSelfBoundingOneThreshold arms best gap integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= 1 + Real.log (((horizon + 1 : Nat) : Real)) + corruption + 100 * reciprocalGap + 25 * reciprocalGap * Real.log ((2 * (((horizon + 1 : Nat) : Real))) / threshold)

Fully explicit `lambda = 1` large-horizon bound, with the continuous threshold rewritten as `25 * S^2 / (K-1)`.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_selfBoundingOne_explicit {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 : Real) (hthresholdOne : 1 <= 25 * ((arms.erase best).sum (fun action => 1 / gap action)) ^ 2 / ((arms.erase best).card : Real)) (hthresholdHorizon : 25 * ((arms.erase best).sum (fun action => 1 / gap action)) ^ 2 / ((arms.erase best).card : Real) <= ((horizon + 1 : Nat) : Real)) (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 / gap action) integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= 1 + Real.log (((horizon + 1 : Nat) : Real)) + corruption + 100 * reciprocalGap + 25 * reciprocalGap * Real.log ((2 * (((horizon + 1 : Nat) : Real)) * ((arms.erase best).card : Real)) / (25 * reciprocalGap ^ 2))