Bandit Algorithms
Tor Lattimore and Csaba Szepesvári
- Edition
- Cambridge University Press 2020; author-hosted formal PDF
- Publisher
- Cambridge University Press, 2020
Canonical textbook sequence
Textbook Spine / Part IV: Lower Bounds
A chapter-by-chapter, source-faithful formalization of finite-armed bandit lower bounds. This layer is separate from the curated ten-chapter Book Map and reports compiled, partial, planned, and blocked evidence without implying that the whole textbook is formalized.
Scope boundary. These are the source-numbered lower-bound chapters of the Bandit Book. The existing ten-chapter Book Map remains a curated curriculum and is not relabeled as a completed formalization of the entire book.
Canonical source
Chapters 13–17
Work advances in source order. A chapter can expose compiled leaves while its broader source theorem remains partial or planned.
Chapter 13
Compiled
Lower Bounds: Basic Ideas
155–159 print · 189–194 PDF
Theorem 13.1 compiles through Chapter 15 with c=1/54. Chapter 13 also compiles fixed-class minimax-optimality, the canonical iid Gaussian empirical-mean law, midpoint error events, the Chernoff companion, and both exact Mills-ratio bounds of Eq. (13.4) rescaled to the printed Eq. (13.1). The broader 1-subgaussian class with gaps in [0,1] now has a compiled fixed-horizon MOSS upper bound and constant-factor near-minimax theorem. The frozen main-text contract is complete: PR #105, authoritative-main checks, Pages deployment and live desktop/mobile acceptance pass for b38630c. Notes and Exercises remain optional and unformalized.
Chapter 14 Compiled Foundations of Information Theory 160–169 print · 195–206 PDFThe frozen required body is compiled: Huffman optimality, exact-real arithmetic block coding and converse, finite/partition/common-density KL, the source affinity/overlap route, and Gaussian testing. Independent review, PR #106, main run 33959196451, Pages and live desktop/mobile acceptance passed. The singleton and uniform-code qualifications below are part of the accepted boundary; optional Notes/Exercises are not claimed complete.
Chapter 15 Compiled Minimax Lower Bounds 170–176 print · 207–214 PDFThe frozen required body (§15.1–15.2) is compiled: Lemma 15.1 and Theorem 15.2 use one arbitrary randomized HistoryAlgorithm, the canonical finite-history law, exact unit-Gaussian construction and 1/27 constant, with worst-case and minimax consequences. Optional Exercise 15.7 remains partial: measurable-map KL contraction reuses Chapter 14's trim API, and the fixed-horizon observation corollary compiles; stopped-history information and F_tau factorization remain open. Notes and other exercises are outside the required-body completion contract.
Chapter 16 Compiled Instance-Dependent Lower Bounds 177–184 print · 215–223 PDFDefinition 16.1, Theorem 16.2, Lemma 16.3, and Theorem 16.4 compile with the source quantifiers, information branches, constants, and positive-part placement.
Chapter 17 Compiled High-Probability Lower Bounds 185–190 print · 224–230 PDFAll 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.
Part IV dependency spine
The graph is a route map, not proof evidence. Each chapter page names the declarations and missing bridges that determine its status.
flowchart LR C13["Chapter 13 · basic ideas<br/>required body compiled<br/>optional Notes/Exercises excluded"] C14["Chapter 14 · information theory<br/>required body compiled<br/>optional Notes/Exercises excluded"] C15["Chapter 15 · minimax lower bounds<br/>required body compiled<br/>optional Exercise 15.7 partial"] C16["Chapter 16 · instance-dependent bounds<br/>required body compiled<br/>optional Notes/Exercises excluded"] C17["Chapter 17 · high-probability bounds<br/>required body compiled with corrections<br/>Claim 17.6 non-strict; delta at most 1/32"] L13["minimax semantics<br/>least-explored arm<br/>two-environment algebra"] KL["relative entropy<br/>binary/event KL<br/>history change of measure"] MM["testing and tuning<br/>Gaussian minimax terminal"] ASY["policy consistency + d_inf<br/>exact finite-time and liminf terminals compiled"] HP["Stochastic tails and corrected adversarial terminal<br/>c=1/160, C=64; strict CDF tail"] L13 --> C13 C13 --> C14 C14 --> KL KL --> C15 C15 --> MM MM --> C16 C16 --> ASY ASY --> C17 C17 --> HP classDef compiled fill:#dff5e7,stroke:#247249,color:#123b29 classDef partial fill:#fff2cc,stroke:#9a6b00,color:#563c00 classDef planned fill:#eef2f7,stroke:#64748b,color:#334155 class L13,C13,C14,C15,C16,C17,KL,MM,ASY,HP compiled