Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Chapter 26 bounded the rate of uniform convergence by the Rademacher complexity; Chapter 27 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), introduces a second, metric measure of the size of a set of vectors, its covering numbers , the smallest number of Euclidean balls of radius needed to cover , and connects the two through Dudley's chaining. Covering numbers behave well under scaling and under coordinatewise Lipschitz maps (Lemmas 27.2–27.3), they are easily bounded for sets lying in a low-dimensional subspace (Example 27.1), and the chaining lemma turns a bound on at all scales into a bound on (Lemma 27.4), with the clean corollary when (Lemma 27.5). The chapter's example recovers for sets in a -dimensional subspace, the technique that the book says would sharpen the fundamental theorem's sample complexity from to .
For with the Euclidean metric, is an -cover of if every is within distance of some , and is the cardinality of the smallest -cover (Definition 27.1). The Rademacher complexity is Mission XX's. Chaining is run at the scales , , where is a radius of a ball containing , the book's being the smallest such radius.
For a nonempty , , contained in the ball of radius about some , and every integer ,
Example 27.1 (the grid -cover of a set of norm at most in a -dimensional subspace, of size ); Lemma 27.2 (scaling and translation); Lemma 27.3 (the contraction principle); Lemma 27.5 (the corollary of chaining). Further item: Example 27.2 ( for sets in a -dimensional subspace).
Chaining is the standard way to get sharp uniform convergence rates: a single-scale union bound (Massart's lemma at one resolution) loses a logarithmic factor, and summing Massart bounds over a geometric sequence of scales, applied to the increments between successive nearest cover points, recovers it. Lemma 27.4 is the discrete Dudley integral, and Lemma 27.5 is the form in which it is used: any polynomial-in- covering number gives -type bounds without the extra logarithm. On the platform these items complete the complexity toolbox begun in Mission XX and provide covering numbers as a reusable notion; the contraction and scaling lemmas mirror their Rademacher counterparts.
Lemmas 27.2 and 27.3 are immediate: the image of an -cover under the affine map is an -cover, and under a coordinatewise -Lipschitz map a -cover, since ; formally they are manipulations of the infimum in . Example 27.1 needs an orthonormal basis of the subspace (Gram–Schmidt, or Mathlib's orthonormal bases of finite-dimensional inner product subspaces of with the Euclidean structure) and the rounding of coordinates to a grid. Lemma 27.4 is the real work: after centering, take minimal -covers , the near-maximizer of (which depends on ), its nearest points , the telescoping , the bound , and Massart's lemma (Mission XX) on the sets of increments, of cardinality at most ; a formal proof must handle the supremum not being attained (approximate maximizers) and the dependence of all choices on inside the finite average. Lemma 27.5 lets using and . Example 27.2 combines Example 27.1 at the scales with Lemma 27.5, with the book's constant . The book's derivation uses the count without , so a proof needs the volumetric covering bound for and a direct count for .
Vectors are Fin m → ℝ with an explicit Euclidean norm, because Mathlib's norm on that type is the sup norm; covers are arbitrary finsets of and is an infimum in , so no junk value arises when no finite cover exists, and the chaining statements read through ENat.toNat for the bounded sets they concern, where it is finite. Subspaces are Mathlib Submodules with finrank = d. Two statements are given with the constants their proofs support, and the item texts say so. Example 27.1's grid has points per coordinate, so the cover has size , not , which is less than for and cannot bound a covering number of a nonempty set; Example 27.2 correspondingly has in place of . Lemma 27.4 is stated for any enclosing radius about any center, since the proof only uses that is a -cover of ; the book's minimal radius is the special case, and this is the form Example 27.2 needs (with and ). Lemma 27.5 keeps the book's .
Not stated: nothing else is in the chapter beyond the bibliographic remarks.
The book is discriminative almost throughout: it learns predictors, not distributions, following Vapnik's advice not to solve a more general problem as an intermediate step. Chapter 24 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), presents the generative alternative: assume a parametric form for the data distribution and estimate its parameters. The maximum likelihood principle is introduced on Bernoulli and Gaussian samples, shown to be empirical risk minimization for the log-loss, and analyzed through the decomposition of the true log-loss risk into a relative entropy plus an entropy (24.5), which explains both its consistency under a correct model and its overfitting on small samples. Naive Bayes and linear discriminant analysis show how generative assumptions reduce the number of parameters and make the Bayes classifier linear (24.8). The chapter's main theorem concerns the Expectation-Maximization algorithm of Dempster, Laird and Rubin for latent-variable models such as Gaussian mixtures: EM never decreases the log-likelihood (Theorem 24.3), because it is an alternate maximization of a lower bound that touches the likelihood at the posterior (Lemma 24.2). The chapter ends with Bayesian reasoning and the rule of succession.
A Bernoulli sample has log-likelihood and estimator (24.1); a Gaussian sample has . The log-loss is (24.4); on a finite domain, and . A latent-variable model is a parametric joint , , with ; , over the set of row-stochastic matrices, and EM alternates the E-step (24.10) with the M-step (24.11).
For a positive parametric joint , a sample , and any run of EM (each M-step returning some maximizer of ), the log-likelihood never decreases:
Equation (24.2) (Hoeffding for the Bernoulli estimator); the Gaussian maximum likelihood estimates of §24.1.1; Equation (24.5) (the risk decomposition ); Equation (24.8) (the LDA log-likelihood ratio is affine); Lemma 24.2 (EM as alternate maximization of , with and equality at the posterior). Further items: Gibbs' inequality, the Bernoulli maximum likelihood estimator (24.1)/(24.3), Exercise 1 (the biased variance estimate), Equation (24.6), the overfitting example of §24.1.3, Exercise 3 / (24.14), the weighted-centroid M-step (24.13), and the rule of succession of §24.5.
Theorem 24.3 is the guarantee that makes EM a sensible algorithm: it does not find the maximum likelihood estimate, but it climbs monotonically, and Lemma 24.2 identifies why, the E-step chooses the tightest lower bound at the current parameter and the M-step maximizes it. This variational view underlies a large part of modern latent-variable inference. Equation (24.5) is the information-theoretic content of maximum likelihood: the true risk is the entropy of the data plus the relative entropy to the model, so the best parameter is a projection of the data distribution onto the model class, and Gibbs' inequality is what makes that projection meaningful. The Bernoulli and Gaussian computations are the standard first examples, and Equation (24.8) is the reason linear classifiers appear in generative modeling. On the platform, the mission adds the relative entropy on finite domains, the EM objects, and Gaussian-integral identities that later probabilistic work can reuse.
The Bernoulli and Gaussian maximum likelihood facts are calculus, but as global maximization statements they need the concavity of and an explicit completion of squares rather than the book's stationary-point argument; the Gaussian case reduces to minimizing . Equation (24.5) is a finite-sum identity; Gibbs' inequality is Jensen for with the equality case, or the elementary . Lemma 24.2 is Jensen's inequality applied row by row to , with care at entries , where the convention is exactly Lean's junk value; Theorem 24.3 chains the lemma's three parts as the book does. The Gaussian expectation identities (Exercise 1 and (24.6)) require the moments of gaussianReal and Fubini over the product law. Hoeffding's inequality (24.2) is Mission II's Theorem for Bernoulli variables; the overfitting example is the inequality on . The rule of succession is a Beta-function identity provable by integration by parts.
Parametric families are functions from a parameter type to real-valued probabilities or densities, following the book's convention (p. 344) that denotes either; no measure-theoretic densities are needed except in the two Gaussian-integral items, which use gaussianReal and the i.i.d. law of Mission I, and in the two Bernoulli probability items, which use the Bernoulli law of Mission XIV. Lean's log 0 = 0 is handled explicitly: the EM items assume a positive joint, since with junk logarithms Theorem 24.3 is false (the M-step could pick a parameter with a zero component and inflated ), while the entropy terms use the convention that the book intends; the Bernoulli maximum likelihood statement ranges over ; the log-loss decomposition and Gibbs' inequality take the second distribution positive. The M-step is a predicate ("some maximizer"), so Assumption 24.1 is not modeled, and an EM run is any sequence of such steps. The Gaussian maximum likelihood statement requires a nonconstant sample, without which the likelihood is unbounded; the overfitting example is stated for , the range on which the book's inequality holds. Equation (24.8) is stated as a matrix identity for any symmetric in place of ; the soft k-means M-step is stated as the weighted-centroid minimization it amounts to.
Not stated: Naive Bayes (24.7), which is a rewriting of Bayes' rule; the mixture density itself and the E-step formula (24.12); the Bayesian derivations (24.16) and maximum a posteriori estimation; Exercise 2.
Dimensionality reduction maps data in to , , by a linear map , for computational reasons, for generalization (Chapter 19's curse of dimensionality) and for interpretability. Chapter 23 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), studies three ways to choose . Principal Component Analysis chooses the pair of compression and recovery matrices that minimizes the total squared reconstruction error, and the answer is the eigenvectors of for the largest eigenvalues (Theorem 23.2). Random projections choose with independent Gaussian entries, and the Johnson–Lindenstrauss lemma says that the norms of any finite set of vectors are then preserved up to with (Lemma 23.4). Compressed sensing exploits sparsity: a matrix with the restricted isometry property compresses every -sparse vector losslessly (Theorem 23.6), the reconstruction can be done by minimization, a linear program, with an error bound that degrades gracefully for approximately sparse inputs (Theorem 23.8, due to Candès), and Gaussian random matrices with rows are RIP with high probability (Theorem 23.9).
Vectors are functions with , and . The PCA problem (23.1) is , and . A random matrix has independent entries, in Lemma 23.3 and afterwards. is -RIP if for every with (Definition 23.5); is restricted to an index set .
Let , , and let be eigenvectors of for its largest eigenvalues, formalized as the first columns of a spectral decomposition with and nonincreasing. Then with minimizes (23.1): for every ,
Lemma 23.1 (the reduction of (23.1) to orthonormal and ); Lemma 23.4 (Johnson–Lindenstrauss); Theorem 23.6 (exact recovery under RIP); Theorem 23.8 (Candès' recovery bound); Theorem 23.9 (Gaussian matrices are RIP). Further items: Equation (23.3), Exercise 2, Remark 23.1 (the optimal value ), the eigenvector transfer of §23.1.1, Lemma 23.3, Theorem 23.7, Lemma 23.10, Lemma 23.11 and Lemma 23.12.
Theorem 23.2 is the Eckart–Young–Mirsky theorem in the form the book states it: PCA is the optimal linear compression-and-recovery scheme in the least-squares sense, and its solution is spectral. The Johnson–Lindenstrauss lemma is the basic tool of randomized dimensionality reduction, with a bound independent of , and the book's variant with explicit constants is what later chapters and the compressed-sensing proofs use. Theorems 23.6–23.9 together are the three "surprising results" of compressed sensing: information-theoretic recoverability from RIP, efficient recovery by convex relaxation, and the existence of RIP matrices by randomness; their proofs, Candès' cone argument and Baraniuk–Davenport–DeVore–Wakin's net-plus-union-bound, are among the cleanest in applied mathematics and are natural formalization targets. On the platform, the mission introduces Gaussian random matrices as product measures and the RIP predicate, usable by later work on sparse recovery.
Lemma 23.1 requires building an orthonormal basis of the range of , padded to vectors when the range has smaller dimension, and the identity ; Equation (23.3) is a trace computation. Theorem 23.2 combines (23.3), the change of basis with , the bound from extending to an orthogonal matrix, and Exercise 2, a rearrangement inequality; Remark 23.1 adds . Lemma 23.3 is the concentration of a variable (Lemma B.12), which must itself be established from the Gaussian moment generating function; the Johnson–Lindenstrauss lemma is then a union bound. Theorem 23.6 is a two-line contradiction with RIP applied to . Theorem 23.8 is the substantial one: the partition of into blocks of largest remaining entries, the bound , the -minimality inequality (23.8), Lemma 23.10, and the two claims combined through (23.5); a formal proof must handle the last, possibly shorter block, which the book's "assume is an integer" sidesteps. Lemma 23.11 is a volumetric net bound; Lemma 23.12 applies the Johnson–Lindenstrauss lemma to the image of an -net of the unit sphere of and closes the gap by the "smallest " argument, and Theorem 23.9 is a union bound over index sets.
Vectors are plain functions Fin d → ℝ with explicit norms, and matrices are Mathlib matrices, so the objectives are finite sums with no coercions between normed spaces. Random matrices are functions Fin n → Fin d → ℝ with the product of Gaussian laws gaussianReal 0 v, applied through Matrix.of; probability statements bound the outer measure of the failure event, and the failure events of Lemmas 23.4 and 23.12 are written with so that the book's strict conclusions follow. "Eigenvectors corresponding to the largest eigenvalues" is formalized as the first columns of a spectral decomposition with nonincreasing diagonal, which is exactly the set of such systems and avoids Mathlib's eigenvalue ordering conventions. Minimizers (, , ) are arbitrary elements of the argmin.
Five statements are given as their proofs support them, and the item texts say so. Lemma 23.3 and the Johnson–Lindenstrauss lemma are stated for : the printed range (and ) is false, since the upper tail decays like , slower than for (at it fails for ); the audit found this. Lemma 23.1 as printed, "every solution has orthonormal columns and ", is false, since has the same objective as ; the item states what the proof shows, that every is dominated by some with , which is all that (23.2) needs. Theorem 23.9 is stated with : Lemma 23.12 with (so that lies within ) and , followed by a union bound over the at most index sets, gives these constants, and the printed and are not reached by the argument. Theorem 23.8's proof assumes is an integer for simplicity; the statement is given without that assumption, since only the last block of the partition can be short and the block inequality still holds. Lemma 23.3 has , and the Johnson–Lindenstrauss lemma , since for its is and the conclusion fails.
Not stated: §23.1.2 (implementation), Remarks 23.2–23.3, §23.4 (the comparison of PCA and compressed sensing), Exercises 1 and 3–6.
Clustering is the most widely used tool of exploratory data analysis and, at the same time, the least well defined: similar points should share a cluster and dissimilar points should not, but similarity is not transitive while cluster membership is, and without labels there is no ground truth against which to evaluate a proposed grouping. Chapter 22 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), surveys the main paradigms, linkage-based algorithms, cost minimization with the k-means family, spectral relaxations of graph cuts, and the information bottleneck, and then returns to the question of what clustering is through Kleinberg's axioms. Its one theorem about that question is negative: no clustering function is simultaneously scale invariant, rich and consistent (Theorem 22.4). The mission formalizes this impossibility together with the chapter's positive facts: an iteration of the k-means algorithm never increases the k-means objective (Lemma 22.1), the RatioCut objective is the trace of a quadratic form of the graph Laplacian over cluster indicator vectors (Lemma 22.3), and the farthest-first traversal is a 2-approximation for the k-diam objective (Exercise 3).
A clustering of a finite set is a partition . For the k-means objective is with the centroid of , equivalently (22.1); the k-means algorithm alternately reassigns each point to a nearest centroid and recomputes the centroids. For a similarity matrix , the degree matrix is , the unnormalized graph Laplacian is (Definition 22.2), and . Kleinberg's setting is a clustering function that takes a dissimilarity over , symmetric, zero on the diagonal and positive off it, and returns a partition; the three axioms are Scale Invariance (), Richness (every partition is some ) and Consistency (shrinking within-cluster and expanding between-cluster dissimilarities leaves unchanged). The k-diam objective is , and the farthest-first traversal picks arbitrarily and maximizing , then clusters by nearest center.
For a finite domain with at least two points, there is no function from dissimilarities over to partitions of satisfying Scale Invariance, Richness and Consistency.
Lemma 22.1 (a k-means iteration does not increase ); the Laplacian identity from the proof of Lemma 22.3; Lemma 22.3 ( and for ); Exercise 3 (farthest-first traversal is a 2-approximation for k-diam). Further item: the centroid minimizes , the content of (22.1)–(22.3).
Kleinberg's theorem is the chapter's conceptual center: it says there is no ideal clustering function, only trade-offs, and the choice of a method must encode prior knowledge about the task, the unsupervised analogue of the No-Free-Lunch theorem. Its proof is short but delicate about what a dissimilarity is, and formalizing it fixes the exact hypotheses. Lemma 22.1 is the only guarantee the book offers for Lloyd's algorithm, and it is the reason the algorithm terminates on finite data. Lemma 22.3 is the bridge from a combinatorial cut objective to the spectrum of the Laplacian, the starting point of spectral clustering and of the PCA-type argument used in Chapter 23. The farthest-first result of Exercise 3 is Gonzalez's classical 2-approximation for k-center-type objectives, stated here for the diameter objective, and it is tight in the sense that no better constant is possible unless P = NP.
Theorem 22.4 follows the book: Richness gives with all-singleton output and with a different output; positivity lets one scale above pointwise, and Scale Invariance and Consistency then force two different values for . Formally the work is in building the scaled dissimilarity and in comparing Setoids. Lemma 22.1 is two inequalities: the nearest-centroid reassignment does not increase for the old centroids, because it minimizes it pointwise over assignments, and recomputing centroids does not increase it either, because the centroid minimizes the within-cluster sum of squares; the latter is the separate centroid item, a completing-the-square computation in an inner product space. The Laplacian identity is a finite double-sum manipulation that uses the symmetry of ; Lemma 22.3 applies it to the columns of and computes from the partition structure. Exercise 3 is the hint's argument: let be the distance from the next farthest-first point to the chosen centers; every point is within of its center, so every cluster of the algorithm has diameter at most , while the points are pairwise at distance at least , so two of them share a cluster of any -clustering, whose diameter is then at least . When the argument degenerates but the statement stays trivially true.
Partitions are -indexed families of finsets covering each point of the data exactly once, and nearest-center assignments and farthest-first centers are predicates rather than functions, so every tie-breaking rule is covered. The k-means items live in as EuclideanSpace; the centroid of an empty cluster is , which never enters any sum. The spectral items use Mathlib matrices over Fin m, Matrix.diagonal, Matrix.trace, the root-namespace dotProduct, and require symmetric, which the identity needs and which every similarity matrix satisfies; Lemma 22.3 requires nonempty clusters, without which has a zero column. Kleinberg's function is formalized on a fixed finite domain, as a map from Dissimilarity X to Setoid X, dissimilarities being positive on distinct points as in Kleinberg (2003): the book's model of p. 309 only asks for , but the scaling step of the proof of Theorem 22.4 requires positivity, and the theorem is stated for domains with at least two points, since the proof uses two partitions only. The k-diam theorem is stated without a maximum: every cluster of the algorithm has diameter at most twice the diameter of some cluster of the competitor, which is without conventions for empty index sets, and Metric.diam gives on sets of fewer than two points, the exercise's convention.
Not stated: the linkage-based algorithms and dendrograms of §22.1 (no theorem is stated about them), the k-medoids and k-median objectives, the spectral clustering algorithm itself, the information bottleneck of §22.4, Exercises 1, 2 and 4–6.
When a charged particle scatters, it can radiate photons of arbitrarily low energy. In perturbative quantum electrodynamics this shows up as infrared divergences: loop integrals over very soft virtual photons diverge logarithmically, and so do the rates for emitting soft real photons. The standard resolution, due to Bloch and Nordsieck and systematized by Yennie, Frautschi and Suura, is that the divergences cancel in any rate that sums over undetectable soft emissions below an energy resolution .
S. Weinberg's paper Infrared Photons and Gravitons (Phys. Rev. 140, B516 (1965)) shows that the same mechanism works for gravitons, derives explicit formulas for the exponents that control the soft factors, and proves that the extra "collinear" divergences produced by massless hard particles cancel for gravitons but not for photons. The soft-graviton factor (2.5)–(2.7) used there is the factor that appears in Weinberg's soft graviton theorem, and the spectrum formula is used in the paper to estimate the gravitational radiation from thermal collisions in the sun.
Timeline.
Work in units with the paper's metric: for four-vectors and , . A process has finitely many external lines ; line has mass , three-momentum , on-shell energy , charge , and sign (outgoing) or (incoming). The relative velocity of lines is
For a unit vector (the direction of a soft quantum) define the photon and graviton angular functions
and the infrared exponents and , integrals over the unit sphere against surface measure. With infrared cutoff and dividing point , virtual soft quanta multiply a rate by or , and summing over real soft emission of total energy at most gives the cutoff-free factors and of Eqs. (2.51)–(2.52).
For masses ,
with for the diagonal terms. This is the formula for graviton bremsstrahlung in an arbitrary collision.
The exponents and are the only process-dependent quantities in the soft factors: once they are known in closed form, the infrared behaviour of any rate, the shape or of the soft spectrum, and the soft power spectrum (2.53) follow. The Sec. III cancellation is the statement that gravitation, unlike massless electrodynamics or Yang–Mills theory, is free of unremovable collinear divergences at this level; the paper uses the contrast to argue that charged massless particles are problematic. The expansion (4.9) feeds the nonrelativistic quadrupole formula (4.13) behind the solar estimate.
The paper's arguments are informal physics derivations. This mission makes the mathematical content of those derivations precise and machine-checkable: the angular integrals, the sign statements, the limiting behaviour as a mass goes to zero, and the combinatorial factorization.
The closed forms need the solid-angle integral of a product of two denominators for two arbitrary, non-collinear momenta; the one-denominator case is a textbook integral in polar coordinates, but the two-denominator case does not reduce to it by an obvious choice of axis. The positivity statements are false without the conservation laws, so any proof must use them in an essential way. The massless-limit statements concern the interplay of a logarithmically divergent term with a coefficient that vanishes only at the limiting configuration, so a termwise limit fails.
Three-momenta live in EuclideanSpace ℝ (Fin 3); energies are the on-shell values and are not free variables. Solid-angle integrals are Bochner integrals on the unit sphere against Mathlib's volume.toSphere (total mass ). External lines are indexed by an arbitrary Fintype; the signs are real numbers constrained to by hypothesis. Sums over run over all ordered pairs, including , where ; the kernels and are extended by their limits and at , so the formulas are not trivialized by Lean's convention . The printed Eq. (4.6) has an exponent on the logarithm's argument that contradicts (2.26), (4.5) and (4.9); the definition of drops it. The prescriptions are suppressed. The integration in (2.13) is carried out, leaving an integral over the shell . Positivity is stated as , because in degenerate configurations. Sec. IV beyond (4.9) (the velocity expansion (4.8), the quadrupole formula (4.13), the solar estimate) and the Coulomb phases of Sec. V are out of scope for this mission.
A complete development needs solid-angle integration on (a spherical-coordinates change of variables for volume.toSphere), integration in polar coordinates on , and elementary inequalities for Minkowski products of timelike and null vectors. These are reusable beyond this mission, and contributions of them as separate lemmas are welcome.
Solitons (localized, finite-energy, non-dissipating solutions of classical field equations) are the simplest examples of the topological objects that dominate the non-perturbative physics of gauge theories: vortices, magnetic monopoles and instantons. G. 't Hooft's lecture notes Monopoles, Instantons and Confinement (arXiv:hep-th/0010225) open with the two textbook examples in one space and one time dimension, the φ⁴ kink and the sine-Gordon soliton, because every later construction in the notes (the Abrikosov–Nielsen–Olesen vortex, the 't Hooft–Polyakov monopole, the BPST instanton) repeats the same pattern: a degenerate vacuum, a static solution interpolating between two vacua, and an energy (or action) bounded below by a topological quantity — the Bogomol'nyi bound — which the soliton saturates.
This mission formalizes that pattern in its cleanest setting, Chapter 1 (Sections 1.1–1.2) together with Exercise (i) of the notes.
A static real scalar field is a function . Its energy (eq. (1.5)) for a potential is
Two potentials are considered, with parameters :
The static field equation is . The notes give the explicit solutions
which interpolate between and (case (a)) and between and (case (b)).
For every : in case (a) the kink has energy and no differentiable configuration with , has smaller energy; in case (b) the soliton has energy and no differentiable configuration with , has smaller energy:
The result identifies the soliton mass with a boundary term, with , so the mass depends only on the pair of vacua joined, and shows the kink is a global energy minimizer in its topological sector — the classical stability statement behind treating the kink as a particle of mass , heavy in the weak-coupling regime.
The physics is classical and fully known. What this mission adds is a machine-checked account: explicit verification of the closed-form solutions, exact evaluation of improper energy integrals, and a rigorous Bogomol'nyi argument for configurations that are merely differentiable, with limits at rather than compact support. No existing platform theorem matching these statements was found by a library search at drafting time.
The pointwise inequality is elementary; the difficulty lies in turning it into a statement about improper integrals over for arbitrary differentiable fields. One must handle configurations of infinite energy, pass from integrals over to using only the boundary limits, and deal with being non-smooth at the vacua of and at every vacuum of (a configuration may overshoot a vacuum). The explicit energy computations require exact evaluation of and type integrals as Lebesgue integrals.
deriv. Every competitor in the bounds is assumed differentiable everywhere, and boundary values are expressed as limits at and .MonopolesInstantonsConfinement, intended to be shared by later missions drawn from the same notes.Lecture 5 of the Les Houches lectures on deep learning at large and infinite width (arXiv:2309.01592, Section 5, lectures by B. Hanin) shows that a random ReLU network evaluated at a single input can be solved exactly. The statistics of the network depend on depth and width through the inverse temperature . The input–output Jacobian is the simplest quantity where this can be seen. Its second moment does not depend on depth or width. Its fourth moment grows like , which gives a quantitative sense in which the regime where both and are large is controlled by rather than by or alone. The lectures derive this through a combinatorial sum-over-paths formalism developed in Hanin's earlier papers (references [20–22] of the notes).
Fix a depth and widths . Let be a probability measure on that has a density with respect to Lebesgue measure, is symmetric (), and has variance . The weights are
all biases are , and the preactivations at an input are
The network output is . The input–output Jacobian has entries . A path is a tuple with , and is the set of paths with and . Along a path, and .
For every fixed input and all ,
Identity (124) says that, with the initialization and zero biases, the typical size of the input–output Jacobian does not depend on depth or width. This is the exact form of the "criticality" of ReLU at . The fourth-moment statement shows that the fluctuations are not controlled in this way: they grow exponentially in . Together with Proposition 5.2, these results turn questions about deep random ReLU networks at one input into questions about products of random matrices with dropout. As far as the drafter knows, these statements have not been machine-checked before. The mission asks for formal proofs of the lecture's exact identities.
The ReLU network is not a linear function of the weights. Its activation pattern depends on the weights of all earlier layers, so the path sum cannot be averaged term by term without first showing that the activation pattern is, in distribution, independent of the weights. That is the content of Proposition 5.2, which is argued only in sketch form in the notes. On top of that, the Jacobian must be identified with the path sum almost surely: at inputs where a preactivation vanishes the network is not differentiable. This requires the density assumption on and a separate treatment of layers in which every neuron is inactive.
n : ℕ → ℕ; only are used. The normalized weights are coordinates of the product measure on a finite index set (weightLaw). The Bernoulli masks are coordinates of the uniform product measure on Bool (maskLaw).fderiv) of at applied to the -th basis vector. Mathlib returns at points of non-differentiability, which form a null event for .At infinite width a randomly initialized network is a Gaussian process (Mission I of this series). Real networks have finite width , and the leading departure from Gaussianity is measured by the connected four-point function . It captures both correlations between neurons and non-Gaussian fluctuations. Lecture 4 of the Les Houches lectures (arXiv:2309.01592, lectures by B. Hanin) states the central finite-width result, Theorem 4.2: is of order and obeys an explicit layer-to-layer recursion up to . At criticality this gives the effective depth as the parameter controlling finite-width effects. The result was first derived at a physics level of rigor by Yaida (2020) and in Roberts–Yaida–Hanin (2022), and later derived more mathematically by Hanin (reference [19] of the notes).
A network of depth with widths and nonlinearity has preactivations and . The parameters are independent, with and , where and (eqs. (118)–(119)). At a single input , write for the average of against . The infinite-width kernel is and (eq. (120)). The parallel susceptibility is . The normalized connected four-point function is
If the hidden widths satisfy , then and
with constants independent of the widths.
Theorem 4.2 is the first quantitative statement that finite-width networks at initialization are not Gaussian processes. The size of the deviation is per layer, and it accumulates linearly in depth at criticality. This is the basis for the claim of Lecture 4 that controls correlations between neurons, fluctuations and, in later lectures, feature learning. As far as the drafter knows these statements have not been machine-checked. Lemma 4.4 and the covariance exercise are exact finite-width identities and are natural first targets.
The next layer is Gaussian only conditionally, with a random variance that is an average over dependent neurons. Establishing the recursion to order requires expanding Gaussian averages around the mean of and controlling all higher cumulants of this collective observable uniformly in the widths. The nonlinearity is only assumed polynomially bounded, so smoothness must come from Gaussian averaging, not from .
LesHouchesWidth_GaussianMLP: the network mlpZ, stdGaussianParams, nngpKernel, uniformWidths) are reused. Mission I must be launched first, and its definition then added to this proposal as a reference item.LesHouchesWidth_FiniteWidth): gaussAvg, gaussAvgVec, gaussVarSq, chiParallel, PolyBounded, kappa4, dressedTwoPoint, collectiveSigma.A fully connected neural network with random Gaussian weights defines a random function of its input. Lecture 1 of the Les Houches lectures on deep learning at large and infinite width (arXiv:2309.01592, lectures by Y. Bahri) explains that, when the hidden layers become infinitely wide, this random function becomes a Gaussian process (the "neural network Gaussian process", NNGP). Its covariance kernel is computed by an explicit layer-to-layer recursion. The observation goes back to Neal (1996) for one hidden layer. It was extended to deep networks by Matthews et al. and Lee et al. (2018). It underlies Bayesian inference with infinitely wide networks (Section 1.6) and the analysis of signal propagation at large depth (Section 1.7). Lecture 2 introduces Wick's theorem, the tool for computing moments of Gaussian vectors that the lectures then use for finite-width corrections.
A network of depth with widths and nonlinearity maps an input to preactivations
with independent and (eqs. (1)–(3) and (5); layers are indexed as in Lectures 4–5, so of Lecture 1 is here). For a covariance write (eq. (15)). The NNGP kernel is
A pairing of is a partition into two-element blocks.
For a network with one hidden layer of width , fixed inputs and output width , as the vector converges in distribution to a centered Gaussian with covariance
A further item states the deep version of the limit, eqs. (13)–(14), in the simultaneous-width limit. It is included as a supporting theorem rather than a milestone.
Result 1 and its deep extension identify the prior over functions induced by random initialization. They also make the NNGP kernel the central computational object of the infinite-width theory. The finite-width covariance identities (9)–(11) are exact and explain where the recursion comes from. Formula (16) makes the recursion explicit for ReLU. Wick's theorem is the basic tool of the finite-width perturbation theory of later lectures. These are classical results. The mission asks for their formal proofs against a single shared model of random networks that the later missions of this series reuse.
Result 1 is a multivariate central limit theorem for sums of i.i.d. vectors whose entries are products of a Gaussian weight and a nonlinear function of Gaussian first-layer preactivations. No assumption beyond square-integrability of against the relevant Gaussians is imposed, so the CLT must be applied in its form. The deep limit is harder: for the hidden preactivations are not Gaussian at finite width, and one must control a triangular array in which the widths of all layers grow together. The ReLU formula (16) is an explicit but delicate Gaussian integral over a cone.
stdGaussianParams), scaled by and (mlpBias, mlpWeight). This is equality in law with the prior (5).multivariateGaussian. Convergence in distribution is stated with bounded continuous test functions: for every bounded continuous .Big-bang nucleosynthesis and the acoustic peaks of the cosmic microwave background fix the baryon density of the universe to about 5% of its total energy density, but in the low-redshift universe only some 10% of those baryons are seen in galaxies, with another 10% in the circumgalactic and intracluster medium. Simulations place the remainder — the missing baryons — in a diffuse warm-hot intergalactic medium (WHIM) at – K, spread along the filaments of the cosmic web. Absorption-line studies and X-ray emission from individual filaments probe the cool and the hot ends of that range respectively, leaving the bulk poorly constrained.
de Graaff, Cai, Heymans & Peacock (2019) attack the problem statistically, by stacking the Planck Compton- map over pairs of CMASS galaxies and measuring the residual signal in the bridge between each pair. Interpreting that residual requires an analytic model of a filament, and that model — a cylinder with a Gaussian cross-section, convolved with the instrument beam — is what this mission formalizes. The same model, applied to the CMB lensing convergence map, converts the measured signals into a gas density and temperature, and hence into a baryon fraction.
A filament is modelled as an infinite cylinder seen side-on. In the plane perpendicular to the filament axis, write for the line-of-sight coordinate and for the transverse coordinate on the sky. The electron density is taken to be a two-dimensional Gaussian
with central density , intrinsic width and beam width ; the transverse direction, unlike the line of sight, is smoothed by the instrument beam, which is why appears only there.
The Compton parameter of a line of sight is the optical-depth-weighted temperature of the scattering electrons,
with the Boltzmann constant, the Thomson cross-section, the electron rest energy and the electron temperature, assumed constant across the filament. The convergence of CMB lensing is the analogous projection of the total matter density contrast ,
with the Hubble constant, the matter density parameter, the scale factor and the comoving distances of lens and source. For a structure thin compared with the lensing kernel, the geometric factor is constant across it and reduces to a line-of-sight integral of against a fixed prefactor.
The significance of the measurement is assessed with a second, statistical layer. A stack of binned profiles ( the map index, the bin index) has mean profile and covariance estimator ; the deviation of the mean profile from zero is measured by . Because the stacked maps overlap on the sky, the paper replaces by a jackknife covariance built from sky sub-samples, , and multiplies the inverse by the Hartlap factor , with the number of bins.
Measurements enter through two numbers: the mean Compton parameter and the mean convergence over the boxed filament region, together with the empirical observation that the peak of each profile is close to times its mean. Every statement in this mission imposes that calibration as a hypothesis on the model.
This is the quantity the paper's baryon budget is computed from: given the measured , an assumed temperature and the beam width, it fixes the number of electrons in a filament of length .
Both and are symmetric and positive semidefinite, for every data set and every sample size.
The four displayed identities are the entire inferential chain from two stacked maps to a baryon fraction. Eq. (A.2) says what the model predicts for the observable; Eq. (A.3) inverts it at the filament axis; Eq. (A.4) turns the inversion into a total electron count, from which the paper obtains gas at and K, accounting for of the cosmic baryon budget; Eq. (A.5) supplies the independent lensing constraint that breaks the density–temperature degeneracy of the SZ measurement alone. The statistical milestones cover the other half of the analysis: the covariance estimators of Eqs. (3) and (5)-(6) that turn a stack into an error bar, the nonnegativity of the of Eq. (4) that is converted into the quoted , and the Hartlap rescaling of Eq. (7). The beam-dominance milestone quantifies the paper's claim that the result barely depends on the one free shape parameter, the intrinsic width , which is taken from simulations rather than measured.
Formalizing them contributes a machine-checked derivation layer for a widely used observational technique: the projection of a Gaussian cylinder onto a Compton- or convergence map, and the inversion of that projection, recur throughout stacked-SZ and stacked-lensing analyses. What this mission adds over the paper is a statement of each identity with all its hypotheses exposed — which positivity conditions are needed, which parameters genuinely drop out — rather than a new physical result. The physics is not re-derived and the measurement is not re-analysed; the empirical inputs , and the peak-to-mean ratio enter as hypotheses, not as claims.
The identities are Gaussian integrals, so the mathematical depth is modest; the difficulty is bookkeeping and faithfulness. Three specific traps. First, the line-of-sight and transverse directions have different widths — against — and the asymmetry is what makes the final answer depend on the beam; a formalization that symmetrizes them is a different theorem. Second, the paper's is not free: it is pinned by the calibration , so the goal must carry that equation as a hypothesis rather than substituting a closed form for silently. Third, the total electron count is an iterated integral over the plane, and the inner and outer variables must be kept in the paper's order.
Everything is stated over with no units, so every physical constant is an explicit real variable; integrals are Bochner integrals over the whole real line with Lebesgue measure, which return on a non-integrable integrand. The definition bundle fixes the model once — the SZ prefactor, the Gaussian cylinder profile, the Compton parameter, the thin-lens convergence prefactor, the convergence and the total electron content — and every statement is phrased against it. The convergence definition is the thin-lens specialization of Eq. (2): the geometric kernel is a constant prefactor, not an integral over lens distance, and the mission does not claim the reduction from the full Eq. (2) to that form.
Degenerate readings are ruled out as follows. The calibration hypotheses are satisfiable for every admissible choice of constants, so no statement is vacuous; conversely they genuinely constrain the central amplitude, so no statement holds for a trivial reason. The positivity hypotheses are the minimal ones that make the denominators nonzero, and the widths enter as with unrestricted, so the beam-free case is included rather than excluded. The statistical layer is finite-dimensional: profiles are real arrays indexed by a finite bin type, covariances are real matrices, and matrix inversion is the nonsingular inverse, which returns the zero matrix on a singular argument — hence the positive-definiteness hypothesis in the milestone. Counts are natural numbers but all arithmetic in the prefactors is performed after casting to the reals, so is a genuine real subtraction and may be negative. The statistical statements assert the structural properties of the estimators as written; they do not assert unbiasedness, nor the reduction for the covariance of a mean, nor any property of the resampling scheme. Only Mathlib's Gaussian-integral, measure-theory and positive-semidefinite-matrix API is needed; no new infrastructure is required, and the resulting projection lemmas are reusable for any other stacked-profile analysis.
The Rydberg constant is the constant of spectroscopy that sets the scale of the hydrogen spectrum. It first appeared as an empirical fitting parameter in J. Rydberg's formula for the hydrogen spectral series; N. Bohr later showed that its value can be computed from more fundamental constants within his model of the atom. Before the 2019 revision of the SI it was, together with the electron spin -factor, among the most accurately measured physical constants (relative standard uncertainty about , CODATA 2022). This mission formalizes the algebraic content of the standard account of as presented in the Wikipedia article Rydberg constant: its closed form, its reduced-mass correction, its alternative expressions through the fine-structure constant, and the Bohr-model derivation of the Rydberg formula.
Fix five strictly positive real numbers: the electron rest mass , the elementary charge , the vacuum permittivity , the Planck constant and the speed of light . From them define
the Compton wavelength , Compton frequency , Compton angular frequency , Bohr radius , classical electron radius , and the Rydberg unit of energy .
For a nucleus of mass the reduced mass is and the corrected Rydberg constant is ; for hydrogen and .
A Bohr orbit with principal quantum number of a particle of mass and charge about a fixed charge is a circular orbit of radius and speed such that the Coulomb force supplies the centripetal force and the angular momentum is quantized:
Its energy is . The infinite-nuclear-mass model uses ; the reduced-mass model uses .
For distinct positive integers and Bohr orbits of mass with quantum numbers , the wavenumber of the photon emitted in the transition satisfies
These identities are the standard bridge between the empirical Rydberg formula and the constants : they explain why a single constant governs all hydrogen series, why isotopes such as deuterium show shifted lines (the shift led to the discovery of deuterium), and how relates to , and the Compton scales. The results are classical and not open; the mission's contribution is a machine-checked, reusable layer of definitions (Bohr orbits, reduced mass, the named atomic length and energy scales) on which later atomic-physics formalizations can build.
The content is elementary algebra with positivity side conditions. The main point to handle carefully is that the Bohr-orbit conditions determine and only implicitly; the energy must be computed from the two defining equations rather than from explicit formulas, and every division must be justified by positivity of the constants.
All constants are real numbers bundled in a structure with strict positivity fields; no SI numerical values (CODATA figures, , etc.) are formalized, and the precision-measurement and QED discussion of the source is out of scope. The Bohr model is formalized for a single particle of mass orbiting a fixed charge (hydrogen-like, ); the reduced-mass correction is modelled, as in the source, by substituting for . The photon wavenumber is taken to be the orbital energy difference divided by . The Bohr-orbit hypotheses are satisfiable for every and every , so the Bohr-model statements are not vacuous. Contributions of alternative proofs and of generalizations (nuclear charge , explicit orbit radii and speeds) are welcome.
Since the 2019 revision of the International System of Units (SI), the elementary charge is no longer a measured quantity: it is one of the seven defining constants of the SI and is fixed by definition at
Before that revision, had to be extracted from experiment, and the metrology literature accumulated several independent routes to it: Faraday's laws of electrolysis combined with the Avogadro constant, Millikan and Fletcher's oil-drop experiment (1909), shot-noise analysis, and — since the 1980s — the combination of the Josephson effect and the quantum Hall effect. Each route is a short algebraic recipe that turns other measured constants into . The 2019 redefinition did not delete those recipes; it inverted their role. With , the Planck constant , the Avogadro constant and the speed of light all fixed exactly, the recipes become exact arithmetic identities between defining constants, and the residual measurement uncertainty migrates to the constants that are no longer fixed (the vacuum magnetic permeability , equivalently the fine-structure constant ).
This mission formalizes exactly those identities, as they are stated in the source article, together with the two quantization statements the same article records: Dirac's 1931 argument that a magnetic monopole forces charge quantization, and the closure property behind the observation that although quarks carry charges in multiples of , isolatable particles carry integer multiples of .
All quantities are real numbers carrying SI units implicitly; the Lean development works in ℝ and fixes the numerical values as exact rationals, never as floating-point approximations.
The defining constants used here are (coulomb), (per mole), (joule second) and (metre per second).
From these the article builds four derived constants, each of which is a definition in this mission rather than an axiom:
A fifth definition captures the natural unit of charge of those natural unit systems in which , with the electric constant and the reduced Planck constant.
The goal theorem asserts that the three determination routes recorded in the source return one and the same number, the fixed SI value of , and that the electrolysis route's intermediate constant has its exact SI value:
The milestones are the individual identities, each stated for arbitrary positive values of the constants rather than only at the SI values, plus the two quantization statements:
The result itself. The content is the coherence of the SI's electrical sector: the same comes out of an electrochemical measurement chain, a quantum-electrical one and the CODATA relation, and the arithmetic that links them is exact. Milestones 6 and 7 record the two quantization statements in the source: the Dirac argument is a genuine implication (a monopole forces the charge spectrum into a discrete subgroup), while milestone 7 isolates the algebraic half of "stable groupings of quarks carry integer charge" — closure of a quantized spectrum under composition.
Formalizing it. What this mission produces is a small, faithful, reusable encoding of the 2019 SI defining constants and of the standard derived constants, with the exact rational values rather than floating-point ones, and with the degenerate cases made explicit. Nothing here is an open problem, and the mission should not be read as one: the value is a checked reference layer for physics-flavoured formalization, not a research advance.
Low, and stated as such deliberately. Milestones 1–3 are field arithmetic; 4 and 5 are field arithmetic plus Real.sqrt of a square, which needs the positivity hypotheses that are carried explicitly; 6 and 7 are elementary manipulations of ℤ-multiples and of AddSubgroup.closure. The only places a solver can go wrong are the degenerate ones: division by a constant that has not been assumed nonzero, and Real.sqrt of a quantity not known to be nonnegative — which is why every statement carries positivity or nonvanishing hypotheses rather than leaving Lean's junk values to decide the outcome.
Conventions this mission commits to:
eSI = 1602176634 / 10 ^ 28), so the numeric milestone is an exact identity, provable by norm_num, not a floating-point comparison.Real.sqrt a nonnegativity or positivity hypothesis, so no statement is discharged by a Lean junk value.ℝ, using only Mathlib.Contributions welcome beyond the current list: the shot-noise and oil-drop routes, which the source describes qualitatively rather than by a formula, would need a probabilistic or mechanical model before they can be stated, and that model would be a worthwhile addition.
The Boltzmann constant is the proportionality factor relating the average thermal energy of the particles of a system to its thermodynamic temperature. It appears wherever a microscopic energy has to be compared with a macroscopic temperature: in the ideal gas law written per molecule, in the equipartition theorem, in the Boltzmann factor that governs equilibrium occupation probabilities, in Boltzmann's entropy formula , in the thermal voltage of a – junction, and in the Johnson noise of a resistor.
The constant also has an unusual documentary history. Boltzmann linked entropy and probability in 1877 but never introduced a constant; Max Planck first wrote , and gave the first numerical value ( J/K, about 2.5% below the modern figure), in his 1900–1901 derivation of the black-body law — the terse on Boltzmann's tombstone is Planck's formulation. For most of the twentieth century was a measured quantity; the 2017 acoustic gas thermometry campaign reached a relative uncertainty of 0.2 ppm, and as part of the 2019 revision of the SI the constant was defined to the exact value J·K⁻¹, which is now what fixes the kelvin.
This mission formalizes the elementary quantitative content of that picture: the identities that make a conversion factor, and the exact arithmetic that the 2019 SI definitions make possible.
Work throughout with real numbers; units are carried in the prose, not in the types. Fix the exact post-2019 SI values
and define the molar gas constant as the product .
A gas sample is described by its pressure , volume , absolute temperature , amount of substance , molecule count , particle mass , and mean square particle speed . A system with a finite set of microstates is described by an energy function ; its partition function is and its Boltzmann probabilities are . For a distribution on , the Gibbs entropy is , the Shannon entropy (in nats) is , and for equiprobable microstates Boltzmann's entropy is . The thermal voltage is . All logarithms are natural.
The goal theorem is the statement that fixes the physical meaning of : kinetic theory plus the per-molecule gas law determine the mean translational kinetic energy. From
conclude
The milestones are the surrounding identities, in the order of the source: the equivalence ; equipartition, per degree of freedom; the ratio law ; normalisation of the Boltzmann factors, ; the reduction of the Gibbs entropy on the uniform distribution to ; the identification Shannon entropy; the energy of one nat of rescaled entropy; and three numerical facts — mV, eV/K, and the exact value J·K⁻¹·mol⁻¹.
The results. Individually these are the standard first facts of kinetic theory and statistical mechanics; together they pin down what the constant does. The equipartition chain converts a temperature into a velocity distribution scale and explains the measured room-temperature rms speeds from helium (about 1370 m/s) to xenon (about 240 m/s). The entropy statements make precise the claim that thermodynamic entropy is Shannon entropy in energy units, with as the exchange rate — the statement behind the natural-unit convention . The numerical milestones exercise the consequence of the 2019 SI revision that unit conversions involving are now exact rational arithmetic rather than propagated measurement uncertainty.
Formalizing them. All of these are settled physics; nothing here is open. What the mission produces is a small, reusable Lean development of the SI defining constants and of the elementary statistical-mechanical vocabulary (Boltzmann weights, partition function, Gibbs/Shannon/Boltzmann entropies), with each textbook identity stated against that shared model rather than re-derived ad hoc. It is a suitable entry-level mission and a foundation other physics missions can import.
The mathematics is elementary; the difficulty is entirely one of faithful modelling, and solvers should expect the friction to be there rather than in the proofs. Three specific points. First, Lean's division and logarithm are total: is defined at and evaluates to , and for , so statements must carry the positivity hypotheses that keep them physically meaningful rather than relying on the definitions to exclude bad inputs. Second, the entropy definitions are stated for an arbitrary real-valued weight function, not for a distribution; normalisation is a hypothesis where it is needed, never an assumption baked into the type. Third, the numerical milestones are claims about specific decimal numerals, and the tolerance in each is part of the statement: two of them are genuine approximations and one, the value of , is an exact identity, which is only true because both factors are exact SI numerals.
Quantities are real numbers (ℝ); no dimensional-analysis layer is used, and unit
correctness is a convention of the prose. Finite state spaces are Finsets over an
arbitrary index type, with nonemptiness stated as a hypothesis where the partition
function must be nonzero. Entropies use the natural logarithm, so they are measured in
nats, and the Shannon entropy is the Gibbs entropy divided by by construction.
Temperatures, masses, volumes and particle counts are positive reals where the physics
requires it. The mean square speed is a free real variable constrained only by the
stated equations; it is not built from a velocity distribution, and extending the
development to an actual Maxwell–Boltzmann distribution is out of scope here and a
natural follow-up mission.
The statements are deliberately non-vacuous: every hypothesis set in the mission is
satisfiable (positive temperature, positive mass, nonempty state space), and the
numerical items admit no trivializing reading since they are closed claims about fixed
numerals. Only Mathlib is required — Real.exp, Real.log, Real.sqrt, and
Finset.sum. The definition file is intended to be reusable: any later mission about
thermodynamics, black-body radiation, or the Shockley diode equation can import the SI
constants and entropy vocabulary unchanged.
How large can the power set of an infinite set be? For a regular cardinal (one that is not the supremum of fewer than smaller ordinals) the answer is: almost anything. Easton's theorem (1970) shows that the function on regular cardinals can be prescribed arbitrarily in any model of ZFC, subject only to monotonicity and König's inequality . For a long time it was expected that singular cardinals — those that are such a supremum, like — would behave the same way.
They do not. In 1974 Jack Silver proved that the Generalized Continuum Hypothesis cannot fail for the first time at a singular cardinal of uncountable cofinality: if for every infinite and , then . This was the first ZFC theorem constraining the continuum function at singular cardinals, and it opened the area now called the singular cardinal problem.
A short timeline:
This mission is the first in a series formalizing Thomas Jech, Set Theory (Third Millennium Edition, Springer 2003). It covers Chapter 8, "Stationary Sets" (pp. 91–98).
Fix a regular uncountable cardinal and regard it as the well-ordered set of ordinals below it. A set is closed unbounded, or a club, if it is unbounded in and contains all of its limit points below (an ordinal is a limit point of when ). A set is stationary if for every club . Clubs are closed under intersections of fewer than of them, so they generate a -complete filter, the club filter; its dual is the nonstationary ideal.
The club filter has a second closure property with no analogue for ordinary filters. The diagonal intersection of a -indexed family is
and a filter closed under diagonal intersections is called normal. A function defined on is regressive if for all nonzero .
For cardinal arithmetic, denotes the cofinality of (the least length of an unbounded sequence in ), the cardinal successor, and is singular when . The Singular Cardinal Hypothesis (SCH) is the assertion that for every singular with . A sequence of cardinals is normal if it is strictly increasing and continuous at limits.
This is the weakest statement of the chapter that still needs the full machinery: it fixes no particular and no particular cofinality, and it stays correct no matter how the singular cardinal problem develops above it.
Silver's theorem is the boundary between the two halves of cardinal arithmetic. Above it sit the ZFC theorems of pcf theory; below it sit the consistency results (Magidor, Prikry, Radin forcing) that show how much freedom is left, and they are confined to cofinality precisely because Theorems 8.12 and 8.13 close off everything else. Its proof also packages tools used throughout set theory: the normality of the club filter, Fodor's pressing-down lemma, and the technique of bounding almost disjoint families of functions by a stationary-set argument.
Formalization status: Mathlib already has clubs and stationary sets in an arbitrary well-ordered type (IsClub, IsStationary), with the finite and -indexed intersection lemmas — Jech's Lemma 8.2 and Theorem 8.3. It does not have diagonal intersections, Fodor's theorem, Solovay's splitting theorem, or any singular cardinal arithmetic beyond the definitions of regular and singular cardinals. Each milestone below is therefore a genuine addition, and the first three are reusable well outside this mission.
The naive route to the goal — induct on and pass to the limit — fails immediately: for singular is not determined by the values for in any elementary way; that is exactly the content of the independence results. What the proof must do instead is bound the number of functions on , and it gets that bound from a stationary set rather than from a club: uncountable cofinality is what makes the set of relevant stages stationary, and stationarity is what survives the diagonal argument. Cofinality breaks this at the first step, since every subset of that is unbounded is already a club and Fodor's theorem is empty.
The two hard pieces are Lemma 8.14 and, inside it, Lemma 8.16: given an almost disjoint family of functions with and on a stationary set of , one must show by assigning to each a pair (stationary set, bounded restriction) and checking the assignment is injective. That argument uses Fodor's theorem on a set of functions, and the bookkeeping does not simplify.
The ambient order is Mathlib's type of ordinals below a cardinal, k.ord.ToType (written Below k in the mission's definition bundle); clubs and stationary sets are Mathlib's IsClub and IsStationary on that type, so a set is closed in the sense of being closed under suprema of directed subsets — equivalent, for a well-order with the order topology, to Jech's "contains its limit points". Families indexed by "" are functions out of that same type, which is what makes the diagonal intersection typecheck without a side condition. Cardinal exponentiation, cofinality (Ordinal.cof of k.ord) and the successor cardinal (Order.succ) are Mathlib's.
One trivializing formalization is ruled out explicitly: the GCH hypothesis of the goal is stated for infinite cardinals only. Quantified over all cardinals it would be unsatisfiable — — and Silver's theorem would become vacuous.
A complete development needs: diagonal intersections and the normality of the club filter; Fodor's theorem; the sets and their stationarity; Solovay's splitting theorem via Lemmas 8.8 and 8.9; almost disjoint families of ordinal functions and the counting Lemmas 8.15 and 8.16; and Theorem 5.22(ii) on cardinal powers, which Jech's proof of Theorem 8.13 cites. Contributions of any of these as separate reductions are welcome, as are alternative proofs of the goal (for instance via a generic elementary embedding) that bypass some of the chain.
Chapter 5 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks what happens to PAC learning when the labels are unreliable. In the classification noise model of Angluin and Laird, each label returned by the oracle is flipped independently with a fixed probability . The algorithms of Chapter 1 collapse at once: the elimination algorithm deletes a correct literal on the strength of a single mislabeled example, and the tightest-fit rectangle may not exist. The chapter's remedy is to learn from statistics: an algorithm that forms its hypothesis only from estimates of probabilities of simple events is insensitive to occasional wrong labels. Kearns's statistical query model makes this precise, replacing the example oracle by an oracle that returns the probability of any predicate of a labeled example to within a tolerance, and the main theorem (5.3) shows that every class learnable from statistical queries is PAC learnable in the presence of classification noise. The proof rests on a single identity, Equation (5.2), that expresses the true value of a statistical query in terms of three quantities that can each be estimated from noisy examples, and on the observation that a hypothesis's disagreement with the noisy label is an affine function of its true error, which lets the best of several candidate hypotheses be recognized without clean data.
The framework is that of Mission I. The noisy example law is that of with and flipped with probability . A statistical query is a predicate of a labeled example with value . The inputs split into , where the label matters to , and , where it does not; and is conditioned on . For conjunctions over , is the probability that a literal is set to and the probability that it is on a positive example; is significant if and harmful if .
For and every statistical query ,
the probabilities on the right being taken under the noisy oracle.
The §5.2 analysis behind Theorem 5.2 (the conjunction of all significant, non-harmful literals has error at most ); the product estimate bound of p. 115 (); the identity of p. 117 ().
Equation (5.2) is the entire mechanism of noise-tolerant learning in the statistical query model: the noisy oracle cannot be de-noised example by example, but the probability of any predicate can be recovered exactly from noisy probabilities, because on the inputs where the label matters the noise acts as a known affine contraction and on the others it acts not at all. Together with the p. 117 identity, which turns hypothesis selection into a comparison of noisy disagreement rates, and the Chernoff bounds of Mission IV, it yields Theorem 5.3 and hence noise-tolerant algorithms for every class the book has learned so far (conjunctions, decision lists, -CNF). The §5.2 analysis is the first statistical-query algorithm and shows the pattern: a hypothesis defined by thresholds on a few probabilities, with enough slack between the thresholds that estimates suffice. None of this is machine-checked. The formalization fixes the noisy example law on the platform's sample framework and proves the exact identities on which the noise-tolerant simulation depends.
Equation (5.2) is a computation with the pushforward of a product measure: one must express the noisy law on as a mixture of the clean law and its label-flipped image, solve the affine relation for the clean probability, and combine with the restriction to , where the flipped and unflipped labels give the same value of ; the degenerate case , in which the conditional measure is zero and the first term vanishes, must be handled separately. The p. 117 identity is the same computation without the split. The §5.2 analysis is two union bounds over the literals after the observation that a literal of the target is never harmful and that a literal of the hypothesis is never insignificant. The product lemma is elementary arithmetic with a case split at .
The noisy oracle is a measure on labeled examples obtained by mapping the product of and a Bernoulli() coin; the conditional is Mathlib's conditional measure; queries are arbitrary measurable predicates of a labeled example, with no tolerance or query-count bookkeeping. Theorem 5.3 itself, the definitions of efficient learnability from statistical queries (Definition 14) and of efficient noisy PAC learnability (Definition 13), Theorem 5.1, Theorem 5.2 as a statement about an algorithm with oracle access, and Corollary 5.4 are not stated: they quantify over query algorithms and their running times, for which this series has no model; the mission carries their exact probabilistic content. The error-propagation analysis of §5.4.2–5.4.3 with tolerance and the guessing resolution is not stated beyond the product lemma, since the factor is not in and the book's constant does not account for it. Hypotheses: for the decomposition, for the disagreement identity, for the conjunction analysis, all reals in for the product lemma.
Trivializing readings are excluded: the decomposition is an exact identity for every measurable query, and the conjunction bound is for the exact thresholds with the union bound's . Welcome contributions: the mixture representation of the noisy law, the restriction of a pushforward to , and the two union bounds.
Chapter 4 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks whether the PAC model's demand for arbitrarily small error and confidence is essential. A weak learning algorithm need only, with some fixed positive probability, output a hypothesis that beats random guessing by a fixed margin. Schapire's theorem, the chapter's main result, says that this apparently much weaker requirement is equivalent to the original one: any weak learner can be converted, by running it on carefully filtered distributions and combining its hypotheses by majority votes, into a strong learner. The construction is boosting, which became one of the most influential ideas in machine learning. The chapter proves the equivalence in two steps. Boosting the confidence is elementary: run the learner several times and validate. Boosting the accuracy is the substance: a modest procedure that combines three hypotheses, each with error at most on its own distribution, into a majority with error at most , applied recursively until the error is driven below the target. The Chernoff bounds of the Appendix, the book's workhorse for estimating probabilities from samples, are what makes the validation steps rigorous.
The framework is that of Mission I. A class is weakly learnable using if for some advantage , confidence and sample size , an algorithm outputs hypotheses in that, for every target in and every distribution, have error at most with probability at least ; the algorithm's prediction is a measurable function of the sample and the instance together, as it is for every algorithm. Given a hypothesis , the filtered distribution gives weight to the instances on which errs and to those on which it is correct, preserving relative weights within each part, and is conditioned on ; the modest procedure outputs . Ternary majority trees over are the closure of under the majority of three. For confidence boosting, independent samples yield hypotheses, and a fresh sample selects the one with the fewest mistakes. Bernoulli trials are independent coin flips with success probability .
If is weakly PAC learnable using measurable hypotheses in , then is PAC learnable using the class of ternary majority trees with leaves from : for all some sample size and some algorithm outputting majority trees achieve error at most with probability at least , for every target in and every distribution.
Theorem 9.2 (the additive and multiplicative Chernoff bounds); the two facts of §4.2 behind confidence boosting (independent runs all fail with probability at most ; the fewest-mistakes selection loses at most with probability at least ); Lemma 4.1 (the modest procedure: error at most ).
Theorem 4.9 is one of the landmark results of learning theory: it shows that the PAC model has no intermediate strength, that Occam learning, weak learning and strong learning coincide, and that the resources of a strong learner can be bounded polylogarithmically in in memory and hypothesis size. Its constructive proof is the first boosting algorithm, ancestor of AdaBoost and of gradient boosting. Lemma 4.1 is the analytic core, a clean inequality about three hypotheses and three distributions in which the filtered distribution is exactly calibrated so that has no advantage on it. The Chernoff bounds are the concentration inequalities invoked throughout the book, and their formalization on the product law of Bernoulli trials makes every later "estimate to within with confidence " step reusable. None of these is machine-checked in this form; the boosting theorem in the sample-complexity sense is, to our knowledge, not formalized anywhere.
Lemma 4.1 is a computation with conditional measures: writing of the majority as the weight of the instances on which and both err plus times the weight of their disagreement, mapping weights under back to by the factors and (Equation (4.1)), and maximizing the resulting polynomial in ; the degenerate cases where a conditioning event is null must be handled separately. The Chernoff bounds require the exponential moment method on a finite product measure. The confidence-boosting facts are the product bound for independent blocks and Hoeffding plus a union bound. The goal is a genuine construction: from a large sample of one must simulate the recursive algorithm Strong-Learn, whose calls to the weak learner on filtered distributions are served by rejection sampling from the remaining examples, bound the depth of the recursion by the growth of iterates (Lemma 4.2), bound the number of examples consumed at each node (Lemmas 4.3–4.7) and allocate the confidence over all the places the simulation can fail; then package the result as a deterministic function of a sample of fixed size. An alternative route is available: weak learnability with a fixed sample size forces a finite VC dimension (a class shattering a large set defeats any fixed-size learner on the uniform distribution over it), after which Theorem 3.3 gives a consistent strong learner; but its hypotheses lie in , not in the majority trees over , so it does not prove the stated conclusion.
The weak-learning hypothesis is the book's with constants in place of the inverse polynomials, which is what the definition says for a fixed class; hypotheses in are required to be measurable, and the weak learner jointly measurable in the sample and the instance, because Strong-Learn runs it on distributions filtered through its own earlier outputs and the analysis integrates over the earlier samples (for an arbitrary function the combined failure event need not be measurable, and outer-measure bounds on separate runs do not combine); the conclusion is the book's hypothesis class, the majority trees over , built as an inductive predicate. Filtered distributions use Mathlib's conditional measure, so that a null conditioning event yields the zero measure; Lemma 4.1 is stated for and holds in those degenerate cases too. The confidence-boosting milestone states the two probabilistic facts rather than the composite algorithm, whose sample indexing across runs and validation is bookkeeping; the selection rule is any rule minimizing mistakes. Chernoff's bounds are stated with non-strict inequalities in the events, for and . Running time, the recursion-depth and sample-size lemmas with unspecified constants (4.2–4.8), and Exercises 4.1–4.3 are not stated.
Trivializing readings are excluded: the weak-learning guarantee is uniform over all targets and distributions with an advantage strictly positive, the strong conclusion is for every , and Lemma 4.1 requires all three error bounds on their respective distributions. Welcome contributions: Lemma 4.1 itself, the Hoeffding bound on the product law, and the rejection-sampling lemma that turns a sample of into a sample of a filtered distribution.
The bandit processes that motivated the index theorem are sampling processes: an arm is a population from which one draws i.i.d. observations whose distribution has an unknown parameter, and each draw both earns something and teaches something. Chapter 7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), develops the theory of such processes in the Bayesian setting: the state of the process is the current posterior for the parameter, continuing it samples the next value from the predictive distribution and moves to the new posterior. When the observations are themselves the rewards one has a reward process, the classical Bayesian multi-armed bandit; when the aim is to find as quickly as possible an individual whose measurement reaches a target (a compound active enough to warrant further testing, in the drug-screening problem from which the index theorem came) one has a target process, which is a job that completes when the target is reached. Two questions organize the chapter. When can the index be written down without any optimization, and when do symmetries of the model reduce the index to a function of fewer variables? The first is answered by the notion of a favourable prior (Section 7.3): if no run of observations below the target can raise the current probability of success, then the index is that probability, exactly, by Proposition 2.7. The second is answered by the invariance theorems of Section 7.4: a location parameter with a conjugate prior gives , a scale parameter gives , and for target processes the target can be absorbed into the state, . These identities are what make the tables of Chapter 8 one-dimensional.
A sampling model consists of a likelihood , a family of priors on the parameter indexed by the parameters of a conjugate family, and the Bayes update of those parameters after observing ; the family is conjugate if the posterior of given is . The predictive distribution is . The reward process moves from to with and earns . The target process with target moves to the completion state if and to otherwise, earning the current probability of success , and in . A state is favourable if for every finite sequence of observations . For the invariance theorems the parameters are with the update ; is a location parameter of the likelihood if is shifted by , and is a location parameter of the prior family if is shifted by ; scale parameters are defined with , . The Gittins index is that of the Bandit Algorithms model on these chains.
If is a location parameter of a reward process with a conjugate prior family in which is a location parameter and the parameters update as the sample mean and count, then for every
under the standing assumptions that the observations have a mean and the discounted rewards of the chain are integrable.
Proposition 7.4 (favourable state: ); Example 7.5 (Bernoulli target process, ); Example 7.6 (normal target process with known variance, for ); Theorem 7.11 (scale parameter: ); Theorem 7.17 (target process with a location parameter: ).
Theorem 7.9 and its companions are the reason the Gittins index of the normal reward process is tabulated as a function of alone and that of the exponential process as a function of and one ratio; every computational method of Chapter 8 starts by reducing the state space with them. Proposition 7.4 is the source of every closed-form index in the book: it identifies the states in which sampling for information is worthless, so that the index collapses to the immediate expected reward, and Examples 7.5 and 7.6 show that for the Bernoulli target process this is every state and for the normal target process every state with a nonnegative posterior mean. The formalization gives the platform its first Bayesian sampling-process model, in which the state is a posterior and conjugacy is stated through the posterior kernel of the likelihood, and its first index identities on unbounded-reward chains, which is where the integrability assumptions of the Bandit Algorithms model do real work.
None of this is machine-checked. The invariance theorems are stated in the proper-prior form of the corollaries, with the model's symmetry as hypotheses, so that they apply to any conjugate family with the stated structure rather than to a particular density.
The invariance theorems require showing that the chain of parameters from the shifted (scaled) state is the image of the chain from the original state under the shift (scaling) of trajectories, which is an equivariance of the Ionescu–Tulcea construction with respect to a measurable bijection commuting with the kernel; that stopping times are carried to stopping times; that the discounted reward of a stopping time shifts by times the discounted time; and that the supremum of a nonempty bounded set of reals shifts and scales accordingly. Boundedness of the set of ratios is where the integrability assumption enters. Proposition 7.4 is the chain-level statement that all rewards along every trajectory from a favourable state are at most , which needs an induction on the trajectory law of the target chain, followed by the argument of Proposition 2.7. Example 7.6 needs the monotonicity of in the observations below the target, a small inequality, plus the Gaussian probability of a half-line as the current probability of success; Example 7.5 needs only that decreases.
The sampling model is a structure with Markov likelihood and prior kernels and a jointly measurable update; the predictive distribution is the kernel composition; conjugacy is an almost-everywhere identity between Mathlib's posterior of the likelihood with respect to the prior and the prior at the updated parameters, and is carried as a hypothesis of the invariance theorems and of Proposition 7.4 so that their subject is the Bayesian process. For the parameters it is required on only (IsConjugateOn): a proper prior has , and conjugacy at every is impossible with a location parameter, since at the update divides by zero and sends every observation to one state, which made the first draft's location theorems vacuous. The chains are built with Kernel.map of product kernels, so their measurability is structural, and the target process lives on P ⊕ Unit with the completion state absorbing. The book's improper priors are replaced by proper conjugate families with the location or scale structure of Corollaries 7.10 and 7.12, as those corollaries do; the discrete-time correction factor of Section 2.8 is not applied since it cancels in every identity stated. The two examples are built directly from a uniform or Gaussian seed with the transition probabilities the book computes (the beta and normal posterior computations of Exercise 7.1 are not formalized). Hypotheses: ; integrable observations and L&S Assumption 35.6 for the reward processes; for the invariance theorems and for the scale theorem; ; and for the normal example.
Trivializing readings are excluded: the indices are the genuine suprema of the Bandit Algorithms definition with integrable rewards, the update rule is the book's and not a free parameter, and the favourability condition ranges over all finite observation sequences. Welcome contributions: the equivariance of the trajectory measure under a state bijection commuting with the kernel, the transport of stopping times, and the reward bound along the target chain from a favourable state.
Every proof of the index theorem in Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), uses the fact that a bandit not being processed is frozen. Chapter 6 drops that: Whittle's restless bandits evolve under the passive action too, by a different law, and of must be active at every time. The problem is PSPACE-hard in general, so Whittle proposed a heuristic built from a Lagrangian relaxation: replace the hard constraint by a subsidy paid whenever a bandit is passive, solve the resulting single-bandit average-reward problem, and read off, for each state, the least subsidy at which the passive action becomes optimal. When the set of states where passivity is optimal grows monotonically with , the bandit is indexable and is its Whittle index; the Whittle index policy activates the bandits of largest index. It reduces to the Gittins index policy when the passive action freezes, it is asymptotically optimal as grows under a fluid-stability condition (Weber and Weiss), and it has become the standard heuristic for sensor management, opportunistic channel access, maintenance and queueing control. The price is that indexability must be established model by model. Section 6.5 shows how easy this is when the single-bandit problem is solved by a monotone policy, on two bi-directional models: the spinning plates asset, which improves under investment and deteriorates when neglected, and the vigour bandit of Whittle's Ehrenfest project, which tires when worked and recovers when rested.
A restless bandit is a Markov decision process with two actions, active () and passive (), each with its own transition kernel and reward. Under a deterministic stationary Markov policy with passive subsidy the reward in state is , and the average reward from is the Cesàro limit of the expected rewards. The optimal average reward is the supremum over such policies and initial states; a policy is optimal if it attains from every initial state; is the set of states in which some optimal policy is passive; the bandit is indexable if is nondecreasing in ; and .
The spinning plates asset lives on : active moves at rate , passive moves at rate , , and is earned under both actions, increasing. Uniformized so that rates are at most one, it is a discrete-time bandit whose kernels move with the rate's probability and otherwise stay. The monotone policy is passive exactly on ; under it the asset alternates between and , spending the fraction of its time at , so its average reward is with , and . The vigour bandit is the mirror image: active moves down at rate and earns , passive moves up at rate and earns nothing, , and .
For the spinning plates asset: (i) if is strictly decreasing over the thresholds , the asset is indexable; (ii) if additionally is strictly decreasing over the states, the Whittle index is
Eqs. (6.9)–(6.10): the monotone policy earns from every initial state and , because a monotone policy always achieves ; Theorem 6.5, the same two statements for the vigour bandit with increasing and increasing.
Theorem 6.4 is the chapter's template for proving indexability: the single-bandit value is the upper envelope of finitely many lines whose slopes decrease in the threshold, so the optimal threshold moves monotonically with the subsidy and the hinge points of the envelope are the indices. The same argument gives Theorem 6.5, the admission-control indices of Section 6.7, and the marginal productivity indices of Niño-Mora; it is the reason Whittle indices are computable in closed form for bi-directional models. Its formalization establishes, on the platform, the first restless-bandit model with a proved index, and the general notions of passive set, indexability and Whittle index that every later restless-bandit statement will use.
None of this is machine-checked. The average-reward optimality notion is stated without the DP equation (6.6), through optimality from every initial state, which is what the equation's solution encodes on a finite state space and avoids the relative value function altogether.
The proof in the book is two paragraphs, but it stands on the reduction to monotone policies, which is only sketched: every deterministic stationary policy, from every initial state, drives the asset into an absorbing endpoint or a two-state cycle whose average reward is that of the monotone policy , so no policy beats the best monotone one and the passive set under an optimal-from-everywhere policy is exactly for the smallest maximizing threshold. Formalizing this needs the average reward of a finite Markov chain as a limit determined by the stationary distribution of the recurrent class reached, for the two-point kernels of the model, and a case analysis of policies as -strings. The envelope argument then needs that the smallest maximizer of is nonincreasing in when is strictly decreasing, and that with strictly decreasing the maximizer is exactly when . Theorem 6.5 is the same with the roles of up and down exchanged. Nothing in Mathlib computes Cesàro limits of finite Markov chains.
Restless bandits are the two-action DecisionProcesses of the superprocess module; average reward is a real limsup of Cesàro means of Bochner integrals over the chain law of the Bandit Algorithms model under the stationary kernel; the optimal average reward is a supremum over the finite type of deterministic stationary Markov policies and the finite state space, bounded by the reward bound. Both models are on Fin k with the book's states shifted down by one, kernels driftKernel p f that move to f x with probability p x, and the boundary conventions of and (the book's "convenient positive values") replaced by their values and at the two extreme thresholds; the model assumptions , , rates in , and increasing and nonnegative are hypotheses. Theorem 6.5's "increasing" is read as strictly increasing, as in Theorem 6.4, since a nonstrict admits zero interior rates for which the monotone reduction fails. The milestone (6.9) requires and positive interior rates, which Theorem 6.4's hypothesis (i) implies.
Trivializing readings are excluded: indexability is monotonicity of the passive set over all real subsidies, the passive set is defined through policies optimal from every initial state, and the index identity is for every state. Welcome contributions: the average reward of a two-state cycle, the reduction of an arbitrary -policy to a monotone one, and the envelope lemma for lines with decreasing slopes.
Chapter 5 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), presents the achievable region methodology of Tsoucas, Bertsimas and Niño-Mora, Glazebrook and Garbe, and Dacre, Glazebrook and Niño-Mora: instead of arguing about policies, one argues about the set of performance vectors they can produce. For a multi-armed bandit the natural performance of a policy is the vector of discounted numbers of times each state is continued; the expected return is linear in it; and the set of achievable performances turns out to be a polytope cut out by conservation laws, one inequality per subset of states, with equality exactly for the priority policies that put that subset last. Optimizing a linear objective over a polytope is a linear program, its dual is solved by an adaptive greedy algorithm, and the primal solution is the performance of a priority policy whose priorities are the algorithm's outputs, the Gittins indices. This gives yet another proof of the index theorem (Section 5.3) and, more importantly, a definition, generalized conservation laws (Section 5.4), of the class of systems for which the same argument works: branching bandits, multi-class queues, job scheduling with discounted rewards, systems with imposed priority classes. The chapter's main result, Theorem 5.5, is the statement that every such system is solved by an index policy.
There are job types . A policy has a performance , a vector of expectations; a permutation of defines the permutation policy giving highest and lowest priority, and is the set of the lowest-priority types. The system satisfies GCL(1) if there are a base function and a matrix , positive on and zero off it, such that for every policy
with equality in the first for every permutation policy whose lowest-priority types are . GCL(2) reverses the inequality. The adaptive greedy algorithm picks maximizing , sets to the maximum, removes , and repeats with the adjusted rewards divided by ; its outputs are the order , the dual variables and the indices .
For the SFABP of Section 5.3, identical bandit processes on with kernel and discount factor in the model of the Bandit Algorithms series, is the discounted number of continuations of a bandit in state , is the discounted return time to from , and is the minimal cost , namely with the number of continuations needed to bring every bandit into .
For a GCL(1) system whose achievable region is convex, and any reward vector : the achievable region is the polytope
its extreme points are performances of permutation policies; has an output; and for every output the permutation policy in the order it finds, the Gittins index policy, maximizes over all policies.
Lemma 5.1 (the SFABP satisfies the conservation laws, with equality for policies giving priority to states outside ); the identification on p. 123 of the adaptive greedy indices of a SFABP with the Gittins indices, together with their monotonicity along the order found; Theorem 5.10, the GCL(2) counterpart of the goal for cost minimization.
Theorem 5.5 is the index theorem in its most general form of this kind: it says nothing about Markov chains, only that performances are expectations, objectives are linear and conservation laws hold, and it delivers both the optimal policy and the algorithm that computes its priorities in polynomial time in the number of job types. It is the theorem behind the index results for branching bandits and Klimov's multi-class queue and behind the suboptimality bounds of Sections 5.5 and 5.7, all of which are calculations on the polytope. Lemma 5.1 and the p. 123 identification are what tie the abstract theorem to the Gittins index: they show that the multi-armed bandit is a GCL(1) system and that the priorities the algorithm produces are the same indices as Chapters 2 to 4 define through stopping times.
None of these is machine-checked. Formalizing Theorem 5.5 puts an LP-duality index theorem on the platform in a form any system can instantiate by verifying its conservation laws; formalizing Lemma 5.1 relates the Bandit Algorithms run law to the single-chain return times, which is the first conservation law on that model; and the p. 123 theorem gives an algorithmic characterization of the Gittins index on finite chains, distinct from the restart and largest-remaining-index characterizations of Chapter 2.
The goal's optimality clause is weak LP duality once one shows that the greedy dual variables are nonpositive except and satisfy the dual constraints with equality, which is a finite induction on the stages; the extreme-point clause needs that every vertex of a polyhedron is the unique maximizer of some linear functional, and the region clause that a compact convex set is the convex hull of its extreme points (Krein–Milman in finite dimension, or the polyhedral fact directly). None of this is in Mathlib in the required form. Lemma 5.1 is probabilistic: the lower bound requires the strong Markov property of the continued bandit under an arbitrary past-measurable policy, a pathwise accounting of the discounted periods paid for by each continuation from , and the observation that at most slots can be spent on bandits that have never been in ; the equality for priority policies requires that these policies use exactly those slots first and then tile the future with return excursions, and the product form of requires independence of the bandits' process-time trajectories under the run law, which is built decision time by decision time rather than as a product. The p. 123 theorem is the computation (5.13) to (5.14) combined with the optimal-stopping characterization of Chapter 2 for the stop sets , which lie between and ; ties make the induction delicate, and the statement is claimed for every tie-breaking.
GCL(1) and GCL(2) systems are structures over an arbitrary policy type: performance, base function, matrix, permutation policies and the three laws are fields, so the theorems are statements about finite-dimensional data and the platform's proof needs no probability. The adaptive greedy algorithm is specified relationally, as the set of its possible outputs with arbitrary tie-breaking, and the conclusion holds for each of them; existence of an output is asserted separately. The optimality clause is stated as a comparison with every policy rather than as a real supremum. The hypothesis that the achievable region is convex is explicit: the book's argument from extreme points to the whole polytope uses randomization of policies, and without it the region of a system with only its permutation policies is finite. The SFABP items use identical bandits on Fin N in the Bandit Algorithms model, the coefficients through Mission I's stoppedTime at the return time, and in the product form , which is the minimal cost the argument on p. 120 establishes; the book prints a sum, which is when all bandits start in where the minimal cost is . Discount factors are in throughout.
Trivializing readings are excluded: for is part of the structure and of Lemma 5.1's conclusion, the polytope equations are over all subsets, and the index clause quantifies over every greedy output. Welcome contributions: the nonpositivity and dual feasibility of the greedy variables, the vertex-exposure lemma for polyhedra, and the product decomposition of the run law of identical bandits.
A recommendation system learns from the users it serves: the diner who tries a restaurant produces the review the next diner reads. Each user would rather exploit what is already known than explore for the benefit of those who come later, so a population of self-interested agents under-explores, and an alternative that looks bad on sparse early evidence may never be tried again even when it is the best. Chapter 11 of Slivkins, Introduction to Multi-Armed Bandits (arXiv:1904.07272), treats incentivized exploration: a principal who cannot force the agents but can recommend, and who, because it aggregates what earlier agents observed, knows more than any one of them. The question is whether recommendations alone can induce enough exploration to learn as fast as an ordinary bandit algorithm. The model is that of Kremer, Mansour and Perry (JPE 2014) and the results are those of Mansour, Slivkins and Syrgkanis (EC 2015, Operations Research 2020), specialized to two arms; the single-round problem is Bayesian persuasion in the sense of Kamenica and Gentzkow (AER 2011).
There are arms and rounds. A mean reward vector is drawn from a known prior , and each pull of arm yields a reward drawn from a known family with mean . In round the principal recommends an arm ; agent , who knows the prior, the family, the algorithm and the round but not the past, sees only , chooses , collects and leaves; the principal observes . The chapter works with two arms, ordered so that the prior means satisfy , with a prior of finite support and finitely many reward values.
An algorithm is Bayesian incentive-compatible (BIC, Definition 11.4) if following its recommendation is in every agent's interest given what the agent knows: for every round and arms with ,
where is the event that all previous agents complied. A BIC algorithm is then an ordinary bandit algorithm whose recommendations are followed, and the run has the law of the Bayesian bandit of Chapter 3. Two contrasting policies frame the chapter. GREEDY reveals the history and lets agents exploit, (11.2); it is BIC and it fails. HiddenExploration (Algorithm 11.1) hides a little exploration in a lot of exploitation: on a signal , with probability it recommends a target arm , otherwise the arm maximizing , ties to arm 1. Its posterior gap is . RepeatedHE (Algorithm 11.2) runs it round after round with an arbitrary bandit algorithm as the target: initial rounds recommend arm 1; afterwards, with probability the round is an exploration round in which chooses (and is fed the reward), and otherwise the exploitation branch recommends , where is the data of all exploration rounds so far (11.10). The quantity that governs everything is (11.11), the posterior gap after samples of arm 1, and Property (11.12), that for some : arm 2 can appear better after enough samples of arm 1.
RepeatedHE with exploration probability and initial samples of arm 1 is BIC as long as
for any bandit algorithm and any horizon. The threshold depends on the prior alone.
Theorem 11.7 (GREEDY never chooses arm 2 with probability at least ) and Corollary 11.8 (linear Bayesian regret of GREEDY under independent priors); Lemma 11.10 (HiddenExploration is BIC when ) with Claim 11.12 (the arm-2 side of the constraint suffices); Corollary 11.14 (RepeatedHE is BIC under the round-by-round condition); Theorem 11.19 (without Property (11.12) no BIC algorithm ever plays arm 2, ties to arm 1).
The results say when exploration can be incentivized at all and how. Theorem 11.7 shows that revealing everything is not a solution: the greedy dynamics gets stuck on arm 1 with a probability that does not shrink with , and Corollary 11.8 turns that into Bayesian regret. Theorem 11.15 shows that a recommendation-only principal can induce any amount of exploration it wants, with arbitrary, at a per-round rate fixed by the prior; Theorem 11.17 (stated with a proof sketch, and omitted here) then transfers 's regret to RepeatedHE up to the prior-dependent factors and , so regret is attainable subject to incentives. Theorem 11.19 closes the picture: Property (11.12) is necessary as well as sufficient. Together they characterize which priors admit incentivized exploration and give an algorithm that works for all of them.
Nothing of this is machine-checked. The mission adds to the Bayesian layer of mission III (prior, posterior by Bayes' rule, Bayesian regret) the BIC constraint on a joint law, GREEDY as a policy, the single-round HiddenExploration on an abstract finite signal, and the law of RepeatedHE; all of it is reusable for the -arm and the "explore all explorable arms" extensions of the literature review.
Theorem 11.7 is a martingale argument: the posterior gap along the history is a Doob martingale, the first round in which arm 2 is chosen is a bounded stopping time, and optional stopping gives ; all of this has to be set up on the joint law of of mission III, where the posterior is defined by Bayes' rule and the identification with a conditional expectation is itself a theorem (posterior_eq_condProb). Lemma 11.10 is the heart of the chapter and is not a computation about : it works with , splits along the two branches, uses that the exploitation branch recommends arm 2 exactly when , and closes with ; the only place where the analysis uses that both branches are functions of the signal is the step , and a formalization has to make that step explicit. Theorem 11.15 requires seeing each later round of RepeatedHE as a HiddenExploration with signal , where 's choice is a randomized function of , and then the monotonicity of in , a two-line consequence of determining that presupposes the posterior given is the Bayes posterior of the exploration data alone, which is true because the exploration decisions do not depend on given that data. Corollary 11.8 needs the independence of the event " and arm 2 is never chosen" from . Theorem 11.19 is an induction in which the inductive hypothesis is a probability-zero statement about all earlier rounds.
Arms are Fin 2, the book's arm 1 being index 0; rounds are Fin T. The prior is a probability measure on mean vectors supported on a finite set , with as a hypothesis; the reward family is mission III's RewardFamily (finitely many values, mean for ). BIC is defined on a joint law of of the run in which every agent complies, with the recommendation of each round read off the record; the compliance event of (11.1) is the sure event of that law, which is the standard reading of "the agents believe all previous agents complied". For a bandit policy the law is mission III's jointMeasure. Conditional expectations are written as finite sums over , so there are no integrals and no integrability side conditions; a posterior mean off the support is a junk that never enters a theorem. GREEDY allows arbitrary tie-breaking; HiddenExploration's exploitation branch breaks ties toward arm 1 as Algorithm 11.1 does; the tie convention of Theorem 11.19 is the strict form of BIC for arm 2. The law of RepeatedHE is an explicit finitely supported measure, and record weighted by the prior times the product of the round probabilities (initial rounds forced to arm 1, then the -coin, 's kernel on its own history, or the exploitation arm, then ); it is written this way because is fed a history of variable length. Two conditions are stated exactly as printed: Lemma 11.10 with (non-strict, checked at equality) and Theorem 11.15 with the strict inequality.
Trivializations are excluded: throughout; the BIC condition is asserted only where the recommendation has positive probability, and the sums in it are over the finite support, so an unsatisfiable hypothesis cannot hide in a measure-zero set. Welcome contributions: the optional-stopping argument on jointMeasure, the identification of explPostMean with the conditional expectation given the exploration data, the Bayes-rule algebra behind Lemma 11.10, and the counting lemmas on heRecords.
Airlines selling last seats, Priceline's name-your-own-price, procurement of supply contracts: Chapter 6 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) treats auctions as pricing mechanisms and asks what revenue they earn and how to design them. Its centre is Myerson's (1981) theory for independent private values: whatever the mechanism, so long as bidders with higher valuations are more likely to win and the lowest type gains nothing, the firm's expected revenue is the expected virtual value of the winners, with (Theorem 6.1, the revenue equivalence theorem). Maximizing that expression pointwise gives the optimal auction: the standard first- or second-price auction with a reserve price at the zero of (Theorem 6.2). This mission formalizes the second-price form of Theorem 6.2 as its goal, with the dominant-strategy and first-price equilibria of the informal analysis, Theorem 6.1, the optimal allocation and Proposition 6.1 on list prices as supporting results.
customers have i.i.d. valuations on with a continuously differentiable,
strictly increasing distribution and positive density (PrivateValues, IsRegular); the
joint law is the product measure (joint). A direct-revelation mechanism (Mechanism) maps
reported valuations to allocations , at most units in total, and
payments . For a report by customer , is the win probability,
the expected payment and the surplus (winProb, expPayment,
expSurplus); incentive compatibility, , is the equilibrium
condition of the direct mechanism (IsIncentiveCompatible). The chapter's mechanisms are the
-unit second-price auction with reserve price (secondPriceReserve: the highest
valuations above win and pay the larger of and the highest losing valuation), the
list-price mechanism for (listPrice), and the single-unit first-price auction with
its equilibrium bid , (firstPriceBid).
With strictly increasing (Assumption 7.2) and its zero, the -unit second-price
auction with reserve price is a feasible, incentive-compatible mechanism with monotone
allocations and zero surplus at zero, and its expected revenue is at least that of every such
mechanism: reserve_price_auction_optimal.
Bidding one's valuation is dominant in the second-price auction (Sect. 6.2.2.1); the bid (6.4) solves the first-order condition (6.3), is a symmetric equilibrium of the first-price auction and shades below the valuation (Sect. 6.2.2.2); Theorem 6.1, revenue equals expected virtual surplus and each expected payment is ; the pointwise optimal allocation of Sect. 6.2.5; and Proposition 6.1, a list price at is optimal when .
Proposition 6.2 (asymptotic optimality of list prices, a law-of-large-numbers statement about scaled auctions), the first-price form of Theorem 6.2 with its equilibrium (6.9) stated without proof, and the dynamic, replenishment and network auctions of Sects. 6.3-6.5 (Propositions 6.3-6.11, from Vulcano, van Ryzin and Maglaras and from Cooper and Menich) are not targets of this mission.
Theorem 6.1 is the tool that lets revenue be computed from allocations alone, which is why the first- and second-price auctions of Examples 6.1-6.3 earn the same and why any dynamic pricing scheme that ends with the same winners earns the same as the optimal auction (Sect. 6.2.6.3). Theorem 6.2 says a firm with private-value customers cannot do better than a standard auction with the right reserve price, and Proposition 6.1 that with enough capacity a list price already does it: auctions are a small-numbers phenomenon. These are the foundations on which the chapter's dynamic auctions and the list-price comparisons of Sects. 6.3-6.4 rest, and Myerson's optimal auction has no machine-checked proof in its multi-unit form.
Theorem 6.1 is an envelope argument in measure-theoretic clothing: incentive compatibility gives the two-sided inequalities of Appendix 6.A, monotonicity of makes convex with derivative almost everywhere, so , and then an integration by parts against the density converts into ; the win probabilities are integrals over a product measure with one coordinate replaced, and Fubini is needed to return to . The goal then needs the reserve-price auction shown incentive compatible (a dominant-strategy argument on the threshold payment), measurable, monotone and with zero surplus at zero, and the pointwise optimal allocation integrated. The first-price item is calculus on an interval integral with a vanishing denominator at and a monotone comparative-statics argument for the equilibrium inequality.
Mechanisms are direct-revelation mechanisms on , as the book reduces to in Sect. 6.2.3.1; expectations over the other customers are integrals over the joint law with customer 's coordinate overwritten by the report. Payments are assumed bounded on reports in (not on all of , where the second-price payment is unbounded) and the rules measurable. Ties in the second-price auction are broken by index, a null event, and when every customer wins the losing supremum is so the winner pays the reserve. Theorem 6.2 is stated for the second-price auction; the first-price version with reserve price, whose equilibrium (6.9) the book asserts without proof, is left out and noted. Optimality is over mechanisms satisfying conditions (i) and (ii) of Theorem 6.1 and incentive compatibility, which is the class the book compares against. The virtual value's zero is a parameter with rather than the maximum of (6.8), which under strict monotonicity is the same point.
Chapter 10 of Axsäter's Inventory Control turns to reorder points and safety stocks in multi-echelon systems, where the installations cannot be treated separately: a large stock downstream lets an upstream site run lean, and a long upstream lead-time argues for stock at the top. The best-known exact technique for serial systems is the decomposition of Clark and Scarf (1960), which the book presents in the infinite-horizon form of Federgruen and Zipkin (1984). It is also where the echelon stock measure comes from. The section's argument is short and self-contained, and its conclusion is a complete description of the optimal policy for a two-level serial system: order-up-to levels at both installations, one of them a newsboy solution, the other the minimizer of a convex function in which upstream shortages appear as an induced cost. It is the capstone of Chapter 10.
Installation 1 faces normally distributed period demand with mean and standard deviation , independent across periods, so the demand over periods, , is normal with mean and standard deviation . Installation 1 replenishes from installation 2 with lead-time periods; installation 2 replenishes from an outside supplier with infinite supply and lead-time . Demand that cannot be met is backordered. Costs per unit and period are echelon holding costs , so the installation holding costs are and , and a shortage cost at installation 1; there are no ordering costs. Events in a period occur in the order: installation 2 orders, its delivery arrives, installation 1 orders, its delivery arrives, demand, cost evaluation.
Consider an arbitrary period . After ordering, installation 2 has an echelon inventory position , and by the standard argument its echelon stock in period is . Installation 1 then orders, realizing an echelon position that cannot exceed what is available: (Eq. 10.1). Its inventory level after the demand in period is . The expected period costs are at installation 2 and at installation 1, and the book reallocates the term to obtain
with and . As a function of a free , is the newsboy-type function of Eq. (10.6), minimized at the level given by the fractile equation (10.8). Passing everything available up to to installation 1, , gives the total cost of Eq. (10.9), whose minimizer is the order-up-to level of installation 2.
With from (10.8) and a minimizer of : for every and every allocation rule with and finite expected cost,
and the order-up-to policy attains .
Eq. (10.3), the stage-1 period cost through the expected backorders; the reallocation (10.4)-(10.5), which leaves the total unchanged; the closed form (10.6) of through the loss function ; the convexity of , its derivative (10.7), and the fractile characterization (10.8) of its minimizers; the pointwise rule that is the cheapest feasible ; the identity (10.9); and the convexity of (Problem 10.1) with the existence of its minimizer when .
The result itself. The decomposition reduces a two-dimensional stochastic control problem to two one-dimensional convex problems solved in sequence, from downstream to upstream, and it identifies the optimal policy class. The downstream level is a newsboy solution with overage cost , the value added, and underage cost , and it is independent of the upstream installation altogether; the upstream level sees the downstream installation only through the induced shortage cost, the last term of (10.9). The book notes the extensions the argument admits, to more echelons, to batch ordering at the top, and, via Rosling's equivalence, to assembly systems, and its Sect. 10.1.2 adapts it, now only approximately, to distribution systems under the balance assumption. Example 10.1 shows the typical outcome: the optimal average stock at the upstream installation is slightly negative.
Formalizing it. The section's mathematics is a chain of expectations under Gaussian laws and two convexity arguments. Formalizing it fixes what "optimal" means, a per-period comparison against every allocation rule, and separates the two convexity claims the book makes in one clause each. Nothing here is open; no statement has a machine-checked proof yet.
The pointwise allocation rule and the newsboy fractile are the same arguments as in the newsboy mission. The two places where work is needed are the identity (10.9), an expectation of a piecewise function split at , and the convexity of , which requires seeing that is convex precisely because is a minimizer of the convex (for any other cut-off the function is not convex), and that convexity is preserved by integrating against the law of , which needs the integrability of the linearly growing . Existence of then follows from the growth of at both ends, which comes from the asymptotics of the loss function: as and as .
is csDemand mu sigma n, the Gaussian law newsboyDemand (n μ) (√n σ) from the newsboy
mission, so the loss function and its closed form are reused as references. The costs are
parametrized by with and written out; ,
, the pre-reallocation period cost and are Bochner integrals against these
laws. Every statement assumes ; the goal and the convexity statements assume
and , the book's cost signs. is allowed and makes a
point mass, which is the setting of the book's Problem 10.2.
enters as any solution of the fractile equation (10.8) and as any minimizer of ; the other items show that both exist when . When the fractile is , no exists, and the goal is vacuous, which is faithful: the book observes that then and installation 2 never carries stock. Symmetrically, when and , decreases towards its infimum without attaining it, so no exists and the goal is again vacuous: with free upstream holding the optimal is unbounded. Allocation rules are arbitrary functions of the realized with an integrability hypothesis; without it Lean's integral of a non-integrable cost would be and could undercut , which is negative in Example 10.1's stage-1 term.
What is not modelled is the infinite-horizon dynamic problem: the book's optimality claim is made period by period, and the passage to the stationary policy rests on the remark that the outside supplier has infinite supply, so the same can be chosen in every period. The definitions are reusable for the three-echelon extension and for the distribution system of Sect. 10.1.2; contributions formalizing Problem 10.2 () as a first step are welcome.
A firm that holds inventory in five warehouses needs more safety stock than one that holds the same inventory in one warehouse, because the demands of five regions do not all run high at once. Eppen (1979) made this precise for a multi-location newsvendor and gave it its name, the risk-pooling effect. Chapter 7 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) follows the same idea through three settings in which pooling happens without physical consolidation: two retailers who ship stock to each other after seeing demand (transshipments, after Tagaras 1989), and plants that can each make more than one product (process flexibility, after Jordan and Graves 1995). The chapter's capstone is the theorem of Simchi-Levi and Wei (2012) that, among designs in which every plant makes two products and every product is made at two plants, a single long chain through all of them is best. This mission formalizes the chapter's numbered results, with that theorem as its goal.
Risk pooling. distribution centers face normally distributed per-period demands
with correlation coefficients , and each runs a
base-stock policy with holding cost and backorder cost per unit per period, so its
optimal expected cost is the optimal newsvendor cost optNvCost h p D, the infimum over
base-stock levels of . Merging the centers gives one
facing the total demand, normal with mean and variance
(pooledVariance).
Transshipments. Two retailers with base-stock levels face independent
demands. After demand is observed, under complete pooling the retailer with a surplus sends
the retailer with a shortage units (transship), and
nothing moves otherwise. The type-1 service level is the probability of no stockout,
without and with
transshipments; the type-2 service level is the fill rate, one minus expected unmet demand
over expected demand, and likewise.
Process flexibility. A flexibility design on products and plants is a set
of (product, plant) pairs, an edge meaning plant can make product . Given a
demand realization and a common plant capacity , the performance (perf)
is the maximum sales obtainable by assigning production along the edges of without
exceeding any capacity or demand, the linear program (7.22) to (7.26). A balanced system
(BalancedSystem) has equal capacities and an exchangeable demand vector, one whose joint
law is invariant under permutations of the products, and is the
expected performance (expPerf). The named designs are the dedicated design ,
the long chain in which plant also makes product (and plant makes
product ), the open chain obtained from by deleting the edge , and
, the open chain on the first pairs together with the dedicated edges of the rest. A
2-flexibility design (TwoFlex) is one in which every product has exactly two plants and
every plant exactly two products; is one, and so is any union of disjoint shorter chains.
For a balanced system of size with exchangeable demand,
that is, is a 2-flexibility design and for every 2-flexibility design .
This is long_chain_optimal.
The chapter's route to the goal: Lemma 7.5, supermodularity of sales in the flexible edges of the long chain for every realization, for ; Corollary 7.6, the same in expectation; Lemma 7.7, the increments are nondecreasing in , ending with ; and Lemma 7.8, .
Risk pooling, Theorem 7.1: , the optimal cost of the merged center is at most the sum of the optimal costs of the separate ones, with the covariance inequality as a separate lemma.
Transshipments, Theorems 7.2 to 7.4: , , and all four post-transshipment service levels are nondecreasing in .
Theorem 7.9 is the analytical answer to a question that had been settled only by simulation: Jordan and Graves reported that one chain through all plants achieves nearly twice the sales benefit of three short chains with the same number of edges, and Simchi-Levi and Wei proved that no arrangement of the same edge budget does better. It is the justification for the chaining guideline used in automotive and semiconductor capacity planning, and Lemma 7.8, which expresses the long chain through open chains, is what makes the long chain's performance computable by a greedy pass. Theorem 7.1 is the quantitative basis for consolidation decisions and for postponement, since a generic product is pooled inventory. Theorems 7.2 to 7.4 quantify what transshipments buy in service, which is the argument for allowing them despite their cost.
None of these results has a machine-checked proof. The book proves Lemma 7.7, Lemma 7.8 and Theorem 7.9 in full given Lemma 7.5, which it cites to Simchi-Levi and Wei, and omits the proofs of Theorems 7.3 and 7.4 and the identity (7.30) behind Lemma 7.8. Formalizing Lemma 7.5 and (7.30) means formalizing the structure of maximum flows on a cycle, which is reusable for the later results of Simchi-Levi and Wei on the long chain's performance relative to full flexibility and for the multi-echelon flexibility models the chapter cites.
The obvious approach to Theorem 7.9 is to compare with an arbitrary 2-flexibility design directly. Nothing in the definitions supports that: the two designs share no structure beyond their degree sequences. The book's argument instead routes everything through the long chain's own edges. Lemma 7.5 gives supermodularity only for subsets of , and the decomposition of an arbitrary 2-flexibility design into disjoint cycles, each a relabeled long chain on a subsystem, is what allows the comparison. A solver must therefore prove that a 2-regular bipartite graph is a disjoint union of even cycles, that exchangeability makes every relabeling of a cycle worth the same as on its subsystem, and that the performance of a disjoint union is the sum of the performances of its parts.
Lemma 7.5 itself is where the combinatorics lives. It says that on the cycle the maximum flow is supermodular in the flexible edges, and the proof in Simchi-Levi and Wei goes through the structure of augmenting paths on a cycle. The natural first idea, that supermodularity follows from some general property of maximum flows, is false: maximum flow is not supermodular in arbitrary edge sets, and the lemma is specific to subsets of a single cycle.
Lemma 7.7 is where exchangeability is used, and it is used in a way that is easy to state and tedious to formalize: removing the edge from leaves a design that is only after the pair is moved to the end, so the argument needs the invariance of under relabeling the products and plants by a common permutation. The book notes that Lemma 7.7, unlike Lemma 7.5, is false realization by realization.
For the transshipment theorems, the book differentiates a density formula by Leibniz's rule. Under the weaker hypothesis stated here, laws without atoms and with finite means, the derivative of in has to be obtained by dominated convergence from the pointwise derivative of a piecewise-linear function whose kinks lie on null sets.
perf is a supremum over a set of reals, nonempty because is feasible when
and , and bounded by ; the demand is nonnegative for every outcome and the
capacity nonnegative in BalancedSystem, and Lemma 7.5 carries these as hypotheses. The
supremum is attained, but the definition does not assert it. Expected performance is a Lebesgue
integral; the demand is integrable by assumption and is -Lipschitz in , so the
integrand is integrable, and a solver must prove this measurability rather than assume it.
Exchangeability is the equality of the laws of and for every
permutation . Designs are finite sets of pairs of Fin n; the chains are defined with
finRotate, so indices wrap modulo and the closing edge of is in the book's
numbering, which is the edge its proofs and Figure 7.3(c) use. Lemma 7.8 involves open chains on
subsystems of sizes and ; these are designs on Fin k evaluated on the first
coordinates of the demand (subDemand, subPerf).
Theorem 7.1 states the optimal costs as infima of the newsvendor cost over all base-stock
levels, on Mathlib's gaussianReal; a nonpositive pooled variance gives a degenerate law, for
which the inequality still holds, so the statement is not trivialized by that convention. The
transshipment theorems take the two demand laws as probability measures on with no
atoms (Theorem 7.2) and finite, positive means; the quantity is defined for all
outcomes and the service levels are probabilities and expectations under the product law.
The definition module is shared by all eleven items. Beyond the milestones, formalizing the
identity (7.30) as its own lemma and the disjoint-union additivity of perf would be natural
contributions.
Procter & Gamble observed in the 1990s that the orders its distributors placed for diapers were far more variable than the retail sales of diapers, and that its own orders to suppliers were more variable still, although the end demand for diapers is about as stable as demand gets. The phenomenon, a growing amplification of variability as one moves upstream in a supply chain, is the bullwhip effect. Lee, Padmanabhan and Whang (1997) argued that it is not a symptom of irrational behaviour: four rational responses of an inventory manager to their own environment each produce it. Chapter 13 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) makes three of the four quantitative, following Chen, Drezner, Ryan and Simchi-Levi (2000) for demand signal processing, Lee et al. for the rationing game, and Cachon (1999) for order batching. This mission formalizes those three models and the theorems the chapter proves about them.
Demand signal processing. A retailer faces a demand process , , that follows the stationary first-order autoregressive model
with a constant , a correlation constant , and errors that are independent variables, each independent of the demands before period . In steady state every has the law . The retailer replenishes with a lead time of periods under a base-stock policy but does not know the demand parameters, so it estimates the lead-time demand from a moving average of the previous demands:
and sets the base-stock level , where
is a safety factor. The book writes the constant in as and does
not give its form; here it is a free parameter . Each period the retailer orders
, which may be negative. In Lean the process is the structure
AR1Demand, whose fields are the parameters, the errors, the demands, the recursion, the
independence properties and the stationary law; muHat, err, sigmaHat, baseStock and
order are the five quantities above.
Order batching. retailers face independent demands in every period and
each orders once every periods, the order being its demand over the previous
periods. The supplier's order in a given period is the total ordered by the retailers whose
ordering day falls in that period. Three patterns are compared: random ordering, in which each
retailer's day is uniform over the days, so the number of retailers ordering on a given
day is binomial; positively correlated ordering, in which all retailers order on the
same day, so with probability and otherwise; and balanced ordering, in which
the retailers are spread as evenly as possible, so with , , is
with probability and otherwise. The structure BatchOrders P N R mu sigma carries the
demands, the ordering count independent of them, and supplierOrder, the sum of the last
demands of retailers ; each pattern enters a theorem as a hypothesis on the law of .
Rationing game. Two identical retailers face single-period demand with distribution function , holding cost and stockout penalty , so the newsvendor quantity satisfies . With probability the supplier can deliver only units in total and allocates them pro rata to the orders, retailer 1 receiving ; with probability supply is unlimited. Retailer 1's expected cost when the retailers order and is
with the newsvendor cost; this is rationingCost.
with equality when . This is bullwhip_signal_processing. The bound exceeds
whenever , whatever the value of : a lead time and a moving-average forecast are
enough to produce the effect.
The chapter's own route to the goal, each a milestone: the steady-state moments (13.2) to (13.4), , and ; the identity ; Lemma 13.1, for ; the vanishing of the cross term (13.12); and the variance of the demand part, .
Order batching, Theorem 13.4: under the three patterns the supplier's order has mean and
through the three variance formulas , and .
The rationing game, Theorem 13.3: if is a symmetric Nash equilibrium, that is, minimizes over positive order quantities when the other retailer orders , then .
The three theorems are the quantitative core of the chapter. Theorem 13.2 is the single-stage building block that Theorems 13.6 and 13.7 later iterate along a serial chain, giving the product-form and the exponential lower bounds on the amplification at stage ; its comparative statics, the bound decreasing in and increasing in , are the basis of the remedies the chapter recommends (shorter lead times, smoother forecasts, sharing point-of-sale data). Theorem 13.4 ranks the ordering patterns and justifies the advice to balance ordering days when batching cannot be avoided. Theorem 13.3 shows that pro-rata rationing alone inflates orders; the book is careful to note that inflated orders are not by themselves inflated variances, and that the variance statement for this model is due to Rong, Shen and Snyder (2017).
None of these results has a machine-checked proof. The book's proofs of Theorems 13.2 and 13.4 are complete but informal, and the proof of Lemma 13.1 is omitted with a citation to Ryan's 1997 thesis; formalizing it requires a self-contained argument. The variance decomposition of and the conditioning argument for Theorem 13.4 are reusable for the multistage results of Sect. 13.2.5, which are natural follow-up missions on the same definitions.
The obvious computation of expands the order into its demand part and its safety-stock part and hopes the cross term disappears. It does, but not for a reason visible in the formulas: is a square root of a sum of squares of forecast errors, a nonlinear function of demands, and its covariance with a single demand is zero only because the errors are jointly Gaussian with mean zero and is an even function of them, so the covariance is the expectation of an odd function of a centred Gaussian vector. That is Lemma 13.1, and the vanishing of the cross term needs two further covariances, and , which the book reduces to the lemma through the recursion (the second reduction divides by ) but which hold for every by the same symmetry. A solver must set up the joint Gaussian structure of the demand vector and prove the odd-function argument; nothing in Mathlib does this directly.
The second obstacle is that the moments (13.2) to (13.4) are not assumed but derived: the structure carries the stationary law of each and the independence of from the past, and the autocovariance has to be obtained from the recursion by induction on the lag, with integrability supplied by the Gaussian laws.
For Theorem 13.4 the work is the conditioning on : given the supplier's order is a sum of independent normals, so its conditional mean is and conditional variance , and the total variance is . The order is defined by a sum over retailers , so the independence of from the demands has to be used through the indicator structure rather than through a conditional-expectation library result.
For Theorem 13.3 the argument is a first-order condition. It requires that the newsvendor cost be differentiable with derivative , which holds when is continuous, and that the symmetric equilibrium be an interior minimizer, which is why and the minimization over are hypotheses.
Time is indexed by so that exists for every . AR1Demand asserts the
recursion for every outcome, the independence of the whole error family, the independence of
from , and the stationary law of every ; these are the
"steady-state" assumptions the book makes in words. The structure is satisfiable: the stationary
Gaussian AR(1) process on a full-measure set of error sequences has all these properties. The
constant is a free real parameter ; no theorem depends on its value.
The goal divides by , which is under the structure's
hypotheses and , so the ratio is a genuine quotient. Mathlib's
ProbabilityTheory.variance and covariance are used; both are the ordinary real quantities
for square-integrable variables, which every variable here is, included.
In BatchOrders the demands are indexed by Fin N × Fin R, the count is a natural-valued
random variable bounded by and independent of the demand family, and supplierOrder sums the
demands of retailers , the book's "without loss of generality" choice. The laws
of are hypotheses on point probabilities P.real {ω | X ω = j}; with each of the
three families of hypotheses is satisfiable by a structure with the corresponding law. The
subtractions and are real.
In the rationing game the demand law is a probability measure on whose distribution function is continuous and strictly increasing on ; the newsvendor loss is assumed integrable at every order quantity. The pro-rata allocation uses Lean's total division, which is never at in the theorem since .
Beyond the ten milestones, the multistage Theorems 13.6 and 13.7 and the centralized-information
bound of Theorem 13.5 are welcome as extensions on the same AR1Demand.
When a system is controlled indefinitely and decisions are frequent — a router admitting packets, a queue accepting jobs, a machine being maintained — discounting future rewards is often unjustified, and what matters is the long-run average reward per period. Puterman's Chapter 8 (doi:10.1002/9780470316887) develops the theory of this criterion, and its central object is a single equation, the average reward optimality equation , whose unknowns are a scalar gain and a bias function . For unichain models, in which every stationary policy generates a Markov chain with one recurrent class, this equation determines the optimal gain and an optimal stationary policy. The results go back to Howard (Dynamic Programming and Markov Processes, MIT Press, 1960) for the recurrent case and to Blackwell (Discrete dynamic programming, Annals of Mathematical Statistics 33, 1962, doi:10.1214/aoms/1177704593) and Derman for the general finite case; Puterman's Section 8.4 proves them through the discounted theory of mission II, by letting the discount factor tend to one.
The model is stationary (Assumption 8.0.1): a finite set of states, for each a finite nonempty set of actions, a reward and transition probabilities , none depending on the decision epoch. A policy may randomize and may depend on the whole history; the deterministic stationary policy applies the decision rule at every epoch. Its transition matrix is .
For a policy , is the expected reward over epochs. Since the limit of need not exist (Example 8.1.1), the chapter works with the lim sup and lim inf average rewards and , and with . A policy is average optimal when for all and , the strongest of the three criteria of Section 8.1.2.
The optimality residual is , and the optimality equation is . A decision rule is -improving when it attains at every state. A transition matrix is unichain when it consists of a single recurrent class plus a possibly empty set of transient states, and the MDP is unichain when is unichain for every deterministic decision rule.
For a finite unichain model: (a) some deterministic stationary policy is average optimal; (b) the optimality equation has a solution, and (d) its scalar satisfies for every ; (c) for every solution, every -improving decision rule gives an average optimal stationary policy.
If then ; if then ; if then .
In a finite unichain model has a solution, and every solution has the same .
If and is -improving, then is average optimal.
Theorem 8.4.1(c) is what the source calls "one of the most important results for average reward models": a solution of the optimality equation with constant pins down the optimal gain under every criterion at once, so that in finite unichain models the three optimality criteria of Section 8.1.2 coincide. Theorem 8.4.3 guarantees such a solution exists, and Theorem 8.4.4 reads an optimal policy off it. Together, Theorem 8.4.5 reduces the infinite-horizon average reward problem over all history-dependent randomized policies to a finite system of equations in , which is what policy iteration, value iteration and linear programming solve in Sections 8.5 to 8.8.
The results are classical and proved. Formalizing them fixes the chain-structure hypothesis in
a checkable form and pins down which criterion "average optimal" means, two places where the
literature is loose. The platform's MarkovDecisionProcesses series has the finite-horizon
(mission I) and discounted (mission II) models; this mission adds the undiscounted stationary
model, the gains, and the unichain classification, on which Chapter 9's multichain optimality
equations and Chapter 10's sensitive discount optimality can be built.
The obvious argument for Theorem 8.4.3 is to take the discounted optimal value of mission II and let . It fails as stated because blows up like ; what converges is the Laurent expansion of the value of a fixed stationary policy, Corollary 8.2.4, and that expansion needs the limiting matrix and the deviation matrix of a unichain chain. So the proof must first develop the Markov chain theory of Section 8.2 and Appendix A, choose a subsequence of discount factors along which one policy is discount optimal (possible because is finite), and only then pass to the limit in the discounted optimality equation.
Theorem 8.4.1 looks elementary and hides the analytic step: iterating along an arbitrary history-dependent policy and dividing by requires the telescoping term to vanish, which uses boundedness of , and requires the reduction from history-dependent randomized to Markov randomized policies (Theorem 8.1.2). For Theorem 8.4.4 the step is Corollary 8.2.7, that forces the gain of to be , which is the multiplication by that annihilates .
The traps are in the definitions. Recurrence and the unichain property must be stated so that the source's Example 8.4.3 comes out as the book says — the policy using has the absorbing state as its single recurrent class — and the optimality residual must use the lim sup / lim inf gains, since a definition through a limit that need not exist would be a junk value on the policies of Example 8.1.1.
State and action spaces are Fintypes and admissible actions are nonempty Finsets, as in
missions I and II; the stationary model is a new structure because mission II's DiscountedMDP
bundles a discount factor, and carries the same data otherwise. Policies are history-dependent
and randomized, so "average optimal" has its full strength; a stationary policy is the
deterministic one built from a decision rule. Expected total reward is defined by the policy
evaluation recursion, as in the earlier missions, rather than through a measure on
trajectories.
Gains are Filter.limsup and Filter.liminf of on ; these are
the source's because the sequence is bounded by , and the suprema over the
nonempty family of policies are genuine real suprema for the same reason. The residual
is a Finset.sup' over the admissible actions. Recurrence is "every state reachable from
reaches " and unichain is "any two recurrent states communicate", the definitions of Appendix
A for finite chains, applied to for every admissible deterministic decision rule.
Restrictions relative to the printed text, all noted in the items: Theorem 8.4.1 is stated for finite where the source says countable, since the chapter's standing assumption and the model are finite; the gain of a stationary policy in (8.4.5) is written as its lim inf gain, which equals it; and the chain of (8.4.6) is stated through and , since presupposes existing limits. Nothing is trivialized: the existential in Theorem 8.4.5(a) has to produce a decision rule, and with a junk maximum is impossible since every is nonempty. Welcome contributions beyond the milestones: Theorem 8.1.2 (reduction to Markov policies), Corollary 8.2.7 (the gain of a stationary policy from the evaluation equations), and the equivalence of the three optimality criteria in finite models.