BanditRLProof.TsallisSelfBounding

Unit mass at one action, used as the fixed optimal-arm comparator.

def pointMass {Action : Type u} [DecidableEq Action] (best : Action) : Action -> Real

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

theorem finiteSimplex_pointMass {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (hbest : best ∈ arms) : FTRL.finiteSimplex arms (pointMass best)

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

theorem linearLoss_pointMass {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (hbest : best ∈ arms) (loss : Action -> Real) : FTRL.linearLoss arms (pointMass best) loss = loss best

One-round regret against a point mass is the probability-weighted gap.

theorem linearLoss_sub_pointMass_eq_gapMass {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (hbest : best ∈ arms) (prob loss gap : Action -> Real) (hprob : FTRL.finiteSimplex arms prob) (hgap : ∀ action ∈ arms, loss action - loss best = gap action) : FTRL.linearLoss arms prob loss - FTRL.linearLoss arms (pointMass best) loss = arms.sum (fun action => prob action * gap action)

Gap mass accumulated by the generated actual-time sampling laws.

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

Paper-facing scalar form of a `(Delta, C, T)` self-bounding constraint.

def HasSelfBoundingRegret (expectedGapMass regret corruption : Real) : Prop

A predictable fixed-gap law identifies environment regret pathwise.

theorem sampledHalfTsallisPredictableEnvironmentRegret_pointMass_eq_gapMass {Env : Type u} {Action : Type v} [MeasurableSpace Env] [MeasurableSpace Action] [DecidableEq Action] (arms : Finset Action) (harms : arms.Nonempty) (eta : Real) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (gap : Action -> Real) (horizon : Nat) (hgap : ∀ t sample action, action ∈ arms -> Exp3.predictableLossAt loss t sample action - Exp3.predictableLossAt loss t sample best = gap action) (sample : Env × ((k : Nat) -> Action × Real)) : sampledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon sample = sampledHalfTsallisPredictableGapMass arms harms eta gap horizon sample

The fixed-gap predictable environment satisfies the integrated self-bounding condition, with any nonnegative corruption allowance.

theorem integral_sampledHalfTsallisPredictableEnvironmentRegret_hasSelfBounding {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 : Real) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (gap : Action -> Real) (horizon : Nat) (hgap : ∀ 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 := canonicalHalfTsallisFiniteHistorySelectorMeasurability arms harms eta let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment HasSelfBoundingRegret (integral mu (sampledHalfTsallisPredictableGapMass arms harms eta gap horizon)) (integral mu (sampledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon)) corruption

Actual generated environment-regret upper bound specialized to the optimal-arm point-mass comparator.

theorem integral_sampledHalfTsallisPredictableEnvironmentRegret_pointMass_le {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 : Real) (heta : 0 < eta) (loss : Exp3.PredictableLossVector Env Action) {best : Action} (hbest : best ∈ arms) (horizon : Nat) : let selector := canonicalHalfTsallisFiniteHistorySelectorMeasurability arms harms eta let mu := prior ⊗ₘ sampledHalfTsallisTrajectoryKernel arms harms eta selector loss.environment integral mu (sampledHalfTsallisPredictableEnvironmentRegret arms harms eta loss (pointMass best) horizon) <= 2 * eta * powerSum arms (1 / 2 : Real) (initialHalfTsallisDistribution arms harms eta) + integral mu (fun sample => (Finset.range horizon).sum (fun n => sampledHalfTsallisHalfPowerBoundAt (Env := Env) arms harms eta n (sampledHalfTsallisHistoryAt n sample))) + ((powerSum arms (1 / 2 : Real) (initialHalfTsallisDistribution arms harms eta) - powerSum arms (1 / 2 : Real) (pointMass best)) / (1 - (1 / 2 : Real))) / eta

Coordinate completion of squares used by the self-bounding conversion.

theorem two_mul_coeff_mul_sqrt_sub_gap_mul_le_sq_div_gap (coeff probability gap : Real) (hprobability : 0 ≤ probability) (hgap : 0 < gap) : 2 * coeff * Real.sqrt probability - gap * probability ≤ coeff ^ 2 / gap

Finite `(Delta, C, T)` self-bounding conversion after a refined upper bound has removed every zero-gap coordinate.

theorem regret_le_two_mul_base_add_sum_sq_div_gap_add_corruption {Index : Type u} (indices : Finset Index) (probability coeff gap : Index -> Real) (regret base corruption : Real) (hprobability : ∀ index ∈ indices, 0 ≤ probability index) (hgap : ∀ index ∈ indices, 0 < gap index) (hselfBounding : indices.sum (fun index => gap index * probability index) - corruption ≤ regret) (hupper : regret ≤ base + indices.sum (fun index => coeff index * Real.sqrt (probability index))) : regret ≤ 2 * base + indices.sum (fun index => coeff index ^ 2 / gap index) + corruption

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

theorem powerSum_pointMass_half {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (hbest : best ∈ arms) : powerSum arms (1 / 2 : Real) (pointMass best) = 1

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

theorem sum_erase_sqrt_pointMass {Action : Type u} [DecidableEq Action] (arms : Finset Action) (best : Action) : (arms.erase best).sum (fun action => Real.sqrt (pointMass best action)) = 0

The existing total half-power budget cannot uniformly be replaced by a suboptimal-arm square-root budget. A refined `(1-p)` factor is genuinely needed before the self-bounding conversion can consume the trajectory bound.

theorem not_forall_powerSum_half_le_sum_erase_sqrt {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (hbest : best ∈ arms) : ¬ ∀ p : Action -> Real, FTRL.finiteSimplex arms p -> powerSum arms (1 / 2 : Real) p ≤ (arms.erase best).sum (fun action => Real.sqrt (p action))