BanditRLProof.TsallisSqrtScheduleSelfBoundingRefinedTuning

No declaration docstring is present; use the chapter context and exact statement below.

theorem sum_one_div_lambda_mul_eq_div {Action : Type u} [DecidableEq Action] (actions : Finset Action) (gap : Action -> Real) (lambda : Real) (hlambda : lambda ≠ 0) (hgap : ∀ action ∈ actions, gap action ≠ 0) : actions.sum (fun action => 1 / (lambda * gap action)) = actions.sum (fun action => 1 / gap action) / lambda

With the coefficient-aware alpha/lambda change of variables, the actual continuous threshold used by the generated theorem is exactly `2 * (horizon + 1) / beta`.

theorem sampledScheduledHalfTsallisSelfBoundingThreshold_refinedLocalLambda_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (gap : Action -> Real) (hsuboptimal : (arms.erase best).Nonempty) (hgap : ∀ action ∈ arms.erase best, 0 < gap action) (horizon : Nat) (beta : Real) (hbetaLower : 2 <= beta) (hbetaUpper : beta <= (2 * ((arms.erase best).card : Real) * (((horizon + 1 : Nat) : Real))) / (25 * ((arms.erase best).sum (fun action => 1 / gap action)) ^ 2)) : sampledScheduledHalfTsallisSelfBoundingThreshold arms best gap (refinedLocalLambda (2 * ((arms.erase best).card : Real) * (((horizon + 1 : Nat) : Real))) ((arms.erase best).sum (fun action => 1 / gap action)) beta) = (2 * (((horizon + 1 : Nat) : Real))) / beta

The generated-regret scalar bound after substituting the coefficient-aware beta-dependent learning-rate multiplier.

noncomputable def refinedLocalTunedRegretBound (scale horizonMass reciprocalGap corruption beta : Real) : Real

The Lambert-free explicit estimate for the local tuned scalar bound.

theorem refinedLocalTunedRegretBound_le_explicit (scale horizonMass reciprocalGap corruption beta : Real) (hscale : 0 < scale) (hhorizonMass : 1 <= horizonMass) (hreciprocalGap : 0 < reciprocalGap) (hcorruption : 0 < corruption) (hbeta : 1 <= beta) (hbetaUpper : beta <= scale / (25 * reciprocalGap ^ 2)) (hcorruptionUpper : corruption * reciprocalGap <= scale) (hroot : refinedLocalBetaEquation scale reciprocalGap corruption beta = 0) : refinedLocalTunedRegretBound scale horizonMass reciprocalGap corruption beta <= 1 + Real.log horizonMass + 10 * Real.sqrt (corruption * reciprocalGap) * (2 + Real.sqrt (Real.log (scale / (corruption * reciprocalGap)) + 1))

The coefficient-aware scalar root now drives the actual generated theorem: it constructs the beta-dependent lambda, discharges the floor-threshold window, and rewrites the logarithmic tail as `log beta`.

theorem exists_integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_refinedLocalTuned {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) (hcorruption : 0 < corruption) (hscalarLower : 2 <= (2 * ((arms.erase best).card : Real) * (((horizon + 1 : Nat) : Real))) / (25 * ((arms.erase best).sum (fun action => 1 / gap action)) ^ 2)) (hscalarThresholdOne : (2 * ((arms.erase best).card : Real) * (((horizon + 1 : Nat) : Real))) / (25 * ((arms.erase best).sum (fun action => 1 / gap action)) ^ 2) <= 2 * (((horizon + 1 : Nat) : Real))) (hcorruptionUpper : 2 * (corruption * (arms.erase best).sum (fun action => 1 / gap action)) <= 2 * ((arms.erase best).card : Real) * (((horizon + 1 : Nat) : Real))) (hcorruptionLower : 25 * ((arms.erase best).sum (fun action => 1 / gap action)) * (Real.log ((2 * ((arms.erase best).card : Real) * (((horizon + 1 : Nat) : Real))) / (25 * ((arms.erase best).sum (fun action => 1 / gap action)) ^ 2)) + 2) <= corruption) (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 horizonMass : Real := ((horizon + 1 : Nat) : Real) let scale := 2 * ((arms.erase best).card : Real) * horizonMass exists beta, beta ∈ Set.Icc 2 (scale / (25 * reciprocalGap ^ 2)) ∧ refinedLocalBetaEquation scale reciprocalGap corruption beta = 0 ∧ let weight := corruption * reciprocalGap / scale * beta 1 <= weight ∧ weight <= (1 + Real.sqrt (Real.log (scale / (corruption * reciprocalGap)) + 1)) ^ 2 ∧ refinedLocalLambda scale reciprocalGap beta ∈ Set.Ioc (0 : Real) 1 ∧ integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= refinedLocalTunedRegretBound scale horizonMass reciprocalGap corruption beta

The coefficient-aware generated route with the auxiliary root eliminated. The constants reflect the local floor theorem's amplitude `5 * (1 + lambda)`; this is intentionally not presented as the paper's sharper constant.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_refinedLocalExplicit {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) (hcorruption : 0 < corruption) (hscalarLower : 2 <= (2 * ((arms.erase best).card : Real) * (((horizon + 1 : Nat) : Real))) / (25 * ((arms.erase best).sum (fun action => 1 / gap action)) ^ 2)) (hscalarThresholdOne : (2 * ((arms.erase best).card : Real) * (((horizon + 1 : Nat) : Real))) / (25 * ((arms.erase best).sum (fun action => 1 / gap action)) ^ 2) <= 2 * (((horizon + 1 : Nat) : Real))) (hcorruptionUpper : 2 * (corruption * (arms.erase best).sum (fun action => 1 / gap action)) <= 2 * ((arms.erase best).card : Real) * (((horizon + 1 : Nat) : Real))) (hcorruptionLower : 25 * ((arms.erase best).sum (fun action => 1 / gap action)) * (Real.log ((2 * ((arms.erase best).card : Real) * (((horizon + 1 : Nat) : Real))) / (25 * ((arms.erase best).sum (fun action => 1 / gap action)) ^ 2)) + 2) <= corruption) (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 horizonMass : Real := ((horizon + 1 : Nat) : Real) let scale := 2 * ((arms.erase best).card : Real) * horizonMass integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= 1 + Real.log horizonMass + 10 * Real.sqrt (corruption * reciprocalGap) * (2 + Real.sqrt (Real.log (scale / (corruption * reciprocalGap)) + 1))