Part IV — Lower Bounds for Bandits with Finitely Many Arms

Chapter 17: High-Probability Lower Bounds

All Chapter 17 body endpoints pass the full Lean/Tests/harness gate, including same-policy hard-law coupling and deterministic matrix extraction; integrated into main via PR #101. Approved corrections: Claim 17.6 uses T_i ≤ n/2; Theorem 17.4 uses 0 < δ ≤ 1/32 with c=1/160, C=64 and a strict CDF tail. This is corrected-chapter closure, not a proof of the unchanged printed statements or every optional exercise.

CompiledPrinted pp. 185–190PDF pp. 224–230

Source map

Bandit Algorithms, Tor Lattimore and Csaba Szepesvári, Cambridge University Press (2020), DOI 10.1017/9781108571401.

Chapter DOI. 10.1017/9781108571401.022 · CUP chapter page

§17.1 Stochastic Bandits (CUP pp. 186–188 / author-online pp. 216–218 / PDF pp. 225–227)
§17.2 Adversarial Bandits (CUP pp. 188–190 / author-online pp. 218–220 / PDF pp. 227–229)
§17.3 Notes (CUP p. 190 / author-online p. 220 / PDF p. 229)
§17.4 Bibliographic Remarks (CUP p. 190 / author-online p. 220 / PDF p. 229)
§17.5 Exercises (CUP p. 190 / author-online p. 221 / PDF p. 230)

Open Chapter 17 at PDF p. 224

Learning goals

Distinguish deterministic expected regret, stochastic random pseudo-regret, and adversarial random regret.
Preserve each probability direction, confidence quantifier, logarithm, square root, and constant in Theorem 17.1 and Corollaries 17.2–17.3.
Understand why Theorem 17.4 first randomizes a bounded reward matrix and then extracts one deterministic matrix with Claim 17.5.
Track the shared Gaussian noise, clipping count, pull-small event, and pathwise regret comparison without inventing independence across arms.

Necessary definitions and statements

Stochastic random pseudo-regret

Compiled

Stochastic random pseudo-regret. Formula renderer unavailable; readable fallback: Random pseudo-regret is the sum of each gap times its random pull count.\[\bar R_n=\sum_{i=1}^k T_i(n)\Delta_i.\]

Theorem 17.1 threshold

Compiled

Theorem 17.1 threshold. Formula renderer unavailable; readable fallback: One quarter multiplies the minimum of the horizon and the confidence-dependent expected-regret tradeoff.\[b_{17.1}=\frac14\min\left\{n,\frac1B\sqrt{(k-1)n}\log\frac1{4\delta}\right\}.\]

Corollary 17.2 threshold

Compiled

Corollary 17.2 threshold. Formula renderer unavailable; readable fallback: The minimax stochastic threshold keeps one half inside the square root and one quarter outside the whole minimum.\[b_{17.2}=\frac14\min\left\{n,\sqrt{\frac{n(k-1)}2\log\frac1{4\delta}}\right\}.\]

Theorem 17.4 adversarial threshold

Compiled

Theorem 17.4 adversarial threshold. Formula renderer unavailable; readable fallback: The adversarial random-regret obstruction scales as a universal constant times the square root of horizon, arms, and the log confidence penalty.\[b_{17.4}=c\sqrt{nk\log\frac1{2\delta}}.\]

Claim 17.5 first-moment witness

Compiled

Claim 17.5 first-moment witness. Formula renderer unavailable; readable fallback: If the average tail probability over random reward matrices is at least delta, at least one deterministic matrix has tail probability at least delta.\[\mathbb E_Q[1-F_X(u)]\ge\delta\;\Longrightarrow\;\exists x:\;1-F_x(u)\ge\delta.\]

Equation (17.8) regret bridge

Compiled

Equation (17.8) regret bridge. Formula renderer unavailable; readable fallback: Random regret is at least the gap times the rounds that neither pull the hard arm nor hit a clipping boundary.\[\widehat R_n\ge\Delta\left(n-T_i(n)-\sum_{t=1}^n\mathbf 1\{\exists j:\,X_{tj}\in\{0,1\}\}\right).\]

proof pseudocode

Source-faithful stochastic and adversarial routes

Stochastic: select the least-pulled alternative arm
Use the uniform expected-regret envelope to control one arm among i>1, then raise only its Gaussian mean by 2Δ.
Stochastic: compare the two history laws
Apply Bretagnolle–Huber with the compiled original-to-alternative history KL identity under the same randomized policy; this tail-event consumer now compiles in Theorem 17.1.
Stochastic: calibrate Δ and preserve the tail event
Choose the exact minimum in the source and keep the outer quarter, log(1/(4δ)), and probability at least δ.
Adversarial: sample a correlated clipped-normal reward matrix
Share one Gaussian noise variable across arms at each round, while keeping each arm IID across time; do not assume within-round independence.
Adversarial: combine pull and clipping events
Claim 17.6 supplies probability 2δ, Claim 17.7 removes at most δ, and Eq. (17.8) leaves regret at least nΔ/4.
Adversarial: extract a deterministic witness
Apply the compiled Claim 17.5 first-moment theorem to obtain one reward matrix x with the desired random-regret tail.

Key source theorem and boundary

Source theorem · faithful restatement

Theorem 17.1 (stochastic high-probability lower bound)

Original chapter ↗Compiled

A policy whose expected regret is uniformly at most B times the square root of (k−1)n over the Gaussian class must have, on some instance, random pseudo-regret above the exact confidence threshold with probability at least delta.

Theorem 17.1 (stochastic high-probability lower bound). Formula renderer unavailable; readable fallback: The uniform expected-regret premise forces an exact random-pseudo-regret tail obstruction on some unit-Gaussian instance.\[\sup_{\nu\in\mathcal E^k}R_n(\pi,\nu)\le B\sqrt{(k-1)n}\;\Longrightarrow\;\exists\nu\in\mathcal E^k:\;\mathbb P_\nu^\pi\!\left(\bar R_n\ge\frac14\min\left\{n,\frac1B\sqrt{(k-1)n}\log\frac1{4\delta}\right\}\right)\ge\delta.\]

Lean boundary. The theorem's premise is quantified over the full gap-at-most-one Gaussian source class; its witness comes from the embedded unit-cube subfamily. The proof preserves the same randomized policy, original-to-alternative history KL, and original-law expected pulls. The corrected adversarial terminal separately passes focused compilation; full local gates pass.

Lean correspondence

Only declarations that exist in the current index and pass the verified build may render as compiled.

Lean declaration	Status	Role and exact type
`BanditRLProof.LowerBounds.tailAtLeast`	Compiled	Exact greater-than-or-equal tail-event direction. Exact compact Lean statement `def tailAtLeast {Omega : Type*} (quantity : Omega -> Real) (threshold : Real) : Set Omega`
`BanditRLProof.LowerBounds.stochasticHighProbabilityThreshold`	Compiled	Theorem 17.1 threshold with the quarter outside the whole minimum. Exact compact Lean statement `def stochasticHighProbabilityThreshold (horizon alternativeArms : Nat) (B delta : Real) : Real`
`BanditRLProof.LowerBounds.stochasticMinimaxHighProbabilityThreshold`	Compiled	Corollary 17.2 threshold with the half inside the square root. Exact compact Lean statement `def stochasticMinimaxHighProbabilityThreshold (horizon alternativeArms : Nat) (delta : Real) : Real`
`BanditRLProof.LowerBounds.adversarialHighProbabilityThreshold`	Compiled	Theorem 17.4 threshold with log(1/(2δ)). Exact compact Lean statement `def adversarialHighProbabilityThreshold (horizon arms : Nat) (c delta : Real) : Real`
`BanditRLProof.LowerBounds.exists_cdfTail_ge_of_integral_ge`	Compiled	Exact first-moment content of Claim 17.5, with integrability explicit. Exact compact Lean statement `theorem exists_cdfTail_ge_of_integral_ge {Instance : Type*} [MeasurableSpace Instance] (Q : Measure Instance) [IsProbabilityMeasure Q] (cdf : Instance -> Real -> Real) (threshold delta : Real) (hIntegrable : Integrable (fun x => 1 - cdf x threshold) Q) (hAverage : delta <= ∫ x, 1 - cdf x threshold ∂Q) : exists x, delta <= 1 - cdf x threshold`
`BanditRLProof.LowerBounds.measureReal_diff_ge_delta`	Compiled	Probability subtraction combining the 2δ pull event and δ clipping event. Exact compact Lean statement `theorem measureReal_diff_ge_delta {Omega : Type} [MeasurableSpace Omega] (P : Measure Omega) [IsFiniteMeasure P] (pullSmall clippingBad : Set Omega) (delta : Real) (hPullSmall : 2 delta <= P.real pullSmall) (hClippingBad : P.real clippingBad <= delta) : delta <= P.real (pullSmall \ clippingBad)`
`BanditRLProof.LowerBounds.adversarialRegretLowerExpression_ge_quarter`	Compiled	Deterministic quarter-horizon consequence after Eq. (17.8). Exact compact Lean statement `theorem adversarialRegretLowerExpression_ge_quarter (horizon pullCount clippingCount : Nat) (gap : Real) (hGap : 0 <= gap) (hPull : (pullCount : Real) <= (horizon : Real) / 2) (hClipping : (clippingCount : Real) <= (horizon : Real) / 4) : gap * ((horizon : Real) / 4) <= adversarialRegretLowerExpression horizon pullCount clippingCount gap`
`BanditRLProof.LowerBounds.randomRegret_ge_quarter_of_clippingDecomposition`	Compiled	Conditional transfer that keeps the construction-specific Eq. (17.8) comparison as a premise. Exact compact Lean statement `theorem randomRegret_ge_quarter_of_clippingDecomposition (horizon pullCount clippingCount : Nat) (gap randomRegret : Real) (hGap : 0 <= gap) (hPull : (pullCount : Real) <= (horizon : Real) / 2) (hClipping : (clippingCount : Real) <= (horizon : Real) / 4) (hSource : adversarialRegretLowerExpression horizon pullCount clippingCount gap <= randomRegret) : gap * ((horizon : Real) / 4) <= randomRegret`
`BanditRLProof.LowerBounds.gaussianRandomPseudoRegret_ge_theorem17_1`	Compiled	Exact Theorem 17.1 premise over the full gap-at-most-one Gaussian source class; unit-cube witness. Exact compact Lean statement theorem gaussianRandomPseudoRegret_ge_theorem17_1 {alternatives horizon : Nat} (halternatives : 0 < alternatives) (hhorizon : 0 < horizon) (B delta : Real) (hB : 0 < B) (hdelta : 0 < delta) (hdelta_one : delta < 1) (algorithm : Thompson.HistoryAlgorithm (Fin (alternatives + 1)) Real) (hExpected : forall environment : GapOneGaussianBanditEnvironment (alternatives + 1), gapOneGaussianExpectedPseudoRegretReal algorithm environment (horizon - 1) <= B * Real.sqrt ((alternatives : Real) * (horizon : Real))) : exists environment : UnitGaussianBanditEnvironment (alternatives + 1), delta <= (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel environment.mean) (horizon - 1)).real (tailAtLeast (gaussianRandomPseudoRegret environment (horizon - 1)) (stochasticHighProbabilityThreshold horizon alternatives B delta))
`BanditRLProof.LowerBounds.gaussianRandomPseudoRegret_ge_corollary17_2`	Compiled	Exact Corollary 17.2 minimax tail under Eq. (17.6). Exact compact Lean statement theorem gaussianRandomPseudoRegret_ge_corollary17_2 {alternatives horizon : Nat} (halternatives : 0 < alternatives) (hhorizon : 0 < horizon) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta < 1) (hside : (horizon : Real) * delta <= Real.sqrt ((horizon : Real) * (alternatives : Real) * Real.log (1 / (4 * delta)))) (algorithm : Thompson.HistoryAlgorithm (Fin (alternatives + 1)) Real) : exists environment : UnitGaussianBanditEnvironment (alternatives + 1), delta <= (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel environment.mean) (horizon - 1)).real (tailAtLeast (gaussianRandomPseudoRegret environment (horizon - 1)) (stochasticMinimaxHighProbabilityThreshold horizon alternatives delta))
`BanditRLProof.LowerBounds.noUniformGaussianRandomPseudoRegretTail_corollary17_3`	Compiled	Exact one-policy/all-horizon/all-confidence Corollary 17.3 impossibility over the full gap-at-most-one Gaussian class. Exact compact Lean statement theorem noUniformGaussianRandomPseudoRegretTail_corollary17_3 {alternatives : Nat} (halternatives : 0 < alternatives) (p B : Real) (hp : 0 < p) (hp_one : p < 1) (hB : 0 < B) : ¬ exists algorithm : Thompson.HistoryAlgorithm (Fin (alternatives + 1)) Real, forall horizon : Nat, 0 < horizon -> forall delta : Real, 0 < delta -> delta < 1 -> forall environment : GapOneGaussianBanditEnvironment (alternatives + 1), (canonicalBanditHistoryMeasure algorithm (unitGaussianKernel environment.mean) (horizon - 1)).real (tailAtLeast (gapOneGaussianRandomPseudoRegret environment (horizon - 1)) (B * Real.sqrt ((alternatives : Real) * (horizon : Real)) * (Real.log (1 / delta)) ^ p)) < delta
`BanditRLProof.LowerBounds.adversarialRandomRegret_ge_eq17_8`	Compiled	Construction-level Eq. (17.8) for shared-noise clipped rewards and max-over-fixed-arms random regret. Exact compact Lean statement `theorem adversarialRandomRegret_ge_eq17_8 {horizon alternatives : Nat} (eta : Fin horizon -> Real) (gap : Real) (hgap : 0 <= gap) (distinguished : Fin alternatives) (actions : Fin horizon -> Fin (alternatives + 1)) : gap * ((horizon : Real) - adversarialPullCountReal actions distinguished - adversarialClippingCountReal eta gap) <= adversarialRandomRegret (adversarialClippedGaussianReward eta gap distinguished) actions`
`BanditRLProof.LowerBounds.adversarialNoiseHistoryJoint_pull_le_half_claim17_6`	Compiled	Compiled; full local gate passed: approved non-strict half-pull event under the same-policy joint law. Exact compact Lean statement `theorem adversarialNoiseHistoryJoint_pull_le_half_claim17_6 {m : Nat} (hm : 0 < m) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (n : Nat) (sigma delta : Real) (hs : sigma ≠ 0) (hd : 0 < delta) (hd8 : delta < 1 / 8) : ∃ i : Fin (m + 1), 2 * delta <= (adversarialNoiseHistoryJoint (horizon := n + 1) algorithm sigma (adversarialClaim17_6Gap (n + 1) m sigma delta) i n).real {p \| finiteHistoryPullCountReal n p.2 i <= ((n + 1 : Nat) : Real) / 2}`
`BanditRLProof.LowerBounds.adversarialFullBoundaryCount_tail_claim17_7`	Compiled	Compiled; full local gate passed: literal full-family boundary clipping count. Exact compact Lean statement `theorem adversarialFullBoundaryCount_tail_claim17_7 {horizon m : Nat} (hn : 0 < horizon) (delta gap : Real) (hd : 0 < delta) (hd1 : delta < 1) (hg : 0 <= gap) (hg8 : gap < 1 / 8) (i : Fin (m + 1)) (horizon_condition : 32 * Real.log (1 / delta) <= horizon) : (adversarialCenteredNoiseLaw horizon (1 / 10)).real {eta \| (horizon : Real) / 4 <= adversarialFullBoundaryCount eta gap i} <= delta`
`BanditRLProof.LowerBounds.integrable_adversarialTableRandomRegret`	Compiled	Compiled; full local gate passed: random regret has a well-defined separate expectation. Exact compact Lean statement `theorem integrable_adversarialTableRandomRegret {m : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (table : AdversarialRewardTable (m + 1)) (n : Nat) : Integrable (adversarialTableRandomRegret table n) (adversarialTableHistoryKernel algorithm n table)`
`BanditRLProof.LowerBounds.adversarialRandomRegret_ge_theorem17_4`	Compiled	Compiled; full local gate passed: corrected strict CDF tail, δ ≤ 1/32, c=1/160, C=64. Exact compact Lean statement theorem adversarialRandomRegret_ge_theorem17_4 {m : Nat} (hm : 0 < m) (algorithm : Thompson.HistoryAlgorithm (Fin (m + 1)) Real) (n : Nat) (delta : Real) (hd : 0 < delta) (hd32 : delta <= 1 / 32) (horizon : 64 * ((m + 1 : Nat) : Real) * Real.log (1 / (2 * delta)) <= ((n + 1 : Nat) : Real)) : ∃ table : AdversarialRewardTable (m + 1), (∀ t arm, table t arm ∈ Set.Icc (0 : Real) 1) ∧ delta <= 1 - adversarialTableCDF algorithm table n (adversarialHighProbabilityThreshold (n + 1) (m + 1) (1 / 160) delta)

Dependency graph

ch13least-pulled alternative armCompiled

ch14Bretagnolle–Huber event testingCompiled

ch15-armunit-Gaussian arm KLCompiled

thresholdsexact Chapter 17 thresholdsCompiled

claim17-5Claim 17.5 first-moment witnessCompiled

historysame-policy adaptive-history KLCompiled

stochasticTheorem 17.1 and Corollaries 17.2–17.3Compiled

cor17-3Corollary 17.3 all-confidence impossibilityCompiled

clipped-lawsame-policy shared-noise joint lawCompiled

claim17-6corrected Claim 17.6Compiled

eq17-8construction-level Eq. (17.8)Compiled

claim17-7Claim 17.7 exact clipping concentrationCompiled

adversarialcorrected Theorem 17.4 deterministic witnessCompiled

Reading path

Start with the chapter opening and keep random regret separate from expected regret.
Read §17.1's definition of random pseudo-regret, then verify Theorem 17.1's uniform premise, outer quarter, and original-to-alternative history comparison.
Read Corollaries 17.2 and 17.3 with their exact horizon-confidence and one-policy/all-confidence quantifiers.
In §17.2, trace the random reward-matrix law, conditional policy interaction, Claim 17.5, and the shared-noise clipped-normal construction.
Finish with Claims 17.6–17.7 and Eq. (17.8), treating the compiled probability and algebra leaves as dependencies rather than terminal proofs.

Strict status and remaining gaps

None recorded.