Part IV — Lower Bounds for Bandits with Finitely Many Arms

Chapter 16: Instance-Dependent Lower Bounds

Definition 16.1, Theorem 16.2, Lemma 16.3, and Theorem 16.4 are source-frozen. Generic consistency, d_inf, Gaussian-candidate, eventual power, and eventual log-growth leaves compile; the bandit information, liminf, and finite-time terminals remain blocked.

PartialPrinted pp. 177–184PDF pp. 215–223

Source map

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

Chapter DOI. 10.1017/9781108571401.021 · CUP chapter page

Chapter opening (CUP p. 177 / author-online p. 206 / PDF p. 215)
§16.1 Asymptotic Bounds (CUP pp. 177–179 / author-online pp. 207–208 / PDF pp. 216–217; Definition 16.1 and Theorem 16.2)
§16.2 Finite-Time Bounds (CUP p. 180 / author-online pp. 209–210 / PDF pp. 218–219; Lemma 16.3 and Theorem 16.4)
§16.3 Notes (CUP p. 181 / author-online p. 210 / PDF p. 219)
§16.4 Bibliographic Remarks (CUP p. 181 / author-online p. 211 / PDF p. 220)
§16.5 Exercises (CUP pp. 181–184 / author-online pp. 211–214 / PDF pp. 220–223)

Open the formal PDF

Learning goals

Read consistency with its exact quantifier order: every environment and every real exponent p greater than zero.
Keep d_inf extended-real, the confusing alternative strictly better, and KL directed from the original arm law to the alternative.
Trace how consistency controls log(R_n(nu)+R_n(nu-prime))/log(n) before the liminf extraction.
Separate Theorem 16.2's asymptotic product-class result from Lemma 16.3 and Theorem 16.4's finite-time Gaussian route.

Necessary definitions and statements

Policy consistency (Definition 16.1)

Compiled

Policy consistency (Definition 16.1). One policy is consistent over the class when its regret is smaller than every positive polynomial order on every environment.\[\forall \nu\in\mathcal E\;\forall p>0:\quad \lim_{n\to\infty}\frac{R_n(\pi,\nu)}{n^p}=0.\]

Distribution-class information cost

Compiled

Distribution-class information cost. The information cost is the least original-to-alternative KL among laws in the class whose mean is strictly above the target mean.\[d_{\inf}(P,\mu^*,\mathcal M)=\inf\{D(P\Vert P'):\;P'\in\mathcal M,\;\mu(P')>\mu^*\}.\]

Per-arm asymptotic information constraint

Blocked

Per-arm asymptotic information constraint. A consistent policy must sample each suboptimal arm at a logarithmic rate set by the cheapest confusing alternative.\[\liminf_{n\to\infty}\frac{\mathbb E_{\nu,\pi}[T_i(n)]}{\log n}\ge\frac{1}{d_{\inf}(P_i,\mu^*,\mathcal M_i)}.\]

Finite-time Gaussian lower-bound shape

Blocked

Finite-time Gaussian lower-bound shape. Under the local C times n to the p regret envelope, the Gaussian lower bound sums the positive part of one explicit logarithmic term per suboptimal arm.\[R_n(\pi,\nu)\ge\frac{2}{(1+\varepsilon)^2}\sum_{i:\Delta_i>0}\left(\frac{(1-p)\log n+\log(\varepsilon\Delta_i/(8C))}{\Delta_i}\right)^+.\]

proof pseudocode

Instance-dependent lower-bound proof flow

Freeze consistency
Require R_n(pi,nu)/n^p to converge to zero for every environment in the class and every real p>0.
Choose a confusing alternative
Change one suboptimal arm to a law in its component class whose mean is strictly above the original optimal mean and whose original-to-alternative KL approaches d_inf.
Lift arm KL to history KL
Use the compiled one-common-policy Lemma 15.1 identity to obtain the original-law realized expected pull-count cost.
Test the pull event
Apply Bretagnolle–Huber to A={T_i(n)>n/2}, preserving the event complement and the two environment-specific regrets.
Extract the rate
Use the compiled consistency power/log leaves, then take the required liminf and sum gap times expected pulls; the bandit terminal remains blocked.
Specialize finite time
For Theorem 16.4 shift a Gaussian mean by Delta_i(1+epsilon), apply Lemma 16.3, and retain the exact positive part and factor 2/(1+epsilon)^2.

Key source theorem and boundary

Source theorem · faithful restatement

Definition 16.1, Theorem 16.2, Lemma 16.3, and Theorem 16.4

Blocked

Chapter 16 turns one-arm change of measure into asymptotic and finite-time instance-dependent regret obstructions.

Definition 16.1, Theorem 16.2, Lemma 16.3, and Theorem 16.4. A consistent policy pays the source d_inf logarithmic constant on every unstructured instance; under the finite-time local Gaussian envelope, an explicit positive-part lower bound holds at every selected horizon.\[\liminf_{n\to\infty}\frac{R_n(\pi,\nu)}{\log n}\ge\sum_{i:\Delta_i>0}\frac{\Delta_i}{d_{\inf}(P_i,\mu^*,\mathcal M_i)},\qquad R_n(\pi,\nu)\ge\frac{2}{(1+\varepsilon)^2}\sum_{i:\Delta_i>0}\left(\frac{(1-p)\log n+\log(\varepsilon\Delta_i/(8C))}{\Delta_i}\right)^+.\]

Lean boundary. The generic consistency, d_inf, Gaussian-candidate, power, log-growth, and Chapter 15 history-KL leaves compile. The Chapter 16 one-arm information consumer, exact d_inf-to-liminf bandit bridge, Lemma 16.3, and both regret terminals do not.

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.IsConsistentRegret`	Compiled	Exact scalar every-positive-real-power consistency predicate. Exact compact Lean statement `def IsConsistentRegret (regret : Nat -> Real) : Prop`
`BanditRLProof.LowerBounds.IsConsistentPolicyOver`	Compiled	Generic environment-class wrapper preserving the source quantifier order. Exact compact Lean statement `def IsConsistentPolicyOver {Policy Environment : Type*} (environmentClass : Set Environment) (regret : Policy -> Environment -> Nat -> Real) (policy : Policy) : Prop`
`BanditRLProof.LowerBounds.IsConsistentRegret.add`	Compiled	Closure for the two-environment regret sum used by Theorem 16.2. Exact compact Lean statement `theorem IsConsistentRegret.add {first second : Nat -> Real} (hfirst : IsConsistentRegret first) (hsecond : IsConsistentRegret second) : IsConsistentRegret (fun n => first n + second n)`
`BanditRLProof.LowerBounds.IsConsistentRegret.eventually_add_le_rpow`	Compiled	Every positive polynomial eventually dominates the regret sum. Exact compact Lean statement `theorem IsConsistentRegret.eventually_add_le_rpow {first second : Nat -> Real} (hfirst : IsConsistentRegret first) (hsecond : IsConsistentRegret second) {p : Real} (hp : 0 < p) : ∀ᶠ n : Nat in atTop, first n + second n <= (n : Real) ^ p`
`BanditRLProof.LowerBounds.IsConsistentRegret.eventually_log_add_div_log_le`	Compiled	Direction-correct eventual logarithmic growth bound before the limsup step. Exact compact Lean statement `theorem IsConsistentRegret.eventually_log_add_div_log_le {first second : Nat -> Real} (hfirst : IsConsistentRegret first) (hsecond : IsConsistentRegret second) (hpositive : ∀ᶠ n : Nat in atTop, 0 < first n + second n) {p : Real} (hp : 0 < p) : ∀ᶠ n : Nat in atTop, Real.log (first n + second n) / Real.log n <= p`
`BanditRLProof.LowerBounds.divergenceInfimum`	Compiled	Extended-real distribution-class d_inf with strict mean improvement. Exact compact Lean statement `def divergenceInfimum {Reward : Type*} [MeasurableSpace Reward] (P : Measure Reward) (muStar : Real) (distributionClass : Set (Measure Reward)) (mean : Measure Reward -> Real) : ENNReal`
`BanditRLProof.LowerBounds.divergenceInfimum_le`	Compiled	Any confusing alternative upper-bounds d_inf in the original-to-alternative KL direction. Exact compact Lean statement `theorem divergenceInfimum_le {Reward : Type*} [MeasurableSpace Reward] {P P' : Measure Reward} {muStar : Real} {distributionClass : Set (Measure Reward)} {mean : Measure Reward -> Real} (hclass : P' ∈ distributionClass) (hbetter : muStar < mean P') : divergenceInfimum P muStar distributionClass mean <= relativeEntropy P P'`
`BanditRLProof.LowerBounds.parametricDivergenceInfimum`	Compiled	Family-indexed form for parametric law classes. Exact compact Lean statement `def parametricDivergenceInfimum {Reward Parameter : Type*} [MeasurableSpace Reward] (law : Parameter -> Measure Reward) (mean : Parameter -> Real) (parameter : Parameter) (muStar : Real) : ENNReal`
`BanditRLProof.LowerBounds.parametricDivergenceInfimum_le`	Compiled	Strictly better parameter candidate inequality. Exact compact Lean statement `theorem parametricDivergenceInfimum_le {Reward Parameter : Type*} [MeasurableSpace Reward] {law : Parameter -> Measure Reward} {mean : Parameter -> Real} {parameter alternative : Parameter} {muStar : Real} (hbetter : muStar < mean alternative) : parametricDivergenceInfimum law mean parameter muStar <= relativeEntropy (law parameter) (law alternative)`
`BanditRLProof.LowerBounds.unitGaussianDivergenceInfimum`	Compiled	Unit-variance Gaussian parametric d_inf interface. Exact compact Lean statement `abbrev unitGaussianDivergenceInfimum (mu muStar : Real) : ENNReal`
`BanditRLProof.LowerBounds.unitGaussianDivergenceInfimum_le_perturbed`	Compiled	Exact cost of the candidate mean muStar+epsilon; no exact infimum equality is claimed. Exact compact Lean statement `theorem unitGaussianDivergenceInfimum_le_perturbed (mu muStar epsilon : Real) (hepsilon : 0 < epsilon) : unitGaussianDivergenceInfimum mu muStar <= ENNReal.ofReal (((muStar - mu) + epsilon) ^ 2 / 2)`
`BanditRLProof.LowerBounds.consistentPolicy_liminf_expectedRegret_div_log_ge`	Blocked	Reserved exact Theorem 16.2 terminal; no declaration is claimed.No local declaration is indexed.
`BanditRLProof.LowerBounds.expectedPullCount_ge_log_regret_changeOfMeasure`	Blocked	Reserved exact Lemma 16.3 terminal; no declaration is claimed.No local declaration is indexed.
`BanditRLProof.LowerBounds.gaussianExpectedRegret_ge_finiteTimeInstanceDependent`	Blocked	Reserved exact Theorem 16.4 terminal; no declaration is claimed.No local declaration is indexed.

Dependency graph

ch14Chapter 14 event testingCompiled

ch15-gaussianChapter 15 unit-Gaussian arm KLCompiled

consistencyDefinition 16.1 consistency and log growthCompiled

dinfextended-real d_inf and candidate inequalitiesCompiled

gaussian-dinfexact Gaussian d_inf equalityPartial

historysame-policy history KL identityCompiled

asymptoticTheorem 16.2 liminf regret terminalBlocked

finiteLemma 16.3 and Theorem 16.4Blocked

Reading path

Read Definition 16.1 and verify the order forall environment, forall real p>0.
Read d_inf and Theorem 16.2 with strict alternative mean, original-to-alternative KL, and an unstructured product class.
Trace the source event A={T_i(n)>n/2}, the two regret laws, and the compiled subpolynomial log-growth adapter.
Read Lemma 16.3 before Theorem 16.4 and preserve the unit-Gaussian local class, selected horizon set, constants, and positive part.
Treat the Chapter 16 one-arm history-information consumer, liminf, and finite-time terminals as blockers, not as consequences of the compiled Chapter 15 identity or analytic interfaces.

Strict status and remaining gaps

The Chapter 16 one-arm original-law expected-pull information consumer and measurable event bridge built from the compiled Chapter 15 identity.
The exact Gaussian d_inf equality with empty, zero, finite, and infinite information branches.
Theorem 16.2's per-arm and summed liminf terminal, Lemma 16.3, and Theorem 16.4.