Lean module · Tsallis-FTRL
BanditRLProof.TsallisRefinedSuboptimalStability
# Refined half-Tsallis stability to suboptimal-arm budgets The paper's refined stability term contains `sum_a sqrt (p a) * (1 - p a)`. This module proves the finite-simplex elimination of one optimal arm and connects that bound to the compiled self-bounding completion-of-squares consumer. Producing the refined all-arm stability bound from the generated algorithm is separate: it requires the conjugate-potential stability estimate and the time-varying penalty route, rather than the existing fixed-learning-rate `<p_t - p_(t+1), hatLoss_t>` upper bound.
Module map
Imports
BanditRLProof.TsallisSelfBounding
Imported by
BanditRLProof, BanditRLProof.TsallisOracleRestartRefinedStabilityTuning, BanditRLProof.TsallisScheduledSuboptimalExpectedBound
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Tsallis.probability_le_sqrt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem probability_le_sqrt (probability : Real) (hprobability : 0 <= probability) (hprobability_le_one : probability <= 1) : probability <= Real.sqrt probability
theorem
BanditRLProof.Tsallis.sqrt_mul_one_sub_le_sqrt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sqrt_mul_one_sub_le_sqrt (probability : Real) (hprobability : 0 <= probability) : Real.sqrt probability * (1 - probability) <= Real.sqrt probability
theorem
BanditRLProof.Tsallis.sqrt_mul_one_sub_le_one_sub
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem sqrt_mul_one_sub_le_one_sub (probability : Real) (hprobability_le_one : probability <= 1) : Real.sqrt probability * (1 - probability) <= 1 - probability
theorem
BanditRLProof.Tsallis.one_sub_eq_sum_erase
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem one_sub_eq_sum_erase {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (hbest : best ∈ arms) (probability : Action -> Real) (hprobability : FTRL.finiteSimplex arms probability) : 1 - probability best = (arms.erase best).sum probability
theorem
BanditRLProof.Tsallis.sum_sqrt_mul_one_sub_le_two_mul_sum_erase_sqrt
Compiled
Eliminate one distinguished arm from the paper's refined half-power stability budget.
theorem sum_sqrt_mul_one_sub_le_two_mul_sum_erase_sqrt {Action : Type u} [DecidableEq Action] (arms : Finset Action) {best : Action} (hbest : best ∈ arms) (probability : Action -> Real) (hprobability : FTRL.finiteSimplex arms probability) : arms.sum (fun action => Real.sqrt (probability action) * (1 - probability action)) <= 2 * (arms.erase best).sum (fun action => Real.sqrt (probability action))
theorem
BanditRLProof.Tsallis.regret_le_of_refinedHalfPowerSelfBounding
Compiled
A finite time-by-suboptimal-arm consumer for the paper-shaped refined stability budget. The remaining algorithmic obligation is exactly `hupper`.
theorem regret_le_of_refinedHalfPowerSelfBounding {Time : Type u} {Action : Type v} [DecidableEq Time] [DecidableEq Action] (times : Finset Time) (arms : Finset Action) {best : Action} (hbest : best ∈ arms) (probability : Time -> Action -> Real) (coefficient : Time -> Real) (gap : Action -> Real) (regret base corruption : Real) (hprobability : ∀ time ∈ times, FTRL.finiteSimplex arms (probability time)) (hcoefficient : ∀ time ∈ times, 0 <= coefficient time) (hgap : ∀ action ∈ arms.erase best, 0 < gap action) (hselfBounding : times.sum (fun time => (arms.erase best).sum (fun action => gap action * probability time action)) - corruption <= regret) (hupper : regret <= base + times.sum (fun time => coefficient time * arms.sum (fun action => Real.sqrt (probability time action) * (1 - probability time action)))) : regret <= 2 * base + (times.product (arms.erase best)).sum (fun index => (2 * coefficient index.1) ^ 2 / gap index.2) + corruption