All missions

Motivation

The MDL and Occam principles of Chapter 7 rank hypotheses by description length and pay for a hypothesis according to its rank. Chapter 31 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), generalizes this to the PAC-Bayesian approach of McAllester: prior knowledge is a prior distribution $P$ over the class, the learner outputs a posterior $Q$, read as the randomized predictor that draws $h \sim Q$, and the price of $Q$ is its Kullback–Leibler divergence from $P$. The PAC-Bayes theorem (Theorem 31.1) says that with probability $1 - \delta$, simultaneously for every posterior, the generalization loss exceeds the training loss by at most $\sqrt{(D(Q\|P) + \ln(m/\delta))/(2(m-1))}$. Its proof is a compact and elegant argument: Markov's inequality for an exponential moment, a change of measure from $Q$ to $P$ by Jensen's inequality, an exchange of expectations that is possible because the prior does not depend on the sample, and a moment bound for the deviation of a single hypothesis. The bound suggests the learning rule of Remark 31.1, minimize $L_S(Q)$ plus the divergence penalty, which is regularized risk minimization in disguise, and for a finite class with a uniform prior it recovers an Occam-type bound (Exercise 2).

Setting

$H$ is a measurable space of hypotheses, $\ell : H \times Z \to [0,1]$ a jointly measurable loss, $D$ a distribution over $Z$, and $P$ a prior probability measure on $H$. For a posterior $Q$, $\ell(Q, z) = \mathbb{E}_{h \sim Q}[\ell(h, z)]$, $L_D(Q) = \mathbb{E}_{h \sim Q}[L_D(h)]$ and $L_S(Q) = \mathbb{E}_{h \sim Q}[L_S(h)]$, and $D(Q\|P) = \mathbb{E}_{h \sim Q}[\ln(dQ/dP)]$ is the Kullback–Leibler divergence, a real number when $Q \ll P$ and the log-density is $Q$-integrable.

Formalization targets

Goal: Theorem 31.1

For $m \ge 2$ and $\delta \in (0,1)$, with probability at least $1 - \delta$ over $S \sim D^m$, every probability measure $Q \ll P$ with finite divergence satisfies

$$L_D(Q) \le L_S(Q) + \sqrt{\frac{D(Q\|P) + \ln(m/\delta)}{2(m-1)}}.$$

Milestones

The identity $\mathbb{E}_{z \sim D}[\ell(Q, z)] = L_D(Q)$ (§31.1); the moment bound $\mathbb{E}_S[e^{2(m-1)\Delta(h)^2}] \le m$ of the proof (p. 417); Exercise 2, the bound for a finite class with the uniform prior.

Significance

PAC-Bayes bounds are among the tightest generalization bounds known in practice, and the reason is visible in Theorem 31.1: the complexity term is not a property of the class but of the posterior actually chosen, measured against a prior, so a learner that stays close to its prior generalizes even in a huge class. The theorem is the ancestor of a large literature (Seeger, Langford, Catoni, Maurer) and of modern nonvacuous bounds for neural networks. Formally it is a pleasant target: the change-of-measure inequality $\mathbb{E}_{h \sim Q}[f(h)] - D(Q\|P) \le \ln\mathbb{E}_{h \sim P}[e^{f(h)}]$ is the Donsker–Varadhan inequality, of independent value, and the moment bound is a sharp sub-Gaussian fact. On the platform, the mission introduces Gibbs risks and the Kullback–Leibler divergence between measures on a class, ending the book's series with its last learning principle.

Difficulty

The Gibbs risk identity is Fubini for a bounded jointly measurable function. The moment bound is the delicate step: the book derives it from Hoeffding's tail bound through Exercise 1, whose one-sided hypothesis is not enough (a constant negative variable satisfies it with an unbounded moment), and even the two-sided tail integrates only to $2m - 1$; the claim $\le m$ is nevertheless true, for instance by writing $e^{a\Delta^2} = \mathbb{E}_g[e^{\sqrt{2a}\,g\Delta}]$ for a standard Gaussian $g$ and applying Hoeffding's lemma to the sample mean, which gives $\mathbb{E}_S[e^{2(m-1)\Delta^2}] \le (1 - (m-1)/m)^{-1/2} = \sqrt m$. Theorem 31.1 then follows the book: Markov's inequality on $e^{f(S)}$ with $f(S) = \sup_Q(2(m-1)\mathbb{E}_{h \sim Q}\Delta(h)^2 - D(Q\|P))$, the change of measure (31.2) by Jensen's inequality for $\ln$ applied to the density $dQ/dP$ (the Donsker–Varadhan inequality, which needs $Q \ll P$ and an integrable log-density), the exchange of expectations (31.4) by Fubini, the moment bound, and finally Jensen for $x^2$ in (31.6); formally the supremum over all posteriors is handled by proving the bound for each $Q$ on the event $\{S : \mathbb{E}_{h \sim P}[e^{2(m-1)\Delta(h)^2}] \le m/\delta\}$, whose complement has probability at most $\delta$ by Markov, which sidesteps any measurability question about $f$. Exercise 2 is the theorem with $Q = \delta_h$, for which $D(Q\|P) = \ln|H|$.

Formalization scope

The class is an arbitrary measurable space, priors and posteriors are probability measures on it, and $Q(h)/P(h)$ is Mathlib's Radon–Nikodym derivative; the divergence is a Bochner integral, so the theorem quantifies over posteriors $Q \ll P$ whose log-density is $Q$-integrable, exactly the posteriors with a finite divergence, for which the bound has content, and no junk value can make a case false. Posteriors may depend on the sample: the statement bounds the outer measure of the set of samples for which some admissible $Q$ violates the bound. The loss is jointly measurable so that $h \mapsto L_D(h)$ and $(S, h) \mapsto L_S(h)$ are measurable and the Gibbs risks are genuine integrals; $m \ge 2$ is forced by the denominator $2(m-1)$. The moment bound is stated as the claim the proof needs rather than as Exercise 1, whose printed hypothesis is insufficient; the item text records this. Exercise 2 is stated as a simultaneous bound over the finite class, the form in which the theorem delivers it.

Not stated: Remark 31.1 (a learning rule, not a theorem), Exercise 1 as printed, and the second part of Exercise 2.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 31. doi:10.1017/CBO9781107298019
• D. A. McAllester, Some PAC-Bayesian theorems, Machine Learning 37, 1999. doi:10.1023/A:1007618624809
• D. A. McAllester, PAC-Bayesian stochastic model selection, Machine Learning 51, 2003. doi:10.1023/A:1021840411064
• A. Maurer, A note on the PAC Bayesian theorem, arXiv:cs/0411099, 2004.
• M. Seeger, PAC-Bayesian generalisation error bounds for Gaussian process classification, Journal of Machine Learning Research 3, 2002.
• J. Langford, J. Shawe-Taylor, PAC-Bayes and margins, NIPS 2002.

Motivation

A feedforward neural network is a directed acyclic graph of neurons, each computing a fixed scalar activation of a weighted sum of its inputs; fixing the graph and the activation and letting the weights vary gives a hypothesis class. Chapter 20 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), studies these classes through the book's three lenses. Approximation: every Boolean function is implemented by a network of depth 2 (Claim 20.1), but only at exponential size (Theorem 20.2), while a sign neuron implements conjunctions and disjunctions (Lemma 20.4), the bridge to Boolean circuits and hence to everything computable in bounded time. Estimation: the VC dimension of the class of sign networks over a graph with $|E|$ edges is $O(|E|\log|E|)$ (Theorem 20.6), so the sample complexity is governed by the number of weights. Optimization: training is NP-hard even for tiny networks, and the practical answer is SGD with the gradient computed by backpropagation, whose correctness the chapter derives from the chain rule.

Setting

A layered graph has layers $V_0, \dots, V_T$, every edge joining $V_{t-1}$ to $V_t$; $V_0$ holds the $n$ inputs and a constant neuron outputting $1$. With weights $w : E \to \mathbb{R}$ and an activation $\sigma$, the outputs are computed layer by layer, $a_{t+1,i} = \sum_{j : (v_{t,j}, v_{t+1,i}) \in E} w_{t,i,j}\,o_{t,j}$ and $o_{t+1,i} = \sigma(a_{t+1,i})$. The class $H_{V,E,\sigma} = \{h_{V,E,\sigma,w} : w : E \to \mathbb{R}\}$ (20.1); for binary classification the output layer is a single neuron and $\sigma$ is the sign function, so $H_{V,E,\operatorname{sign}}$ is a set of $\{\pm1\}$-valued predictors on $\mathbb{R}^n$. The size of the network is $|V|$, its depth $T$. The growth function $\tau_H(m) = \max_{|C| \le m}|H_C|$ extends to classes with any finite codomain (p. 275), and the proof of Theorem 20.6 uses two of its properties, stated as Exercises 3 and 4: the growth function of a product class is at most the product of the growth functions, and likewise for a composition class. For backpropagation the activation is any differentiable $\sigma$ and the loss is $\frac12\|o_T - y\|^2$; the backward pass sets $\delta_T = o_T - y$ and $\delta_t = \delta_{t+1}\operatorname{diag}(\sigma'(a_{t+1}))W_t$.

Formalization targets

Goal: Theorem 20.6

The VC dimension of $H_{V,E,\operatorname{sign}}$ is $O(|E|\log|E|)$. Explicitly, for a layered graph of depth at least $1$ with a single output neuron,

$$\operatorname{VCdim}(H_{V,E,\operatorname{sign}}) \le 2|E|\log_2(16|E|),$$

stated as: every $m \le \operatorname{VCdim}$ satisfies this bound (so the VC dimension is finite).

Milestones

Claim 20.1 (the depth-2 graph with $|V_1| = 2^n + 1$ whose sign class contains every function $\{\pm1\}^n \to \{\pm1\}$); Theorem 20.2 (every sign network implementing all functions $\{0,1\}^n \to \{0,1\}$ has $2^{n/3} \le 2|V|$); Lemma 20.4 (conjunction and disjunction as sign neurons); Exercise 4 (growth function of a composition); the correctness of backpropagation (§20.6: the partial derivative for the edge $(v_{t,j}, v_{t+1,i})$ is $\delta_{t+1,i}\sigma'(a_{t+1,i})o_{t,j}$). Further items: Exercise 3 (growth function of a product) and the intermediate bound $\tau_H(m) \le (em)^{|E|}$ of the proof of Theorem 20.6.

Significance

Theorem 20.6 is the reason networks are learnable at all in the book's sense: by the fundamental theorem, a class with finite VC dimension is agnostic PAC learnable with sample complexity linear in that dimension, and here the dimension is essentially the number of tunable parameters. The proof technique, due to Kakade and Tewari's lecture notes, is a composition-and-product argument on growth functions that applies to any layered class of threshold units and is reusable well beyond this chapter. Theorem 20.2 is the matching negative fact on expressive power, and it is a corollary of the same bound: a class that shatters $2^n$ points needs $\Omega(2^n)$ edges. Backpropagation's correctness is the one theorem about training the chapter can offer, given the hardness results, and it is the algorithm every practitioner runs.

Difficulty

Claim 20.1 and Lemma 20.4 are explicit constructions: the neuron $g_i(x) = \operatorname{sign}(\langle x, u_i\rangle - n + 1)$ detects $x = u_i$ because $\langle x, u_i\rangle \le n - 2$ otherwise, and the output neuron takes the disjunction; formally one must build the weight function and evaluate the forward pass on the $2^n$ inputs. Exercises 3 and 4 are counting: a restricted product is determined by its two restricted factors, and a restricted composition $f_2 \circ f_1$ on $C$ is determined by $f_1|_C$ and $f_2|_{f_1(C)}$, with $|f_1(C)| \le |C|$. Theorem 20.6 then needs: the class of one neuron is the class of homogenous halfspaces on its $d_{t,i}$ incoming coordinates, of VC dimension at most $d_{t,i}$ (Mission VI), Sauer's lemma in the form $\tau(m) \le (em)^{d}$ for every $m \ge 1$ (Mission IV; for $m \le d$ use $2^m \le (em)^m$), the layer class as a product and the network as a composition of layer classes, and finally the arithmetic $2^m \le (em)^{|E|} \Rightarrow m \le 2|E|\log_2(16|E|)$, which replaces the book's appeal to Lemma A.2 (for $m \ge 8|E|$ one has $\ln m \le \frac{m\ln 2}{2|E|}$). Theorem 20.2 follows from the goal with $|E| \le |V|^2$. Backpropagation is a chain-rule computation in a single real variable: the loss as a function of one weight is a composition of finitely many differentiable maps, and the derivative unwinds to the backward recursion; the formal effort is in the induction along layers with the natural-number indexing of the model.

Formalization scope

Layers and neurons are indexed by natural numbers: a LayeredGraph records the depth, the layer widths and, for each $t < T$, the finite set of edges $(v_{t,j}, v_{t+1,i})$ as pairs $(i, j)$ within the layer widths. Weights are functions on all index triples, and only those on edges are used, so the class is the image of all weight functions, as in (20.1). The forward computation netOutput is a recursion on the layer index; netInput is $a_{t+1,i}$. The sign activation returns $\pm1$ with $\operatorname{sign}(0) = -1$, the book's convention elsewhere, and a neuron with no incoming edges outputs $\sigma(0)$ (p. 270). The binary class signNetClass n G is Bool-valued, true iff the output neuron's input is positive, and is stated for graphs of depth at least $1$ (for depth $0$ the edges out of the input layer would be used but not counted in $|E|$). Growth functions with finite codomain are growthY, an sSup over restriction sizes, well defined because the codomains are finite; the Bool case is Mission IV's growth, and VC dimension and shattering are Mission IV's. Theorem 20.6 and Theorem 20.2 are given with explicit constants derived from the proof, since $O(\cdot)$ statements have no formal content; the drafter verified $\max\{m : 2^m \le (em)^{|E|}\} \le 2|E|\log_2(16|E|)$ numerically for $|E|$ up to $3000$ and at $10^4, \dots, 10^7$, and $2^n \le 2|V|^2\log_2(16|V|^2) \le 8|V|^3$. Backpropagation is stated for an arbitrary layered graph (phantom edges have weight $0$, p. 279), any differentiable activation, and one edge at a time as a HasDerivAt of the loss in that weight; $\delta_t$ is defined by recursion on $T - t$. The book's layer indices in (20.3) are shifted by one in the statement.

Not stated: Theorem 20.3 (Turing machines), Theorem 20.5 and Exercise 1 (sigmoid approximation, which needs a convention for outputs in $[-1,1]$ that the chapter leaves open), Theorem 20.7 and Exercise 6 (NP-hardness), Exercise 5 (the $\Omega(|E|^2)$ sigmoid lower bound, which assumes an exact threshold), the sigmoid half of Theorem 20.2, and the SGD pseudocode of §20.6, which is a heuristic without a stated guarantee.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 20. doi:10.1017/CBO9781107298019
• M. Anthony, P. L. Bartlett, Neural Network Learning: Theoretical Foundations, Cambridge University Press, 1999. doi:10.1017/CBO9780511624216
• D. E. Rumelhart, G. E. Hinton, R. J. Williams, Learning representations by back-propagating errors, Nature 323, 1986. doi:10.1038/323533a0
• I. Parberry, Circuit Complexity and Neural Networks, MIT Press, 1994.
• E. B. Baum, D. Haussler, What size net gives valid generalization?, Neural Computation 1(1), 1989. doi:10.1162/neco.1989.1.1.151

Motivation

Whether the gravitational field must be quantized is a long-standing foundational question. A well-known family of arguments tries to settle it by consistency alone: if a classical field were coupled to a quantum system, some basic principle — momentum conservation, the uncertainty relations, or the impossibility of superluminal signalling — would allegedly be violated. The two best-known versions are the gedanken experiment of Eppley and Hannah (1977) and the measurement-theoretic argument of DeWitt (1962).

Albers, Kiefer and Reginatto (Phys. Rev. D 78, 064051 (2008)) re-examine both arguments. Their paper is largely conceptual, but several of its steps are precise, checkable mathematical claims. This mission collects those claims and makes them machine-checkable.

Timeline.

• 1962 — DeWitt's measurement analysis of the gravitational field, using Peierls brackets and a "universal principle" for apparatus uncertainties.
• 1977 — Eppley and Hannah's gedanken experiment: a classical gravitational wave scattered off a quantum particle would imply momentum non-conservation, a violation of the uncertainty principle, or superluminal signalling.
• 2008 — Albers, Kiefer and Reginatto argue that neither gedanken experiment forces quantization, and exhibit a consistent hybrid classical–quantum model.

Setting

Photon pair and detector (Sec. II). Each photon carries a polarization qubit with orthonormal basis $|\uparrow\rangle$ (horizontal) and $|\downarrow\rangle$ (vertical). A detector with state space $\mathcal H$ (an arbitrary complex inner-product space) is coupled to photon 1. Before the measurement the joint state of photon 1, photon 2 and the detector is

$$|\Psi_0\rangle = \tfrac{1}{\sqrt2}\bigl(|\uparrow\rangle_1|\downarrow\rangle_2 - |\downarrow\rangle_1|\uparrow\rangle_2\bigr)|\Phi_0\rangle, \qquad (1)$$

and after the detector has measured photon 1 it is

$$|\Psi\rangle = \tfrac{1}{\sqrt2}\bigl(|\uparrow\rangle_1|\downarrow\rangle_2|\Phi_\uparrow\rangle - |\downarrow\rangle_1|\uparrow\rangle_2|\Phi_\downarrow\rangle\bigr). \qquad (2)$$

The reduced density operator of photon 2 is obtained from $|\Psi\rangle\langle\Psi|$ by tracing out photon 1 and the detector; the paper asserts that for both states it equals

$$\hat\rho = \tfrac12\bigl(|\uparrow\rangle_2\langle\uparrow|_2 + |\downarrow\rangle_2\langle\downarrow|_2\bigr). \qquad (3)$$

Mass cube and gravitational wave (Sec. III B). The disturbance $\delta T^{\mathrm{GW}}_{00}$ of the averaged energy density of the scattered wave depends on the cube's edge length $a$ and speed $v$, with sensitivities $T_a = \partial\,\delta T^{\mathrm{GW}}_{00}/\partial a$ and $T_v = \partial\,\delta T^{\mathrm{GW}}_{00}/\partial v$. With $\Delta a \approx \Delta x$ and $\Delta v \gtrsim \hbar/(2m\Delta x)$ the uncertainty $\Delta T^{\mathrm{GW}}_{00} = \sqrt{(T_a\Delta a)^2 + (T_v\Delta v)^2}$ has a strictly positive lower bound.

DeWitt's argument (Sec. V). A system observable $s$ reconstructed from apparatus data has uncertainty $\Delta s^2 = \Delta A^2/g^2 + g^2(\Delta D_\Omega s)^2$, where $g$ is the coupling constant.

Formalization targets

Goal — no signalling through photon 2 (Eq. (3))

For all unit vectors $\Phi_0, \Phi_\uparrow, \Phi_\downarrow \in \mathcal H$,

$$\rho_2(\Psi_0) = \hat\rho \quad\text{and}\quad \rho_2(\Psi) = \hat\rho .$$

Milestones

1. Eq. (1) ⇒ (3): $\rho_2(\Psi_0) = \hat\rho$.
2. Eq. (2) ⇒ (3): $\rho_2(\Psi) = \hat\rho$.
3. Sec. III B lower bound: $\Delta T^{\mathrm{GW}}_{00} \ge \sqrt{\tfrac{\hbar}{m} T_v T_a}$ whenever $\Delta x > 0$ and $\Delta v \ge \hbar/(2m\Delta x)$.
4. Sec. III B optimum: the function $\Delta x \mapsto \sqrt{(T_a\Delta x)^2 + (T_v\hbar/(2m\Delta x))^2}$ attains its minimum over $\Delta x>0$ at $\Delta x_{\min} = \sqrt{\tfrac{\hbar}{2m}\tfrac{T_v}{T_a}}$, with value $\sqrt{\tfrac{\hbar}{m}T_vT_a}$.
5. Eq. (61): $\min_{g\ne0}\sqrt{\Delta A^2/g^2 + g^2\Delta D^2} = \sqrt{2\,\Delta A\,\Delta D}$.
6. Eq. (64): if $\Delta A\,\Delta C \ge \hbar/2$ then $\sqrt{\hbar\,|D_s s|} \le \sqrt{2\,\Delta A\,\Delta C\,|D_s s|}$.

Significance

The goal is the precise content of the paper's rebuttal of the superluminal-signalling branch of the Eppley–Hannah argument: the state of photon 2 accessible to a probe (such as a classical gravitational wave) is the same whether or not photon 1 has been measured, so a probe of photon 2 alone cannot tell whether photon 1 was measured. Milestones 3–6 are the quantitative estimates the paper uses in Sec. III B (a coupling to a test body obeying the uncertainty principle transfers a minimum uncertainty to the classical wave) and Sec. V (DeWitt's limitation on a single observable, Eq. (64)).

The results are elementary once stated; the value of the mission is to pin the paper's claims down exactly, including the hypotheses under which they hold. None of the statements has, to our knowledge, a machine-checked proof on the platform.

Difficulty

The goal and Milestones 1–2 need a workable representation of the partial trace over a factor that is an arbitrary (possibly infinite-dimensional) inner-product space; the cross terms between the two branches vanish because the two branches are orthogonal on photon 1, not because of any property of the detector states. Milestones 3–6 are single-variable optimization statements; the main care is in the side conditions (positivity, excluding $g=0$ and $\Delta x = 0$).

Formalization scope

• The joint space $\mathbb C^2\otimes\mathbb C^2\otimes\mathcal H$ is represented by functions $\{0,1\}\times\{0,1\}\to\mathcal H$ (component $\Psi_{ij}$ along $|i\rangle_1|j\rangle_2$; index $0 = \uparrow$, $1 = \downarrow$). The reduced density matrix of photon 2 has entries $\rho_2(j,j') = \sum_i \langle \Psi_{ij'}, \Psi_{ij}\rangle_{\mathcal H}$, and $\hat\rho$ is a $2\times2$ complex matrix.
• The detector states are only assumed to be unit vectors. Orthogonality of $|\Phi_\uparrow\rangle$ and $|\Phi_\downarrow\rangle$ (a physical property of a detector that records the outcome) is not assumed, because Eq. (3) does not depend on it.
• In Sec. III B the sensitivities $T_a, T_v$, the mass $m$ and $\hbar$ are positive reals; the paper's approximate relations $\Delta a\approx\Delta x$ and $\Delta p\gtrsim\hbar/\Delta x$ are encoded as $\Delta a = \Delta x$ and the hypothesis $\Delta v \ge \hbar/(2m\Delta x)$.
• In Eq. (61) the coupling constant ranges over all non-zero reals.
• Sections IV (hybrid classical–quantum ensembles for Nordström gravity) and the appendices are out of scope for this mission.

Selected references

• M. Albers, C. Kiefer, M. Reginatto, Measurement analysis and quantum gravity, Phys. Rev. D 78, 064051, 2008. https://doi.org/10.1103/PhysRevD.78.064051
• K. Eppley, E. Hannah, The necessity of quantizing the gravitational field, Found. Phys. 7, 51–68, 1977. https://doi.org/10.1007/BF00715241
• B. S. DeWitt, Definition of commutators via the uncertainty principle, J. Math. Phys. 3, 619, 1962. https://doi.org/10.1063/1.1724265

Motivation

The book The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) develops a perturbative, physics-style theory of wide deep neural networks. Every later computation in the book, from the statistics of preactivations at initialization to the neural tangent kernel, reduces to Gaussian expectations of polynomials. The single tool that evaluates these expectations is Wick's theorem (eq. 1.45), which the authors ask the reader to "put a box around". This mission formalizes Chapter 1, §1.1 (Gaussian Integrals), culminating in that theorem. It is the first mission of a series formalizing the book, all in the Lean namespace DeepLearningTheory.

Setting

Fix $N \ge 0$ and a symmetric positive-definite real $N\times N$ matrix $K = (K_{\mu\nu})$, the covariance. Write $K^{\mu\nu} = (K^{-1})_{\mu\nu}$ for its inverse. The zero-mean multivariable Gaussian distribution with covariance $K$ (eq. 1.31) has density on $\mathbb{R}^N$

$$p(z) = \frac{1}{\sqrt{|2\pi K|}} \exp\Big(-\tfrac12 \sum_{\mu,\nu=1}^N z_\mu K^{\mu\nu} z_\nu\Big), \qquad |2\pi K| = \det(2\pi K) = (2\pi)^N \det K,$$

and the expectation of an observable $F$ is $\mathbb{E}[F(z)] = \int d^N z\, p(z) F(z)$ (eqs. 1.36, 1.46), an integral against Lebesgue measure. A pairing of the labels $1,\dots,2m$ is a partition into $m$ unordered pairs; equivalently, a fixed-point-free involution $\sigma$ of $\{1,\dots,2m\}$ pairing $a$ with $\sigma(a)$. There are $(2m-1)!!$ pairings.

Formalization targets

Goal: Wick's theorem (eq. 1.45)

For all indices $\mu_1,\dots,\mu_{2m} \in \{1,\dots,N\}$ (repetitions allowed),

$$\mathbb{E}[z_{\mu_1}\cdots z_{\mu_{2m}}] = \sum_{\text{pairings } \sigma}\ \prod_{a<\sigma(a)} K_{\mu_a \mu_{\sigma(a)}}.$$

Milestones

1. Eq. (1.30) — the normalization $\int d^N z\, e^{-\frac12 z^\top K^{-1} z} = \sqrt{|2\pi K|}$.
2. Eq. (1.41) — the generating function $\int d^N z\, e^{-\frac12 z^\top K^{-1} z + J\cdot z} = \sqrt{|2\pi K|}\, e^{\frac12 J^\top K J}$ for every source $J \in \mathbb{R}^N$.
3. Odd moments vanish (p. 22, discussion after eq. 1.42).
4. Eq. (1.43) — $\mathbb{E}[z_{\mu_1} z_{\mu_2}] = K_{\mu_1\mu_2}$.
5. Eq. (1.44) — $\mathbb{E}[z_{\mu_1}z_{\mu_2}z_{\mu_3}z_{\mu_4}] = K_{\mu_1\mu_2}K_{\mu_3\mu_4} + K_{\mu_1\mu_3}K_{\mu_2\mu_4} + K_{\mu_1\mu_4}K_{\mu_2\mu_3}$.

Significance

Wick's theorem (also known as Isserlis' theorem, 1918) is used throughout the book: the Gaussianity of the first layer (Chapter 4), the four-point correlators of deep linear networks (Chapter 3), and all perturbative expansions around the infinite-width limit are evaluated by Wick contractions. A machine-checked version stated in the book's own density-based conventions gives later missions of this series a dependable foundation. The result is classical; the work remaining is its formalization in exactly this form. A related statement for general (possibly degenerate) Gaussian measures already exists on the platform as FeynmanWick.wick_theorem_gaussian; the present mission keeps the book's formulation via the explicit density and a positive-definite covariance.

Difficulty

The book's derivation differentiates the generating function (1.41) $2m$ times at $J=0$, which requires justifying differentiation under the integral sign and organizing the combinatorics of the product rule into pairings. Both the analytic step (dominated convergence for Gaussian tails, in $N$ dimensions) and the combinatorial step (a bijection between surviving terms and pairings, with the $1/(2^m m!)$ normalization) are routine on paper but need care in Lean. Computing the normalization (1.30) itself requires diagonalizing $K$ and a linear change of variables.

Formalization scope

• Vectors are functions Fin N → ℝ with Lebesgue measure; $K$ is a Matrix (Fin N) (Fin N) ℝ with K.PosDef (which includes symmetry). The inverse is Mathlib's K⁻¹.
• gaussianDensity K z and gaussExpect K F are exactly the book's $p(z)$ and $\mathbb{E}[F]$; gaussQuadForm K z is $\sum z_\mu K^{\mu\nu} z_\nu$.
• pairings (2m) is the finite set of fixed-point-free involutions of Fin (2m); the product is over labels $a$ with $a<\sigma(a)$, so each pair contributes once.
• Positive definiteness is assumed exactly as in the book; no statement is vacuous since, e.g., $K = I$ satisfies every hypothesis.

Selected references

• D. A. Roberts, S. Yaida (with B. Hanin), The Principles of Deep Learning Theory, Cambridge University Press, 2022. arXiv:2106.10165
• L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12 (1918). doi:10.1093/biomet/12.1-2.134

Motivation

A magnetohydrodynamic (MHD) equilibrium is a magnetic field $B$ and a scalar pressure $p$ on a region of $\mathbb R^3$ satisfying

$$(\nabla\times B)\times B=\nabla p,\qquad \nabla\cdot B=0 .$$

Under the substitution $B\mapsto u$ these are exactly the equations of a steady incompressible Euler flow, with $p$ replaced by the Bernoulli function, so every statement in this mission is simultaneously a statement about stationary solutions of the 3D Euler equations. Magnetic confinement of a fusion plasma requires equilibria whose pressure surfaces are nested tori, because $B\cdot\nabla p=0$ forces $p$ to be constant on the surfaces swept out by field lines.

Whether such equilibria exist without a continuous symmetry has been open since Grad, who conjectured in 1967 that smooth toroidal equilibria with non-constant pressure do not exist unless the configuration is symmetric (for instance axisymmetric), and restated the claim in 1985 as the assertion that, apart from the symmetric exceptions, there are no families of solutions depending smoothly on a parameter. Modern formulations of the conjecture appear in the work of Constantin–Drivas–Ginsberg (2021), Enciso–Luque–Peralta-Salas (2025) and Cardona–Duignan–Perrella (2025, Conjecture 2.5). Partial results have always relaxed something: Lortz (1970) obtained non-symmetric toroidal equilibria only with mirror symmetry and vanishing rotational transform; Bruno–Laurence (1996) and Enciso–Luque–Peralta-Salas (2025) allow discontinuous pressure and current sheets; Weitzner–Sengupta (2020) work in a topological torus rather than true toroidal geometry; near-axis and high-aspect-ratio expansions (Mercier 1964, Garren–Boozer 1991) give only approximate solutions.

Landreman (2026) exhibits explicit, fully non-axisymmetric, smooth analytic solutions on a genuine solid torus, with exact nested flux surfaces, finite aspect ratio and non-zero rotational transform. This mission formalizes the first of the two families presented there — the family with uniform rotational transform $\iota=2$ — in Lean 4.

Setting

Fix a parameter $0<\epsilon<1$ and set $a=\sqrt{1+\epsilon}$, $b=\sqrt{1-\epsilon}$. For a Cartesian point $x=(x_0,x_1,x_2)$ (written $(x,y,z)$ in the paper) define

$$s=\frac{x_0^2}{a^2}+\frac{x_1^2}{b^2},\qquad F=\sqrt{1-(1-s)^2-4x_2^2},$$

and the vector field

$$B=\left(\frac{2x_2x_0-(a/b)Fx_1}{s},\ \frac{2x_2x_1+(b/a)Fx_0}{s},\ 1-s\right).$$

The natural domain is the open set $U_\epsilon=\{x: 1-(1-s)^2-4x_2^2>0\}$, on which $s>0$ and all the expressions above are smooth. With

$$Q=\frac{x_0^2+x_1^2+4x_2^2}{2},\qquad H=Q+\frac{|B|^2}{2},$$

the flux label and the pressure are

$$\psi=\frac{H-1+\epsilon^2/2}{2},\qquad p=p_a-2\psi ,$$

where $p_a$ is an arbitrary constant. The level sets of $\psi$ are the pressure surfaces. For $0<\delta<(1-\epsilon)^2/4$ the region $\Omega_\delta=\{x\in U_\epsilon:\psi\le\delta\}$ is a solid torus bounded by a $\psi$-surface, and this is the plasma domain.

Field lines are described by a second coordinate system. For labels $(u,v)$ with $u^2+v^2<1/4$, putting $q^2=u^2+v^2$ and $L=\big((1+\sqrt{1-4q^2})/2\big)^{1/2}$, the position map is

$$r(u,v,\zeta)=\Big(a\big[L\cos\zeta+\tfrac{u\cos\zeta+v\sin\zeta}{L}\big],\ b\big[L\sin\zeta+\tfrac{v\cos\zeta-u\sin\zeta}{L}\big],\ v\cos2\zeta-u\sin2\zeta\Big).$$

The curve $\zeta\mapsto r(u,v,\zeta)$ is an integral curve of $B$, the pair $(u,v)$ labels the field line, and $\zeta$ acts as a toroidal angle of period $2\pi$. The magnetic axis is the field line $u=-\epsilon/2$, $v=0$, on which $\psi=0$; it is the non-planar closed curve $\gamma(\zeta)=(\sqrt{1-\epsilon^2}\cos\zeta,\ \sqrt{1-\epsilon^2}\sin\zeta,\ \tfrac{\epsilon}{2}\sin 2\zeta)$.

Target

The goal theorem asserts that for every $0<\epsilon<1$, every $0<\delta<(1-\epsilon)^2/4$ and every constant $p_a$, the pair $(B,p)$ above is a smooth equilibrium on $U_\epsilon$ that is genuinely three-dimensional:

$$\nabla\cdot B=0,\qquad (\nabla\times B)\times B=\nabla p,\qquad B\cdot\nabla p=0 \quad\text{on } U_\epsilon,$$ $$\nabla p(x)=0 \iff \psi(x)=0 \quad\text{for } x\in\Omega_\delta ,$$

together with smoothness of $B$ and $p$ on $U_\epsilon$ and the failure of axisymmetry: there is a rotation about the $z$ axis and a point of $\Omega_\delta$ whose image lies in $\Omega_\delta$ and carries a different pressure.

The milestones are the individual equations of Section 2 of the paper: divergence-freedom, the tension identity $(B\cdot\nabla)B=-\nabla Q$, force balance, invariance of $\psi$ along $B$, the field-line position map and its Jacobian $-ab$, the expressions $H=1+2\epsilon u+2(u^2+v^2)$ and $\psi=(u+\epsilon/2)^2+v^2$ in field-line labels, the magnetic axis, the enclosed volume $V=2\pi^2ab\,\psi$, the uniform rotational transform $\iota=2$, and the averages $\frac{1}{2\pi}\int_0^{2\pi}|B|^2\,d\zeta=1-\epsilon^2/2+2\psi$ and $\langle|B|^2\rangle_V=1-\epsilon^2/2+\delta$.

Significance

The solutions contradict the strict formulation of Grad's conjecture used in the recent literature (for example Conjecture 2.5 of Cardona–Duignan–Perrella), since they are smooth, have non-constant pressure, exact nested toroidal flux surfaces, no continuous Euclidean symmetry, finite aspect ratio and non-zero rotational transform, and they form continuous families parameterized by $\epsilon$ and $\delta$. Because MHD equilibrium is isomorphic to steady Euler flow, the same objects are explicit non-symmetric stationary Euler flows with invariant tori. They also serve as exact benchmarks for numerical equilibrium codes, where analytic three-dimensional solutions with known flux surfaces are otherwise unavailable.

The paper's derivations are elementary but long: they are algebraic identities among square roots and rational functions, verified in the paper by hand and by supporting numerical scripts. A machine-checked development removes the remaining doubt about sign conventions and domains, which is precisely what a counterexample to a conjecture requires. Nothing in this development is currently formalized in Mathlib: there is no curl, no divergence, and no notion of MHD equilibrium, so the mission also produces a small reusable vector-calculus layer on $\mathbb R^3$.

Difficulty

Force balance is an identity between derivatives of expressions containing $\sqrt{1-(1-s)^2-4z^2}$ and division by $s$; differentiating it directly produces large expressions whose simplification needs the domain hypotheses ($s>0$ and positive radicand) at every step, so field_simp-style automation must be driven with those side conditions in hand. The statements about field-line coordinates require knowing that the position map is a diffeomorphism onto its image, which the paper establishes by a covering argument rather than by computation. The transform $\iota=2$ is the hardest milestone: it is a winding-number statement about the poloidal displacement of a field line relative to the magnetic axis, and the paper's proof is a continuity-in-$\epsilon$ argument, which in Lean needs an honest treatment of continuous angle lifts. The volume and average identities need the change of variables theorem with the constant Jacobian $-ab$ over a solid torus.

Formalization scope

Points of space are Fin 3 → ℝ; partial derivatives are fderiv applied to the standard basis vector, and gradient, divergence, curl, cross product, the directional derivative $B\cdot\nabla f$ and the tension $(B\cdot\nabla)B$ are defined from it in the first definition file. Squared length is $\sum_i u_i^2$, so the Pi-type norm is never used. All the paper's objects — $a$, $b$, $s$, $F$, $B$, $U_\epsilon$, $Q$, $H$, $\psi$, $p$, $\Omega_\delta$, $L$, $r(u,v,\zeta)$, $\gamma$, rotation about the $z$ axis, and the complex poloidal displacement used for the transform — are given in the second definition file, in the same notation as this description. Smoothness is ContDiffOn ℝ ⊤; volumes are the Lebesgue measure on Fin 3 → ℝ; integrals are Bochner integrals.

Everything is stated with the explicit field of Section 2 rather than an abstract existence claim, so no statement can be satisfied by a degenerate or symmetric configuration. The equilibrium conditions are asserted pointwise on $U_\epsilon$, which is open and non-empty for $0<\epsilon<1$, so no milestone is vacuous. Contributions of the auxiliary calculus lemmas (differentiability of $s$, $F$ and $B$ on $U_\epsilon$, and the product and quotient rules in this partialD formulation) are welcome and reusable by the companion family of Section 3, which is not part of this mission.

Selected references

• M. Landreman, Analytic toroidal 3D MHD equilibria and steady Euler flows with invariant surfaces, J. Plasma Phys. (submitted), arXiv:2609.26742 (2026). https://arxiv.org/abs/2609.26742
• H. Grad, Toroidal containment of a plasma, Phys. Fluids 10 (1967) 137–154. https://doi.org/10.1063/1.1761965
• R. Cardona, N. Duignan, D. Perrella, Asymmetry of MHD equilibria for generic adapted metrics, Arch. Ration. Mech. Anal. 249 (2025) 1. https://doi.org/10.1007/s00205-024-02072-x
• A. Enciso, A. Luque, D. Peralta-Salas, MHD equilibria with nonconstant pressure in nondegenerate toroidal domains, J. Eur. Math. Soc. 27 (2025) 2251–2291. https://doi.org/10.4171/JEMS/1328
• P. Constantin, T. D. Drivas, D. Ginsberg, Flexibility and rigidity in steady fluid motion, Comm. Math. Phys. 385 (2021) 521–563. https://doi.org/10.1007/s00220-021-04048-4
• O. P. Bruno, P. Laurence, Existence of three-dimensional toroidal MHD equilibria with nonconstant pressure, Comm. Pure Appl. Math. 49 (1996) 717–764. https://doi.org/10.1002/(SICI)1097-0312(199607)49:7<717::AID-CPA3>3.0.CO;2-C

Motivation

Chapter 3 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks how many random examples suffice to learn a concept from an infinite class. The cardinality bound of Occam's Razor is useless there, yet the rectangle game of Chapter 1 shows that some infinite classes are learnable from a finite sample. The answer is the Vapnik–Chervonenkis dimension: the size of the largest set on which the class realizes every labeling. Sauer's lemma says that a class of VC dimension $d$ realizes only $\Phi_d(m) = \sum_{i \le d}\binom{m}{i} \le (em/d)^d$ labelings on any $m$ points, polynomially many rather than $2^m$, and the ε-net theorem of Blumer, Ehrenfeucht, Haussler and Warmuth turns this into a sample bound: a consistent hypothesis from a class of VC dimension $d$ is probably approximately correct once $m$ is of order $(1/\epsilon)(\log(1/\delta) + d\log(1/\epsilon))$. A matching lower bound shows that $\Omega(d/\epsilon)$ examples are necessary. The chapter thus gives a single combinatorial parameter that characterizes, up to a logarithmic factor, the sample complexity of learning any class in the distribution-free model.

Setting

For a class $C$ of concepts $X \to \{0,1\}$ and a finite $S \subseteq X$, $\Pi_C(S)$ is the set of dichotomies of $S$ realized by $C$; $S$ is shattered if all $2^{|S|}$ are realized; $\mathrm{VCD}(C)$ is the supremum of the sizes of shattered sets, possibly $\infty$; $\Pi_C(m)$ is the largest $|\Pi_C(S)|$ over $|S| = m$; and $\Phi_d(m)$ is defined by $\Phi_d(m) = \Phi_d(m-1) + \Phi_{d-1}(m-1)$, $\Phi_d(0) = \Phi_0(m) = 1$. For a target $c$ the error regions are $c \,\Delta\, h$ for $h$ in the hypothesis class, and a set of points is an ε-net if it meets every error region of weight at least $\epsilon$ under the target distribution $D$. Samples, their product law, consistency and the error of a hypothesis are those of Mission I.

Formalization targets

Goal: Theorems 3.3 and 3.4

Let $H$ be a class of VC dimension at most $d$, well-behaved for the target $c$ (the double-sample event of the proof is null-measurable), and $m \ge 8/\epsilon$. The points of a random sample of $m$ examples of a target $c$ fail to be an ε-net for the error regions $\{c \,\Delta\, h : h \in H\}$ with probability at most

$$2\,\Phi_d(2m)\,2^{-\epsilon m/2},$$

so any algorithm that outputs a hypothesis in $H$ consistent with its sample has error greater than $\epsilon$ with at most that probability; with $m \ge (4/\epsilon)\log_2(2/\delta)$ and $m \ge (8d/\epsilon)\log_2(13/\epsilon)$ the probability is at most $\delta$; and, if $H$ is nonempty, every class contained in $H$ for whose targets $H$ is well-behaved is PAC learnable using $H$.

Milestones

Lemma 3.1 (Sauer's lemma, $\Pi_C(m) \le \Phi_d(m)$); Lemma 3.2 ($\Phi_d(m) = \sum_{i \le d}\binom{m}{i}$); the polynomial bound $\Phi_d(m) \le (em/d)^d$ of p. 57; Theorem 3.5 (the $\Omega(d/\epsilon)$ lower bound, in the two explicit forms of its proof).

Significance

Theorem 3.3 is the fundamental theorem of PAC learning: it replaces $\log|H|$ in Occam's Razor by the VC dimension and thereby covers rectangles, halfspaces, polygons, neural networks with a fixed architecture, and every class whose dichotomies grow polynomially. Its proof, the double sample and random partition argument, is the origin of symmetrization in empirical process theory. Sauer's lemma is a cornerstone of extremal combinatorics with independent proofs by Sauer, Shelah and Vapnik–Chervonenkis, and the lower bound of Theorem 3.5 shows that the upper bound is tight to within $\log(1/\epsilon)$, so the VC dimension genuinely characterizes sample complexity. None of these is machine-checked. Formalizing them puts on the platform the VC dimension, the growth function and the ε-net theorem with explicit constants, stated on the same sample law as the rest of this series, and the first information-theoretic lower bound for learning.

Difficulty

Sauer's lemma is a double induction on $d$ and $m$ through the auxiliary class $C'$ of dichotomies whose two extensions to a distinguished point are both realized, which needs care with the identification of dichotomies of $S$ and of $S \setminus \{x\}$. The ε-net theorem needs: the reduction $\Pr[A] \le 2\Pr[B]$ from a failed ε-net on the first half to a region hit at least $\epsilon m/2$ times by the second half, which is a Chebyshev bound on a binomial variable and is where $m \ge 8/\epsilon$ enters; the exchangeability of the $2m$ draws with a random partition into two halves; the counting bound $\binom{m}{\ell}/\binom{2m}{\ell} \le 2^{-\ell}$; and Sauer's lemma applied to the error regions, whose growth function equals that of $H$. The explicit constants require the numerical inequality $2(2em/d)^d 2^{-\epsilon m/2} \le \delta$ under the two stated conditions. The lower bound is a probabilistic argument with a random target: conditional on the sample, the labels of unseen points are fair coins, so the number of errors on them is binomial and exceeds half its range with probability at least $1/2$; the refined bound scales this construction to a region of weight $16\epsilon$ and uses Markov's inequality to bound the number of draws landing in it. Measurability of the failure sets is avoided by stating outer-measure bounds, except for the double-sample event, which the proof integrates: it is assumed null-measurable (the well-behavedness of Blumer et al., without which the theorem is false for a class of VC dimension $1$ on $\omega_1$). For the lower bound it is avoided by working over a finitely supported distribution on a space with measurable singletons.

Formalization scope

The VC dimension is a supremum in $\mathbb{N} \cup \{\infty\}$, the growth function a supremum in $\mathbb{N}$ (bounded by $2^m$), and $\Phi_d$ the book's recurrence, with its closed form and polynomial bound stated as separate theorems. The goal is stated for a hypothesis class $H$ (Theorem 3.4), Theorem 3.3 being the case $C = H$; it carries the exact bound of the proof, the explicit constants of Blumer et al. in place of the book's $c_0$, the requirement $m \ge 8/\epsilon$ of the proof's Chebyshev step, measurability of the hypotheses and the target, well-behavedness of $H$ for the target, and $0 < \epsilon, \delta < 1$. PAC learnability of the subclasses of $H$ needs $H$ nonempty, since no algorithm outputs hypotheses in the empty class. The lower bound is stated for every deterministic learning function, on an instance space with measurable singletons, for a class shattering some set of $d \ge 1$ points, with the explicit constants derived in the proof sketch ($m \le d/2$: error $\ge 1/8$ with probability $\ge 1/2$; $\epsilon \le 1/16$ and $m \le (d-1)/(64\epsilon)$: error $> \epsilon$ with probability $\ge 1/4$). Running time is not modelled. The composition bound for layered networks (Theorems 3.6 and 3.7) is not stated.

Trivializing readings are excluded: the ε-net event ranges over every hypothesis of $H$, the failure bounds are uniform over all consistent learners, and the lower bound holds for every learning function. Welcome contributions: Sauer's lemma, the closed form and the $(em/d)^d$ bound, the random-partition counting lemma, and the binomial median inequality used in the lower bound.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 3. doi:10.7551/mitpress/3897.001.0001
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4), 1989. doi:10.1145/76359.76371
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and its Applications 16(2), 1971. doi:10.1137/1116025
• N. Sauer, On the density of families of sets, Journal of Combinatorial Theory, Series A 13(1), 1972. doi:10.1016/0097-3165(72)90019-2
• A. Ehrenfeucht, D. Haussler, M. Kearns, L. Valiant, A general lower bound on the number of examples needed for learning, Information and Computation 82(3), 1989. doi:10.1016/0890-5401(89)90002-3

Motivation

A decision-maker has $n$ projects, each a Markov reward process, and at every decision time may advance exactly one of them; the others stay frozen. Which project to advance so as to maximize the expected total discounted reward? Posed as a dynamic program the problem has a state space that is the product of the $n$ state spaces, and the size of that product defeats every general method. The index theorem of Gittins and Jones (1974) says the dynamic program is solved exactly by an index policy: there is a real number $\nu(B, x)$, computable for each bandit process $B$ from its own data and its own current state $x$, such that always advancing a process of greatest index is optimal. Chapter 2 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), introduces the index, proves the theorem three times, and works out the properties of the index that the rest of the book, from jobs and superprocesses to restless bandits, is built on: which stopping time attains it, how it is computed, how it moves with the discount factor, and when it collapses to the myopic rule.

The index theorem itself is already on the platform, proved, as BanditAlgorithm.gittins_index_theorem in the Bandit Algorithms series (Lattimore and Szepesvári, Theorem 35.9). This mission cites it and formalizes what Chapter 2 establishes around it.

Setting

A bandit process $B$ (§2.3–2.4) is a Markov reward process on a countable state space $E$: transition probabilities $P(y \mid x)$, a bounded reward $r(x)$ received each time the continuation control is applied in state $x$, and a discount factor $a \in (0, 1)$; the freeze control leaves the state unchanged and yields nothing. The law of the process started at $x$ is $\mathbb{P}_x$ and $x(t)$ is its state at process time $t = 0, 1, 2, \dots$. A stopping time $\tau$ is a past-measurable rule for switching from continuation to freezing, taking values in $\{1, 2, \dots\} \cup \{\infty\}$. For such $\tau$, $R_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t r(x(t))]$ is the expected discounted reward and $W_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t]$ the expected discounted time; their ratio $\nu_\tau(B, x)$ (2.7) is the equivalent constant reward rate of that portion of $B$. The Gittins index is

$$\nu(B, x) = \sup_{\tau > 0} \frac{R_\tau(B, x)}{W_\tau(B, x)} \tag{2.6}$$

and, equivalently, the fair charge (2.5): the greatest rent $\lambda$ per period for which continuing $B$ for one or more periods, paying $\lambda$ each period, can be done without expected loss. A simple family of alternative bandit processes (SFABP) is $n$ such processes with a common discount factor, one of which is continued at each decision time; an index policy continues a process of greatest index. In the Lean development the single-arm model is the platform's (GittinsIndex): the chain law is built by the Ionescu–Tulcea construction, stopping times are adapted $\mathbb{N}\cup\{\infty\}$-valued maps on trajectories, and gittinsIndex P r a x is (2.6).

Formalization targets

Goal: Lemma 2.2, the optimal stopping set

The supremum in (2.6) is attained. For the initial state $\xi$, the attaining stopping rule may be taken to be "stop at the first time $t \ge 1$ at which the state lies in $\Sigma_0$" for any set $\Sigma_0$ with

$$\{x : \nu(B, x) < \nu(B, \xi)\} \subseteq \Sigma_0 \subseteq \{x : \nu(B, x) \le \nu(B, \xi)\},$$

and every such rule has $\nu_\tau(B, \xi) = \nu(B, \xi)$.

Milestones

Theorem 2.1 as a reference to the proved platform theorem; Eq. (2.5), the fair-charge characterization of the index; the restart-in-state formulation of §2.6.4 as the convergence of the Katehakis–Veinott value iteration; Theorem 2.3, monotonicity in the discount factor; Lemma 2.4, the interchange of two bandit portions; Propositions 2.5–2.8, the monotone-index cases in which the index is the immediate reward, or is attained only after the first step, or only at $\tau = \infty$.

Significance

Lemma 2.2 is the working form of the index: it turns the supremum over all stopping times into a specific rule, the first time the index falls below its starting value, and it is what the interchange proof of §2.7, the modified-forwards-induction policies of §2.6.6, the monotone-index propositions of §2.11 and the treatment of jobs in Chapter 3 all use. The fair-charge form (2.5) is the prevailing-charge proof of the theorem (Weber 1992) and the interpretation that carries over to superprocesses and restless bandits. The restart formulation is how indices are computed in practice (Katehakis and Veinott 1987), and Theorem 2.3 is the first of the comparative statics used throughout Chapters 7 and 8. Lemma 2.4 is the elementary inequality behind the original proof of Gittins and Jones.

Of these, only the index theorem has a machine-checked proof today. Formalizing the rest gives the platform the index as a usable object: a characterization of the optimal stopping rule, a convergent algorithm for it, and the monotonicity facts, all stated against the existing model so that every later mission of this series and every future use of the L&S model can build on them.

Difficulty

The obvious first move for Lemma 2.2, "take the stopping time that achieves the supremum", is what has to be proved: the supremum is over an uncountable family, and attainment comes from the optimal stopping problem with charge $\lambda = \nu(B, \xi)$, whose value function satisfies $\varphi(x) = \max\{0, r(x) - \lambda + a\mathbb{E}[\varphi(x(1)) \mid x(0) = x]\}$, together with the fact that its optimal stopping set is characterized by the strict and non-strict inequalities $\lambda > \nu(B, x)$ and $\lambda \ge \nu(B, x)$. That last step is the content: it identifies the local decision "stop or continue" with a comparison of indices, which is why any set between the two level sets works. On the platform's model this requires the dynamic-programming theory of discounted optimal stopping on a countable space (Theorem 2.10 of the book), the identification of fairChargeProfit with that value function, and the strong Markov property of markovChainMeasure at a trajectory stopping time. Theorem 2.3 needs randomized stopping times (a geometric kill) and the fact that they do not enlarge the supremum. The restart iteration is monotone and bounded but its operator is not a contraction in the restart value, so its limit has to be identified with the restart problem's value directly; that value is $\max(0, \nu/(1-a))$, not $\nu/(1-a)$, because restarting forever is free.

Formalization scope

The state space is a countable type with measurable singletons, so every subset is measurable; rewards are bounded; $a \in (0, 1)$. The chain law, stopping times, the discounted stopped sums and the index are the platform's, unchanged. Expectations are Bochner integrals; with bounded rewards they are finite and no total-function default value enters. IsPositiveStoppingTime fixes $\tau \ge 1$ everywhere, so $W_\tau \ge 1$ and the ratio (2.7) is a genuine quotient. The stopping rule of Lemma 2.2 is the hitting time from time $1$ of a set, with $\infty$ when the set is never hit. The fair-charge profit is a real supremum over the nonempty bounded family of positive stopping times, and (2.5) is stated with the outer supremum over $\{\lambda : \text{profit}(\lambda) \ge 0\}$, a nonempty set bounded above. The restart iteration is stated as a limit, with the value $\max(0, \nu(B, \xi)/(1-a))$: for a nonnegative index this is the book's $\nu/(1-a)$, and the maximum is forced by a one-state example with negative reward. The propositions' hypotheses are almost-sure events under $\mathbb{P}_x$, written as events of measure one.

Two trivializing readings are excluded: the index is never taken over all $\mathbb{N}\cup\{\infty\}$-valued maps but over adapted stopping times, and the stopping set of the goal is not restricted to the two extreme level sets. Contributions welcome: the optimal-stopping dynamic program on markovChainMeasure (value iteration, the strong Markov property at a stopping time), the equivalence of randomized and non-randomized stopping times for the supremum, and the monotone convergence of the restart iteration.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 2. doi:10.1002/9780470980033
• J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (Gani, ed.), North-Holland, 1974.
• R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4), 1992. doi:10.1214/aoap/1177005588
• M. N. Katehakis, A. F. Veinott, The multi-armed bandit problem: decomposition and computation, Mathematics of Operations Research 12(2), 1987. doi:10.1287/moor.12.2.262
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

Which fares to open, and when to close them

An airline sells one flight, a hotel one night, a car-rental firm one day of one car: a fixed capacity, perishable at a deadline, sold to customers who arrive over time and are willing to pay different amounts. Chapter 2 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) is the theory of that single resource. Its three models answer the same question with increasing generality: Littlewood's two-class rule, the $n$-class static model and its dynamic-arrival version give the seller a protection level per class, a booking limit or a bid price, all three equivalent; the discrete-choice model, in which customers buy down when a cheaper fare is open, replaces classes by offer sets and shows that only the efficient sets, ordered by their purchase probability, are ever offered, with a higher set the more capacity or the less time remains. This mission formalizes that last result, Theorem 2.3, together with the structural results of the two earlier models that it generalizes.

Setting

Static model. Classes $1, \dots, n$ with prices $p_1 \ge \dots \ge p_n \ge 0$ arrive in stages, lowest class first, with demands $D_j$ distributed on $\mathbb N$. With $x$ units left at stage $j$ the seller observes $D_j$ and accepts $u \le \min\{D_j, x\}$ units; the value function is the Bellman equation (2.3), $V_j(x) = \mathbb E[\max_u \{p_j u + V_{j-1}(x-u)\}]$, $V_0 = 0$ (staticValue), and $\Delta V_j(x) = V_j(x) - V_j(x-1)$ is the marginal value of capacity. The protection level $y_j^* = \max\{x : p_{j+1} < \Delta V_j(x)\}$ (protLevel), the booking limit $b_j^* = C - y_{j-1}^*$ (bookLimit) and the bid price $\pi_{j+1}(x) = \Delta V_j(x)$ (bidPrice) define the three controls of Theorem 2.1.

Dynamic model. Over $T$ periods at most one request arrives per period, of class $j$ with probability $\lambda_j(t)$; the value function (2.17) is $V_t(x) = V_{t+1}(x) + \mathbb E[\max_{u \in \{0,1\}} (R(t) - \Delta V_{t+1}(x))u]$ (dynValue), with time-dependent protection levels (2.19), booking limits (2.20) and bid prices (2.18).

Choice model. When the set $S$ of classes is open an arriving customer buys class $j \in S$ with probability $P_j(S)$; $Q(S) = \sum_{j \in S} P_j(S)$ is the purchase probability and $R(S) = \sum_{j \in S} P_j(S) p_j$ the expected revenue (purchaseProb, expRevenue). The value function (2.26) is $V_t(x) = \max_{S} \lambda_t (R(S) - Q(S)\Delta V_{t+1}(x)) + V_{t+1}(x)$ (choiceValue). A set $T$ is inefficient (Definition 2.1, IsInefficient) if a randomization $\alpha$ over the subsets has $\sum_S \alpha(S) Q(S) \le Q(T)$ and $\sum_S \alpha(S) R(S) > R(T)$, and efficient otherwise.

Formalization targets

Goal: Theorem 2.3

In every period with capacity left, some efficient set maximizes (2.26); and, the efficient sets being ordered by $Q$, the largest optimal set is nondecreasing in the remaining capacity $x$ and nondecreasing in the period $t$: choice_optimal_policy. Monotonicity is stated as "every efficient optimal set at $(t, x)$ is matched by one at $(t, x')$, $x' \ge x$, with at least as large a purchase probability", and likewise in $t$.

Supporting targets

Littlewood's rule (2.1), $\Delta V_1(x) = p_1 \mathbb P(D_1 \ge x)$ and the acceptance criterion; Proposition 2.1, the marginal values of the static model are decreasing in $x$ and increasing in the stages remaining; Theorem 2.1, nested protection levels, nested booking limits and bid-price tables each attain the Bellman maximum at every stage; Proposition 2.2 and Theorem 2.2, the same two results for the dynamic model, with marginal values now decreasing in time; Proposition 2-2.A.4 of the appendix, the marginal values of the choice model are decreasing in $x$ and in $t$; Proposition 2.3, an inefficient set is never optimal; and the ordering of efficient sets, $Q(S) \le Q(S')$ implies $R(S) \le R(S')$ when $S'$ is efficient.

The continuous-demand optimality conditions (2.9) of Sect. 2.2.2.3, stated without proof, the computational and heuristic methods of Sects. 2.2.3-2.2.4, the overbooking models of Sect. 2.7 and the nested-policy characterization of Sect. 2.6.2.5 are not targets.

Significance

Theorem 2.3 is the structural result behind choice-based revenue management: it reduces the $2^n$ offer sets to the efficient frontier of $(Q(S), R(S))$, orders that frontier, and shows the optimal policy walks up it as capacity grows or the deadline nears. It was the analytical core of Talluri and van Ryzin's (2004) choice-model paper and is the reason the efficient sets, not the fare classes, are the unit of control when customers substitute between fares. The static and dynamic results, from Littlewood (1972) and Brumelle and McGill (1993) to Lee and Hersh (1993), are the foundation of every airline seat inventory control system; the equivalence of protection levels, booking limits and bid prices is what lets the same optimal policy be implemented on any of the three kinds of reservation system. None of these results has a machine-checked proof.

Difficulty

The two marginal-value propositions are inductions in which the inductive step is the discrete concavity of a max-plus convolution, Lemma 2-2.A.1 of the appendix: $x \mapsto \max_{0 \le a \le m}\{ap + g(x-a)\}$ is concave when $g$ is, which in Lean requires reasoning about the argmax on $\mathbb N$ and the truncated subtraction. The static model's expectation is a tsum against a pmf, so every step also needs summability of a bounded family. The protection-level theorems then need the down-set structure of $\{x : p_{j+1} < \Delta V_j(x)\}$ under monotonicity of $\Delta V_j$, and the three controls have to be shown to coincide unit by unit. For the choice model, Proposition 2.3 is a one-line convexity argument once $\Delta V \ge 0$ is known, and the monotonicity in Theorem 2.3 is a monotone comparative-statics argument on the objective $R(S) - Q(S)\Delta$, which is easy in $\Delta$ but must be combined with Proposition 2-2.A.4 in both $x$ and $t$; the existence of an efficient maximizer uses Proposition 2.3 and the finiteness of the subsets.

Formalization scope

Capacities, stages and periods are natural numbers, the value functions recurse on the stage or on the number of periods to go, and the book's ranges ($x \le C$, $t \le T$, $j \le n$) are hypotheses of the theorems. Demand in the static model is a pmf on $\mathbb N$ rather than a random variable, so the expectation in (2.3) is a tsum; the dynamic model's expectation over $R(t)$ is written out, including the no-arrival term, which vanishes under nonnegative prices. The choice model is defined by its compact form (2.26), and the maximization includes the empty offer set. Optimality of a control means attaining the inner maximum of the Bellman equation at every state, which is what the book's proofs establish. The bid-price control is formalized with the bid price $\pi_{j+1}(x + 1 - z)$ of the $z$-th unit allocated; the book prints $x - z$, which is one unit off from (2.5). The appendix's Proposition 2-2.A.4 prints its time monotonicity in the reverse direction; the formal statement is the direction consistent with Proposition 2.2 and Theorem 2.3. The ordering of efficient sets is stated with non-strict inequalities, since Definition 2.1 admits ties in revenue.

Selected references

• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 2. https://doi.org/10.1007/b139000
• K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 2005. https://doi.org/10.1057/palgrave.rpm.5170134
• S. L. Brumelle and J. I. McGill, Airline seat allocation with multiple nested fare classes, Operations Research 41(1), 1993. https://doi.org/10.1287/opre.41.1.127
• T. C. Lee and M. Hersh, A model for dynamic airline seat inventory control with multiple seat bookings, Transportation Science 27(3), 1993. https://doi.org/10.1287/trsc.27.3.252
• K. T. Talluri and G. J. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• C. J. Lautenbacher and S. Stidham, The underlying Markov decision process in the single-leg airline yield-management problem, Transportation Science 33(2), 1999. https://doi.org/10.1287/trsc.33.2.136