Lean module · Tsallis-FTRL
BanditRLProof.TsallisImportanceWeightedMoment
# Tsallis importance-weighted power moments This module isolates the finite-sum power-moment calculation used by the Tsallis-INF stability analysis. The sampled importance-weighted loss is weighted by the inverse Hessian scale `p^(2 - alpha)`. Taking the finite sum weighted by the sampling masses gives exactly the power-weighted second moment `sum_i loss_i^2 * p_i^(1 - alpha)`. The result is deterministic finite-sum algebra. It does not prove the preceding Hessian/conjugate-potential stability inequality, identify a conditional action law, or establish a regret theorem.
Module map
Imports
BanditRLProof.Exp3ImportanceWeighted, BanditRLProof.TsallisRegularizer
Imported by
BanditRLProof, BanditRLProof.TsallisFTRLOneStepStability, BanditRLProof.TsallisRefinedImportanceWeightedMoment
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Tsallis.powerWeightedSquaredImportanceWeightedLoss
Compiled
The inverse-Hessian-weighted square of one sampled loss estimate.
noncomputable def powerWeightedSquaredImportanceWeightedLoss {Action : Type u} (arms : Finset Action) (alpha : Real) (prob loss : Action -> Real) (chosen : Action) : Real
theorem
BanditRLProof.Tsallis.powerWeightedSquaredImportanceWeightedLoss_eq_selected
Compiled
Pathwise power-moment identity: only the sampled coordinate remains.
theorem powerWeightedSquaredImportanceWeightedLoss_eq_selected {Action : Type u} [DecidableEq Action] (arms : Finset Action) (alpha : Real) (prob loss : Action -> Real) (chosen : Action) (hchosen : chosen ∈ arms) (hprob : 0 < prob chosen) : powerWeightedSquaredImportanceWeightedLoss arms alpha prob loss chosen = (loss chosen) ^ 2 * (prob chosen) ^ (-alpha)
theorem
BanditRLProof.Tsallis.sum_prob_mul_powerWeightedSquaredImportanceWeightedLoss_eq
Compiled
The sampling-mass-weighted finite sum equals the power-weighted loss square.
theorem sum_prob_mul_powerWeightedSquaredImportanceWeightedLoss_eq {Action : Type u} [DecidableEq Action] (arms : Finset Action) (alpha : Real) (prob loss : Action -> Real) (hprob : forall action, action ∈ arms -> 0 < prob action) : arms.sum (fun chosen => prob chosen * powerWeightedSquaredImportanceWeightedLoss arms alpha prob loss chosen) = arms.sum (fun action => (loss action) ^ 2 * (prob action) ^ (1 - alpha))
theorem
BanditRLProof.Tsallis.sum_prob_mul_powerWeightedSquaredImportanceWeightedLoss_le_powerSum
Compiled
For losses in `[0,1]`, the Tsallis importance-weighted power moment is bounded by the finite power sum with exponent `1 - alpha`.
theorem sum_prob_mul_powerWeightedSquaredImportanceWeightedLoss_le_powerSum {Action : Type u} [DecidableEq Action] (arms : Finset Action) (alpha : Real) (prob loss : Action -> Real) (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 * powerWeightedSquaredImportanceWeightedLoss arms alpha prob loss chosen) <= powerSum arms (1 - alpha) prob