BanditRLProof.TsallisRefinedImportanceWeightedMoment

Inverse-half-Tsallis-Hessian quadratic moment after subtracting a baseline.

noncomputable def shiftedHalfPowerImportanceWeightedMoment {Action : Type u} (arms : Finset Action) (prob loss : Action -> Real) (chosen : Action) : Real

Positive cubic remainder used by the refined Taylor bound.

noncomputable def shiftedPositiveCubicImportanceWeightedMoment {Action : Type u} (arms : Finset Action) (prob loss : Action -> Real) (chosen : Action) : Real

Reindex a weighted sum over complements using simplex normalization.

theorem sum_mul_sum_erase_eq_sum_mul_one_sub {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob weight : Action -> Real) (hsum : arms.sum prob = 1) : arms.sum (fun chosen => prob chosen * (arms.erase chosen).sum weight) = arms.sum (fun action => weight action * (1 - prob action))

Exact sampled-action expansion of the shifted quadratic moment.

theorem prob_mul_shiftedHalfPowerImportanceWeightedMoment_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) {chosen : Action} (hchosen : chosen ∈ arms) (hprob : 0 < prob chosen) : prob chosen * shiftedHalfPowerImportanceWeightedMoment arms prob loss chosen = (loss chosen) ^ 2 * (Real.sqrt (prob chosen) * (1 - prob chosen) ^ 2 + prob chosen * (arms.erase chosen).sum (fun action => Real.sqrt (prob action) * prob action))

The sampled shifted quadratic IW moment is bounded by the refined all-arm half-power mass.

theorem sum_prob_mul_shiftedHalfPowerImportanceWeightedMoment_le {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) (hprobability : FTRL.finiteSimplex arms prob) (hprob : forall action, action ∈ arms -> 0 < prob action) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) : arms.sum (fun chosen => prob chosen * shiftedHalfPowerImportanceWeightedMoment arms prob loss chosen) <= arms.sum (fun action => Real.sqrt (prob action) * (1 - prob action))

Exact sampled-action expansion of the positive cubic remainder.

theorem prob_mul_shiftedPositiveCubicImportanceWeightedMoment_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) {chosen : Action} (hchosen : chosen ∈ arms) (hprob : 0 < prob chosen) (hprobLeOne : prob chosen <= 1) (hlossNonneg : 0 <= loss chosen) : prob chosen * shiftedPositiveCubicImportanceWeightedMoment arms prob loss chosen = prob chosen * (loss chosen) ^ 3 * (arms.erase chosen).sum (fun action => (prob action) ^ 2)

The sampled positive cubic IW remainder is at most one.

theorem sum_prob_mul_shiftedPositiveCubicImportanceWeightedMoment_le_one {Action : Type u} [DecidableEq Action] (arms : Finset Action) (prob loss : Action -> Real) (hprobability : FTRL.finiteSimplex arms prob) (hprob : forall action, action ∈ arms -> 0 < prob action) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) : arms.sum (fun chosen => prob chosen * shiftedPositiveCubicImportanceWeightedMoment arms prob loss chosen) <= 1

Paper-shaped finite-sum consumer for a shifted Taylor/Hessian stability bound. The remaining hypothesis is deliberately pointwise: a producer must compare its instantaneous stability quantity with the shifted quadratic and positive cubic moments. This theorem performs all sampled-action averaging.

theorem sum_prob_mul_stability_le_refinedHalfPower_add_square {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (prob loss stability : Action -> Real) (heta : 0 <= eta) (hprobability : FTRL.finiteSimplex arms prob) (hprob : forall action, action ∈ arms -> 0 < prob action) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) (hpointwise : forall chosen, chosen ∈ arms -> stability chosen <= eta / 2 * shiftedHalfPowerImportanceWeightedMoment arms prob loss chosen + eta ^ 2 / 2 * shiftedPositiveCubicImportanceWeightedMoment arms prob loss chosen) : arms.sum (fun chosen => prob chosen * stability chosen) <= eta / 2 * arms.sum (fun action => Real.sqrt (prob action) * (1 - prob action)) + eta ^ 2 / 2

Exact current-FTRL-expression wrapper around the shifted-moment consumer. The sole unresolved premise is the deterministic shifted Taylor/Hessian comparison for each sampled-action update.

theorem sum_prob_mul_linearLoss_sub_next_importanceWeightedLoss_le_refined_of_shiftedTaylor {Action : Type u} [DecidableEq Action] (arms : Finset Action) (eta : Real) (prob loss : Action -> Real) (next : Action -> Action -> Real) (heta : 0 <= eta) (hprobability : FTRL.finiteSimplex arms prob) (hprob : forall action, action ∈ arms -> 0 < prob action) (hloss : forall action, action ∈ arms -> 0 <= loss action ∧ loss action <= 1) (hshiftedTaylor : forall chosen, chosen ∈ arms -> FTRL.linearLoss arms prob (Exp3.importanceWeightedLoss prob loss chosen) - FTRL.linearLoss arms (next chosen) (Exp3.importanceWeightedLoss prob loss chosen) <= eta / 2 * shiftedHalfPowerImportanceWeightedMoment arms prob loss chosen + eta ^ 2 / 2 * shiftedPositiveCubicImportanceWeightedMoment arms prob loss chosen) : arms.sum (fun chosen => prob chosen * (FTRL.linearLoss arms prob (Exp3.importanceWeightedLoss prob loss chosen) - FTRL.linearLoss arms (next chosen) (Exp3.importanceWeightedLoss prob loss chosen))) <= eta / 2 * arms.sum (fun action => Real.sqrt (prob action) * (1 - prob action)) + eta ^ 2 / 2