Stochastic finite arms
Start with bookkeeping, add concentration, then compare ETC and optimism.
A student-first route
How to read the formalization
You do not need to read thousands of declarations in source order. Begin with the deterministic language, learn the probability interfaces, then follow one algorithm route from assumptions to a compiled endpoint.
Choose a route before choosing a chapter
The same finite-sum and probability leaves recur across algorithms. Pick a question, follow its short dependency route, and return to the complete map when you need a neighboring technique.
Linear and contextual
Build the probability interface before moving from optimism to confidence ellipsoids.
Bayesian
Use the common probability layer, then follow posterior sampling and its information route.
Adversarial and OCO
Move from importance weighting in EXP3 to regularized FTRL and Tsallis geometry.
Finite-horizon RL
Reuse probability and optimism interfaces before entering Bellman recursion and UCBVI.
Reading rule. Read the plain-English statement first, then the mathematical reading, then the exact Lean signature. Save tactic details for the second pass.
Four Lean ideas to recognize
Structures
Bundle mathematical data with invariant proofs, such as a finite model and its best-arm certificate.
Typeclasses
Supply ambient facts such as measurable spaces, finite types, probability measures, and nonempty action sets.
Almost everywhere
Conditional distributions and kernel identities are usually equal almost everywhere, not pointwise.
Thin wrappers
Algorithm-specific theorems should reuse general finite-sum, measure, concentration, and optimization leaves.
Formalized textbook map
Book map
The main spine is Lattimore and Szepesvári's Bandit Algorithms. OFUL, Tsallis-INF, and UCBVI add their original papers. Online-edition pages are shown on every chapter card; the source pages themselves explain the exact algorithms and full assumptions.
1. Finite bandits, traces, and regret
Extension and milestone ledger · 13 compiled · 1 partial
Ch. 1 and Ch. 4, especially §4.5 · online pp. 8–16 and 56–69; regret decomposition pp. 62–63
The deterministic language shared by the entire project: finite models, action and reward traces, pull counts, gaps, reward sums, pseudo-regret, and count-to-regret decompositions.
Reader. Start here if you know basic probability or machine learning but are new to this Lean library.
2. Probability, kernels, filtrations, and concentration
Extension and milestone ledger · 7 compiled
Ch. 2, Ch. 3, and Ch. 5 · online pp. 18–42, 46–54, and 74–81
Measure-theoretic infrastructure for generated histories, conditional reward laws, martingale differences, posterior kernels, stopping times, and concentration.
Reader. Read after Foundations; familiarity with conditional expectation helps but is not required.
3. Explore-Then-Commit
Extension and milestone ledger · 3 compiled
Ch. 6 · online pp. 91–96
Round-robin exploration, empirical means, measurable commit choices, wrong-commit tails, and expected-regret assemblies under bounded or sub-Gaussian arm laws.
Reader. The shortest end-to-end stochastic-bandit route in the repository.
4. UCB: confidence events to regret
Extension and milestone ledger · 18 compiled · 1 partial
Ch. 7; KL-UCB extension in Ch. 10 · online pp. 102–111; KL-UCB pp. 133–141
History-based ordinary-UCB and KL-UCB scores, count thresholds, generated policies, arm streams, same-trajectory confidence, finite-arm reward kernels, and expected regret.
Reader. Read ETC first if confidence-event arguments are new to you.
5. OFUL, self-normalized confidence, and stopping times
Extension and milestone ledger · 8 compiled
Ch. 19–20; stopping times in §3.3 · online pp. 238–262; stopping-time basics pp. 50–54
The scoped canonical finite-action linear-bandit route compiles from elliptical potential and self-normalized ridge confidence through one horizon-free generated OFUL policy with all-horizon regret and stopping consumers, plus a separately identified horizon-indexed expected-consistency family.
Reader. Read the Probability layer and UCB chapter before this linear-bandit route.
6. Thompson sampling and Bayesian regret
Extension and milestone ledger · 6 compiled · 1 partial
Ch. 34 and Ch. 36 · online pp. 421–436 and 460–475
The scoped stationary finite-arm Thompson route compiles from posterior kernels and probability matching on the actual recursive generated history through clipped-UCB decomposition, latent-stream confidence, and an explicit Bayesian regret terminal.
Reader. Best read after the Probability layer.
7. EXP3 and adversarial concentration
Extension and milestone ledger · 7 compiled
Ch. 11–12 · online pp. 148–172
The scoped canonical generated EXP3 route compiles from exponential-weight potentials and importance-weighted conditional moments through horizon-tuned expected and best-arm high-probability endpoints, plus a distinct fixed-process all-positive-prefix realized-regret event and a sparse-loss extension.
Reader. Read Foundations first; later sections use the Probability layer heavily.
8. Tsallis-FTRL, corruption, and nonstationarity
Extension and milestone ledger · 4 compiled
Ch. 28 (FTRL and mirror-descent foundation) · online pp. 327–344
The scoped canonical half-Tsallis FTRL route compiles from finite-simplex minimizers and one-step stability through a measurable scheduled generated trajectory, score alignment, expected self-bounding, and a finite-arm IID bounded reward-law logarithmic regret terminal; corruption and nonstationary routes remain labelled extensions.
Reader. This is one of the longest routes; read EXP3 and the Probability layer first.
9. Finite-horizon reinforcement learning
Extension and milestone ledger · 7 compiled
Ch. 38 · online pp. 512–538
Finite MDPs, Bellman optimality, generated trajectories and occupancy regret, plus a canonical known-reward Hoeffding UCBVI-CH route whose recurrent planner, same-source confidence, optimism, raw cumulative episode pseudo-regret, high-probability terminal, and failure-aware expectation consumer share one adaptive generated process.
Reader. Read Foundations, Probability, UCB, and the OFUL stopping-time material first.
10. Automation, resources, and open routes
Extension and milestone ledger · 2 blocked · 13 compiled · 5 partial · 1 planned
Parts VII–VIII as a background index · online pp. 358–538
The proof harness, task vocabulary, resource stopping leaves, literature registry, partial source-frozen delayed-feedback, succinct-lower-bound, and stochastic-gradient-bandit audits, and planned BwK, preference, robust, federated, neural-bandit, and sharp KL-asymptotic work.
Reader. Read this chapter to contribute a new route or understand what is deliberately not claimed.
Canonical source sequence
Part IV: Lower Bounds
This Bandit Book group preserves the exact textbook order and page mapping for Chapters 13–17. Status is per chapter and per Lean declaration.
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.