Part IV — Lower Bounds for Bandits with Finitely Many Arms

Chapter 17: High-Probability Lower Bounds

Claim 17.5's first-moment witness and reusable threshold, event-subtraction, and deterministic Eq. (17.8) algebra compile. The stochastic tail terminals and clipped-normal adversarial construction remain blocked.

PartialPrinted 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 the formal PDF

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

Partial

Stochastic random pseudo-regret. 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. 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. 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. 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. 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

Blocked

Equation (17.8) regret bridge. 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; the Chapter 17 tail-event consumer remains open.
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)

Blocked

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). 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 threshold definition and Lemma 15.1 same-policy history KL identity compile, but the theorem does not: its stochastic tail-event consumer and constant assembly remain absent. Corollaries 17.2–17.3 and Theorem 17.4 are also blocked and are not implied by the compiled leaves.

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); it does not prove 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`	Blocked	Reserved exact Theorem 17.1 terminal; no declaration is claimed.No local declaration is indexed.
`BanditRLProof.LowerBounds.gaussianRandomPseudoRegret_ge_corollary17_2`	Blocked	Reserved exact Corollary 17.2 terminal; no declaration is claimed.No local declaration is indexed.
`BanditRLProof.LowerBounds.noUniformGaussianRandomPseudoRegretTail_corollary17_3`	Blocked	Reserved Corollary 17.3 terminal; no declaration is claimed.No local declaration is indexed.
`BanditRLProof.LowerBounds.adversarialRandomRegret_ge_theorem17_4`	Blocked	Reserved exact Theorem 17.4 terminal; no declaration is claimed.No local declaration is indexed.

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.3Blocked

clipped-lawcorrelated clipped-normal reward-matrix lawBlocked

claim17-6Claim 17.6 pull-small eventBlocked

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

claim17-7Claim 17.7 clipping concentrationBlocked

adversarialTheorem 17.4 deterministic adversarial witnessBlocked

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

The Chapter 17 stochastic tail-event consumer built from the compiled Chapter 15 identity.
Theorem 17.1, Corollary 17.2's expectation contradiction, and Corollary 17.3's exact tail integration.
The Borel clipped-normal reward-matrix law with within-round arm dependence and across-time IID.
Claim 17.6's information calculation, construction-level Eq. (17.8), Claim 17.7's exact clipping concentration, and Theorem 17.4.