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.

Recommended path

flowchart LR
  Start["New to Lean or bandit/RL proofs"] --> F["1. Foundations"]
  F --> P["2. Probability layer"]
  F --> ETC["3. ETC"]
  ETC --> UCB["4. UCB"]
  P --> UCB
  UCB --> OFUL["5. OFUL + stopping times"]
  P --> TS["6. Thompson sampling"]
  F --> E["7. EXP3"]
  P --> E
  E --> T["8. Tsallis-FTRL"]
  P --> T
  P --> RL["9. Finite-horizon RL"]
  OFUL --> RL
  UCB --> RL
  RL --> Frontier["10. Frontier + contribution workflow"]
  T --> Frontier
  TS --> Frontier

  IDE["Research IDE: LaTeX ↔ Lean ↔ tree"] -. "use beside every chapter" .-> F
  IDE -.-> RL

Recommended learning path through the chapters · editable Mermaid source

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.

Compiled 1. Finite bandits, traces, and regret Canonical scope compiled · 7 compiled · 3 blocked 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.

Compiled 2. Probability, kernels, filtrations, and concentration Canonical scope compiled · 6 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.

Compiled 3. Explore-Then-Commit Canonical scope compiled · 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.

Compiled 4. UCB: confidence events to regret Canonical scope compiled · 5 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.

Compiled 5. OFUL, self-normalized confidence, and stopping times Canonical scope compiled · 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.

Compiled 6. Thompson sampling and Bayesian regret Canonical scope compiled · 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.

Compiled 7. EXP3 and adversarial concentration Canonical scope compiled · 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.

Compiled 8. Tsallis-FTRL, corruption, and nonstationarity Canonical scope compiled · 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.

Compiled 9. Finite-horizon reinforcement learning Canonical scope compiled · 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.

Planned 10. Automation, resources, and open routes Canonical scope planned · 2 blocked · 7 compiled · 2 partial · 1 planned Parts VII–VIII as a background index · online pp. 358–538 The proof harness, task vocabulary, resource stopping leaves, literature registry, a partial source-frozen delayed-feedback audit, 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

Use this separate spine when you want the exact textbook order and page mapping for Chapters 13–17. Status is per chapter and per Lean declaration.

Chapter 13 Partial Lower Bounds: Basic Ideas 155–159 print · 189–194 PDF

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.

Chapter 14 Partial Foundations of Information Theory 160–169 print · 195–206 PDF

The source-faithful §14.2 relative-entropy and Bretagnolle–Huber spine is compiled. Entropy/source coding in §14.1 and full sub-sigma-algebra data processing remain outside this scoped gate.

Chapter 15 Partial Minimax Lower Bounds 170–176 print · 207–214 PDF

Lemma 15.1 now compiles for finite arms, a countably generated reward space, arbitrary Markov arm laws, and one common randomized history policy. The unit-Gaussian dependency slice also compiles; Theorem 15.2 and the 1/27 minimax terminal remain blocked.

Chapter 16 Partial Instance-Dependent Lower Bounds 177–184 print · 215–223 PDF

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.

Chapter 17 Partial High-Probability Lower Bounds 185–190 print · 224–230 PDF

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.