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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
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?
Gibbons and Hawking conjectured that the cosmological horizon of a de Sitter static patch carries an entropy, computed semiclassically by the Euclidean gravitational path integral on the sphere. For three-dimensional de Sitter gravity the relevant quantity is , whose leading term is the Gibbons–Hawking entropy . A microscopic account of this entropy — a count of states in some ordinary quantum or statistical system — is one of the long-standing goals of de Sitter holography.
Collier, Eberhardt and Mühlmann (arXiv:2501.01486) propose that pure dS quantum gravity is dual to the double-scaled two-matrix integral of the complex Liouville string (arXiv:2409.17246). In §4.4 they test this by counting the "effective number of eigenvalues" of the matrix model and comparing with . The comparison reduces to explicit identities between elementary functions of the Liouville parameter ; this mission formalizes exactly those identities.
Fix a complex number with , i.e. with (the paper's footnote 2; then the central charge lies in ). Write and let be the genus-counting parameter of the matrix model.
For any function whose modulus equals for a fixed constant (the content of (4.5)), there is a real constant , independent of and , such that
This is the paper's statement that the matrix-model count reproduces the de Sitter entropy "regardless of the specific value of ", up to the order-one constants that (4.37) later fixes.
The identity (4.36) is the step the authors single out as "a genuinely nontrivial check": it holds for the complex Liouville string but, as they note, not for the Virasoro minimal string. The goal packages the argument of §4.4 into one exact statement, valid for every admissible (i.e. exactly in ), under the single physical input (4.5). The physical assumptions — the choice of cutoff at the first zero, the interpretation of as an entropy, and (4.5) itself — are not formalized; they enter as definitions and as the hypothesis on . The mathematical content is a definite-integral evaluation plus trigonometric/hyperbolic identities for complex arguments.
The integral in (4.32) has a complex-looking integrand, a branch of , and an upper limit given by a complex cosine; one must first show that everything is real in the admissible regime and then evaluate the integral exactly, including the endpoint behaviour at where is not differentiable. The entropy statements additionally involve the complex principal logarithm, so one must control the argument (positivity) of and of the tension ratio; identities such as fail for general complex .
Real.arcosh (defined as ); its values for never enter.Complex.log), and is complex-valued; the goal forces it to equal a real number.Heisenberg's uncertainty principle is the first quantitative statement a student meets about the incompatibility of position and momentum measurements in quantum mechanics. In A. O. Lopes' textbook Uma Breve Introdução à Matemática da Mecânica Quântica (31º Colóquio Brasileiro de Matemática, IMPA, 2017), written for mathematics students with no physics background, it is the capstone of Chapter 8 (Princípio da Incerteza e o Pacote de Onda Gaussiano), Teorema 8.2, p. 131. It collects the operator formalism built in Chapters 1, 3 and 4 — position and momentum operators, commutators, expected values — into one inequality. This mission is the first of a series formalizing the capstone results of the book.
A wave function is a map . The book uses the inner product (linear in the first slot) and the norm . A state is a wave function with . Fix , an index and the (reduced) Planck constant .
For every state ,
The inequality is the prototype of all Robertson-type uncertainty relations and is the point where the commutator formalism of the book produces a numerical, physically testable consequence. Milestone 5 shows the constant cannot be improved. The mathematics is classical and fully proved in the source; what this mission adds is a machine-checked version of the textbook's operator calculus on — integration by parts for compactly supported functions, symmetry of and , commutation relations, and explicit Gaussian integrals — reusable by later missions of the series (Ehrenfest's theorem, density operators, quantum statistical mechanics).
The algebraic core is a short Cauchy–Schwarz argument, but it silently uses facts about unbounded operators: that may be rewritten as requires integration by parts with vanishing boundary terms, and the reduction to mean-zero observables requires the expected values to be real. Each of these needs integrability bookkeeping that the book leaves implicit. The Gaussian milestone requires evaluating first and second moments of Gaussian integrals in dimensions.
EuclideanSpace ℝ (Fin n) with Lebesgue measure; wave functions are plain functions ℝⁿ → ℂ (not classes), operators are maps on such functions, and domains are imposed as explicit hypotheses (InPositionDomain, InMomentumDomain).Contributions welcome: integration-by-parts lemmas on for compactly supported functions, Gaussian moment computations, and an abstract Robertson inequality.
Ramsey's theorem says that every red/blue colouring of the pairs of an infinite set has an infinite monochromatic subset. For well-ordered sets one can ask for more: the monochromatic set should have the same order type as the whole set. Erdős and Rado introduced the partition relation to measure exactly this, and asked which countable ordinals satisfy — every colouring either has a red copy of the whole order or a blue triangle. Such ordinals are called partition ordinals. Every partition ordinal is a power of , so the question becomes: for which countable is a partition ordinal? This is Erdős Problem 592.
The question is a basic test case for ordinal Ramsey theory: it is the smallest nontrivial "unbalanced" relation (a whole order type against a finite clique), and progress on it has repeatedly required new combinatorial methods.
Timeline (as recorded on erdosproblems.com/592):
The case where is a sum of exactly three indecomposable ordinals appears to be the remaining open case.
An ordinal is identified with a well-ordered set of order type . A red/blue colouring of the complete graph on assigns to every pair of distinct vertices exactly one of two colours; equivalently, it is a pair of complementary simple graphs (red, blue) on .
For ordinals and a cardinal , the partition relation holds when every red/blue colouring of has
The Lean predicate is Erdos592.OrdinalCardinalRamsey α β c, following the encoding used by the Formal Conjectures project. A partition ordinal is an with .
An ordinal is additively indecomposable if it is nonzero and for all ; the additively indecomposable ordinals are exactly the powers . An ordinal is the sum of indecomposable ordinals when
i.e. its Cantor normal form has terms counted with multiplicity. The Lean predicate is Erdos592.IsSumOfIndecomposables k γ.
This is the positive answer in the open case, as predicted by the Galvin–Larson conjecture. Because the truth is unknown, a formal disproof (exhibiting a countable with three Cantor-normal-form terms for which the relation fails) is an equally valid resolution of the goal. Together with the milestones below, a proof of the goal gives a complete answer to Problem 592: for countable , is a partition ordinal iff or with a sum of at most three indecomposables.
The result itself. A resolution of the three-term case would, together with the results above, finish the classification of countable partition ordinals of the form asked for in Problem 592. Either answer is informative: a positive answer shows the threshold between the positive and negative cases lies between three and four terms, and a negative answer shows it lies between two and three.
Formalizing it. The drafter is not aware of any of the milestone results in Mathlib. The Formal Conjectures entry for Problem 590 links an external Lean formalization of Chang's theorem; the other results (Specker's positive and negative theorems, Galvin–Larson, Schipperus) have, to the best of the drafter's knowledge, no public machine-checked proofs. Formalizing them is a substantial project on its own, independent of the open case, and the goal itself is an open research problem.
The property is not monotone in : it holds for , fails for every finite , holds again for , and, by Schipperus, both holds and fails for various larger depending on the number of terms in the Cantor normal form of . So no induction on can settle the question, and a naive transfer of the argument for a smaller exponent to a larger one can fail. The known positive and negative results use different arguments, and the three-term case lies exactly on the boundary between the ranges they cover.
Ordinal.{u} and Cardinal.{u} in an arbitrary universe u; "countable" is γ.card ≤ ℵ₀.α.ToType, the canonical well-ordered type of order type α; a colouring is a pair of complementary SimpleGraphs (IsCompl red blue). A red is a red clique s with typeLT s = β; a blue is a blue clique of cardinality exactly 3.IsSumOfIndecomposables k γ requires a non-increasing list of exponents of length exactly k; without the ordering requirement, "sum of " would not be well defined, since for instance .ω ^ ω ^ γ means .The goal is not trivially satisfiable: the hypotheses hold, for example, for and , and the conclusion is a genuine partition relation on an infinite ordinal.
Useful reusable infrastructure includes Cantor-normal-form combinatorics for countable ordinals, order-type calculations for subsets of , and a library of the classical colourings (Specker-type constructions). Contributions formalizing any milestone are welcome.
This mission formalizes §5 of J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, doi:10.5169/seals-87877: the definition of Thompson's group and Thompson's proof that is simple.
Thompson's groups and , introduced in unpublished notes of Richard Thompson in 1965, were the first known examples of infinite, finitely presented, simple groups. Every finitely presented simple group known before them was finite. The notes of Cannon, Floyd and Parry were written in part "to make available Thompson's unpublished proofs … of the simplicity of and " (p. 216), and §5 is that proof for .
is the circle's counterpart of Thompson's group . Earlier missions on this platform formalize and its commutator subgroup (§1 and §4 of the same notes), its tree-diagram normal form (§2), and its two presentations (§3). is not simple: its abelianization is . is simple, it has elements of finite order (the generator below has order ), and it contains as the stabilizer of a point.
The circle is with its endpoints identified, in Lean UnitAddCircle (); denotes the image of . Maps compose right to left, , and , the convention of the notes.
The group (pp. 233–234) consists of the piecewise linear homeomorphisms of that map images of dyadic rationals to images of dyadic rationals, are differentiable except at finitely many images of dyadic rationals, and have slopes that are powers of . In Lean a permutation of the circle satisfies IsThompsonCircle f when it has a lift to the line: an order isomorphism of with and , mapping dyadic rationals to dyadic rationals, and affine with slope a power of between consecutive integer translates of finitely many dyadic breakpoints. T is the subgroup generated by these maps. That they already form a group is the first milestone.
The elements , , (Example 5.1). and are the generators of from the §1 mission (mapA, mapB), carried to the circle by toCircle, which sends an order isomorphism of to . (mapC) is given on by , and on , and . symT sends the formal symbols , , to these three maps.
The presented group (p. 236) is the free group on formal symbols , , modulo six relators:
In , and (XT1); and (CT1) for . An element is positive (IsPositiveT1) when it is a product of nonnegative powers of the .
The goal is the sentence in which the notes state what §5 does, "In §5 we define and give Thompson's proof that is simple" (p. 216):
The route is the section's own. Lemma 5.2 shows that , , generate and satisfy the six relations, so maps onto (Lemma 5.3). Lemmas 5.4–5.6 and a normal form (Theorem 5.7, every is with , positive and ) lead to Theorem 5.8, is simple, and hence to Corollary 5.9, . The goal follows.
The result. The simplicity of is one of the two facts that made Thompson's groups famous: is an infinite, finitely presented, simple group. Corollary 5.9 gives more, an explicit presentation of on three generators and six relators.
Formalizing it. No machine-checked proof that is simple exists on this platform, and Mathlib has nothing on Thompson's groups. The proof in the notes is short and complete. This mission connects the analytic definition of with the combinatorial group , reusing the platform's formalization of : the presentation of (Theorem 3.4), its normal form (Corollary 2.7), and the fact that its proper quotients are Abelian (Theorem 4.3).
The algebra of (Lemmas 5.5 and 5.6) is a chain of explicit inductions. The substance lies at two points.
The first is Theorem 5.7. The notes' proof that the set of elements is closed under multiplication moves past and using the normal form of , transported into through Lemma 5.4, and then re-indexes, all inside the abstract group with no geometry to lean on.
The second is the analytic side of Lemma 5.2. Generation reduces an arbitrary to an element of by composing with and with an element of that moves to . That needs the fact that an element of fixing comes from , which the notes state in one line. The relations are identities between explicit piecewise linear maps of the circle.
Subgroup (Equiv.Perm UnitAddCircle) generated by IsThompsonCircle. The lift makes every element an orientation-preserving homeomorphism, so continuity is not stated separately. Unlike for , the condition that dyadics map to dyadics cannot be dropped: an irrational rotation satisfies every other clause.PresentedGroup on the three-element type FormalABC. Relators are written out as , not with commutator notation.General relativity is summed up, in S. M. Carroll's A No-Nonsense Introduction to General Relativity (2001), by two statements: spacetime is a curved pseudo-Riemannian manifold with a metric of signature , and the metric obeys Einstein's equation . The first exact solution of that equation, and still the most important one, is the Schwarzschild metric: it describes the gravitational field of the Sun outside its surface, the classical tests of GR (perihelion precession, light bending), and non-rotating black holes. Carroll's notes state its key property in one sentence: for a spherically symmetric metric, the vacuum equation has a unique solution, (72) — Birkhoff's theorem. This mission is the first of a series formalizing the capstone results of those notes.
We work in a single coordinate chart of four-dimensional spacetime. A point is ; a metric is a field of real symmetric matrices of signature , i.e. congruent to . From and its inverse one builds, exactly as in Carroll's equations:
In spherical coordinates the general spherically symmetric metric is (71)
and the Schwarzschild metric (72) is the case , .
The goal is the uniqueness statement of §6 of the notes, in the form: for smooth and positive on a rectangle with ,
The milestones follow the notes in order:
The result. Birkhoff's theorem says the exterior field of any spherically symmetric body — static, pulsating or collapsing — is the Schwarzschild field, determined by a single constant . It is why the Schwarzschild solution governs the solar system and spherical collapse, and why spherically symmetric gravitational radiation does not exist. The identities (37), (47)–(51) and (67)–(69) are the working toolkit of every GR computation; (51) is what makes Einstein's equation consistent with local energy–momentum conservation.
Formalizing it. All results here are classical and proved in the textbooks. The value of the mission is a machine-checked, coordinate-level development of the curvature identities in Carroll's exact conventions, and a checked proof of Birkhoff's theorem, which requires solving the vacuum equations as a system of PDEs rather than verifying a given solution. The platform already contains a separate Einstein-field-equations development (built from a Wikipedia-based definition file with a slightly different index placement) in which Ricci-flatness of the Schwarzschild metric is proved; this mission uses its own Carroll-faithful definitions, and that earlier work may help with milestone 12.
Verifying that a given metric is Ricci-flat (milestone 12) is a long but mechanical computation of derivatives of explicit functions. The goal is different in kind: in the "only if" direction one must extract from that (from ), integrate an ODE in to get with independent of , and then show depends on only — all with the coordinate derivatives of the formal definitions, inside a region where are only known to be smooth and positive. The general identities (47)–(51) need symmetry of second and third derivatives and the derivative of the matrix inverse.
Coord = Fin 4 → ℝ, a metric is a function Coord → Matrix (Fin 4) (Fin 4) ℝ, partial derivatives are Fréchet derivatives in coordinate directions. All functions are total: non-differentiable points give derivative , singular matrices have inverse , and . For that reason every statement names the open region (smoothness, signature , , , ) on which it is claimed.CarrollGR_Defs (Christoffel symbols, covariant derivatives, curvature, Einstein tensor in coordinates) is shared by the whole series. Contributions welcome: general lemmas about partialD of products, quotients and matrix inverses, and a tensoriality lemma for the Ricci tensor under changes of coordinates.The bosonic string can be quantized consistently only in spacetime dimensions. In lightcone quantization this appears in two ways in David Tong's Cambridge Part III lecture notes. First (Sections 2.2.2–2.3), the normal-ordering constant in the mass formula is identified with a regularized Casimir energy , using "" ; Lorentz invariance then forces the first excited states to be massless, which happens only for . Second (Section 2.4), the commutator of lightcone Lorentz generators, which must vanish for the quantum theory to be Lorentz invariant, is proportional to a coefficient that vanishes for all oscillator levels exactly when and (Goddard–Goldstone–Rebbi–Thorn 1973).
Let be the number of spacetime dimensions, so there are transverse oscillator directions, and let be the Regge slope. In lightcone gauge the mass of a closed-string state at level is (2.25)
with an undetermined normal-ordering constant . The heuristic evaluation of replaces the divergent zero-point sum by its cut-off regularization , or by the Riemann zeta function value , giving (2.26). The first excited states (2.28) are in number and have . In one sector the level-2 states are (unordered pairs , since the oscillators commute) and . Finally, Section 2.4 states that
For and ,
The result. The critical dimension is the single most-quoted prediction of the bosonic string, and the pair fixes the entire lightcone spectrum: the tachyon , the massless graviton, -field and dilaton, and the massive tower .
Formalizing it. This mission formalizes the mathematical steps of Tong's lightcone derivation: the two regularizations of , the mass-shell and state-counting arithmetic, and the final algebraic step of the Lorentz-algebra argument. It does not formalize the operator computation of in the lightcone Fock space, which Tong quotes ("After a tedious computation, one finds ...") without derivation; that computation is a natural follow-up mission. The value is already available in Mathlib through the Bernoulli-number formula for at negative integers.
The individual statements are elementary once formalized; the difficulty is faithfulness rather than proof. The regularized sum is an asymptotic statement whose leading term diverges, so it has to be stated as an remainder along rather than as an equation; and the goal is a statement for all levels , where a single level () only forces and two levels are needed to force .
The dimension is a natural number and the normal-ordering constant a real number. The regularized sum is Mathlib's tsum of over (the term vanishes), and the asymptotic claim uses Mathlib's big-O along the right neighbourhood filter of . Level-2 states of one sector are counted as unordered pairs with repetition of transverse indices (Mathlib's Sym2 (Fin (D-2))) plus the states ; natural-number subtraction and division are safe because is assumed and is even. The zeta function is Mathlib's riemannZeta, i.e. the analytic continuation.
In 1973 Bardeen, Carter and Hawking showed that stationary black holes in general relativity obey four laws with the same structure as the laws of thermodynamics, with the surface gravity of the horizon playing the role of temperature and the horizon area the role of entropy (Bardeen–Carter–Hawking 1973). Two years later Hawking showed that quantum fields near a black hole produce thermal radiation at temperature (Hawking 1975), which turned the analogy into an identification, with entropy .
The M.Sc. dissertation Termodinâmica de Buracos Negros (F. H. de C. Menezes, UFMG, 2021) presents this construction for the Kerr black hole, the rotating stationary solution of Einstein's vacuum equations. The first law, eq. (3.79), is its central quantitative statement:
relating first-order changes of mass , horizon area and angular momentum between neighbouring Kerr black holes, where is the angular velocity of the horizon.
Timeline: Kerr found the rotating solution (1963); Smarr derived the mass formula (1973); Bardeen, Carter and Hawking stated the four laws (1973); Hawking derived the thermal emission (1974–75).
Units are geometrized, (and for quantum quantities). A Kerr black hole has mass and rotation parameter with ; its angular momentum is . In Boyer–Lindquist coordinates the metric involves
with angular components and . The zeros of are ; the event horizon is .
A Kerr black hole is non-extremal when , equivalently .
Regard as functions of with . For and , the area is differentiable at and, as linear forms in ,
In the dissertation the first law is the sum of the variation (3.45) of the Smarr formula and the relation (3.78).
The first law is the identity behind the identification , : with these values it becomes , the ordinary first law of thermodynamics for a rotating body. The Smarr formula is its integrated (Euler-relation) form, and the vanishing of at extremality underlies the dissertation's formulation of the third law.
All results are classical and proved in the literature. The contribution of the mission is a machine-checked version of the explicit Kerr relations, with the horizon area computed from the metric rather than taken as given, and a check of the dissertation's formulas. One such check is already recorded: the coefficient printed in eq. (3.78) conflicts with the dissertation's own eqs. (3.70) and (3.77), which give , the value required for (3.79); the milestone uses .
The dissertation derives the first law geometrically, from Komar integrals and a perturbation of the horizon Killing field. That route needs Lorentzian geometry, Killing horizons and Stokes' theorem on manifolds, which the Lean library does not provide. The explicit route through the Kerr formulas avoids this, but has its own obstacles: the horizon area is a double integral of a square root of a rational trigonometric expression that simplifies only on the horizon, where ; and the differentials involve , which is not differentiable at extremality, so the non-extremal hypothesis must be used when differentiating.
All quantities are real-valued functions of real arguments, defined in one definition file in the namespace KerrBlackHoleThermo. Every theorem restricts to the physical range explicitly ( and , or and for statements involving derivatives), so Lean's conventions for of negative numbers and division by zero do not enter the physical content. First-order variations "between two neighbouring Kerr configurations" are formalized as Fréchet derivatives (HasFDerivAt) of the explicit family in the coordinates ; the first law is an identity of linear forms on . The horizon area is defined as a metric integral, not as the closed form (3.44), so the goal cannot be reduced to a pure algebraic identity by definition.
Out of scope: the general-spacetime versions of the zeroth, second (area theorem) and third laws, which need a theory of Lorentzian manifolds, event horizons and energy conditions, and the quantum field theory derivation of Hawking radiation in Chapter 4. Contributions building that infrastructure are welcome as separate missions.
For a field , two invariants built from very different data turn out to carry the same mod-2 information. One is Milnor K-theory , defined by generators and relations from the multiplicative group alone. The other is Galois cohomology , the continuous cohomology of the absolute Galois group of . In 1970 Milnor considered a natural map in all degrees, verified that it is an isomorphism for several classes of fields, and remarked that he knew of no field where it fails (Milnor 1970). The statement that it is always an isomorphism when became known as the Milnor conjecture. Its companion conjecture on quadratic forms was later deduced from it (Orlov–Vishik–Voevodsky 2007). Together they identify the graded Witt ring of quadratic forms, Galois cohomology mod 2, and .
Timeline. The attributions below follow the introduction of Voevodsky 2003.
Let be a field with in .
Milnor K-theory. For , is the quotient of the -fold tensor power , taken over with written additively, by the subgroup generated by the pure tensors in which some adjacent pair satisfies . This is the degree- part of , where is the two-sided ideal generated by . The class of is the symbol . In particular and . In Lean these are MilnorK F n and symbol a for a : Fin n → Fˣ.
Galois cohomology. Let be a separable closure and the absolute Galois group, a profinite group under the Krull topology. is the continuous cohomology with trivial action, computed from -invariant continuous homogeneous cochains. In Lean this is H F n, Mathlib's continuousCohomology n of the trivial representation.
The Galois symbol. For fix . The Kummer character is if and otherwise. It is a continuous homomorphism representing the Kummer class . The Galois symbol of is the class of the homogeneous cocycle
the homogeneous form of , i.e. the cup product . In Lean this is galoisSymbol a.
For every field with and every there is a homomorphism
which is surjective and whose kernel is exactly .
Since symbols generate , such a is unique; it is the norm residue homomorphism. The statement is therefore equivalent to via the norm residue map. Its existence, i.e. the fact that the Steinberg relations map to zero, is part of the claim.
The result itself. The theorem gives a presentation of mod-2 Galois cohomology by generators and relations: every class is a sum of cup products of degree-one classes, and every relation among such products comes from Steinberg relations and multiples of 2. With Orlov–Vishik–Voevodsky 2007 it yields Milnor's conjecture on quadratic forms, which classifies quadratic forms up to Witt equivalence by their Galois-cohomological invariants.
Formalizing it. The theorem is proved but not formalized. At the time of writing, Mathlib has neither Milnor K-theory nor cup products in group or continuous cohomology, and has Hilbert 90 only for finite Galois extensions. This mission's definitions provide a sorry-free Galois symbol in Mathlib's continuous cohomology, which already makes the degree 0 and degree 1 cases (Kummer theory) meaningful targets. A complete development would formalize the IHES proof, including motivic cohomology with coefficients and the motivic Steenrod algebra. No part of that is currently available in Lean. Related existing work: on this platform, a graded cup product (groupCohomology.exists_isGradedCupProduct) and a Kummer theory and Hilbert 90 for level-constant cocycles have been formalized on top of Mathlib's discrete groupCohomology. The cup product is for discrete groups, and the Kummer and Hilbert 90 results use finite-level hypotheses in place of continuity, so none of them transfers directly to continuousCohomology.
Degrees 0 and 1 follow from Kummer theory and Hilbert 90. Degree 2 is Merkurjev's theorem, whose proof goes through the K-theory of Severi–Brauer varieties. No argument internal to Galois cohomology or K-theory of fields is known in higher degrees. The known proof reformulates the statement as a vanishing theorem for motivic cohomology of fields, the "Hilbert 90" property for weight . It then argues by induction on through geometry over : splitting varieties of symbols (Pfister quadrics), their motives, and cohomology operations on motivic cohomology. Each of these is a substantial theory, none of it exists in Mathlib, and the induction passes through statements about arbitrary smooth varieties, not only fields.
Scope. The target is the Milnor conjecture, i.e. the prime with coefficients . The Bloch–Kato conjecture for odd primes is out of scope.
Conventions.
F : Type, universe 0. Mathlib's continuousCohomology requires the coefficient module to live in the universe of the group. For in a higher universe this forces ULift (ZMod 2), for which the needed Module and ContinuousSMul instances are not available as global instances. Universe polymorphism is not part of this mission. It does not follow by plain transport, since a field in a higher universe need not be isomorphic to any field in Type; one route is a limit argument, using that both sides commute with directed unions of fields and that every field is the directed union of its countable subfields, each isomorphic to a field in Type.[NeZero (2 : F)].continuousCohomology, built from homogeneous cochains, with as a trivial representation of with the Krull topology.Ruling out trivializations. The Galois symbol is not a free parameter. It is a fixed, sorry-free definition, and the existence of with the prescribed values on symbols is part of the goal. Neither can be chosen to make the statement vacuous.
Route. Reductions should follow Voevodsky 2003 together with Voevodsky 2003b. That route avoids resolution of singularities and works in every characteristic . The following rely on resolution of singularities (or on characteristic-0 reductions) and should not be used as inputs:
Infrastructure needed and reusable. A complete development needs:
Most of this is reusable well beyond the mission. The homogeneous-cochain construction in the definition files, which turns an invariant continuous cocycle into a class in Mathlib's continuousCohomology, applies to any locally compact group with trivial coefficients. Contributions of any of these components, and of the degree 0 and 1 cases, are welcome.
Send a uniformly random string through a memoryless binary symmetric channel with crossover probability : each coordinate is flipped independently with probability , producing . An observer sees and wants to learn about — but the summary of they are allowed to keep is a single bit , computed by a Boolean function chosen in advance. Which choice of makes that one bit most informative about the noisy observation, in Shannon's sense?
The natural candidate is a dictator, : keep one coordinate and forget the rest. It achieves , where is the binary entropy function in bits. Majority, parity, and every other symmetric or balanced construction does worse. Courtade and Kumar conjectured in 2014 that nothing does better: no Boolean function of noisy-channel inputs, however many coordinates it reads and however it combines them, beats a single coordinate.
Fix , a crossover probability , and a Boolean function . With uniform on the cube and its image under the channel, all the relevant quantities are finite sums: the joint mass of is
and mutual information is , all entropies in bits. No measure theory is required, and the endpoints are included by the conventions and .
The goal quantifies over every dimension, including , every Boolean function — balanced or not, monotone or not — and every crossover probability including the three endpoints. Nothing is assumed about : no balance condition, no bound on the number of influential coordinates, no restriction to a range of . The bound is tight, attained by any dictator, so the statement is exactly the assertion that dictators are the most informative Boolean functions.
The inequality is the sharp, one-bit case of a general question in information theory: how much can a lossy summary of a source tell you about a noisy observation of that source? It is the Boolean-function analogue of a hypercontractivity or "small-set expansion" statement — quantities of the form under a noise operator are precisely what appear in the analysis of Boolean functions, in hardness-of-approximation reductions built on noise stability, and in distributed source-coding and common-information problems, where the bound limits what a single bit of a compressed description can carry. Special cases were known and repeatedly used: balanced functions, functions of few coordinates, and asymptotic or high-noise regimes. The general statement resisted those methods, because the extremal structure is a single coordinate while the space of competitors grows doubly exponentially in .
Mutual information is neither convex nor concave in , and the obvious relaxations are false: the corresponding bound for real-valued or non-Boolean summaries fails, so any argument must use Booleanness. Fourier-analytic approaches control noise stability but lose the constant needed for tightness, and the tightness is the whole content — the inequality is an equality for dictators, leaving no slack to absorb approximation. Induction on requires a statement strong enough to survive restriction, and the known strengthenings become false at the endpoints. The regimes also split: near the problem becomes a perturbative curvature computation around the dictator, while for moderate the extremal analysis is a global optimization over a two-parameter family, and the two arguments meet only if their boundaries are matched exactly.
The goal is stated with the entropy and mutual-information definitions of this mission's definition module: binary entropy via Mathlib's Real.binEntropy divided by (so entropies are in bits), the channel as an explicit product kernel, and the joint and marginal masses as explicit finite sums over the cube. The proposition is a single closed statement — no hypotheses beyond — so a solution must establish it for all dimensions uniformly.
A complete machine-checked proof of this statement exists in Lean 4 (Chen–Gohari–Javanmard–Lin–Mirrokni–Nair–Woodruff, 2026): axioms propext, Classical.choice, Quot.sound, no sorry and no native_decide, but 45,500 modules and roughly 50 million lines, most of it kernel-checked numerical certificate data. It is therefore not submittable as a single solution, and the mission's supporting structure — the manuscript route's regional statements and its leaf certificate families — will be added as separate theorems as they are transplanted onto the platform.
Since 20 May 2019 the International System of Units (SI) is no longer defined through material artefacts or particular experiments. Instead, the 26th General Conference on Weights and Measures fixed the exact numerical values of seven defining constants and declared that the SI is the system of units in which these constants take these values. The reference text is the BIPM's SI Brochure, 9th edition (2019), bipm.org. Every calibration certificate, every value in the CODATA tables and every textbook formula expressed in SI units rests on this definition.
The mathematical content of the new definition is small but exact: from the seven fixed values, the Brochure derives, for each of the seven base units, an explicit formula expressing that unit as a rational multiple of a product of integer powers of the defining constants (Section 2.3.1), and it asserts that any SI unit can be written through products and quotients of the defining constants (Section 2.2). These are statements about a free abelian group of unit monomials together with exact rational coefficients, so they can be checked completely.
Timeline. 1960: the 11th CGPM establishes the SI with six base units (the mole is added in 1971). 1983: the metre is redefined by fixing the speed of light . 2018–2019: the 26th CGPM (Resolution 1) redefines the kilogram, ampere, kelvin and mole by fixing , , and ; the new definitions enter into force on 20 May 2019 and are published in the 9th edition of the SI Brochure.
A quantity value is written as a number times a unit. In this mission a quantity value is a pair , written , where is the numerical value and
is a unit monomial in the seven base units second, metre, kilogram, ampere, kelvin, mole and candela (Table 2 of the Brochure). Products multiply numerical values and add exponents; quotients and integer powers are defined accordingly; a real number acts by . Two quantity values are equal exactly when they have the same numerical value and the same seven exponents.
The derived units needed in Section 2.2 are , , , , and . The seven defining constants (Section 2.2, Table 1) are
"The seven constants are chosen in such a way that any unit of the SI can be written either through a defining constant itself or through products or quotients of defining constants." Formally: for every exponent vector there are a real number and integers with
The seven exact expressions of the base units in terms of the defining constants, each in both forms displayed by the Brochure:
together with the rounded decimal values quoted for the five non-trivial numerical factors (, , , , ).
The result itself. The milestones are the operational content of the 2019 redefinition: they say how each base unit is recovered from the fixed constants, and together they show that the matrix of exponents of the seven defining constants with respect to the seven base units is invertible over , which is exactly what the goal asserts. Every derived unit is a monomial in base units, so the goal also covers the derived units.
Formalizing it. The platform already has purely numerical checks of these formulas (rational identities of the form "coefficient constant values "). This mission adds a model with units as first-class data: equalities are between quantity values, so a wrong exponent or a missing factor of is a type-level failure, not a silent numerical coincidence. The definition file is reusable for later missions in this series (derived units, Tables 4–8, prefixes).
The individual milestones are exact finite computations; the only care needed is bookkeeping of exponents and of large decimal constants. The goal requires choosing the integer exponents as functions of and showing that the unit monomials match componentwise — an argument that the exponent matrix is unimodular, not merely invertible over . Solving the system over the rationals is not enough.
Neutrino oscillations are an interference phenomenon, so they are sensitive to any mechanism that degrades quantum coherence during propagation. The open quantum system description models such effects without specifying their microscopic origin: the neutrino is treated as a subsystem whose reduced density matrix evolves under a Markovian master equation. The dissertation of G. F. S. Alves (Instituto de Física, Universidade de São Paulo, 2020) develops this framework for two and three neutrino generations and uses public IceCube atmospheric data to constrain the new parameters. Its two-generation chapter derives closed-form oscillation probabilities under several choices of the dissipative term; this mission formalizes that chapter's mathematical content.
A density matrix is a positive semidefinite complex matrix of unit trace. For a two-level system (two neutrino mass eigenstates) the reduced state obeys the Lindblad equation with constant coefficients,
where are the Pauli matrices and the Kossakowski matrix is Hermitian positive semidefinite (the condition for complete positivity). In the mass basis the vacuum Hamiltonian is , and the mixing matrix with Majorana phase is
The muon neutrino is produced in the state , and the survival probability after a baseline is . The linear entropy and the von Neumann entropy measure the loss of purity.
For the pure-decoherence Kossakowski matrix , , every solution with satisfies, for all ,
The goal is the formula used in the dissertation to show how decoherence damps oscillations: it reduces to the standard vacuum formula at , it tends to at large instead of oscillating, and it does not depend on . The milestones connect the formula to the structure of the Lindblad generator (energy conservation singles out this Dissipator) and to entropy growth. A formal development yields a checked two-level Lindblad toolkit (Pauli expansion of dissipators, explicit solutions, entropy bounds) reusable in other open-system missions. The results are proved informally in the source; none is known to be machine-checked.
The ODE part requires a uniqueness argument for a linear matrix ODE on given only one-sided derivatives at , plus exact trigonometric bookkeeping. The entropy milestones need spectral calculus for Hermitian matrices (Klein's inequality, concavity of ) and, for Appendix B.1, the monotonicity of relative entropy under completely positive trace-preserving maps together with complete positivity of Lindblad semigroups, neither of which is expected to be available off the shelf.
Matrices are Matrix (Fin 2) (Fin 2) ℂ; the Kossakowski matrix is Matrix (Fin 3) (Fin 3) ℂ with indices for the thesis' . Solutions are curves satisfying the Lindblad equation entrywise for (derivatives within ); the exponential is not used. Entropies use the continuous functional calculus. Two printed formulas are corrected in the drafts: the sign of the terms in eq. (3.5), and the overall sign of the off-diagonal entries in eq. (3.23); both corrections are explained in the corresponding items. The two-generation cases (4) and (5) survival probabilities, eqs. (3.25) and (3.27), and the three-generation and IceCube analyses are out of scope.
The Shape Zero model (Shape Zero LLC, unpublished) reaches the Fano plane — the seven-point, seven-line configuration behind the seven imaginary units of the octonions — by a combinatorial route (C1 Formal Proofs, §3). Points are arranged in Steiner triple systems, and each point of each line is given one of three roles. The model's claim is that the role postulates alone force the number of points to be exactly seven. This mission proves that claim.
What this mission does NOT prove.
Two corrections to C1 §3 built into this mission.
Fix a natural number and take the points . A Steiner triple system is a family of subsets, called lines, such that
A role colouring assigns to each point and line a role such that
In Lean these are RolesForceSeven.STS n and RolesForceSeven.RoleColouring S role, with points Fin n and lines Finset (Fin n).
This is RolesForceSeven.roles_force_seven. It asserts the point count only.
The result itself. It turns the model's role postulates into a precise count: whatever the Steiner triple system, if it carries a role colouring and has a point, it has exactly seven points. Corollary A shows the conditions are satisfiable, and Corollary B rules out the next Steiner triple system, AG(2, 3), explicitly.
Formalizing it. The C1 statement omits the non-emptiness hypothesis and is false for the empty system; the formal statement makes the hypothesis explicit and shows it is needed. The numerical check (Fano plane: role colourings; AG(2, 3): ; single triple: ) is replaced by a proof for every .
| system | points | lines through each point | role colourings |
|---|---|---|---|
| Fano plane | 7 | 3 | 48 |
| AG(2, 3) | 9 | 4 | 0 |
| single triple | 3 | 1 | 0 |
| empty system | 0 | — | vacuous (all conditions hold) |
Moderate. The central step is the replication count: the lines through a point must be shown to cover every other point exactly once, two at a time, which is a double-counting argument over the pairs through . The role postulates then fix the replication number at three. The Fano plane corollary is a finite check.
Fin n; lines are finite sets of points, with no ambient geometry assumed.Fin n → Finset (Fin n) → Fin 3; only its values on pairs with a line matter.The book has characterized learnability through uniform convergence and through stability; Chapter 30 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), gives a third sufficient condition, compression: if a learning algorithm's output can be reconstructed from a small subsequence of training examples, then the error on the remaining examples estimates the true error, and the algorithm generalizes with a bound of order (Theorem 30.2, Littlestone and Warmuth). The bound is a union bound over the possible index sequences of a held-out estimate that follows from Bernstein's inequality (Lemma 30.1), and in the consistent case it gives (Corollary 30.3). Classes admitting such compression schemes include axis-aligned rectangles (), homogeneous halfspaces (, through the minimal-norm point of the convex hull and Carathéodory's theorem), separating polynomials by reduction, and any margin-separable data (, through the Perceptron). Whether every class of finite VC dimension has a compression scheme of size is Warmuth's problem, open when the book was written.
A sample is drawn i.i.d. from ; a selection rule picks (repetitions allowed), a reconstruction map produces , and is the set of positions not selected, with the average loss over them. The loss takes values in . A class has a compression scheme of size (Definition 30.4) if for every there are such and with correct on every sample labeled by a member of ; the unrealizable version (Definition 30.5) asks to be an empirical risk minimizer on every sample.
For a -valued loss, , , any reconstruction map and any selection rule, with probability at least over ,
Lemma 30.1 (the held-out Bernstein bound); Corollary 30.3 (the consistent case); Lemma 30.6 (realizable schemes give unrealizable schemes); the compression scheme of size for axis-aligned rectangles (§30.2.1); the separation property of the minimal-norm point of the convex hull (§30.2.2). Further items: the size- scheme for homogeneous halfspaces and the margin scheme of §30.2.4.
Compression bounds are the cleanest generalization argument in the book: no complexity measure of the class enters, only the number of examples needed to encode the output, and the resulting bound is data-dependent through . They explain why support vector machines and the Perceptron generalize in terms of the number of support vectors or updates, and they underlie the sample-compression view of learning that connects to Chapters 9 and 15. Lemma 30.6 shows that compression is robust to label noise in the binary case. The halfspace scheme is a small piece of convex geometry of independent interest, and Warmuth's question about VC classes, settled in the affirmative for finite size by Moran and Yehudayoff after the book appeared, remains open in the form .
Lemma 30.1 is Bernstein's inequality for the held-out losses with variance at most , followed by solving the resulting quadratic in to move the risk from the right-hand side to ; the constant comes out of that step (the exact value is about ). Theorem 30.2 is a union bound over the index sequences with , using and , which needs ; formally the event for the learner is contained in the union of the events of Lemma 30.1 for each fixed index sequence, so no measurability of the selection rule is needed. Corollary 30.3 is immediate. Lemma 30.6 applies the realizable scheme to the subsample on which an ERM hypothesis is correct. The rectangle scheme is bookkeeping about extremal coordinates. The halfspace scheme needs three facts: the minimal-norm point of the hull separates (a one-line perturbation argument), it lies on a face and hence is a convex combination of sample points (Carathéodory's theorem, in Mathlib, applied to a face), and it is the minimal-norm point of the hull of those points (uniqueness of the projection onto a convex set); the existence of the minimizer uses compactness of the hull. The margin scheme is the Perceptron convergence theorem of Mission VI applied to the batch algorithm, whose output is the sum of the updated examples.
Samples are Fin m-indexed under Mission I's iidLaw, and probability statements bound the outer measure of the failure event. Lemma 30.1 splits a sample of size into its first and last entries; Theorem 30.2 takes an arbitrary selection rule and reconstruction map , the held-out set being the positions not in the range of the selection, and requires and in addition to the book's : for the bound reads , which fails, and the book's derivation uses in . Compression schemes are defined for every , since for there is no index to select, with indices allowed to repeat as in and with 's outputs in ; the unrealizable version uses Mission XXIII's multiclass 0–1 loss. The halfspace results are stated for strictly separable -labeled samples, , the book's "w.l.o.g. all labels positive" normalization; this avoids the boundary negatives that a realizable sample may contain under the convention of Mission VI, and it is the setting in which the minimal-norm argument works. The scheme is stated as the existence of indices whose signed examples have a minimal-norm hull point separating the whole sample, which is the content of and without fixing how ties among faces are broken. Rectangles are closed boxes. The margin scheme uses Theorem 9.1's normalization.
Not stated: §30.2.3 (polynomials, a reduction), the bibliographic remarks, and the intermediate Carathéodory step as a separate item.
Chapter 17 introduced multiclass prediction; Chapter 29 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), asks the two questions the fundamental theorem answered for binary classes: which classes of multiclass predictors are PAC learnable with respect to the 0–1 loss, and with what sample complexity. Natarajan's dimension generalizes the VC dimension by shattering with two disagreeing label functions, and the multiclass fundamental theorem (Theorem 29.3) bounds the uniform-convergence, agnostic and realizable sample complexities in terms of it, up to logarithmic factors in the number of labels ; the only new ingredient in its proof is Natarajan's lemma, the multiclass substitute for Sauer's lemma. The chapter then computes or bounds the Natarajan dimension of the classes that matter, One-versus-All and general reductions to binary classifiers, and linear multiclass predictors (Theorem 29.7). Its last section is a warning: unlike the binary case, not all ERMs are equal, and with infinitely many labels a class can be learnable by one ERM and not by another, so learnability and uniform convergence come apart (Claim 29.9).
is a class of functions from to a finite label set with . is shattered by if there are with everywhere on such that every is realized by some agreeing with on and with on (Definition 29.1); is the largest size of a shattered set (Definition 29.2). One-versus-All builds from binary classifiers, the smaller label on ties; a general reduction applies a rule to binary classifiers; the linear class predicts for a class-sensitive feature map (29.1). The class of §29.4 has labels , the finite and cofinite subsets of plus a special label, and hypotheses if and otherwise; returns on an all- sample and returns .
There are absolute constants such that every class with satisfies
the upper bounds by every ERM learner and the lower bounds for small and , in the format of Mission IV's Theorem 6.8.
Lemma 29.4 (Natarajan: ); Lemma 29.5 (the Natarajan dimension of One-versus-All is ); Theorem 29.7 (); Claim 29.9(1) ( needs examples); Claim 29.9(2) ( fails with constant probability on examples). Further items: the equality for two classes, and Lemma 29.6 for general reductions.
Theorem 29.3 is the multiclass fundamental theorem of Natarajan (1989) and Ben-David, Cesa-Bianchi, Haussler and Long (1995): finite Natarajan dimension characterizes multiclass learnability, and the sample complexity is linear in it, with the dependence on confined to logarithms. Natarajan's lemma is the combinatorial core, and the dimension bounds of §29.3 are what make the theorem usable: a One-versus-All scheme over a class of VC dimension costs , and a linear multiclass predictor costs at most its number of parameters, so the multivector construction of Chapter 17 is learnable with examples. Claim 29.9 is a genuine phenomenon of Daniely, Sabato, Ben-David and Shalev-Shwartz (2011): in multiclass classification the choice of ERM matters, and the equivalence "learnable iff uniform convergence" of the binary theory is false, which is why Conjecture 29.10 about good ERMs is open in the form the chapter states it.
The equality with the VC dimension for two labels is a direct comparison of the two shattering definitions. Natarajan's lemma is a Sauer-type induction on , in which a shattered set must be produced from two hypotheses that differ at a point; the exercise-level proof of the book becomes a careful double induction formally. Theorem 29.3's upper bounds follow the binary proof of Chapter 28 with Natarajan's lemma in place of Sauer's, hence Massart's lemma and Theorem 26.5 for the agnostic case and the double-sample argument for the realizable case; the lower bounds reduce to the binary ones by embedding a binary class into a multiclass one on a shattered set. These are long formal developments, and the theorem is stated with unspecified constants for that reason. Lemmas 29.5 and 29.6 are counting: a shattered has , Sauer's lemma bounds the right side by , and the resulting inequality is solved. For Lemma 29.5's printed this fails only at . There a shattered set splits by the label pair into parts shattered by (pairs ) or by (other pairs). The first class has at most traces on points. Theorem 29.7 maps a shattered set into by , up to sign, and shows the image is shattered by homogeneous halfspaces; the tie-breaking rule decides which sign and which halfspace convention to use. Claim 29.9(1) is the bound ; Claim 29.9(2) needs only that at most of the light points appear in the sample, an event of probability at least by Markov's inequality when , which exceeds the claimed .
Labels are an arbitrary finite type, shattering and the Natarajan dimension are stated with witnesses defined on all of , and the dimension is a supremum in . The multiclass 0–1 loss, the ERM property, agnostic PAC learnability and uniform convergence are Mission I's generic notions; the realizable multiclass PAC property is defined here in the shape of Definition 3.1 with as the error, since Mission I's binary version is -specific. Theorem 29.3 is stated exactly as Mission IV states Theorem 6.8, with existential constants, upper bounds for every ERM learner of a nonempty measurable class with the countable-approximation property (the measurability device of Remark 3.1), and lower bounds for , , . Argmax predictors, both One-versus-All and , break ties towards the smallest label; the book states this rule for One-versus-All, and some fixed rule is necessary for Theorem 29.7, since with arbitrary tie-breaking every function is an argmax predictor of the zero mapping. Lemmas 29.5 and 29.6 are stated per shattered set. Lemma 29.5 keeps the printed , which is true although the book's step fails for small . Lemma 29.6 uses , which the counting supports, because the printed is false at . Theorem 29.3's uniform-convergence upper bound is stated for . At the confidence term vanishes as , the bound reaches , and a single example is not representative. The class of §29.4 has labels Option of the subtype of finite-or-cofinite sets, with the discrete σ-algebra, and the two ERMs are predicates fixing the output on all- samples; Claim 29.9(1) is stated for countable with measurable singletons and Claim 29.9(2) for finite of size at least , with the proof's own distribution, as target, and every in place of the book's unspecified constant .
Not stated: Corollary 29.8 (its lower bound is cited, not proved), Conjecture 29.10, the exercises.
Chapter 6 stated the fundamental theorem of statistical learning: a binary class is learnable if and only if its VC dimension is finite, with sample complexity in the agnostic case and in the realizable case. Chapter 28 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), proves it. The agnostic upper bound is obtained from the Rademacher machinery of Chapter 26 with Sauer's lemma and Massart's lemma, up to a factor that only chaining removes (28.1). The agnostic lower bound comes in two parts: a two-point construction giving , and a -point construction giving at confidence , whose heart is Lemma 28.1, the optimality of the Maximum-Likelihood rule against the family of noisy distributions . The realizable upper bound is proved through -nets: with examples a random sample hits every set of measure at least in the class (Theorem 28.3), so any hypothesis consistent with the sample has error below . Mission IV states these bounds with unnamed constants; this mission gives the chapter's explicit ones.
is a class of functions with the 0–1 loss and . For the upper bound, is the loss set of a sample and its Rademacher complexity. For the lower bounds, is a set shattered by and, for and , draws uniformly and labels it with probability ; for these are the distributions of §28.2.1. The Maximum-Likelihood rule predicts at each the majority of the labels seen at . An -net for with respect to is a sample meeting every with (Definition 28.2).
Let , , and . Then with probability at least over , is an -net for .
The two-sided deviation bound of §28.1 ( uniformly over ); the lower bound of §28.2.1; Lemma 28.1; the lower bound of §28.2.2; the realizable upper bound of §28.3 (ERM has error at most with probability for the sample size of Theorem 28.3). Further items: the Rademacher bound , the explicit uniform-convergence sample complexity of §28.1, and the expectation lower bound of §28.2.2.
These are the theorems that make the VC dimension the right measure of learnability, with constants. The upper bounds show what the abstract machinery of Missions II, IV, XX buys when instantiated: Sauer plus Massart plus Theorem 26.5 gives the agnostic rate, and the double-sample symmetrization plus Sauer gives the realizable rate, sharper by a factor because -nets need only one-sided control. The lower bounds are the No-Free-Lunch argument refined to quantify and : the two-point distribution shows that confidence costs , and the -point family with Lemma 28.1 shows that the dimension costs , through the exact optimality of majority voting and a binomial anti-concentration bound. Theorem 28.3 is also the basic -net theorem of Haussler and Welzl, a result of independent importance in computational geometry.
The Rademacher bound is Sauer's lemma (Mission IV) plus Massart's lemma (Mission XX) with ; the deviation bound is Theorem 26.5 applied to and with a union bound; the explicit sample complexity is Lemma A.2, , which a formal proof must establish (the tangent inequality for at ). The two-point lower bound requires the binomial lower-tail estimate of Lemma B.11 and the algebra , valid for , the only nonvacuous range. Lemma 28.1 is a conditioning argument: fixing the instance indices and the labels off , the contribution of is minimized by predicting the more likely given the labels at , which is the majority; the formal proof must decompose the product measure over the positions with . The expectation bound then needs Lemma B.11 again, , Jensen for and , and the probability bound follows by Mission III's reverse Markov inequality with . Theorem 28.3 is the double-sample argument: Claim 1 (, via a Chernoff bound that only needs ), Claim 2 (symmetrization by a random half, ), Sauer's lemma, and Lemma A.2 once more. The realizable upper bound applies Theorem 28.3 to the error sets , a class of the same VC dimension.
All objects are those of the earlier missions: risks, samples and learners from Mission I, vcDim and the countable-approximation property PointwiseSeparable from Mission IV (the measurability device for suprema over , used wherever a symmetrization or Rademacher argument is invoked), condLaw from Mission XIV for the distributions , and rademacher, evalSet, lossClass from Mission XX. Probability statements bound the outer measure of the failure event under iidLaw. The Rademacher and deviation items require , the range in which Mission IV states Sauer's lemma in the form ; the explicit sample complexity of §28.1 implies this range, since its first term dominates the possibly negative , and Lemma A.2 holds for any real , so the book's constants are used verbatim. The lower bounds take a shattered set as an injective with the shattering property written out, use as condLaw of the uniform law on , and state the excess risk against as with , or as a real infimum over in the expectation item; no measurability of the learner is needed because is atomic. Lemma 28.1 compares the sums over of the expected risks, the common term cancelling, for every majority rule with arbitrary tie-breaking. Theorem 28.3 and the realizable bound are stated for , the theorem's own range; the realizable bound is the inner clause of Mission I's IsPACWith on that range rather than a sample-complexity function, since the theorem does not cover with its formula.
Not stated: the realizable lower bound (an exercise), the remark that chaining removes the logarithm in (28.1), and the intermediate claims of the proof of Theorem 28.3 as separate items.
Chapter 4 showed that uniform convergence suffices for learnability; Chapter 26 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), measures its rate. The representativeness of a sample, , is the quantity that controls the excess risk of ERM, and the Rademacher complexity estimates it from the sample itself: the symmetrization argument gives (Lemma 26.2), and McDiarmid's bounded-differences inequality turns expectations into high-probability statements, yielding the generalization bounds of Theorem 26.5, including the data-dependent ones in which the complexity is computed on the training set. A small calculus of Rademacher complexities follows, affine images, convex hulls, Massart's lemma for finite sets and the contraction lemma for Lipschitz compositions, and it is applied to linear classes with and constraints. The chapter's payoff is dimension-free generalization bounds for linear predictors with Lipschitz losses (Theorem 26.12), for hard-SVM (Theorems 26.13–26.14), and for predictors with low norm (Theorem 26.15).
For a loss class and a sample , (26.1), , and for , with uniform on (26.5). The linear classes are in a Hilbert space and with in (26.14). Losses of the form with -Lipschitz (26.18) cover the hinge and absolute losses.
Assume for all and . Then, each with probability at least over :
Lemma 26.2 (symmetrization); Lemma 26.8 (Massart); Lemma 26.9 (contraction); Theorem 26.12 (linear predictors with constraints); Theorem 26.13 (hard-SVM). Further items: Theorem 26.3, Lemma 26.4 (McDiarmid), Lemmas 26.6, 26.7, 26.10, 26.11, Theorem 26.14 and Theorem 26.15.
Rademacher complexity is the modern language of uniform convergence: it is data-dependent, it is dimension-free for linear classes, and it composes with Lipschitz losses, which is why the SVM bounds of this chapter do not depend on the dimension of and apply verbatim to kernel methods (Remark 26.2). Theorem 26.5 is the template every such bound follows, symmetrization plus McDiarmid, and the two data-dependent parts are the first bounds in the book that use the training set both to learn and to certify. Massart's lemma and the contraction lemma are the two tools that make the calculus work, the first converting finiteness into a logarithmic dependence, the second removing the loss function from the picture. Theorem 26.13 finally justifies the margin-based sample complexity of hard-SVM, and Theorem 26.14 gives a bound computable from the output alone.
Lemma 26.2 is the symmetrization argument: a ghost sample, the exchange of and (26.7), the introduction of one Rademacher sign at a time (26.8)–(26.9), and the split of the supremum. Formally it needs Fubini over the product of copies of and the sign average, and the measurability of the suprema, which the statements assume. McDiarmid's inequality is a martingale argument with Hoeffding's lemma at each step; it is the substantial probabilistic input, and Theorem 26.5 combines it with Lemma 26.2, a union bound and Hoeffding's inequality along the decomposition (26.10). Lemma 26.6 is the symmetry ; Lemma 26.7 is the fact that a linear functional on the simplex is maximized at a vertex; Massart's lemma is the exponential-moment bound with Jensen and an optimized scaling; the contraction lemma is Kakade and Tewari's coordinate-by-coordinate argument (26.12)–(26.13), which in a formal proof must be run as an induction over the coordinates. Lemmas 26.10 and 26.11 are Cauchy–Schwarz and Hölder followed by Jensen, respectively Massart on the coordinate vectors. Theorem 26.12 chains contraction, Lemma 26.10 and Theorem 26.5 on the almost-sure event ; Theorem 26.13 specializes it to the ramp loss with , where the hard-SVM output has zero empirical ramp loss; Theorem 26.14 is a union bound over the nested classes with ; Theorem 26.15 repeats Theorem 26.12 with Lemma 26.11.
The Rademacher complexity is a finite average over the sign vectors, so no measure on is needed, and the supremum over is the real supremum over the subtype ; the theorems assume nonempty and bounded, which every evaluation set of a bounded loss class satisfies. Risks are Mission I's risk and empRisk, samples are Fin m-indexed under iidLaw, and probability statements bound the outer measure of the failure event. Expectations of suprema over uncountable classes are Bochner integrals, so Lemma 26.2, Theorem 26.3 and Theorem 26.5 carry explicit hypotheses that and are measurable, the book's Remark 3.1 made visible; for the linear classes of §26.3–§26.4 these hold automatically when the Hilbert space is separable (the supremum over the ball is a supremum over a countable dense subset), which is why Theorems 26.12–26.14 assume SecondCountableTopology. McDiarmid's inequality is stated for a measurable function on a product of arbitrary probability measures. Theorem 26.13's error is , which dominates whatever is, and the hard-SVM learner is any map returning a minimum-norm margin-1 separator on separable samples; measurability of the learner is not needed because the bound is uniform over the ball. Theorem 26.14 is given with the constants of its proof, rather than the printed , and for , where satisfies as the proof requires; the item text records this. Norms on as Fin n → ℝ are sup norms (Lemma 26.11, Theorem 26.15), Euclidean norms are written out (Massart), and inner product spaces carry the Euclidean norm.
Not stated: Definition 26.1 (already Mission II's IsRepresentative), the validation heuristic (26.2)–(26.3), Remark 26.1 (the improved rate under separability, no proof), Remark 26.2.
In PAC learning the learner receives a batch of examples, learns, and only then predicts. Online learning has no such separation: on each round the learner receives an instance, predicts its label, and then sees the true label, and the goal is to make few mistakes over the whole sequence, with no statistical assumption whatsoever on how the sequence is generated, adversarially if need be. Chapter 21 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), develops this model along the same lines as the PAC theory. In the realizable case, mistake bounds replace sample complexity, and a combinatorial dimension due to Littlestone, , characterizes the best achievable bound exactly (Lemmas 21.6 and 21.7), playing the role the VC dimension plays for PAC learning, with and an arbitrarily large gap (Theorem 21.9). In the unrealizable case regret replaces excess risk; deterministic learners can be forced to regret (Cover), but randomized predictions restore sublinear regret through the Weighted-Majority algorithm of Littlestone, Warmuth and Vovk (Theorem 21.11). The chapter closes with online convex optimization, where Online Gradient Descent (Zinkevich) attains regret (Theorem 21.15), and with the online Perceptron, whose mistake bound follows from a round-specific surrogate loss (Theorem 21.16).
An online algorithm is a deterministic map from the history of past examples and the current instance to a prediction. For a sequence labeled by some , is the number of mistakes and the supremum over all such sequences (Definition 21.1). The Consistent algorithm predicts with any hypothesis of the version space (the hypotheses consistent with the past), Halving with its majority label, and SOA with the label for which has the larger Littlestone dimension, ties to . An -shattered tree of depth assigns an instance to every node of a complete binary tree so that every labeling is realized by some along the path it determines; is the maximal such depth (Definitions 21.4–21.5). In the unrealizable case predictions are , the loss is , and the regret against is (21.1). Weighted-Majority maintains over experts with costs and pays . Online Gradient Descent on a closed convex predicts , receives a convex , takes a subgradient at and projects back onto ; the online Perceptron is the special case on rounds with .
For experts, cost vectors , and ,
Theorem 21.3 (Halving makes at most mistakes); Lemma 21.6 ( for every ); Lemma 21.7 (); Theorem 21.15 (the three regret bounds of Online Gradient Descent); Theorem 21.16 (the online Perceptron bound and its separable case). Further items: Corollary 21.2, Theorem 21.9, Example 21.4, Cover's impossibility, Corollary 21.12 and the half of Theorem 21.10.
Corollary 21.8 is one of the cleanest characterizations in learning theory: the Littlestone dimension is exactly the optimal mistake bound, with SOA attaining it and Lemma 21.6 forbidding anything better. Theorem 21.11 is the engine of the unrealizable case and of a large part of online learning: the multiplicative-weights analysis with the potential gives regret against the best of experts, and with the experts of pp. 298–299 it yields Theorem 21.10, regret for any class of finite Littlestone dimension. Theorem 21.15 is the online counterpart of the SGD analysis of Chapter 14, and the derivation of Theorem 21.16 from it shows how a surrogate loss chosen per round turns a regret bound into a mistake bound, the Perceptron bound of Chapter 9 falling out as the separable case. On the platform, these items give the first online-learning model, reusing Mission X's subgradients and projections.
Corollary 21.2 and Theorem 21.3 are counting arguments on the version space, but formally they require tracking the version space along the history and the fact that a mistake by Halving halves it. Lemma 21.6 is the adversary argument: given a shattered tree, feed the instance at the current node and the label opposite to the prediction; the resulting sequence is labeled by some by the shattering property, and the algorithm errs on every round. Lemma 21.7 needs the combinatorial core of the chapter: if both restricted version spaces had Littlestone dimension equal to , their shattered trees could be glued under a new root to a deeper tree. Theorem 21.9 builds a shattered tree with all nodes at depth equal to ; Example 21.4 builds the dyadic tree. Theorem 21.11's proof is the book's: for , , the telescoping potential , the lower bound , and the choice of ; the hypothesis makes . Corollary 21.12 is the reduction of hypotheses to experts, and Theorem 21.10 is the expert construction with the counting bound (21.4) (Lemma A.5) and Lemma 21.13, which simulates SOA on the labels of ; small horizons are covered by the trivial bound . Theorem 21.15 is the telescoping argument of Lemma 14.1 with the projection lemma of Chapter 14 at every step; Theorem 21.16 applies it to with and solves the quadratic inequality (21.6).
Online algorithms are deterministic functions List (X × Y) → X → Y; a sequence is Fin T-indexed and the history at round is its first examples. Mistake bounds and the Littlestone dimension are suprema in ℕ∞, so mistakeBound, ldim and their comparisons are meaningful when infinite. Shattered trees are indexed by paths rather than by the book's node numbers , whose binary expansion is exactly the path; the two descriptions are the same tree. Halving and SOA break ties towards as in the book; Consistent is stated as a property of an algorithm. The unrealizable case uses real-valued predictions with the loss as the book does, and the theorems of that section assert the existence of an algorithm for each horizon , because Weighted-Majority takes as input. Weighted-Majority's distribution is written in unrolled form, , which is the update rule iterated from . Theorem 21.10 is stated for classes with and in its form, the form being Corollary 21.12; its lower bound, proved in Ben-David, Pál and Shalev-Shwartz (2009), is not stated. Online Gradient Descent is driven by a subgradient selector (Mission X's global subgradients), from , on a closed convex containing the comparator; the Lipschitz parts take LipschitzWith ρ (f t) and . The Perceptron's is the set of update rounds , which contains every prediction mistake whatever is and is the set the book's derivation actually uses; is any bound on for . Cover's impossibility is stated for deterministic -valued algorithms, the setting in which the book states it.
Not stated: the Doubling Trick (Exercise 4), Exercises 1–3 (specific tight examples), the SOA-based Expert algorithm as a separate definition (it is internal to the proof of Theorem 21.10), Lemma 21.13 and Corollary 21.14 as items, and the lower bound of Theorem 21.10.
Whether the quantization of the gravitational field is observable is a long-standing question at the interface of general relativity and quantum theory. In his 2013 talk Is a Graviton Detectable? (doi:10.1142/S0217751X1330041X), Freeman Dyson examined three families of hypothetical single-graviton detectors and estimated, for each, why it fails: LIGO-type interferometers (Sec. 3), atoms absorbing a graviton by the gravitoelectric effect (Secs. 4–5), and Gertsenshtein photon–graviton conversion in a magnetic field (Secs. 6–7).
Most of the paper consists of order-of-magnitude physical estimates. A part of it, however, consists of precise mathematical statements: exact algebraic consequences of the stated physical relations, and one genuine analytic inequality about the quadrupole factor that controls the graviton absorption cross-section of a bound particle. This mission collects those statements.
Sections 3. Let be the speed of light, Newton's constant and the reduced Planck constant. The Planck length is (Eq. (5)). A gravitational wave of strain amplitude and angular frequency has energy density (Eq. (2)); a single graviton of frequency has energy density at most (Eq. (3)).
Section 4. For an electron bound in a state with zero angular momentum about the -axis, with real wave function in cylindrical coordinates ( the distance from the -axis), let and define
The s-state of Eq. (19) is with .
Sections 6–7. For a transverse magnetic field , the mixing length is (Eq. (29)) and the photon-to-graviton conversion probability over a distance is (Eq. (28)). Vacuum nonlinearity slows the photon by the fraction (Eq. (36)), where is the fine-structure constant and the critical field, giving the coherence length (Eq. (37)).
For every nonzero, normalizable axially symmetric wave function with finite ,
Eq. (18) is what allows Dyson to conclude that the averaged absorption cross-section (Eq. (14)) is, for every bound particle, of the order of the Planck area; together with Eq. (20) it shows is of order unity for tightly bound s-states. The Section 3 bounds are the precise algebraic content of the argument that measuring distances to Planck accuracy forces the apparatus inside its own Schwarzschild radius. The Section 7 bounds are the algebraic content of the argument that vacuum birefringence limits Gertsenshtein conversion.
None of these statements has, to our knowledge, a machine-checked proof. Eq. (18) is a weighted Hardy-type inequality on the half line with sharp constant, applied slice by slice; formalizing it produces reusable one-dimensional weighted Hardy inequalities. Eq. (20) requires explicit Gamma-function integrals in cylindrical coordinates.
For Eq. (18) the difficulty is analytic: the inequality must hold for all admissible , including functions that are not compactly supported and may be singular on the -axis, and it is strict although its sharp constant is not attained. Boundary terms of the integration by parts behind Eq. (17) must be controlled using only the integrability assumptions. The printed Eq. (17) has the sign ; with that sign the integral is trivially positive and does not imply Eq. (18). The mission uses , the sign under which (17) implies (18). The algebraic milestones are elementary.
All quantities are real. is a function of ; is deriv in the first variable; integrals are Lebesgue integrals over the half plane . The admissible class for Eqs. (17)–(18) is: differentiable at every , and integrable on the half plane, and not almost-everywhere zero there. These hypotheses rule out the degenerate reading (Lean's division returns ). Eq. (20) requires and , the range in which the integrals in Eq. (16) converge. Physical constants are arbitrary positive reals; numerical cgs values (e.g. Eqs. (5), (21), (31)) are not formalized. The heuristic parts of the paper (Bohr–Rosenfeld argument, the sum rule (14), astrophysical source estimates, neutrino backgrounds) are out of scope.
Every learning paradigm of the book so far, ERM, SRM, MDL, RLM, is defined by a hypothesis class: the learner searches a predefined set of functions. Nearest Neighbor is the first method that is not. It memorizes the training set and labels a new point by the labels of its closest neighbors, on the assumption that the features are relevant to the labels in a way that makes close-by points likely to share a label. Chapter 19 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), makes that assumption precise, a Lipschitz conditional probability, and proves a finite-sample guarantee: the expected error of the 1-NN rule on examples is at most twice the Bayes error plus (Theorem 19.3). The classical results of Cover and Hart (1967) and Stone (1977) are asymptotic; the book insists, as it did in §7.4, on a bound that says what a finite sample buys under an explicit prior assumption. The chapter also proves that the exponential dependence on the dimension is not an artifact (Theorem 19.4, the curse of dimensionality) and, in its exercises, extends the analysis to the -NN rule, whose error converges to times the Bayes error (Theorem 19.5).
The instance domain carries a metric ; for the analysis with the Euclidean distance and with the 0–1 loss. For a sample and a point , let reorder the sample by distance to . The -NN rule returns the majority label among ; the 1-NN rule is ; in general, for , the -NN rule with respect to is (19.1).
A distribution over has marginal and conditional probability ; the Bayes optimal rule is , and the standing assumption is that is -Lipschitz: . In the formalization a distribution with conditional probability is written condLaw DX η: draw , then . Every distribution with a regression function is of this form, so nothing is lost.
For , , a distribution over whose conditional probability is -Lipschitz, and the result of the 1-NN rule on ,
Lemma 19.1 (the Lipschitz reduction: ); Lemma 19.2 (the expected mass of the sets among missed by an i.i.d. sample of size is at most ); Theorem 19.4 (for integer and every learning rule there is a distribution with -Lipschitz and Bayes error on which the rule's expected error is at least whenever ); Lemma 19.7 (the majority of independent Bernoulli labels errs, against a label drawn from their mean , at most times as often as ); Theorem 19.5 (the -NN bound ). Lemma 19.6, the -fold version of Lemma 19.2 with bound , is a further item.
Theorem 19.3 is the book's answer to the question it raised in §7.4: consistency results say that the 1-NN error converges to twice the Bayes error, but not how fast, and the rate necessarily depends on the distribution. The Lipschitz constant and the dimension are exactly the prior knowledge the rule relies on, and Theorem 19.4 shows through the No-Free-Lunch theorem that a sample of size exponential in is genuinely required for some distributions in the class. Theorem 19.5 quantifies what larger buys, the factor improving to , at the price of the additive term growing linearly in . On the platform, this mission introduces the conditional-probability model of a distribution over and the Bayes rule, which Chapters 24 (generative models) and the nonparametric parts of the book use again, and the box-cover argument of Lemma 19.2, a small combinatorial-probability tool of independent use.
Lemma 19.1 is a computation once the expectation over and is decomposed as the book does: sample the unlabeled points first, find the nearest neighbor, then draw the two labels; the identity and finish it. Formally the work is in the decomposition itself, which is Fubini for condLaw and the product law, and in the measurability of the rule, which the statement assumes. Lemma 19.2 is and . Theorem 19.3 covers the cube by boxes of side , applies Lemma 19.2 to the boxes and sets ; a formal proof must handle not being an integer (take boxes per side, so when , which is what the book's already allows for) and the regime , where the trivial bound suffices. Theorem 19.4 is the No-Free-Lunch theorem on the grid of spacing , plus the observation that any -valued function on the grid extends to a -Lipschitz -valued function on the cube (McShane). Lemma 19.6 is Chernoff's bound below the mean; Lemma 19.7 is the delicate one: Chernoff with the function and the inequality for , , which the book states without proof. Theorem 19.5 assembles Lemmas 19.6 and 19.7 along the four steps of Exercise 4; to reach the book's constants with an integer number of boxes one takes boxes per side and Chernoff at in Lemma 19.6, or notes that the bound is trivial unless .
Labels are Bool; bernoulliLaw p is the Bernoulli law on Bool, condLaw DX η the distribution with marginal DX and conditional probability η, and bayesRule η the Bayes rule. The cube is the subtype cube d of EuclideanSpace ℝ (Fin d), so its metric is Euclidean and its Borel structure is inherited; the Lipschitz hypothesis is LipschitzWith c η with c : ℝ≥0, together with η x ∈ [0,1] (a conditional probability). A -NN rule is a learner h with IsKNNRuleWith k φ h: for every sample of size and every there is some reordering of the sample by distance to whose first entries feed ; ties are therefore broken arbitrarily, and the theorems hold for every choice. Majority votes predict iff strictly more than half of the labels are , the book's of Lemma 19.7. The nearest-neighbor distance is nnDist S x = ⨅ i, dist x (S i).1. Expectations over are Bochner integrals against iidLaw D m (Mission I), and the expectation statements assume the rule is measurable in , the book's Remark 3.1; without it the integrals would be junk. Lemmas 19.2 and 19.6 are stated for arbitrary measurable subsets of an arbitrary measurable space, as in the book, with (for the left side is while Lean reads as ). Lemma 19.7 uses the product of Bernoulli laws on Fin k → Bool.
Two statements are given as their proofs support them, and the deviations are recorded in the item texts. Theorem 19.4 takes an integer (the grid has spacing ), fixes with before choosing the distribution (Theorem 5.1 produces a distribution per ), and concludes that the expected true error is at least (Equation (5.2) in the proof of Theorem 5.1; the book's "greater than " is what its proof gives for only in the form of that expectation). Theorem 19.5 keeps the book's constants; the drafter checked that they are reachable with an integer number of boxes. Not stated: the general weighted-average rules of §19.1 beyond (19.1), the efficient implementation of §19.3, Exercise 3 (a one-line inequality, absorbed into the proof of Theorem 19.5).
Binary classification is the exception in practice; most prediction tasks have many labels, a structured label space, or ask for a ranking. Chapter 17 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) extends linear predictors to these settings through one idea: a class-sensitive feature mapping that scores a candidate label, with the prediction . A cost-sensitive loss replaces the 0–1 loss, and the generalized hinge loss (17.3), , is its convex surrogate: it upper bounds , is tight under margin, and is convex and Lipschitz in . Multiclass SVM is then regularized loss minimization for this loss, and Corollaries 17.1 and 17.2 transfer the guarantees of Chapters 13 and 14 with no dependence on the number of labels. The same construction handles ranking: a linear ranking predictor scores each item, the Kendall tau loss has a pairwise hinge surrogate, and the NDCG surrogate reduces to an assignment problem whose linear relaxation is exact by the Birkhoff–von Neumann theorem (Claim 17.3, Lemma 17.4).
Labels form a finite nonempty type ; the feature mapping takes values in as in Mission VI, and the RLM rule and the SGD of Chapters 13 and 14 are those of Missions IX and X. An argmax predictor for is any with maximizing ; a canonical one is fixed by choosing among the maximizers, and likewise a canonical maximizer in the generalized hinge loss, which gives the SGD direction . The cost is nonnegative with . For ranking, an example is a list of instances with a score vector ; the linear predictor is , the Kendall tau loss is the fraction of pairs ordered differently, using the three-valued real sign, and permutations of are Mathlib's permutations of Fin r, with doubly stochastic and permutation matrices from Mathlib.
For over , , , and the Multiclass SVM learner with : , and for every with , .
Equation (17.3). The generalized hinge loss bounds for every argmax predictor, equals it under the margin condition, and is convex and -Lipschitz in with .
Corollary 17.2. SGD for multiclass learning with examples has for every .
Equation (17.7). The permutation induced by sorting maximizes over permutation vectors (the rearrangement inequality).
Claim 17.3. The doubly stochastic matrices are the convex hull of the permutation matrices.
Lemma 17.4. The assignment LP over doubly stochastic matrices has an optimal solution that is a permutation matrix.
Further items: Remark 17.2 (the binary case recovers the hinge loss) and the Kendall tau surrogate of §17.4.1 with its convexity and Lipschitz constant.
The generalized hinge loss is the device that lets the whole convex-learning machinery of Part II run on arbitrary finite label sets and on structured outputs, and Remark 17.3's observation that the bounds of Corollaries 17.1 and 17.2 do not depend on is what makes structured prediction (§17.3) and ranking with exponentially many labelings feasible. The ranking half of the chapter shows the pattern at work: the induced permutation is an argmax over a combinatorial set (17.7), so the NDCG loss admits a generalized hinge surrogate, and its subgradient is an assignment problem, solvable by the Hungarian method or, thanks to Birkhoff–von Neumann, by linear programming.
Nothing here is machine-checked except that Mathlib contains the Birkhoff–von Neumann theorem, which the corresponding item restates in the book's form. The statements are faithful with the clarifications that ties are broken canonically, that the Kendall tau surrogate is stated for tie-free score vectors (the book's rewriting of the pairwise indicator assumes ), and that Corollary 17.1 is stated with the measurability conventions of Mission IX.
Remark 17.2 is a two-element maximum and the entry point, and Equation (17.7) is Mathlib's rearrangement inequality for monovarying functions. The properties of the generalized hinge loss are elementary: the bound by choosing , the equality by showing every term is at most and the term is , convexity as a maximum of affine functions, and the Lipschitz bound by Cauchy–Schwarz on each term. Corollary 17.1 is Mission IX's Corollary 13.9 for the generalized hinge loss, which requires verifying convexity, the -Lipschitz property from , nonnegativity and boundedness at the origin (by , finite), the measurability of the loss and of the canonical argmax predictor as functions of , and the pointwise comparison with the -loss; Corollary 17.2 is the same with Mission X's Corollary 14.12 and Claim 14.6 for the subgradient. The Kendall tau surrogate is the pairwise hinge bound under no ties, plus the convexity and Lipschitz constant of an average of hinge terms. Lemma 17.4 follows from Birkhoff–von Neumann by the averaging argument of the book, or directly from the finiteness of the permutation matrices together with the fact that a linear function on a convex hull is minimized at an extreme point.
The label set is finite, so maxima over are attained and the losses are well defined; maximizers are chosen canonically, and every statement about argmax predictors holds for any choice. The multivector and TF-IDF constructions of §17.2.1, the reductions of §17.1, structured output prediction (§17.3), the NDCG loss and its surrogate (17.8), and bipartite ranking (§17.5) are not stated; the NDCG construction would need the sorting permutation and the discount function and is left for a later revision. Exercises are not stated except 17.4 through Equation (17.7).
Trivializing readings are excluded: the -risk in Corollaries 17.1 and 17.2 is that of a genuine argmax predictor, the Lipschitz constants are the book's, and the assignment lemma asserts optimality against every doubly stochastic matrix. Welcome contributions: the Lipschitz constant of a maximum of affine functions, the measurability of a canonical argmax over a finite label set, and the extreme-point argument of Lemma 17.4.
Chapter 15 bounded the sample complexity of large-margin halfspaces by the norms of the data and of the separator, independently of the dimension. Chapter 16 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) removes the remaining obstacle to using halfspaces in very high-dimensional feature spaces: computation. After embedding the data by a feature map into a Hilbert space, every SVM-like problem has the form (16.2), and the representer theorem (Theorem 16.1) says that an optimal solution lies in the span of the mapped examples. Consequently the problem can be rewritten in terms of the coefficients and the kernel alone (16.3): this is the kernel trick. The chapter exhibits the polynomial and Gaussian kernels (Examples 16.1 and 16.2), characterizes the functions that are kernels as the positive semidefinite ones (Lemma 16.2), and shows that the SGD solver for Soft-SVM of §15.5 can be run entirely on kernel evaluations (Lemma 16.3).
A feature map takes values in a real Hilbert space, a complete real inner product space; its kernel is , and a function implements an inner product in some Hilbert space if it is the kernel of some feature map into some Hilbert space, quantified existentially in the universe of the domain. The Gram matrix of a sample is . The general objective (16.2) is with arbitrary and nondecreasing on . The SGD procedure of §15.5 in the feature space keeps with (iterates indexed from ) and, at each step, for the chosen index , adds to when ; its kernelized version keeps coefficients with and tests . Both are driven by the same sequence of chosen indices, which stands for the uniformly random choices of the book.
If is nondecreasing on and the problem (16.2) has an optimal solution, then there is such that is an optimal solution.
Equation (16.3). For the objective equals .
Example 16.1. The polynomial kernel on is for the monomial map into .
Example 16.2. On , the map into has ; the Gaussian kernel on is a kernel for every .
Lemma 16.2. A symmetric is a kernel iff all its Gram matrices are positive semidefinite.
Lemma 16.3. The kernelized SGD reproduces the feature-space SGD: for all , hence the outputs coincide.
Further items: Exercise 16.3 (kernel ridge regression: minimizers of the coefficient objective give minimizers of the ridge objective, and gives one), Exercise 16.4 ( is a kernel), Exercise 16.6 (the nearest-class-mean rule is a halfspace).
The representer theorem is the reason kernel methods exist: it reduces an optimization over an arbitrary Hilbert space to one over , and Lemma 16.2 says the reduction needs nothing but a positive semidefinite similarity function, so one may design the kernel directly, as in the string example of §16.2.1. Lemma 16.3 makes the connection to Chapter 14 concrete: a first-order method never leaves the span of the examples, so it too can be run on the Gram matrix. Together with Chapter 15, the chapter closes the book's treatment of linear predictors: expressive through the embedding, statistically controlled through the margin, and computable through the kernel.
Nothing here is machine-checked. The statements are faithful to the book with two clarifications: the representer theorem assumes the existence of an optimal solution, which the book's proof also assumes, and the kernel-SGD equivalence is stated for a fixed sequence of chosen indices, which is the content of the book's inductive proof.
Equation (16.3) and Exercise 16.6 are inner-product algebra and the entry points. The representer theorem needs the orthogonal decomposition with orthogonal to the span, which is available in Mathlib for the finite-dimensional, hence complete, subspace spanned by the , together with the Pythagorean identity and the monotonicity of . Example 16.1 is the multinomial expansion of as a sum over index vectors, packaged as an inner product in the Euclidean space indexed by . Example 16.2 needs the summability of and the exponential series, and, for the general Gaussian kernel, either an explicit construction or Lemma 16.2 together with the positive semidefiniteness of the Gaussian Gram matrix. Lemma 16.2 in the nontrivial direction is the construction of the reproducing kernel Hilbert space: the pre-Hilbert space of finite combinations of the functions , the inner product defined through , its well-definedness and positive definiteness from the Gram matrices, and the completion, which Mathlib provides for inner product spaces. Lemma 16.3 is an induction on with the identity . Exercise 16.3 combines the representer theorem with the identity between the two objectives on the span and the first-order condition for a convex quadratic; Exercise 16.4 needs a feature map such as , or the positive semidefiniteness of the min matrix.
Hilbert spaces are real, complete inner product spaces; the existential in IsKernel ranges over Hilbert spaces in the universe of the domain, which the reproducing kernel construction respects. The objective (16.2) has real-valued , so the hard-SVM instance with is not covered by the representer item as stated. The SGD procedures are deterministic given the index sequence; the random choice of indices is not modelled, exactly as in Lemma 16.3's proof. The string kernel of §16.2.1 and Exercise 16.1, the kernelized Perceptron (Exercise 16.2), Exercise 16.5 and part (2) of Exercise 16.6 are not stated.
Trivializing readings are excluded: the representer theorem asserts optimality against every , Lemma 16.2 is a biconditional with symmetry assumed as the book does, and the kernels of the examples are exhibited with explicit feature spaces where the book gives them. Welcome contributions: the orthogonal decomposition against a finite span, the multinomial identity of Example 16.1, and the reproducing kernel Hilbert space construction behind Lemma 16.2.
The sample complexity of learning halfspaces in grows with , which is bad news when features are many or infinite. Chapter 15 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) introduces the support vector machine, the learning rule that replaces dimension by geometry. Among the halfspaces separating a sample, Hard-SVM picks the one of largest margin, the distance from the hyperplane to the nearest example (Claim 15.1, Lemma 15.2); if the data are separable with margin and lie in a ball of radius , the resulting classifier has error whatever the dimension (Theorem 15.4), and the Perceptron of Chapter 9 makes at most updates (Remark 15.1). Soft-SVM drops separability by allowing slack variables, and Claim 15.5 identifies it with regularized hinge-loss minimization, so that the stability theory of Chapter 13 applies: the hinge loss is -Lipschitz (Claim 15.6), and Corollary 15.7 gives an expected-risk bound depending only on the norms of the data and of the comparison halfspace. The chapter closes with the optimality conditions that explain the name: the Hard-SVM solution is a combination of the examples on the margin (Theorem 15.8, via the Fritz John conditions, Lemma 15.9).
Vectors live in as in Mission VI; labels are real numbers, with as a hypothesis wherever the book needs it. A sample is linearly separable if some halfspace has for all , and the margin of on the sample is . Hard-SVM solutions are minimizers of subject to , formalized as a relation; the minimizer is unique whenever the constraints are feasible, and the homogenous version sets . A distribution over is separable with a -margin if some unit (and ) has and almost surely. Soft-SVM is the problem under , ; its homogenous form is the regularized loss minimization rule of Mission IX for the hinge loss , and the 0–1 loss is . Expectations over samples are integrals against , with the measurability conventions of Mission IX.
For on almost surely, , and the Soft-SVM learner with : , and for every with , .
Claim 15.1. The distance from to with is .
Lemma 15.2. For a sample with both labels present, the normalized Hard-SVM output has unit norm and margin at least that of every unit-norm halfspace.
Theorem 15.4. Under homogenous -separability, with probability at least the 0–1 risk of the Hard-SVM output is at most .
Claim 15.5. Every feasible slack vector has average at least the hinge loss, and the hinge losses are feasible slacks.
Claim 15.6. For , is -Lipschitz.
Corollary 15.7, first parts. For every , and are at most .
Theorem 15.8. The homogenous Hard-SVM solution is with .
Lemma 15.9. Fritz John conditions, in the correct form with a multiplier on .
Further items: Exercise 15.1 (the two Hard-SVM formulations agree) and Exercise 15.2 (the Perceptron makes at most updates).
SVM is the bridge between the statistical theory of Part I and the kernel methods of Chapter 16: because the bounds of Theorem 15.4 and Corollary 15.7 involve only , and , the same algorithm can be run after an embedding into a huge or infinite-dimensional feature space, and Theorem 15.8, that the solution lies in the span of the examples, is what makes the embedding computable. Corollary 15.7 is also the first place where the abstract machinery of Chapter 13 is applied to a specific learning rule.
Nothing here is machine-checked. One correction is built in: the Fritz John lemma is stated with the multiplier on and nonnegative multipliers not all zero, since the printed form, with unweighted and unrestricted, fails already for and on the line. Theorem 15.8 is unaffected: its constraints are affine, so the multiplier on can be taken to be .
Claim 15.6 and Claim 15.5 are short inequalities and the intended entry points, and Exercise 15.2 is Theorem 9.1 of Mission VI with and . Claim 15.1 is the book's computation with the foot of the perpendicular and a Pythagorean inequality for every other point of the hyperplane, packaged as an infimum distance. Lemma 15.2 is the rescaling argument of the book, together with the observation that both labels force ; Exercise 15.1 needs the positivity of the optimal margin on a separable sample. Corollary 15.7 is Corollaries 13.8 and 13.9 of Mission IX for the hinge loss, whose Lipschitz constant is only on the support of , so the stability argument must be run with the almost-sure bound; the 0–1 clause is the pointwise inequality . Theorem 15.4 is the content of §26.3: Rademacher complexity of the class of norm-bounded halfspaces, the contraction lemma for the ramp loss, the observation that the Hard-SVM output has zero ramp loss on the sample and norm at most , and a concentration step, all of which will be items of the Rademacher mission. Theorem 15.8 is the KKT theorem for a strictly convex quadratic with affine constraints (Slater's condition holds), and Lemma 15.9 is the general Fritz John theorem for differentiable data, whose proof goes through a separation or penalty argument; neither is in Mathlib.
Hard-SVM and Soft-SVM are relations and learners, not programs; the margin is a real infimum over the sample; the ramp loss is defined but its bounds belong to Chapter 26. Theorem 15.4 is stated for any learner that returns the Hard-SVM solution whenever the sample is feasible, which is almost surely the case under the margin assumption, and bounds the failure event in outer measure. Corollary 15.7 carries the measurability conventions of Mission IX. The Fritz John lemma is stated correctly rather than as printed. The duality of §15.4, the SGD implementation of §15.5 (whose guarantee needs the trajectory bound of §14.5.3 rather than Theorem 14.11 as stated in Mission X), Exercises 15.3 and 15.4, and Remark 15.2 are not stated.
Trivializing readings are excluded: both labels must be present for the normalized Hard-SVM output, the margin assumption and the support condition are almost sure with respect to , and the risks are genuine integrals. Welcome contributions: the uniqueness of the Hard-SVM minimizer, the KKT conditions for affine constraints, and the pointwise comparison of the 0–1, ramp and hinge losses.
Chapter 3 of The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) is the book's first complete example of its effective-theory method. For deep linear networks at initialization, the two- and four-point correlators of the network outputs can be computed exactly at any width and depth. The resulting formulas exhibit, in the simplest setting, the phenomena that organize the rest of the book: criticality of the weight variance , non-Gaussianity that grows with depth, and the depth-to-width ratio as the parameter controlling deviations from the infinite-width limit. This mission formalizes §§3.1–3.3. It is the second mission in a series formalizing the book (namespace DeepLearningTheory).
A deep linear network with widths (all positive) and zero biases maps an input to preactivations
(eqs. 3.1–3.2 with ). At initialization all weights are independent centered Gaussians with (eq. 3.4), with a layer-independent . For inputs let (eq. 3.9).
For every layer , a single input , and neurons ,
The closed forms show that a deep linear network is exactly Gaussian only in the strict infinite-width limit: at criticality the connected four-point correlator (3.29)–(3.30) is for equal widths , the first appearance of the depth-to-width ratio as the book's emergent scale. The same recursive method is reused for nonlinear networks in Chapters 4–5. The results are exact computations in the book; this mission formalizes them.
Each correlator is an expectation of a polynomial in exponentially many Gaussian weights. The book's recursion uses that the layer- weights are independent of the layer- preactivations, followed by Wick contraction of the two or four new weights. In Lean this requires independence of a weight family from a measurable function of the earlier layers, integrability of products of Gaussian polynomials, and careful handling of the Kronecker-delta bookkeeping in the sums (3.23).
n : ℕ → ℕ with n 0 the input dimension; neural indices are . Weights are a random field W : Ω → ℕ → ℕ → ℕ → ℝ on a probability space, only entries with , , are used.IsLinearNetInit P n CW W states mutual independence of all these weights and that each has law gaussianReal 0 (CW / n (ℓ-1)).linearPreact n (W ω) x ℓ i is ; inputKernel (n 0) x₁ x₂ is ; kron and wickDelta4 are the Kronecker delta and the three-term tensor structure.Chapter 4 of The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) begins the analysis of general multilayer perceptrons (MLPs) with a nonlinear activation function at initialization. The first layer is exactly Gaussian; the second layer is the first place where non-Gaussianity appears, as a connected four-point correlator suppressed by and governed by the four-point vertex . This mission formalizes §§4.1–4.2, which are exact at any width. It is the third mission in a series formalizing the book (namespace DeepLearningTheory) and reuses the definitions of Mission II (Deep Linear Networks at Initialization).
An MLP with widths and activation maps inputs to preactivations
(eqs. 4.2, 4.30). At initialization all biases and weights are independent centered Gaussians with and (eqs. 4.3–4.4). The first-layer metric is (eq. 4.8), and denotes the expectation over a centered Gaussian vector with covariance (eq. 4.25), with .
with the four-point vertex (eq. 4.40).
These identities are the base case of the book's recursion (Chapter 4.3 onward) for the kernel and four-point vertex in deeper layers, and they show concretely that a finite-width network is not a Gaussian process: the connected correlator is generically nonzero for nonlinear . The results are exact computations in the book; this mission formalizes them.
The second layer is a Gaussian conditional on the first layer, with a random covariance (the stochastic metric, eq. 4.36). Turning this into unconditional correlators requires conditioning on the first-layer preactivations, independence of different first-layer neurons, and the identification of first-layer activation correlators with Gaussian expectations over the metric , which may be degenerate (e.g. repeated inputs). Integrability of against Gaussians must be controlled.
kron, inputKernel, WeightIndex. New definitions: mlpPreact (), IsMLPInit (independent Gaussian biases and weights with layer-dependent ), firstLayerMetric ( on finitely many inputs), gaussAvg (, via Mathlib's multivariateGaussian, which handles singular positive-semidefinite ), and HasPolyGrowth.Fin D (for the specific statements, or inputs, possibly repeated). is assumed where the formulas divide by .Chapter 13 showed that convex-Lipschitz-bounded and convex-smooth-bounded problems are learnable by regularized loss minimization; Chapter 14 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) shows how to learn them with the simplest possible algorithm. Gradient descent moves against the gradient with a fixed step size and outputs the average of its iterates; its analysis (Lemma 14.1) is a single telescoping identity that bounds for any sequence of directions , and this generality is the whole point. It gives the rate for convex Lipschitz functions (Corollary 14.2), extends to nondifferentiable functions through subgradients (Definition 14.4, Lemmas 14.3 and 14.7), and, because it never used that the directions were gradients, extends to stochastic gradient descent, in which each direction is random with a subgradient as its conditional expectation (Theorem 14.8). Applied to the risk with a fresh example at each step, SGD is a learning algorithm whose sample complexity is the iteration count: examples for convex-Lipschitz-bounded problems (Corollary 14.12) and for convex-smooth-bounded ones (Theorem 14.13, Corollary 14.14). A projected, decreasing-step variant for strongly convex objectives has rate (Theorem 14.11).
Hypotheses are vectors in ; convex, Lipschitz and smooth losses, convex-Lipschitz-bounded and convex-smooth-bounded problems, and strong convexity are those of Mission IX. A vector is a subgradient of at if for all . The iterates of an update rule , are indexed from , and the output after steps is . The randomness of SGD is modelled as the chapter uses it in §14.5: a sample drawn i.i.d. from and an oracle with , where is a stochastic subgradient oracle for if for every . This is the book's condition in the case where the direction depends on the past only through and on fresh randomness, which is what every application in the book does; the expectation is then an integral over . For learning, is a subgradient of at , so that is a subgradient of at (14.13). The projection of onto a convex set is a nearest point of , and the strongly convex variant projects after each step with step size .
For a convex , , a measurable oracle with and , any with , and : ; and for every , gives .
Lemma 14.1. For any directions, ; with , and the average is at most .
Corollary 14.2. Subgradient descent on a convex -Lipschitz with has for every , and gives .
Lemma 14.7. A convex on is -Lipschitz iff all its subgradients have norm at most .
Lemma 14.9. For the projection of onto a convex and , .
Theorem 14.11. For -strongly convex , a closed convex , an oracle with and any , the projected variant with has .
Corollary 14.12. SGD on the risk of a convex-Lipschitz-bounded problem with examples has for every .
Theorem 14.13. For convex, -smooth, nonnegative losses and , SGD with gradient directions has .
Corollary 14.14. For a convex-smooth-bounded problem with and any , SGD with and has for every .
Further items: Lemma 14.3, Claims 14.5, 14.6 and 14.10, and the hinge-loss subgradient of Example 14.2.
SGD is the algorithm behind most of modern machine learning, and Theorem 14.8 is its basic guarantee: dimension-free, independent of the form of beyond convexity, and with a sample complexity matching the regularization bound of Chapter 13 up to a constant. Lemma 14.1 isolates the deterministic identity that makes both gradient descent and its stochastic version work, and Lemma 14.7 is the bridge between the Lipschitz assumption of Chapter 12 and the bounded directions the analysis needs. The learning corollaries make the point that runs through Part II of the book: for convex problems, optimization and learning are the same activity, and one pass over the data suffices.
Nothing here is machine-checked. The chapter's statements are essentially correct, and the formalization records the reading choices rather than corrections: the i.i.d.-oracle model of the randomness, the subgradient form of gradient descent, the bound at every point of the ball rather than at a minimizer, and, in Corollary 14.14, the assumptions and under which the derivation from Theorem 14.13 goes through.
Lemma 14.1 is a completed square and a telescoping sum and is the intended entry point; the clause is the substitution of . Corollary 14.2 is Lemma 14.1 with Jensen's inequality for the average and the subgradient inequality at each iterate, plus Lemma 14.7 to bound the directions. The subgradient facts need convex analysis: Lemma 14.3 in the direction "convex implies subgradients exist" is the supporting hyperplane theorem on , which Mathlib does not offer directly; Claim 14.5 uses the first-order characterization of convexity for differentiable functions; Lemma 14.7's "Lipschitz implies bounded subgradients" is the book's one-line argument along . Theorem 14.8 is Lemma 14.1 plus the conditioning argument of the book, which in the i.i.d.-oracle model is Fubini on the product : the iterate is a measurable function of , and integrating over first gives . Theorem 14.11 adds the projection lemma, the strong-convexity inequality of Claim 14.10, the telescoping of and the harmonic sum ; the second-moment hypothesis makes finite inductively. Corollary 14.12 is Theorem 14.8 for with the oracle of (14.13), which requires exchanging a subgradient inequality with the integral over . Theorem 14.13 replaces the Lipschitz bound by self-boundedness, , and rearranges; Corollary 14.14 is its arithmetic under the added assumptions. In all expectation statements the measurability of the iterates in the sample, from the measurability of the oracle, is a routine but necessary lemma.
Iterates are defined by structural recursion, so no argmin is chosen; the sample-driven SGD stops after updates; the projection onto is a chosen nearest point, unique for closed convex . Bounds are stated for every in the ball (or in ) rather than for a minimizer, which is what the proofs give and is stronger. The oracle bound is required surely (the book: with probability ); the almost-sure version is a routine extension. The second-moment hypothesis of Theorem 14.11 is a lower Lebesgue integral, so that a non-integrable oracle cannot satisfy it vacuously. The learning corollaries assume a measurable loss, nonnegative and bounded at the origin, so that the risks are genuine integrals, and a measurable selector of subgradients. Variable step sizes (§14.4.2), other averaging schemes (§14.4.3), SGD for regularized loss minimization (§14.5.3) and the exercises are not stated.
Trivializing readings are excluded: the expectations are over the product law of the examples with measurable integrands, the subgradient conditions are pointwise inequalities, and the iteration counts are the book's. Welcome contributions: Lemma 14.1 as a reusable telescoping lemma, the measurability of the SGD iterates, and the Fubini step that turns an oracle condition into the inequality (14.10).