Part IV — Lower Bounds for Bandits with Finitely Many Arms

Chapter 13: Lower Bounds: Basic Ideas

The Chapter 13 semantic and deterministic slice and Chapter 15 same-policy history KL bridge are compiled. Theorem 13.1 remains blocked on the Gaussian regret/event and caller-free minimax terminal.

PartialPrinted pp. 155–159PDF pp. 189–194

Source map

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

§13.1 Main Ideas Underlying Minimax Lower Bounds (CUP starts p. 155 / author-online pp. 181–182 / PDF pp. 190–191)
§13.2 Notes (CUP p. 158 / author-online p. 183 / PDF p. 192)
§13.3 Bibliographic Remarks (CUP p. 158 / author-online p. 184 / PDF p. 193)
§13.4 Exercises (CUP p. 159 / author-online pp. 184–185 / PDF pp. 193–194)

Open the formal PDF

Learning goals

Read worst-case and minimax expected regret as explicit supremum and infimum operations.
Derive a least-explored alternative arm from the exact expected pull-count budget.
Separate the deterministic two-environment regret algebra from the missing statistical change-of-measure bridge.
Understand why Theorem 13.1 is source-stated here but cannot be marked compiled before the Chapter 15 terminal.

Necessary definitions and statements

Worst-case and minimax expected regret

Compiled

Worst-case and minimax expected regret. The minimax value is the infimum over policies of their worst expected regret over the environment class.\[R_n^*(\mathcal E)=\inf_{\pi}\sup_{\nu\in\mathcal E}R_n(\pi,\nu).\]

Least-explored alternative

Compiled

Least-explored alternative. Among the m alternatives, at least one is pulled no more than the average n divided by m.\[\sum_{a=0}^{m}\mathbb E[T_a(n)]=n\Longrightarrow\exists i\in\{1,\ldots,m\}:\mathbb E[T_i(n)]\le n/m.\]

Two-environment algebra

Compiled

Two-environment algebra. A quantitative upper bound on the pull-count discrepancy leaves a matching error term in the two-environment regret lower bound.\[x-y\le\varepsilon\Longrightarrow\max\{\Delta(n-x),\Delta y\}\ge\tfrac{\Delta(n-\varepsilon)}{2}.\]

proof pseudocode

Minimal source-change proof flow

Choose the base instance
Give arm zero mean Delta and every alternative mean zero.
Find a lightly sampled alternative
Use the expected pull budget to choose i.succ with expected count at most n/m.
Change one source
Raise only that alternative mean to 2 Delta; keep the policy fixed.
Write both regret expressions
Expose the base identity and changed-environment lower expression without identifying their expectations.
Defer indistinguishability
A same-policy history-law KL/change-of-measure theorem must supply a quantitative pull-count discrepancy error before the minimax conclusion can follow.

Key source theorem and boundary

Source theorem · faithful restatement

Theorem 13.1 (source statement; proof deferred to Chapter 15)

Blocked

The source states the finite-arm Gaussian minimax order here and explicitly postpones its proof to Chapter 15.

Theorem 13.1 (source statement; proof deferred to Chapter 15). For unit-variance k-armed Gaussian bandits with means in the unit cube, minimax regret is at least a universal constant times the square root of k times n.\[\exists c>0\;\forall k>1\;\forall n\ge k:\quad R_n^*(\mathcal E^k)\ge c\sqrt{kn},\]

Lean boundary. No local Lean declaration is presented as Theorem 13.1. The compiled declarations below cover only the Chapter 13 semantic and deterministic conversion window.

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.worstCaseExpectedRegret`	Compiled	Worst-case ENNReal supremum over an explicit environment class. Exact compact Lean statement `noncomputable def worstCaseExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (environmentClass : Set Environment) (policy : Policy) : ENNReal`
`BanditRLProof.LowerBounds.minimaxExpectedRegret`	Compiled	Minimax ENNReal infimum over an explicit policy class. Exact compact Lean statement `noncomputable def minimaxExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) : ENNReal`
`BanditRLProof.LowerBounds.expectedRegret_le_worstCaseExpectedRegret`	Compiled	One member is below the class supremum. Exact compact Lean statement `theorem expectedRegret_le_worstCaseExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (environmentClass : Set Environment) (policy : Policy) (environment : Environment) (henvironment : environment ∈ environmentClass) : regret policy environment ≤ worstCaseExpectedRegret regret environmentClass policy`
`BanditRLProof.LowerBounds.minimaxExpectedRegret_le_worstCaseExpectedRegret`	Compiled	The infimum is below every admissible policy value. Exact compact Lean statement `theorem minimaxExpectedRegret_le_worstCaseExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) (policy : Policy) (hpolicy : policy ∈ policyClass) : minimaxExpectedRegret regret policyClass environmentClass ≤ worstCaseExpectedRegret regret environmentClass policy`
`BanditRLProof.LowerBounds.le_minimaxExpectedRegret`	Compiled	A uniform policywise lower bound passes through the minimax infimum. Exact compact Lean statement `theorem le_minimaxExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) (lower : ENNReal) (hlower : ∀ policy : policyClass, lower ≤ worstCaseExpectedRegret regret environmentClass policy.1) : lower ≤ minimaxExpectedRegret regret policyClass environmentClass`
`BanditRLProof.LowerBounds.exists_alternative_le_average`	Compiled	Reusable finite averaging leaf. Exact compact Lean statement `theorem exists_alternative_le_average {m : Nat} (hm : 0 < m) (alternativeExpectedPulls : Fin m -> Real) (budget : Real) (hbudget : ∑ i : Fin m, alternativeExpectedPulls i ≤ budget) : ∃ i : Fin m, alternativeExpectedPulls i ≤ budget / (m : Real)`
`BanditRLProof.LowerBounds.alternativeExpectedPullBudget_le`	Compiled	Remove the nonnegative distinguished-arm contribution from the exact total. Exact compact Lean statement `theorem alternativeExpectedPullBudget_le {m : Nat} (expectedPulls : Fin (m + 1) -> Real) (budget : Real) (hnonneg : ∀ arm, 0 ≤ expectedPulls arm) (htotal : ∑ arm : Fin (m + 1), expectedPulls arm = budget) : (∑ i : Fin m, expectedPulls i.succ) ≤ budget`
`BanditRLProof.LowerBounds.exists_leastExploredAlternative`	Compiled	Source-shaped Fin.succ alternative-arm conclusion. Exact compact Lean statement `theorem exists_leastExploredAlternative {m : Nat} (hm : 0 < m) (expectedPulls : Fin (m + 1) -> Real) (horizon : Nat) (hnonneg : ∀ arm, 0 ≤ expectedPulls arm) (htotal : ∑ arm : Fin (m + 1), expectedPulls arm = (horizon : Real)) : ∃ i : Fin m, expectedPulls i.succ ≤ (horizon : Real) / (m : Real)`
`BanditRLProof.LowerBounds.baseEnvironmentRegret`	Compiled	Equation (13.2) deterministic expression. Exact compact Lean statement `def baseEnvironmentRegret (horizon : Nat) (gap baseFirstExpectedPulls : Real) : Real`
`BanditRLProof.LowerBounds.changedEnvironmentRegretLowerBound`	Compiled	Equation (13.3) lower expression. Exact compact Lean statement `def changedEnvironmentRegretLowerBound (gap changedFirstExpectedPulls : Real) : Real`
`BanditRLProof.LowerBounds.max_base_changed_regretLowerBound_ge_half_sub_error`	Compiled	Quantitative two-environment algebra with the cross-law pull discrepancy exposed as an error premise. Exact compact Lean statement `theorem max_base_changed_regretLowerBound_ge_half_sub_error (horizon : Nat) (gap baseFirstExpectedPulls changedFirstExpectedPulls error : Real) (hgap : 0 ≤ gap) (hpullDifference : baseFirstExpectedPulls - changedFirstExpectedPulls ≤ error) : gap * ((horizon : Real) - error) / 2 ≤ max (baseEnvironmentRegret horizon gap baseFirstExpectedPulls) (changedEnvironmentRegretLowerBound gap changedFirstExpectedPulls)`
`BanditRLProof.LowerBounds.max_base_changed_regretLowerBound_ge_half`	Compiled	Zero-error directional corollary of the quantitative algebra. Exact compact Lean statement `theorem max_base_changed_regretLowerBound_ge_half (horizon : Nat) (gap baseFirstExpectedPulls changedFirstExpectedPulls : Real) (hgap : 0 ≤ gap) (htransport : baseFirstExpectedPulls ≤ changedFirstExpectedPulls) : gap * (horizon : Real) / 2 ≤ max (baseEnvironmentRegret horizon gap baseFirstExpectedPulls) (changedEnvironmentRegretLowerBound gap changedFirstExpectedPulls)`

Dependency graph

minimaxminimax / worst-case semanticsCompiled

budgetexpected pull budgetCompiled

leastleast-explored alternativeCompiled

algebratwo-environment algebraCompiled

transportsame-policy history KL transportCompiled

theorem-13-1Gaussian minimax terminalBlocked

Reading path

Read the source statement and its explicit Chapter 15 proof deferral.
Inspect the minimax definitions before the averaging lemma.
Check the Fin.succ indexing: source arms 2,…,k become Lean alternatives 0,…,m−1.
Read the quantitative algebra theorem and locate its visible cross-environment error premise.
Continue through the compiled Chapter 14 event-testing foundation and Chapter 15 history identity to the still-open Gaussian regret/event terminal.

Strict status and remaining gaps

The Chapter 15 regret/event bridge from the compiled same-policy history KL identity.
The source-specific Gaussian constant assembly and caller-free Theorem 13.1 terminal.