BanditRLProof.TsallisConstrainedQuadraticOptimization

A downward quadratic is bounded by its unconstrained vertex value.

theorem linear_sub_quadratic_le_sq_div_four (b x c : Real) (hc : 0 < c) : b * x - c * x ^ 2 ≤ b ^ 2 / (4 * c)

Coordinatewise completion of squares gives the unconstrained finite-sum branch of the paper's quadratic optimization.

theorem sum_linear_sub_quadratic_le_unconstrained {Index : Type u} [DecidableEq Index] (indices : Finset Index) (b : Real) (c x : Index → Real) (hc : ∀ i ∈ indices, 0 < c i) : indices.sum (fun i => b * x i - c i * x i ^ 2) ≤ b ^ 2 / 4 * indices.sum (fun i => 1 / c i)

If the unconstrained vertex lies beyond a finite `sum x ≤ M` constraint, shift the common linear coefficient and apply completion of squares to obtain the active-constraint branch.

theorem sum_linear_sub_quadratic_le_of_sum_le {Index : Type u} [DecidableEq Index] (indices : Finset Index) (b M : Real) (c x : Index → Real) (hc : ∀ i ∈ indices, 0 < c i) (hreciprocal : 0 < indices.sum (fun i => 1 / c i)) (hxsum : indices.sum x ≤ M) (hthreshold : 2 * M ≤ b * indices.sum (fun i => 1 / c i)) : indices.sum (fun i => b * x i - c i * x i ^ 2) ≤ b * M - M ^ 2 / indices.sum (fun i => 1 / c i)

Positive coefficients on a nonempty finite set have a positive reciprocal sum.

theorem sum_inv_pos_of_nonempty {Index : Type u} [DecidableEq Index] (indices : Finset Index) (hindices : indices.Nonempty) (c : Index → Real) (hc : ∀ i ∈ indices, 0 < c i) : 0 < indices.sum (fun i => 1 / c i)

A finite simplex point has suboptimal square-root mass at most the square root of the number of suboptimal coordinates.

theorem sum_erase_sqrt_le_sqrt_card {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (hbest : best ∈ arms) (probability : Action → Real) (hprobability : FTRL.finiteSimplex arms probability) : (arms.erase best).sum (fun action => Real.sqrt (probability action)) ≤ Real.sqrt ((arms.erase best).card : Real)

The unconstrained one-round branch after substituting `x action = sqrt (probability action)` and `c action = lambda * gap action`.

theorem sum_erase_sqrt_probability_sub_gap_le_unconstrained {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (probability gap : Action → Real) (hprobability : FTRL.finiteSimplex arms probability) (hgap : ∀ action ∈ arms.erase best, 0 < gap action) (b lambda : Real) (hlambda : 0 < lambda) : (arms.erase best).sum (fun action => b * Real.sqrt (probability action) - lambda * gap action * probability action) ≤ b ^ 2 / 4 * (arms.erase best).sum (fun action => 1 / (lambda * gap action))

On the active-constraint branch, finite-simplex square-root mass sharpens the unconstrained coordinatewise bound by the common mass constraint.

theorem sum_erase_sqrt_probability_sub_gap_le_of_threshold {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (hbest : best ∈ arms) (probability gap : Action → Real) (hprobability : FTRL.finiteSimplex arms probability) (hsuboptimal : (arms.erase best).Nonempty) (hgap : ∀ action ∈ arms.erase best, 0 < gap action) (b lambda : Real) (hlambda : 0 < lambda) (hthreshold : 2 * Real.sqrt ((arms.erase best).card : Real) ≤ b * (arms.erase best).sum (fun action => 1 / (lambda * gap action))) : (arms.erase best).sum (fun action => b * Real.sqrt (probability action) - lambda * gap action * probability action) ≤ b * Real.sqrt ((arms.erase best).card : Real) - (arms.erase best).card / (arms.erase best).sum (fun action => 1 / (lambda * gap action))

Generated expected-probability specialization of the unconstrained one-round quadratic branch. All measure and Jensen obligations are discharged by the existing finite-simplex expectation theorem.

theorem sampledScheduledHalfTsallisExpectedProbability_sum_le_unconstrained {Env : Type u} {Action : Type*} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : MeasureTheory.Measure (Env × ((k : Nat) → Action × Real))) [MeasureTheory.IsProbabilityMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat → Real) (t : Nat) {best : Action} (gap : Action → Real) (hgap : ∀ action ∈ arms.erase best, 0 < gap action) (b lambda : Real) (hlambda : 0 < lambda) : (arms.erase best).sum (fun action => b * Real.sqrt (sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action) - lambda * gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action) ≤ b ^ 2 / 4 * (arms.erase best).sum (fun action => 1 / (lambda * gap action))

Generated expected-probability specialization of the active-constraint one-round quadratic branch. This is the direct consumer for the later time-threshold split in the improved self-bounding route.

theorem sampledScheduledHalfTsallisExpectedProbability_sum_le_of_threshold {Env : Type u} {Action : Type*} [MeasurableSpace Env] [MeasurableSpace Action] [MeasurableSingletonClass Action] [DecidableEq Action] (mu : MeasureTheory.Measure (Env × ((k : Nat) → Action × Real))) [MeasureTheory.IsProbabilityMeasure mu] (arms : Finset Action) (harms : arms.Nonempty) (eta : Nat → Real) (t : Nat) {best : Action} (hbest : best ∈ arms) (gap : Action → Real) (hsuboptimal : (arms.erase best).Nonempty) (hgap : ∀ action ∈ arms.erase best, 0 < gap action) (b lambda : Real) (hlambda : 0 < lambda) (hthreshold : 2 * Real.sqrt ((arms.erase best).card : Real) ≤ b * (arms.erase best).sum (fun action => 1 / (lambda * gap action))) : (arms.erase best).sum (fun action => b * Real.sqrt (sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action) - lambda * gap action * sampledScheduledHalfTsallisExpectedProbabilityAt mu arms harms eta t action) ≤ b * Real.sqrt ((arms.erase best).card : Real) - (arms.erase best).card / (arms.erase best).sum (fun action => 1 / (lambda * gap action))