BanditRLProof.TsallisSqrtScheduleFixedGap

The concrete small-rate schedule used by the fixed-gap route.

noncomputable def sampledScheduledHalfTsallisSqrtSchedule (t : Nat) : Real

The finite harmonic budget through the inclusive horizon.

noncomputable def sampledScheduledHalfTsallisHarmonicBudget (horizon : Nat) : Real

The local real-valued budget is the real cast of Mathlib's rational harmonic number.

theorem sampledScheduledHalfTsallisHarmonicBudget_eq_harmonic (horizon : Nat) : sampledScheduledHalfTsallisHarmonicBudget horizon = (harmonic (horizon + 1) : Real)

Mathlib's finite harmonic estimate gives the explicit logarithmic budget.

theorem sampledScheduledHalfTsallisHarmonicBudget_le_one_add_log (horizon : Nat) : sampledScheduledHalfTsallisHarmonicBudget horizon <= 1 + Real.log (((horizon + 1 : Nat) : Real))

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

theorem sampledScheduledHalfTsallisSqrtSchedule_pos (t : Nat) : 0 < sampledScheduledHalfTsallisSqrtSchedule t

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

theorem sampledScheduledHalfTsallisSqrtSchedule_le_half (t : Nat) : sampledScheduledHalfTsallisSqrtSchedule t <= 1 / 2

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

theorem sampledScheduledHalfTsallisSqrtSchedule_succ_le (t : Nat) : sampledScheduledHalfTsallisSqrtSchedule (t + 1) <= sampledScheduledHalfTsallisSqrtSchedule t

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

theorem sampledScheduledHalfTsallisSqrtSchedule_four_mul_sq (t : Nat) : 4 * (sampledScheduledHalfTsallisSqrtSchedule t) ^ 2 = 1 / (((t + 1 : Nat) : Real))

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

private theorem sqrt_succ_sub_sqrt_le_one_div_sqrt_succ (t : Nat) : Real.sqrt (((t + 2 : Nat) : Real)) - Real.sqrt (((t + 1 : Nat) : Real)) <= 1 / Real.sqrt (((t + 2 : Nat) : Real))

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

theorem sampledScheduledHalfTsallisRefinedCoefficient_sqrtSchedule_nonneg (t : Nat) : 0 <= sampledScheduledHalfTsallisRefinedCoefficient sampledScheduledHalfTsallisSqrtSchedule t

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

theorem sampledScheduledHalfTsallisRefinedCoefficient_sqrtSchedule_le (t : Nat) : sampledScheduledHalfTsallisRefinedCoefficient sampledScheduledHalfTsallisSqrtSchedule t <= 5 / Real.sqrt (((t + 1 : Nat) : Real))

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

theorem sampledScheduledHalfTsallisRefinedCoefficient_sqrtSchedule_sq_le (t : Nat) : (sampledScheduledHalfTsallisRefinedCoefficient sampledScheduledHalfTsallisSqrtSchedule t) ^ 2 <= 25 / (((t + 1 : Nat) : Real))

The square-root schedule closes any matching self-bounding route with a finite harmonic budget and an explicit reciprocal-gap factor.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_of_selfBounding {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) (hgapPos : ∀ action, action ∈ arms.erase best -> 0 < gap action) (corruption : 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 integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= sampledScheduledHalfTsallisHarmonicBudget horizon * (1 + 25 * (arms.erase best).sum (fun action => 1 / gap action)) + corruption

The square-root schedule closes the exact fixed-gap route with a finite harmonic budget and an explicit reciprocal-gap factor.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_fixedGap {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) (hgapPos : ∀ action, action ∈ arms.erase best -> 0 < gap action) (hgapLaw : ∀ t sample action, action ∈ arms -> Exp3.predictableLossAt loss t sample action - Exp3.predictableLossAt loss t sample best = gap action) (corruption : Real) (hcorruption : 0 <= corruption) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= sampledScheduledHalfTsallisHarmonicBudget horizon * (1 + 25 * (arms.erase best).sum (fun action => 1 / gap action)) + corruption

The square-root schedule also closes a coordinatewise expected-gap law; no samplewise fixed-gap identity is required.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_expectedGap {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) (hgapPos : ∀ action, action ∈ arms.erase best -> 0 < gap action) (hgapLaw : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment HasScheduledExpectedGapLaw mu arms harms sampledScheduledHalfTsallisSqrtSchedule loss best gap horizon) (corruption : Real) (hcorruption : 0 <= corruption) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= sampledScheduledHalfTsallisHarmonicBudget horizon * (1 + 25 * (arms.erase best).sum (fun action => 1 / gap action)) + corruption

The concrete square-root schedule has an explicit logarithmic fixed-gap regret bound, obtained from Mathlib's finite harmonic estimate.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_log_fixedGap {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) (hgapPos : ∀ action, action ∈ arms.erase best -> 0 < gap action) (hgapLaw : ∀ t sample action, action ∈ arms -> Exp3.predictableLossAt loss t sample action - Exp3.predictableLossAt loss t sample best = gap action) (corruption : Real) (hcorruption : 0 <= corruption) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= (1 + Real.log (((horizon + 1 : Nat) : Real))) * (1 + 25 * (arms.erase best).sum (fun action => 1 / gap action)) + corruption

Mathlib's harmonic estimate turns the coordinatewise expected-gap route into the same explicit logarithmic square-root-schedule bound.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_sqrtSchedule_log_expectedGap {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) (hgapPos : ∀ action, action ∈ arms.erase best -> 0 < gap action) (hgapLaw : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment HasScheduledExpectedGapLaw mu arms harms sampledScheduledHalfTsallisSqrtSchedule loss best gap horizon) (corruption : Real) (hcorruption : 0 <= corruption) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms sampledScheduledHalfTsallisSqrtSchedule loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms sampledScheduledHalfTsallisSqrtSchedule selector.finiteHistory loss.environment integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms sampledScheduledHalfTsallisSqrtSchedule loss (pointMass best) horizon) <= (1 + Real.log (((horizon + 1 : Nat) : Real))) * (1 + 25 * (arms.erase best).sum (fun action => 1 / gap action)) + corruption