Machine Learning

Motivation

Every algorithm through Chapter VI updates its iterate by a Euclidean projection onto the decision set $K$. For many decision sets that arise in practice — bounded-nuclear-norm matrices (matrix completion / recommendation systems), the flow polytope (network routing), the Birkhoff–von Neumann polytope (ranking/permutations), matroid polytopes — a projection requires an expensive operation (an SVD, a quadratic program) while a linear minimization over the same set is comparatively cheap (an eigenvector computation via the power method, a shortest-path or minimum-weight-matching computation, a greedy matroid algorithm). Chapter 7 develops an OCO algorithm that replaces every projection with a call to a linear-minimization oracle, at the cost of a worse regret rate.

Setting

The conditional gradient (CG) / Frank–Wolfe method (Algorithm 25) minimizes a $\beta$-smooth function $f$ over a convex set $K$ (diameter $D$) without ever projecting: at each round it calls the oracle $v_t = \arg\min_{x\in K}\langle x, \nabla f(x_t)\rangle$ and steps $x_{t+1} = x_t + \eta_t(v_t - x_t)$, staying inside $K$ automatically since it is a convex combination of two points of $K$. Theorem 7.1 gives its convergence rate; §7.3.1's matrix completion example and §7.4's routing/ranking/matroid examples motivate why the oracle call is often much cheaper than a projection.

The online conditional gradient (OCG) algorithm (Algorithm 27) lifts this to the OCO setting. Applying CG naively to each $f_t$ separately fails (the method only sees gradient direction, and a single round's direction is not enough information); instead, the algorithm builds the aggregate regularized function $F_t(x) = \eta\sum_{\tau=1}^{t-1}\langle\nabla_\tau, x\rangle + \|x-x_1\|^2$ from all past gradients, calls the linear oracle on $\nabla F_t(x_t)$, and takes a $(1-\sigma_t)/\sigma_t$-weighted step toward the oracle's answer.

Formalization targets

Theorem 7.1 (offline CG convergence, milestone)

Lemma 7.4 (per-round iterate bound, milestone)

Theorem 7.3 — the mission's goal

Online conditional gradient (Algorithm 27) with $\eta = D/(2GT^{3/4})$, $\sigma_t = \min\{1, 2/\sqrt t\}$ attains

Significance

This is the chapter's central trade: Algorithm 27's $O(T^{3/4})$ regret is worse than Chapter III's full-information $O(\sqrt T)$ rate and Chapter V's RFTL rate, but its per-round cost is a single linear-minimization oracle call, not a projection — exactly the trade that makes it the practical choice for the recommendation-system, routing, and ranking applications the chapter develops in detail. Theorem 7.1's offline rate is independently significant as the field's standard Frank–Wolfe convergence guarantee, reused as the analytical engine (via Eq. (7.2)) for both Lemma 7.4's online bound and, historically, for a large family of projection-free methods outside OCO entirely. No prior art was found on the platform for Frank–Wolfe, conditional gradient, or projection-free methods (q=Frank-Wolfe returned 0 hits during planning); this mission drafts the standard textbook account fresh.

Difficulty

Theorem 7.1's proof is a one-step smoothness-plus-convexity inequality (Eq. (7.2)) combined with an induction lemma (Lemma 7.2, not separately drafted — it is a purely algebraic recursion h_{t+1} ≤ h_t(1-η_t) + η_t²c ⟹ h_t ≤ 4c/t, reused verbatim by Lemma 7.4's own induction and not independently central to the chapter's content). Lemma 7.4's proof is the chapter's most delicate step: it applies Theorem 7.1's offline analysis technique to the online aggregate function $F_t$ — not to any single $f_t$, and not even to a fixed function across rounds, since $F_t$ itself changes every round as more gradients accumulate — then combines it with a second inequality (comparing $F_t(x^\star_t)$ to $F_{t+1}(x^\star_{t+1})$ via strong convexity and Cauchy–Schwarz) and a careful algebraic balancing of the $\eta$, $G$, $\sigma_t$ parameters (Eq. (7.6)) to close the induction. Theorem 7.3's own proof is a second reduction: it relates the algorithm's regret against the true cost sequence $f_t$ to Lemma 7.4's bound on $F_t$, via an intermediate comparison to $x^\star_t$ (playing the role of Chapter V's RFTL iterates applied to a shifted cost sequence $\tilde f_t$).

Formalization scope

IsLinearMinimizer makes the "projection-free" linear-oracle call (Eq. (7.4)) an explicit, first-class object, reused by both Algorithm 25 and Algorithm 27's definitions, rather than silently replaced by a projection anywhere. SmoothOn is redeclared under this chapter's own sub-namespace (not imported from Chapter II, which is not yet a published series definition); see MODERATION_NOTES.md. AggregateFunction/AggregateGradient give $F_t$ and its closed-form gradient explicitly, matching Algorithm 27 line 4's formula exactly (the book computes $\nabla F_t$ directly rather than leaving it abstract, so this mission does too). This chunk indexes rounds from 1 throughout (not the 0-indexed Finset.range shift used elsewhere in the series), since Algorithm 27's own line 4 sums $\tau=1$ to $t-1$ and every theorem in this chapter states a per-round or Finset.Icc 1 T-summed bound directly in the book's own round numbers — a deliberate, chunk-local convention choice, not an inconsistency with earlier chapters' definitions (this chunk does not import them). Lemma 7.4 keeps Theorem 7.3's specific parameters and a $G$-Lipschitz hypothesis as explicit premises, since the book's own proof of the lemma uses them, rather than presenting it as a fully parameter-free general fact.

Not formalized: Lemma 7.2 (a routine algebraic recursion, not independently central, and reused identically inside Lemma 7.4's own proof rather than cited as a numbered result on its own); Algorithm 26 and §7.3.1's matrix-completion specialization, §7.4's routing/ranking/matroid examples, and Corollary-level results (illustrative applications, not further formalizable theorems); §7.1's linear-algebra review (singular values, nuclear norm — background, not a formalization target for this mission).

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 7.
• M. Frank, P. Wolfe, "An algorithm for quadratic programming," Naval Research Logistics Quarterly 3(1-2), 1956, 95-110.
• E. Hazan, S. Kale, "Projection-free online learning," ICML 2012 (the chapter's Algorithm 27).

Motivation

Every RL guarantee proved earlier in this series — UCB-VI's regret bound, the contextual bandit oracle reductions — scales with the size of the state space $S$, because the algorithms maintain a separate statistic per state. Real environments (images, sensor readouts, natural language) have combinatorially or infinitely many states, so a tabular guarantee is vacuous there: the only hope is to generalize across states via a class of value functions, the way supervised learning generalizes across inputs via a hypothesis class. The chapter develops two algorithms along this line: LSVI-UCB, the linear-function-approximation analogue of UCB-VI whose regret is independent of $|S|$ (a low-rank MDP result originating with Jin, Yang, Wang, and Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020, arXiv:1907.05388), and BiLinUCB, which attains an analogous sample-complexity guarantee under the strictly more general structural condition of low Bellman rank (Jiang, Krishnamurthy, Agarwal, Langford, and Schapire, Contextual Decision Processes with Low Bellman Rank are PAC-Learnable, ICML 2017, arXiv:1610.09512; the Q-type variant formalized here follows Du, Kakade, Wang, and Yang, Is a Good Representation Sufficient for Sample Efficient Reinforcement Learning?, ICLR 2020, arXiv:1910.03016). This mission formalizes the second, strictly more general track: BiLinUCB and its Bellman-rank guarantee; LSVI-UCB is left out of scope (see Formalization scope).

Setting

Both algorithms act on the finite-horizon episodic MDP $M = (S,A,\{P_h\}_{h=1}^H, \{R_h\}_{h=1}^H,d_1)$ of the earlier chapters of this series (RLBasics.Core), with value $f^M(\pi) = \mathbb E_{s_1\sim d_1}[V_1^{M,\pi}(s_1)]$. For a state-action value function $Q = (Q_h)_{h=1}^H$ (with the convention $Q_{H+1}\equiv 0$), the Bellman residual of $Q$ under policy $\pi$ at layer $h$ is

which vanishes identically when $Q = Q^{M,\star}$, the optimal value function (Bellman optimality). Given a class $\mathcal Q$ of candidate value functions, $M$ has Bellman rank $d$ relative to $\mathcal Q$ (Definition 8) if $d$ is the least integer such that, at every layer $h$, there exist embeddings $X_h(\pi), W_h(Q) \in \mathbb R^d$ with $E_h(\pi,Q) = \langle X_h(\pi), W_h(Q)\rangle$ for every policy $\pi$ and $Q\in\mathcal Q$ — equivalently, the least rank of the $\Pi\times\mathcal Q$ matrix of Bellman residuals, at any layer. A linear MDP (the setting of LSVI-UCB, §7.2) is the special case where the transition kernel and reward themselves factor through a known feature map $\phi : S\times A \to \mathbb R^d$; every linear MDP has Bellman rank at most $d$ relative to the linear value-function class, but Bellman rank captures far more (kernel/neural function classes, and low-rank MDPs whose feature map is unknown).

The chapter presents two algorithms. LSVI-UCB (§7.2.1) runs $T$ episodes of ridge regression per layer against the linear feature map, forming a confidence ellipsoid of radius $\rho \propto \sqrt d$ around each layer's estimated parameter and acting greedily with respect to an upper-confidence bonus built from that ellipsoid — the same optimism-under-uncertainty template as UCB-VI, now regularized rather than tabular; it motivates Bellman rank but is not itself formalized by this mission (see Formalization scope). BiLinUCB (§7.3.1), the algorithm this mission formalizes, instead proceeds in $K$ iterations of $n$ episodes: each iteration plays the greedy policy for the current optimistic-on-average value function $Q_k = \arg\max_{Q\in\mathcal Q_k}\mathbb E_{s_1\sim d_1}[Q_1(s_1, \pi_Q(s_1))]$, collects $n$ fresh episodes, and shrinks the confidence set $\mathcal Q_{k+1}$ by discarding value functions whose empirical Bellman residual along the played policy is large; after $K$ iterations it outputs the policy with the best empirical return observed at any iteration.

Formalization targets

Goal — Proposition 47 (BiLinUCB, sample complexity under Bellman rank)

for $M^\star$ of Bellman rank $d$ relative to $\mathcal Q\ni Q^{M^\star,\star}$, where $\hat\pi$ is BiLinUCB's output policy after $K$ iterations of $n$ episodes. This is the weakest stable form: it fixes the shape of the sample complexity (polynomial in $H,d,\log|\mathcal Q|,1/\varepsilon$, logarithmic in $1/\delta$, independent of $|S|$) and leaves the leading constants — which the book itself introduces only as "a sufficiently large numerical constant" — outside the formal claim. Unlike every other goal in this series, this is a PAC (sample-complexity) guarantee on the algorithm's final output policy, not a bound on cumulative regret accrued while learning: BiLinUCB commits to $\hat\pi$ only after the training phase ends, and its suboptimality is measured post-training.

Reaching it rests on two structural facts about BiLinUCB's confidence sets, each formalized as a milestone in attack order:

• Lemma 29 (confidence-set validity): with the stated threshold $\beta$, with probability at least $1-\delta$, simultaneously at every iteration $k$, every retained value function has true (population) Bellman residual along the played policies bounded by $\beta$ up to a constant, and the realizable $Q^{M^\star,\star}$ is itself always retained.
• Lemma 30 (optimism and elliptic-norm bound): conditioned on Lemma 29's event, every retained value function's embedding $W_h(Q)$ has bounded norm with respect to the Gram matrix of the played policies' embeddings, and the optimistic value function $Q_k$ BiLinUCB selects at each iteration has initial-state value at least $f^{M^\star}(\pi^{M^\star})$.

Significance

Proposition 47 shows that a single structural parameter — Bellman rank — is sufficient for sample-efficient RL with function approximation, with a sample complexity that depends only on the horizon, the rank, and the value-function class's log-cardinality, never on $|S|$. This subsumes the linear-MDP guarantee of Proposition 46 (LSVI-UCB, §7.2.1; not itself a target of this mission, see Formalization scope) as a special case — every linear MDP has Bellman rank $\le d$ — while covering strictly more models (kernelized and neural value-function classes with a low-dimensional Bellman-residual factorization that need not come from a known linear feature map). The result is proved in the source and this mission formalizes its statement and the two structural lemmas its proof rests on, as stated; no new mathematics is contributed. Formalizing it commits, for the first time on this platform, to machine-checkable statements of the Bellman rank abstraction, the elliptic-norm confidence-set machinery it drives, and a PAC- (rather than regret-) style learning guarantee, none of which appear in the platform's existing bandit or tabular-RL missions.

Difficulty

The obvious first attempt is to formalize Bellman rank as an unconstrained integer parameter $d$ attached to the MDP, sidestepping the actual rank condition on the Bellman-residual matrix; this is a trivializing formalization; Bellman rank must be the least dimension admitting the stated bilinear factorization; see Formalization scope. A second obstacle is that BiLinUCB's optimism is only "on average" with respect to the initial state distribution (initValue), unlike LSVI-UCB's pointwise optimism over every state and action — conflating the two confidence-set constructions collapses the chapter's main conceptual contrast. Finally, the two technical lemmas (29 and 30) separate a purely probabilistic statement (validity of the empirical confidence set, via Hoeffding and a union bound) from a purely deterministic consequence (the elliptic-norm bound and optimism, which hold on any sample path where the probabilistic event occurred); keeping this separation is what lets Proposition 47's proof combine them cleanly, and collapsing it into one monolithic high-probability statement would misrepresent the book's proof structure.

Formalization scope

The MDP, policy, and trajectory/history machinery (EpisodicMDP, Policy, IsPolicy, Trajectory, Learner, probEvent) are reused unchanged from the series' published RLBasics.Core/RLBasics.UCBVI definitions. The value-function class $\mathcal Q$ is realized as an abstract finite, nonempty type Qc together with an evaluation map qeval : Qc → ℕ → S → A → ℝ, kept fully abstract rather than specialized to any concrete function class — specializing it to, e.g., linear functions would collapse Proposition 47 back into a restatement of Proposition 46, which is exactly the trivializing formalization this mission avoids. Bellman rank (IsBellmanRank) is defined as the least natural number admitting the bilinear factorization (an IsLeast over the coercion to HasBellmanRankLE), never as a free parameter. Every realized per-step reward is taken equal to its conditional mean $R_h(s,a)$ throughout (exact, by the tower property, and not a restriction to deterministic rewards). The elliptic norm of Lemma 30 is expressed via the direct sum-of-squared-inner-products identity $\|v\|^2_\Sigma = \sum_{x\in xs}\langle x,v\rangle^2$ rather than introducing Matrix/matrix-inverse machinery, since no milestone here needs an explicit matrix inverse. Every place the book writes ≲/∝/"a sufficiently large numerical constant" is formalized as an existentially quantified universal constant, fixed ahead of every MDP, value-function class, and $(\varepsilon,\delta)$ instance — never depending on the instance itself. This mission scopes entirely to the Bellman-rank track (Definition 8, BiLinUCB, Lemmas 29-30, Proposition 47); Proposition 46 (LSVI-UCB) and its supporting Lemmas 27-28 are the chapter's motivating linear special case (Section 7.2) but are left out of this mission's scope for time and are not claimed as proved by it — LSVI-UCB's confidence-ellipsoid construction is materially different from BiLinUCB's empirical-Bellman-residual confidence set (see Difficulty) and would need its own milestone chain. A complete development needs no infrastructure beyond what is already published in RLBasics.Core/RLBasics.UCBVI; contributions completing the sorrys in the two technical lemmas and the goal are welcome.

Selected references

• Foster, D. J. and Rakhlin, A. Foundations of Reinforcement Learning and Interactive Decision Making. arXiv:2312.16730v1, 2023. arXiv:2312.16730
• Jin, C., Yang, Z., Wang, Z., and Jordan, M. I. Provably Efficient Reinforcement Learning with Linear Function Approximation. COLT 2020. arXiv:1907.05388
• Jiang, N., Krishnamurthy, A., Agarwal, A., Langford, J., and Schapire, R. E. Contextual Decision Processes with Low Bellman Rank are PAC-Learnable. ICML 2017. arXiv:1610.09512
• Du, S. S., Kakade, S. M., Wang, R., and Yang, L. F. Is a Good Representation Sufficient for Sample Efficient Reinforcement Learning? ICLR 2020. arXiv:1910.03016

Motivation

Many hard combinatorial optimization problems — finding the maximum cut of a graph, deciding the ground state of an Ising spin system, bounding the correlation of a physical system — can be written as maximizing a bilinear form over sign vectors $x_i \in \{-1, 1\}$. Exhaustive search over $2^n$ sign patterns is intractable, so practitioners relax the problem: replace each sign $x_i$ by a unit vector $X_i$ in a higher-dimensional space and optimize the resulting inner products instead. This relaxation, a semidefinite program, is convex and solvable in polynomial time. The question is how much is lost in the relaxation — whether its optimal value can be far from the true, combinatorial optimum.

Grothendieck's inequality, proved by Alexander Grothendieck in 1953 in the context of Banach space theory (Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79), answers this for a broad class of such relaxations: replacing signs by unit vectors in an arbitrary Hilbert space changes the optimal value by at most an absolute, dimension-free constant factor. The inequality has since become a standard tool across combinatorial optimization, Banach space geometry, and (via the Goemans-Williamson algorithm for maximum cut, Section 3.6 of the source) approximation algorithms; see U. Haagerup, The Grothendieck inequality for bilinear forms on $C^*$-algebras, Adv. Math. 56 (1985) for the tightest known constant, and Alon–Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), for the algorithmic connection this mission's Theorem 3.5.6 sets up.

Setting

Fix positive integers $m, n$. Consider a real $m \times n$ matrix $A = (a_{ij})$. Say $A$ is normalized if for every choice of numbers $x_1, \dots, x_m, y_1, \dots, y_n \in \{-1, 1\}$,

This says $A$, viewed as a bilinear form on $\{-1,1\}^m \times \{-1,1\}^n$, has sup-norm at most $1$. Now let $H$ be any real Hilbert space — a real vector space equipped with an inner product $\langle \cdot, \cdot \rangle$ complete in the induced norm — and consider vectors $u_1, \dots, u_m \in H$ and $v_1, \dots, v_n \in H$, each of unit norm $\|u_i\| = \|v_j\| = 1$. Replacing the scalar product $x_i y_j$ by the inner product $\langle u_i, v_j \rangle$ in the same bilinear form gives $\sum_{i,j} a_{ij} \langle u_i, v_j \rangle$, a real number depending on the choice of $H$ and of the unit vectors. The question is how large this can be, uniformly over every such choice.

Formalization targets

Grothendieck's inequality (Theorem 3.5.1)

for every real Hilbert space $H$ and unit vectors $u_i, v_j \in H$, where $K$ is a constant depending on neither $A$, its dimensions, nor $H$. This mission's goal formalizes the book's own first-pass bound $K \le 288$ (Section 3.5), proved by a Gaussian truncation argument; it does not fix a numeral for $K$, only that some absolute constant works, matching the shape of the true statement rather than a specific numeral that a sharper argument (the book's own Section 3.7 gives $K \le 1.783$) would immediately obsolete. See Formalization scope below for why this is the goal, not the sharper bound.

Significance

The result itself. Grothendieck's inequality is the single fact that makes semidefinite relaxation a provably good algorithmic strategy rather than a heuristic: whatever the true, hard-to-compute combinatorial optimum of a $\{-1,1\}$-valued bilinear optimization is, the tractable Hilbert-space relaxation cannot overshoot it by more than the constant $K$. Milestone Theorem 3.5.6 makes this concrete for positive-semidefinite matrices, showing the semidefinite relaxation SDP$(A)$ of the integer program INT$(A)$ satisfies INT$(A) \le$ SDP$(A) \le 2K \cdot$ INT$(A)$ — the guarantee underlying the Goemans-Williamson 0.878-approximation algorithm for maximum cut (Theorem 3.6.5 of the source, out of scope for this mission; see Formalization scope).

Formalizing it. The inequality and its two chapter milestones are proved but not previously formalized on this platform (checked by concept search for "Grothendieck", "semidefinite", "positive-semidefinite", and "max-cut" — no hits beyond the unrelated Grothendieck-Teichmüller group). What remains after this mission is the sharper $K \le 1.783$ argument of Section 3.7 (the "kernel trick"), a separate, heavier development building on positive-definite kernels, and full proofs of every milestone below (currently open sorry goals).

Difficulty

The statement of Grothendieck's inequality contains no randomness, yet every known elementary proof is probabilistic; this is itself a striking feature of the result. The obvious approach — bound $\sum_{i,j} a_{ij}\langle u_i,v_j\rangle$ directly by exploiting the normalization hypothesis on $A$ — fails because the normalization hypothesis only controls $A$ against sign vectors, and there is no way to project an arbitrary unit vector in a Hilbert space onto $\{-1,1\}$ without losing information. The book's proof instead represents each unit vector $u_i, v_j$ via a scalar Gaussian random variable $\langle g, u_i\rangle$ for a single Gaussian vector $g$, recovering the inner products in expectation (Exercise 3.3.5); but these Gaussian variables are unbounded, so the normalization hypothesis (which bounds $A$ against bounded $\pm 1$ inputs) cannot be applied to them directly. The core technical step is a truncation argument: splitting each Gaussian variable into a bounded part and a small-$L^2$-norm unbounded remainder, applying the hypothesis to the bounded parts, and bounding the remainder terms by treating them as elements of the Hilbert space $L^2$ and invoking the very inequality being proved (Theorem 3.5.1 itself, applied with $H = L^2$) as a self-referential bootstrap — this is why the proof fixes $K$ as the smallest valid constant before starting, rather than building it up from scratch.

Formalization scope

The goal and both milestones work with the real matrix and real inner product space directly; H is required to be a complete real inner product space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), matching the book's "any Hilbert space." No dimension bound on $H$ is imposed — the inequality's content is exactly that $K$ does not grow with $\dim H$.

This mission does not formalize the sharper $K \le 1.783$ bound of Section 3.7, nor Theorem 3.6.5 (the 0.878-approximation guarantee for maximum cut via randomized rounding): the latter's statement quantifies over "the result of a randomized rounding of the solution of the semidefinite program," which would drag a specific algorithm into the audited statement rather than keeping it a self-contained mathematical claim (the statement/proof-separation trap this series' triage rubric flags). Grothendieck's identity (Lemma 3.6.6), the key fact behind that rounding step, is included on its own as a milestone, stated with an explicit, named random sign variable rather than an opaque "rounding procedure."

A trivializing formalization would state the goal with $K$ allowed to depend on $A$, $m$, $n$, or $H$ — every such bound is easy (e.g. $K = \sum_{ij} |a_{ij}|$) and carries none of the theorem's content; the Lean statement rules this out by quantifying $K$ before every other object. $\mathrm{INT}(A)$ and $\mathrm{SDP}(A)$ (Theorem 3.5.6) are defined from scratch in this chunk's namespace, using Matrix.PosSemidef from Mathlib for the positive-semidefiniteness hypothesis (which bundles the real-symmetric condition); Mathlib has no ready-made SDP-value construction to reuse. The sub-gaussian (Orlicz $\psi_2$) norm used by Theorem 3.1.1 is reused, unchanged, from the 01-concentration mission in this series (HighDimProb.Concentration.SubgaussianNorm) rather than redefined.

Selected references

• A. Grothendieck, Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79.
• U. Haagerup, The Grothendieck inequality for bilinear forms on $C^*$-algebras, Adv. Math. 56 (1985), 93–116.
• N. Alon, A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), 787–803.
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995), 1115–1145.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 3, DOI 10.1017/9781108231596.

Motivation

Any dataset of $N$ points can be described exactly by embedding it in $\mathbb R^n$ for $n$ large enough — but a large $n$ is expensive: nearest-neighbor search, clustering, and streaming algorithms all scale with the ambient dimension, not with $N$. The question that opens this mission is whether the dimension can be cut down while leaving the data's geometry — the pairwise distances between points — essentially untouched.

Johnson and Lindenstrauss answered this in 1984, while studying extensions of Lipschitz maps into Hilbert space (W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemp. Math. 26 (1984), 189–206): $N$ points in any Euclidean space, of any dimension $n$, can be mapped by a single linear map into a space of dimension only $O(\varepsilon^{-2}\log N)$, distorting every pairwise distance by at most a factor of $1\pm\varepsilon$. The map does not depend on the data beyond its cardinality — a single random object works simultaneously for the whole point set with high probability. This is now one of the standard tools of randomized dimension reduction, cited across nearest-neighbor search, streaming linear algebra, compressed sensing, and machine learning pipelines that need to shrink feature dimension before a downstream algorithm runs.

Setting

Fix a probability space $(\Omega,\mathcal F,\mathrm{Prob})$. A random orthogonal projection of rank $m$ in $\mathbb R^n$ is a map $P:\Omega\to(\mathbb R^n\to\mathbb R^n)$, continuous and linear for each $\omega$, such that almost surely $P_\omega$ is idempotent ($P_\omega\circ P_\omega = P_\omega$), self-adjoint, and has range of dimension $m$ — i.e. $P_\omega$ is the orthogonal projection onto some $m$-dimensional subspace $E_\omega\subset\mathbb R^n$. It is uniformly distributed in the Grassmannian $G_{n,m}$ (written $E\sim\mathrm{Unif}(G_{n,m})$) when its law is rotation invariant: for every orthogonal transformation $U$ of $\mathbb R^n$, the conjugated map $\omega\mapsto U\circ P_\omega\circ U^{-1}$ has the same law as $P$. Conjugating a projection by $U$ is exactly the projection onto the image of its range under $U$, so this says the law of the random subspace $E=\mathrm{range}(P)$ is invariant under the full orthogonal group — the operational definition Vershynin himself uses for a "uniformly distributed" random subspace, since no coordinate-free formula for such a subspace's law is given directly.

A companion notion drives the proof: a random vector $X$ is uniform on the Euclidean sphere of radius $r$, $X\sim\mathrm{Unif}(r\,S^{n-1})$, when it lies on that sphere almost surely and its law is likewise rotation invariant. And a real random variable $Y$ is sub-gaussian with sub-gaussian ($\psi_2$) norm $\|Y\|_{\psi_2} := \inf\{t>0:\mathbb E\exp(Y^2/t^2)\le 2\}$, the standard non-asymptotic measure of how light-tailed $Y$'s distribution is (a bounded or Gaussian random variable has finite $\psi_2$ norm; the tail probability $\mathbb P\{|Y|\ge s\}$ then decays at least as fast as $2\exp(-cs^2/\|Y\|_{\psi_2}^2)$).

Formalization targets

Goal (Theorem 5.3.1, Johnson-Lindenstrauss Lemma)

for every finite $X\subset\mathbb R^n$, every $\varepsilon>0$, and every random orthogonal projection $P$ of rank $m$ uniformly distributed in $G_{n,m}$. The universal quantifier over pairs $x,y\in X$ sits inside the single probability event — this is the union-bound content that makes the statement a genuine simultaneous guarantee for the whole point set, not a restatement of the single-vector lemma below for one fixed pair. Both constants are the book's own unnamed absolute constants, never depending on $n$, $m$, $N=|X|$, or $\varepsilon$; this is the weakest stable form of the claim (no numeral is hard-coded for $C$ or $c$), matching the book's own statement exactly.

Significance

The lemma gives a universal, data-oblivious dimension-reduction guarantee: the target dimension $m=O(\varepsilon^{-2}\log N)$ depends only on the number of points and the desired distortion, never on the ambient dimension $n$ or on the geometry of the specific point set. This is what makes it usable as a black-box preprocessing step ahead of an algorithm whose cost scales with $n$ — the projection is drawn once, without looking at the data, and works with high probability for every pairwise distance simultaneously. The bound is also known to be essentially optimal in $N$: Alon (Problems and results in extremal combinatorics, Discrete Math. 273 (2003)) showed a lower bound of $\Omega(\varepsilon^{-2}\log N/\log(1/\varepsilon))$ on the target dimension, so the $\log N$ dependence cannot be removed.

The theorem itself has been proved for decades and admits several proof strategies (this book's route through Lipschitz concentration on the sphere; the original volume/measure-concentration argument; later "sparse" or structured variants of the projection for faster computation). This mission formalizes the classical dense-Gaussian-projection proof route as Vershynin presents it, building the sphere-concentration engine (Theorem 5.1.4) and the single-vector projection lemma (Lemma 5.3.2) that the union-bound argument for the goal rests on. No machine-checked formal proof of this chain is known to exist on the platform prior to this mission (see Formalization scope below); what is contributed is the statement infrastructure — the goal and its two direct supporting lemmas, stated with explicit, unpinned absolute constants — for solvers to close.

Difficulty

The natural first idea — bound the distortion of a single fixed vector under a random projection, then take a union bound over the $\binom N2$ pairwise differences — is exactly the strategy Lemma 5.3.2 and the goal use, but it does not by itself explain why the single-vector concentration bound (Lemma 5.3.2(b)) holds with the stated sub-gaussian-type tail. That bound is not elementary: it reduces to a uniform concentration statement for an arbitrary Lipschitz function of a uniformly random point on a high-dimensional sphere (Theorem 5.1.4), since $\|Pz\|_2$, viewed as a function of a rotated copy of $z$, is a $1$-Lipschitz function on the sphere. Proving that every Lipschitz function concentrates — not just linear ones, for which sub-gaussianity was already established in Chapter 3 — needs a genuinely different tool: comparing the sub-level sets of an arbitrary Lipschitz function to spherical caps via an isoperimetric inequality on the sphere. This geometric input is what makes the concentration phenomenon behind Johnson-Lindenstrauss a dimension-free fact rather than a special property of coordinate projections.

Formalization scope

$X$ is a Finset of points in EuclideanSpace ℝ (Fin n), matching "a set of $N$ points"; $N$ is read off as X.card. The random subspace $E\in G_{n,m}$ is represented throughout by the orthogonal projection $P$ onto it (IsUniformProjection), following the book's own statements, which are phrased in terms of $P$ rather than $E$; the scaled map $Q=\sqrt{n/m}\,P$ of the goal is written Real.sqrt (n/m) • P ω applied to x - y, using linearity of $P_\omega$ to realize $Qx-Qy = Q(x-y)$. Both "uniform on the sphere" and "uniform in the Grassmannian" are defined operationally by rotation invariance of the underlying law, since Mathlib has no ready-made normalized surface measure on a general-radius Euclidean sphere or Haar-measure construction on the Grassmannian/orthogonal group to build a canonical uniform object from; rotation invariance uniquely determines the corresponding measure among those supported on the relevant set, so the operational and constructive definitions coincide extensionally. Every "absolute constant" in the book ($C$ in Theorem 5.3.1's sample-complexity hypothesis, $c$ in every failure-probability bound, and the sub-gaussian constant $C$ of Theorem 5.1.4) is existentially quantified ahead of the dimension, sample size, and every other object, and pinned to no numeral — a formalization that hard-coded a specific numeral for any of these would be invalidated by the next sharper constant in the literature and would not match what the book actually proves.

A trivializing formalization is one that states the conclusion for a single fixed pair $x,y$ rather than universally over all pairs inside one event; that would collapse the union-bound content that makes this a dimension-reduction statement for a whole point set (with $N$ points), rather than a restatement of the single-vector Lemma 5.3.2(b). This mission's goal statement is built to rule that out explicitly (see Formalization targets above).

Reusable infrastructure: subgaussianNorm (the Orlicz $\psi_2$ norm, restated per Vershynin Definition 2.5.6) and the rotation-invariance idiom for "uniformly distributed" random geometric objects are of independent interest to any later chapter needing sub-gaussian random vectors or random subspaces/projections (e.g. Chapters 4, 6, 7, 9, 11 of this same book series). Solvers' contributions are welcome on: the isoperimetric inequality on the sphere and its use to prove Theorem 5.1.4 (the mission's hardest open leaf); the coordinate-projection computation underlying Lemma 5.3.2(a); and the concentration-plus-union-bound argument closing the goal from the three supporting lemmas.

Selected references

• W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemporary Mathematics 26 (1984), 189–206.
• N. Alon, Problems and results in extremal combinatorics, I, Discrete Mathematics 273 (2003), 31–53. https://doi.org/10.1016/S0012-365X(03)00227-9
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 5. https://doi.org/10.1017/9781108231596

Motivation

Two-player zero-sum games and linear programming are, on their surface, unrelated pieces of 20th-century mathematics: von Neumann's minimax theorem for games (1928) was proved with tools from topology, and linear programming duality (Dantzig, 1940s) with convexity and geometry. Yet the two are formally equivalent — Dantzig recounts von Neumann conjecturing the equivalence outright, on first hearing a description of linear programming, because he had "just recently completed a book with Oscar Morgenstern on the theory of games" [Albers, Alexanderson, and Reid, More Mathematical People, 1990]. Freund and Schapire (1999) later showed that both concepts reduce, in one uniform way, to online regret minimization: a decades-old topological existence proof and a decades-old LP-duality argument both become corollaries of a single fact about no-regret learning. This mission formalizes the algorithmic content of that reduction — Hazan's Lemma 8.4, which is not merely an existence statement but a concrete, efficient algorithm with an explicit convergence rate.

Setting

A two-player zero-sum game in normal form is a real matrix $A \in \mathbb{R}^{n \times m}$ (Hazan restricts entries to $[-1,1]$ for interpretability as losses/rewards, a convention this mission's theorems drop as inessential — the argument is invariant to scaling and shifting). The row player picks a mixed strategy $x$ in the probability simplex $\Delta_n = \{x \in \mathbb{R}^n : x_i \ge 0, \sum_i x_i = 1\}$; the column player picks $y \in \Delta_m$. The row player's expected loss, and simultaneously the column player's expected reward, is the bilinear form $x^{\mathsf T} A y$.

The row player's guaranteed loss is $\lambda_R = \min_{x \in \Delta_n} \max_{y \in \Delta_m} x^{\mathsf T} A y$: the smallest loss she can secure no matter what the column player does. Symmetrically, the column player's guaranteed reward is $\lambda_C = \max_{y \in \Delta_m} \min_{x \in \Delta_n} x^{\mathsf T} A y$. Always $\lambda_R \ge \lambda_C$ ("weak duality" — an elementary max-min/min-max inequality, Direction 1 of Section 8.3). Von Neumann's minimax theorem (Theorem 8.3) is the nontrivial converse: $\lambda_R = \lambda_C$, a common value $\lambda^\star$ called the value of the game, whose optimal strategies form a Nash equilibrium — already on the platform as AGT.zero_sum_minimax.

Algorithm 28 ("Simple LP", p. 147) computes an approximate equilibrium constructively. The row player runs a multiplicative-weights / Exponentiated Gradient update against the sequence of best-response losses the column player generates in a repeated $T$-round play of the game: starting from the uniform strategy $x_1 = (1/n, \dots, 1/n)$, at each round $t$ the column player best-responds with $y_t \in \arg\max_{y \in \Delta_m} x_t^{\mathsf T} A y$, and the row player updates $x_{t+1}(i) \propto x_t(i)\, e^{-\eta (A y_t)_i}$. The algorithm returns the time-averaged strategy $\bar{x} = \frac{1}{T}\sum_{t=1}^T x_t$.

Formalization targets

Goal — Lemma 8.4

for the vector $\bar{x}$ returned by Algorithm 28 after $T$ rounds with learning rate $\eta = \sqrt{2 \log n / T}$. The book calls $\bar{x}$ a "$\sqrt{2 \log n}/\sqrt{T}$-approximate solution" to the zero-sum game — and, via Section 8.2.1's equivalence, to the linear program the game encodes — in exactly this sense. The goal is stated against $\lambda_R$, the quantity the algorithm's own analysis produces; Theorem 8.3 identifies it with $\lambda_C$ and with the book's $\lambda^\star$, so nothing about the bound is lost by this choice of rendering.

Supporting milestone — Eq. (8.1)

the external-regret bound the row player's multiplicative-weights update achieves against the adaptively-chosen linear loss sequence $f_t(\cdot) = (\cdot)^{\mathsf T} A y_t$ — the single analytical fact the goal's proof needs.

Significance

The result itself. Lemma 8.4 gives a genuinely efficient algorithm: $O(\log n / \varepsilon^2)$ rounds of a trivial multiplicative update to reach an $\varepsilon$-approximate value and equilibrium of an $n \times m$ zero-sum game, and — through the equivalence with LP duality — an approximation algorithm for a broad class of linear programs, predating and prefiguring the multiplicative-weights-based approximation schemes surveyed by Arora, Hazan, and Kale (2012). It is also the constructive engine behind Theorem 8.3: unlike the classical topological proof of the minimax theorem, this one produces the equilibrium, not just its existence.

Formalizing it. The equilibrium-existence half of this story, Theorem 8.3, is already a published, proved-format Prove2Me theorem (AGT.zero_sum_minimax, from the Algorithmic Game Theory series) and is reused here as a reference item rather than redrafted. What that theorem does not capture — and what makes this mission non-trivial rather than a restatement — is the quantitative, algorithmic content: that one specific, simple, Hedge-type update, run for a specific number of rounds, provably gets within a specific, explicit distance of the value, using only the existence of some sublinear-regret online algorithm as a black box.

Difficulty

The tempting shortcut is to formalize only "no-regret learning dynamics converge to an equilibrium" as a qualitative statement, discharging it by citing AGT.zero_sum_minimax (equilibria exist) plus a generic regret bound. That collapses Lemma 8.4 into a restatement of Theorem 8.3 and drops exactly what is new here: the explicit rate $\sqrt{2\log n}/\sqrt{T}$, tied to one concrete update rule (Algorithm 28) rather than an arbitrary sublinear-regret black box. The real content is in chaining three quantitative facts — Eq. (8.1)'s specific regret bound for the multiplicative-weights update, the column player's best-response equality (Eq. (8.2)), and the definitional unfolding of $\lambda_R$ — with none of the slack that a purely qualitative "an algorithm with sublinear regret exists" argument would tolerate.

Formalization scope

Matrices are Matrix (Fin n) (Fin m) ℝ with n, m ≥ 1 (empty strategy sets are excluded throughout, matching this mission's reference item AGT.zero_sum_minimax); mixed strategies use Mathlib's stdSimplex ℝ (Fin n). lambdaR/lambdaC are rendered with iInf/iSup over simplex membership, the same convention Introduction to Online Convex Optimization III fixed for RegretT earlier in this series. Algorithm 28's run is packaged as a Prop-valued structure (IsSimpleLPRun) rather than a computable function, in the style of this series' other algorithm-run definitions (IsHedgeRun, IsOnlineGradientDescent): initial uniform strategy, a best-response condition on the column player at every round, and the multiplicative-weights recursion on the row player, with the learning rate η left free and fixed to √(2 log n / T) only at the point the theorems need the book's specific constant.

The trivializing risk here is stating only that some sublinear-regret algorithm secures the bound (already implied, vacuously, by AGT.zero_sum_minimax plus any regret bound); this mission rules that out by fixing the exact update rule of Algorithm 28 in IsSimpleLPRun and proving the bound for that rule specifically, with the book's exact constant √(2 log n)/√T, not an unspecified O(·).

Chapter 5's Corollary 5.7 (the general RFTL/Exponentiated-Gradient regret bound) belongs to a different mission of this series and is not imported; eg_regret_bound restates, locally and self-containedly, exactly the instance of it this chapter's proof needs. A later mission for Chapter 5, once published, could supersede this local restatement by specializing its general bound — a natural contribution for a solver with that mission's Lean available.

Selected references

• J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen, 1928.
• Y. Freund and R. E. Schapire, "Adaptive Game Playing Using Multiplicative Weights", Games and Economic Behavior, 1999. https://doi.org/10.1006/game.1999.0738
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., 2022. arXiv:1909.05207v3
• N. Nisan, T. Roughgarden, E. Tardos, and V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007. https://doi.org/10.1017/CBO9780511800481
• S. Arora, E. Hazan, and S. Kale, "The Multiplicative Weights Update Method: a Meta-Algorithm and Applications", Theory of Computing, 2012. https://doi.org/10.4086/toc.2012.v008a006

Motivation

Reinforcement learning (RL) formalizes sequential decision-making under uncertainty: an agent repeatedly observes a state, takes an action, receives a reward, and transitions to a new state, with the goal of maximizing cumulative reward over an unknown environment. It underlies applications from game-playing agents to robotics and adaptive medical treatment. What separates RL from the bandit and contextual bandit problems of earlier chapters in this series is state: the environment carries information forward across time steps, so a good action now can pay off many steps later, and a poor exploration strategy can take exponentially long to discover it. This mission formalizes the foundational results of finite-horizon episodic RL — the Markov Decision Process (MDP) model, the Bellman-optimality principle that makes dynamic programming possible, and the analytical toolkit (the performance-difference and Bellman-residual-decomposition lemmas) used throughout the field's regret analyses — culminating in a polynomial regret guarantee for UCB-VI, the canonical optimism-based algorithm for tabular RL introduced by Azar, Osband, and Munos (Minimax Regret Bounds for Reinforcement Learning, ICML 2017, arXiv:1703.05449).

Setting

A finite-horizon episodic Markov Decision Process $M = (S, A, \{P^M_h\}_{h=1}^H, \{R^M_h\}_{h=1}^H, d_1)$ consists of a finite state space $S$, a finite action space $A$, a horizon $H$, per-layer transition kernels $P^M_h : S\times A \to \Delta(S)$ and reward distributions $R^M_h : S\times A \to \Delta(\mathbb R)$, and an initial state distribution $d_1 \in \Delta(S)$. An episode unrolls for $h=1,\dots,H$: the learner selects an action $a_h \sim \pi_h(s_h)$ under a randomized non-stationary policy $\pi = (\pi_1,\dots,\pi_H) \in \Pi^{\mathrm{rns}}$ (each $\pi_h : S \to \Delta(A)$), receives reward $r_h \sim R^M_h(s_h,a_h)$, and transitions to $s_{h+1}\sim P^M_h(s_h,a_h)$. The value of $\pi$ is $f^M(\pi) := \mathbb E^{M,\pi}[\sum_h r_h]$, and the state-action and state value functions $Q^{M,\pi}_h(s,a)$, $V^{M,\pi}_h(s)$ are the analogous reward-to-go quantities from layer $h$ onward. In the online RL problem, $M^\star$ is unknown, the learner interacts with it for $T$ episodes, and the goal is to minimize the regret $\mathrm{Reg} = \sum_{t=1}^T \big(f^{M^\star} (\pi^{M^\star}) - f^{M^\star}(\pi^t)\big)$ against the best policy $\pi^{M^\star} \in \arg\max_{\pi\in\Pi^{\mathrm{rns}}} f^{M^\star}(\pi)$.

Formalization targets

Goal — Theorem 1 (UCB-VI regret)

for the UCB-VI algorithm run with the explicit bonus $b^t_{h,\delta}(s,a) = 2\sqrt{\log(2SAHT/\delta)/n^t_h(s,a)}$, under Assumption 6 (deterministic, known, $[0,1]$-bounded rewards). This is the weakest stable form of the guarantee: it fixes only the shape of the bound (polynomial in $S,A,H,T$, logarithmic in $1/\delta$), leaving the exact leading constant — which the book itself does not pin down on this page — outside the formal claim.

Reaching it rests on three structural facts, each formalized as a milestone in attack order:

• Proposition 25 (Bellman optimality): existence of a single deterministic policy simultaneously optimal at every state, computable by backward induction — the reason dynamic programming solves planning at all.
• Lemma 13 (Performance difference) and Lemma 14 (Bellman residual decomposition): two "credit assignment" identities decomposing a value gap (between two policies, or one policy under two models) into a sum of per-layer, on-roll-in terms.
• Lemma 15 (Error decomposition for optimistic policies): the fact that a greedy policy driven by any optimistic value estimate suffers sub-optimality controlled additively — not exponentially — by that estimate's own Bellman residuals, evaluated on-policy.

Significance

The result itself. Theorem 1 is the chapter's headline result: the first guarantee, in this development, that a learning algorithm — one that does not know the environment's transitions in advance — can achieve regret growing only polynomially in the size of the state space, the action space, and the horizon, and only as $\sqrt T$ in the number of episodes. The chapter's own "combination lock" example (Figure 8) shows this is not automatic: naive exploration strategies (such as $\varepsilon$-greedy, which suffices for ordinary bandits) incur regret exponential in the horizon on some MDPs with as few as $H+2$ states. UCB-VI's guarantee is the sample-complexity foundation on which essentially every subsequent result on tabular, linear, and general function-approximation RL in the book is built.

Formalizing it. No part of this chapter's mathematical content already has a faithful counterpart on the platform (see Difficulty, below, and Formalization scope). This mission contributes: (i) a from-scratch Lean formalization of the finite-horizon episodic MDP model and its value functions, faithful to the book's $0$/$1$-indexing and reward-distribution conventions; (ii) faithful statements (drafted with sorry, not yet proved) of Proposition 25 and Lemmas 13–15; and (iii) a faithful statement of Theorem 1 itself, including a from-scratch construction of the finite $T$-episode adaptive interaction process needed to make sense of a high-probability regret guarantee. Proving these — Proposition 25 by backward induction, Lemmas 13–15 by telescoping, and Theorem 1 by combining Lemma 15's optimism bound with a concentration argument bounding the estimation-error and martingale terms of Eqs. (5.30)–(5.33) (omitted here; see Difficulty) — is open work for solvers.

Difficulty

The obvious approach to Theorem 1 — bound the regret episode-by-episode using only the fact that $Q^t$ is close to $Q^{M^\star,\star}$ in some fixed sense — fails because $Q^t$'s error is itself random (it depends on the transitions observed so far) and compounds across $H$ layers of dynamic programming. Lemma 15 defuses the compounding: it shows the sub-optimality gap is additive in the per-layer Bellman residuals rather than multiplicative, provided $Q^t$ is optimistic. Making $Q^t$ optimistic with high probability, in turn, requires a concentration argument for the empirical transition estimates $\widehat P^t_h$ (an application of Freedman's or the Azuma–Hoeffding inequality, not included among this mission's milestones) and a union bound over all $(s,a,h,t)$ — accounting for the $SAHT$ inside the bonus's logarithm. The final regret sum further requires bounding $\sum_t \sum_h 1/\sqrt{n^t_h(s^t_h,a^t_h)}$ by a pigeonhole/potential-function argument over the visitation counts, which is where the $S\sqrt{AT}$ scaling — rather than a naive $SA\sqrt{T}$ — originates. None of this concentration or counting machinery is included in the current milestones; a solver attempting Theorem 1 needs it as prerequisite lemmas.

Formalization scope

MDP and value functions. States and actions are finite types (Fintype); layers are represented $0$-indexed throughout the Lean development (the book's layer $h$ is h - 1), with the terminal convention V _ _ H _ = 0 matching $V_{H+1}\equiv 0$. Since every value/expectation formula in this chapter uses the reward distribution $R_h(s,a)\in\Delta(\mathbb R)$ only through its mean, EpisodicMDP.R records that mean directly — equivalent, by linearity of expectation, to carrying the full distribution, and changing no theorem's content. Transition kernels and policies are represented as plain real-valued functions (S → A → ℝ-style) rather than as Mathlib's PMF, with IsPolicy/the EpisodicMDP structure's own proof fields asserting the probability-distribution properties (nonnegativity, summing to $1$) where the book requires membership in $\Pi^{\mathrm{rns}}$ or a well-formed kernel; this keeps every expectation a finite Finset.sum, needing no measure theory. The optimal value functions Qstar/Vstar are defined as literal suprema over the entire (uncountable, since $|A|\ge2$) policy type — not via a recursive shortcut — which is what rules out the trivializing formalization of Proposition 25: defining Vstar by the very recursion the proposition asserts would make the proposition a tautology, whereas here it is a genuine claim about a supremum over an enormous space of competitor policies.

UCB-VI and Theorem 1. Because $S$, $A$, $H$, and $T$ are all finite, the $T$-episode adaptive interaction (in which round $t$'s policy is a function of the realized history of the first $t-1$ episodes) is modeled as a finite probability space: the outcome type Fin T → Trajectory S A H is a Fintype, "probability" is a finite sum over it, and "with probability $\ge 1-\delta$" is a plain inequality between two real numbers — no MeasureTheory is used anywhere in this mission. The universal constant $C$ in Theorem 1 is existentially quantified (∃ C > 0, …) rather than given as a literal numeral, since its value is not pinned down by the book on this page and this mission does not carry out the (non-milestoned) concentration argument that would derive it; this is the convention adopted throughout for the book's own "$\lesssim$" notation. The empirical-transition estimator inside $Q^t_h$ is defined to be $0$ when $n^t_h(s,a)=0$ (no data yet collected for that pair) — a boundary case Eq. (5.25) does not address, resolved here by convention rather than proof.

Prior art. The platform's existing BanditAlgorithm.UCRL2Algorithm mission formalizes UCRL2 for the average-reward, infinite-horizon MDP setting with a diameter parameter, and its Bellman-optimality statement is the average-cost optimality equation — genuinely different from this chapter's finite-horizon episodic Bellman recursion, even though both go by the name "Bellman optimality." No reference item was reused; every definition and theorem in this mission is drafted from scratch. Both missions bound regret via optimism over a confidence set of models, but for different objectives (average reward vs. finite-horizon cumulative reward) and different MDP classes.

Reusable infrastructure and open contributions. EpisodicMDP, Policy, V/Q/Qstar/Vstar, and stateDist/stateExp are reusable by any future mission on finite-horizon episodic RL in this book's later chapters. Contributions welcome: proofs of the four milestone lemmas (by backward induction and telescoping, respectively); the concentration lemmas underlying Theorem 1's optimism guarantee (Eqs. (5.30)–(5.33) of the source, not milestoned here); and the final regret proof combining them.

Selected references

• Foster, D. J. and Rakhlin, A., Foundations of Reinforcement Learning and Interactive Decision Making, 2023. arXiv:2312.16730v1
• Azar, M. G., Osband, I., and Munos, R., Minimax Regret Bounds for Reinforcement Learning, ICML 2017. arXiv:1703.05449
• Jaksch, T., Ortner, R., and Auer, P., Near-optimal Regret Bounds for Reinforcement Learning, JMLR 11 (2010).

How quickly does the empirical mean of independent random variables concentrate around the true mean? This question is the analytic engine of the entire theory of stochastic bandits: every optimistic algorithm (Explore-Then-Commit, UCB and its relatives) is calibrated by a tail bound on the sample mean. This mission formalizes the subgaussian framework of Chapter 5 of Lattimore–Szepesvári's Bandit Algorithms: a random variable $X$ is $\sigma$-subgaussian when $\mathbb{E}[e^{\lambda X}] \le e^{\lambda^2\sigma^2/2}$ for all $\lambda$, and the Cramér–Chernoff method converts this moment-generating-function control into the exponential tail $\mathbb{P}(X \ge \varepsilon) \le e^{-\varepsilon^2/(2\sigma^2)}$. The goal theorem is the Hoeffding-type bound: the sample mean of $n$ independent $\sigma$-subgaussian deviations exceeds the true mean by $\varepsilon$ with probability at most $\exp(-n\varepsilon^2/(2\sigma^2))$, together with its confidence form $\mathbb{P}\big(\hat\mu + \sqrt{2\sigma^2\log(1/\delta)/n} \le \mu\big) \le \delta$ — the exact bound every UCB index is built from. These few lines of analysis are cited by every regret bound in the series.