BanditRLProof.TsallisScheduledRefinedExpectedPenalty

The concavity tangent at one bounds the excess of `sqrt x` over `x`.

theorem sqrt_sub_self_le_half_one_sub (x : Real) (hx : 0 <= x) : Real.sqrt x - x <= (1 - x) / 2

Above the point-mass baseline, half-Tsallis potential mass is controlled by the paper's refined suboptimal-arm mass.

theorem halfTsallisPotentialMass_sub_one_le_two_mul_sum_erase_refined {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (hbest : best ∈ arms) (probability : Action -> Real) (hprobability : FTRL.finiteSimplex arms probability) : halfTsallisPotentialMass arms probability - 1 <= 2 * (arms.erase best).sum (fun action => Real.sqrt (probability action) - probability action / 2)

Generated pathwise point-mass penalty with every reciprocal-rate increment retained and every potential mass replaced by its refined suboptimal-arm upper bound.

theorem sum_sampledScheduledHalfTsallisPotentialPenalty_pointMass_le_refined {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (sample : Env × ((k : Nat) -> Action × Real)) {best : Action} (hbest : best ∈ arms) (n : Nat) (heta : forall t, t <= n -> 0 < eta t) (hetaMono : forall t, t < n -> eta (t + 1) <= eta t) : (Finset.range (n + 1)).sum (fun t => sampledScheduledHalfTsallisPotentialPenaltyAtTime arms harms eta (pointMass best) sample t) <= 2 / eta 0 * (arms.erase best).sum (fun action => Real.sqrt (sampledScheduledHalfTsallisProbabilityAtTime arms harms eta 0 sample action) - sampledScheduledHalfTsallisProbabilityAtTime arms harms eta 0 sample action / 2) + (Finset.range n).sum (fun t => 2 * (1 / eta (t + 1) - 1 / eta t) * (arms.erase best).sum (fun action => Real.sqrt (sampledScheduledHalfTsallisProbabilityAtTime arms harms eta (t + 1) sample action) - sampledScheduledHalfTsallisProbabilityAtTime arms harms eta (t + 1) sample action / 2))

Refined suboptimal-arm mass on one generated trajectory sample.

noncomputable def sampledScheduledHalfTsallisRefinedSuboptimalMassAt {Env : Type u} {Action : Type v} [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (best : Action) (t : Nat) (sample : Env × ((k : Nat) -> Action × Real)) : Real

Deterministic Jensen target for one refined suboptimal-arm mass.

noncomputable def sampledScheduledHalfTsallisExpectedRefinedSuboptimalMassAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) (best : Action) (t : Nat) : Real

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

theorem integrable_sampledScheduledHalfTsallisRefinedSuboptimalMassAt {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : Measure (Env × ((k : Nat) -> Action × Real))) [IsFiniteMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat -> Real) {best : Action} (t : Nat) : Integrable (sampledScheduledHalfTsallisRefinedSuboptimalMassAt arms harms eta best t) mu

Jensen transport for the complete refined suboptimal-arm mass at one scheduled time.

theorem integral_sampledScheduledHalfTsallisRefinedSuboptimalMassAt_le_expected {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) {best : Action} (t : Nat) : integral mu (sampledScheduledHalfTsallisRefinedSuboptimalMassAt arms harms eta best t) <= sampledScheduledHalfTsallisExpectedRefinedSuboptimalMassAt mu arms harms eta best t

The generated predictable environment regret retains the refined time-varying penalty after expectation. Unlike the coarse endpoint theorem, no terminal potential mass divided by the final learning rate remains.

theorem integral_sampledScheduledHalfTsallisPredictableEnvironmentRegret_pointMass_le_refinedExpectedPenalty {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 : forall t, t <= horizon -> 0 < eta t) (hetaMono : forall t, t < horizon -> eta (t + 1) <= eta t) : let selector := canonicalHalfTsallisScheduleGeneratedSelectorMeasurability arms harms eta loss let mu := prior ⊗ₘ sampledScheduledHalfTsallisTrajectoryKernel arms harms eta selector.finiteHistory loss.environment integral mu (sampledScheduledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon) <= integral mu (fun sample => (Finset.range (horizon + 1)).sum (fun t => sampledScheduledHalfTsallisAllRatePotentialStabilityBoundAtTime arms harms eta sample t)) + 2 / eta 0 * sampledScheduledHalfTsallisExpectedRefinedSuboptimalMassAt mu arms harms eta best 0 + (Finset.range horizon).sum (fun t => 2 * (1 / eta (t + 1) - 1 / eta t) * sampledScheduledHalfTsallisExpectedRefinedSuboptimalMassAt mu arms harms eta best (t + 1))