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.
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?
Planar flows are tame: the Poincaré–Bendixson theorem says that a bounded forward orbit in the plane tends to a fixed point or a periodic orbit. From dimension three on this fails, and the long-time behavior of a flow has to be described through sets rather than single orbits. Chapter 8 of Gerald Teschl's graduate text Ordinary Differential Equations and Dynamical Systems (AMS GSM 140, 2012; author's preliminary version at mat.univie.ac.at) develops two tools for this. The first is the attracting set produced by a trapping region, the device used to show that the Lorenz equation (Lorenz 1963) has an attractor. The second is volume: Liouville's formula for volumes measures how a flow expands or contracts phase space, which shows that the Lorenz attractor has Lebesgue measure zero, and in the special case of a Hamiltonian system gives Liouville's theorem, that the flow preserves volume. Liouville's theorem, with Poincaré's recurrence theorem as its companion, underlies Hamiltonian mechanics and equilibrium statistical mechanics.
This mission states those results for the local flow of a vector field on an open subset of , as in the book.
Let be open and of class . An integral curve of is a differentiable on an open interval with . For each there is a unique maximal one through at time , defined on the open interval . Its value at time is , the flow. The flow is local: may be bounded.
For , the -limit set is the set of for which there are and with . The stable and unstable sets of are , where is the distance to a set. A set is invariant if it contains the full orbit of each of its points. An invariant is attracting if is a neighborhood of . A trapping region is an open connected with compact closure such that for all .
The divergence of is . On phase space , a Hamilton function defines Hamilton's equations , , whose right-hand side is the Hamiltonian vector field . The Lorenz equation is , , with . Volume is Lebesgue measure.
For on an open , with the flow of on , every measurable and every time at which all points of are alive satisfy
The result itself. Liouville's theorem is the basic structural fact of Hamiltonian dynamics. It rules out asymptotically stable equilibria and attractors of positive measure for Hamiltonian systems. It makes Lebesgue measure invariant, which is the starting point of ergodic theory for mechanical systems. Combined with Theorem 8.11, it gives recurrence for any Hamiltonian motion confined to a bounded energy region. Lemma 8.8 is the quantitative version for arbitrary flows: for the Lorenz equation it gives , so the attractor from Lemma 8.5 has measure zero. Lemmas 8.5 and 8.6 produce attractors and show that they contain the unstable manifolds of their points.
Formalizing it. All of these results are classical and proved in the book. Mathlib has the change-of-variables formula, Poincaré recurrence for conservative measure-preserving maps (MeasureTheory.Conservative), and an -limit set for global flows (omegaLimit). It has no flow of a nonlinear ODE with its differentiable dependence on initial conditions, no volume formula along such a flow, and no Hamiltonian formalism. The mission asks for those pieces in the book's local-flow setting, with its hypotheses made explicit.
Lemma 8.8 and Theorem 8.10 need the flow map to be a diffeomorphism of the set of points alive at time onto its image. They also need its Jacobian to satisfy the first variational equation , whose determinant obeys Liouville's formula for linear systems. None of this is available for a general vector field in Mathlib, which provides local existence and uniqueness of integral curves but not differentiability of the flow in the initial condition. Differentiating under the integral also needs uniform control on a compact set of initial points. That is why Lemma 8.8 asks the closure of , not just , to be alive at . Without that, can have infinite volume (, , ).
Lemmas 8.5 and 8.6 are point-set topology. The obstacle there is the local flow: every statement about must first establish that the points involved are alive at time . The book avoids this by assuming completeness at the start of the chapter. For Lemma 8.7, the Liapunov function from the text has , not , so convergence to the origin requires the Krasovskii–LaSalle argument, not a plain Liapunov one.
is EuclideanSpace ℝ (Fin n) and phase space is EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) with points , momenta first. volume on it is Lebesgue measure on . The flow is a pair satisfying IsMaximalFlow, which makes the unique maximal integral curve on . Nothing assumes . The chapter's standing completeness assumption is replaced by explicit aliveness hypotheses, and these are implied by completeness. The explicit readings are:
A trivializing formalization is excluded. The goal is not stated for a complete or globally Lipschitz flow, not for sets of measure zero or bounded open sets only, and not with assumed. It must be proved for the flow of built from itself.
A complete development needs differentiability of the flow in the initial condition and the first variational equation. It also needs Liouville's formula for linear systems, and change of variables for the flow map. Each is reusable beyond this mission; contributions of any of them as separate lemmas are welcome.
Mathlib/Dynamics/Ergodic/Conservative.lean. https://github.com/leanprover-community/mathlib4Most differential equations that model physical, biological or engineered systems cannot be solved in closed form, yet the question asked about them is usually qualitative: does the system settle down to an equilibrium, and does it stay near the equilibrium when perturbed? Liapunov's direct method answers that question without solving the equation, by exhibiting a function that does not increase along solutions. It is the standard tool of nonlinear stability analysis and of control design, where a controller is typically certified by a Liapunov function for the closed-loop system (Khalil, Nonlinear Systems).
A Liapunov function whose values strictly decrease along every non-constant solution gives asymptotic stability directly. In practice the natural candidate, often the total energy of a damped mechanical system, only satisfies a non-strict inequality. The Krasovskii–LaSalle invariance principle closes that gap: if the function is not constant along any complete orbit other than the equilibrium, the equilibrium is still asymptotically stable. It was established by Barbashin and Krasovskii (1952) and by LaSalle (1960, IRE Trans. Circuit Theory 7).
This mission formalizes Chapter 6 of Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012; author's preliminary version), from the local flow of an autonomous equation, through limit sets, to the principle itself.
Fix , an open set (the phase space) and a vector field of class . The autonomous system is . An integral curve is a differentiable map from an open interval into with for all .
For each there is a maximal interval and a unique maximal integral curve on with : every integral curve through at time is a restriction of it. The map on is the flow. It is a local flow: may be bounded, because solutions can leave or blow up in finite time.
The orbit of is and the forward orbit is ( with ). The -limit set is the set of with for some times in ; uses .
A point with is a fixed point. It is stable if every neighborhood of contains a neighborhood of such that solutions starting in exist and stay in for all . It is asymptotically stable if moreover as for all in some neighborhood of .
A Liapunov function at is a continuous on an open neighborhood of with , on , and for every integral curve and all with . It is strict if the inequality is always strict. denotes the connected component of containing .
Let be a fixed point and a Liapunov function at on . Write for: is not constant on any orbit lying entirely in , i.e. every with has points with . Then
and, under , every whose forward orbit lies in a compact subset of satisfies as .
In attack order: Theorem 6.1 (the maximal flow exists, is open, is on , and ); Lemma 6.3 (a forward orbit in a compact subset of forces ); Lemma 6.6 ( is then nonempty, compact and connected); Lemma 6.7 (); Theorem 6.15 (a function non-increasing along is constant on ); Lemma 6.11 (a closed is positively invariant); Lemma 6.12 ( and ); Theorem 6.13 (Liapunov: a Liapunov function makes stable).
The result itself. The invariance principle is the form of Liapunov's method used in applications. It gives asymptotic stability of damped mechanical systems from their energy, of gradient systems from their potential, and of adaptive and passivity-based controllers, where the natural Liapunov function is only non-increasing. Its limit-set formulation (Theorem 6.15) is also the entry point to the Poincaré–Bendixson theory of the next chapter, which uses the same -limit sets.
Formalizing it. Mathlib has local existence and uniqueness for ODEs and a theory of -limit sets for global flows (omegaLimit, Flow). It has no maximal solution of an ODE, no local flow with its maximal intervals, and no Liapunov stability theory. The results are classical and proved in the book; none has a machine-checked proof on this platform. This mission builds the local-flow and limit-set layer and the Liapunov layer on top of it.
The central difficulty is that the flow is local. The book's arguments pass freely between "the solution stays in a compact set" and "the solution exists for all positive time" (Lemma 6.3). In a formal setting every statement about must first establish , and the maximal interval must be constructed from local solutions. Theorem 6.1 on its own requires gluing local solutions into a maximal one and proving that the domain is open with dependence on initial conditions.
A common first idea is to assume the vector field is complete, so that Mathlib's global Flow and omegaLimit apply directly. That assumption is not available: the goal concerns orbits that stay in the neighborhood , and completeness of such orbits is a consequence of the argument, not a hypothesis. Similarly, is only continuous, so a derivative-based criterion cannot replace condition (6.36).
The state space is EuclideanSpace ℝ (Fin n), so is the Euclidean norm, and is the open ball Metric.ball. The standing assumption , , open, is a binder of every theorem (as ContDiffOn ℝ 1 f M, the weakest case, and for general in Theorem 6.1). The flow enters as a pair (I, Φ) satisfying IsMaximalFlow f M I Φ, which characterizes the maximal integral curves uniquely. Theorem 6.1 proves that such a pair exists, so no completeness or extra regularity is assumed. The two time directions of Lemmas 6.3–6.7 are one statement with a real parameter σ = 1 ∨ σ = -1. The -limit set contains only points of , as in the book.
Stability conclusions include existence of the solution for all . The Liapunov condition quantifies over every integral curve and constrains only the two endpoint values, exactly as (6.36). is a total function whose values off are never read.
Correction to the printed statement. The book's final sentence of Theorem 6.14, "every orbit lying entirely in converges to ", is false as printed. With and a strict Liapunov function, some orbits escape to infinity (Khalil, §4.1). The goal therefore asks for convergence of every forward orbit contained in a compact subset of , which is what the book's argument uses. The other two parts are as printed.
A trivializing formalization is ruled out: stability and asymptotic stability are stated for the maximal flow, with existence for all required, and not for an arbitrary map Φ or a flow assumed global. Asymptotic stability keeps both conjuncts, stability and attraction.
Needed infrastructure: maximal solutions of autonomous ODEs and their continuation (reusable across Chapters 6–13), openness of and smooth dependence on initial data, compactness arguments for limit sets, and connected components of sublevel sets. Contributions of the local-flow layer as standalone lemmas are especially welcome, since later missions of this series rely on the same objects.
Separation of variables reduces the heat equation, the wave equation and the Schrödinger equation on an interval to an eigenvalue problem for a second-order ordinary differential operator with boundary conditions at both ends. Whether the method works depends on one fact: the eigenfunctions of that operator must be complete, so that every reasonable initial profile can be expanded in them. Chapter 5 of Gerald Teschl's Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012) proves this for regular Sturm–Liouville problems. It does so without Lebesgue integration or Hilbert-space completeness: it works in the space of continuous functions with a weighted scalar product, and it develops the necessary spectral theory of compact symmetric operators from scratch.
A short history. Sturm and Liouville (1836–1837) studied the zeros and the eigenvalues of such equations and the expansion of functions in eigenfunctions. Hilbert and Schmidt (1904–1907) put the expansion on a rigorous footing through their theory of integral equations with symmetric kernels, from which the abstract spectral theorem for compact symmetric operators emerged.
Let and let be real functions on with
These regularity assumptions hold throughout. The Sturm–Liouville operator is
acting on the domain
for fixed real (the separated boundary conditions; is Dirichlet, Neumann). The underlying space is with the weighted scalar product
and norm . is an inner product space but it is not complete. A number is an eigenvalue of if for some that does not vanish identically; is an eigenfunction. An orthonormal basis of is an orthonormal sequence such that for every .
For the abstract part, is any complex inner product space (again not assumed complete). A linear operator on a dense subspace is symmetric if ; an everywhere defined is compact if has a convergent subsequence in whenever is bounded.
For let , solve with , , , . Their Wronskian is , which does not depend on the point where it is evaluated. When , the resolvent is the integral operator with the Green function and weight .
There are real numbers and real-valued eigenfunctions , , such that:
Theorem 5.11 is the statement that makes eigenfunction expansions legitimate: Fourier sine and cosine series are its special case , , and it covers any positive weight and any smooth positive stiffness with separated boundary conditions. Solutions of the heat and wave equations on an interval with variable coefficients are built from it. The uniform convergence for is the version needed to differentiate or evaluate such series pointwise. Lemma 5.12 provides the variational characterisation of the lowest eigenvalue, the starting point for comparison theorems and eigenvalue estimates.
On the formal side, Mathlib has the spectral theorem for self-adjoint operators on finite-dimensional spaces, compact operators on normed spaces, and spaces. It has no Sturm–Liouville theory, no Green functions for boundary value problems, and no spectral theorem for compact symmetric operators on incomplete inner product spaces. The platform has finite-dimensional Rayleigh-quotient results and compactness of convolution operators, but nothing on this setting. The results here are classical and proved; what is missing is a machine-checked proof in the book's elementary setting of continuous functions.
The operator is unbounded on (Problem 5.16), so the obvious first idea, applying a spectral theorem for compact or bounded symmetric operators to itself, does not work. Completeness of the eigenfunctions is also subtle because is not complete. Hilbert-space arguments that produce limits in a completion, or that go through , do not by themselves give an expansion of a continuous function in continuous eigenfunctions with convergence in , still less uniform convergence. Simplicity of the eigenvalues depends on the separated boundary conditions and fails for periodic ones. On the formal side, one needs analytic dependence of solutions of a linear ODE on a complex parameter, one-sided derivatives at the endpoints, and interval integrals of piecewise-defined kernels.
[NormedAddCommGroup E] [InnerProductSpace ℂ E] and no CompleteSpace. Symmetry on a dense domain is IsSymmetricOp; for everywhere defined operators it is Mathlib's LinearMap.IsSymmetric. Compactness is IsCompactOp: subsequences converge in itself. is represented by functions continuous on Set.Icc a b, with SLInner the weighted scalar product (5.52) as an interval integral. It is not and not a HilbertBasis.SLOp, SLDomain, IsSLEigenfunction implement (5.53)–(5.55) with derivWithin on Set.Icc a b (one-sided at the endpoints) and ContDiffOn ℝ 2. RegularSL is (5.45), including . are arbitrary reals.IsLUB of , and Theorem 5.5 assumes . In Theorem 5.6, is ℕ∞: in infinite dimension and otherwise. The minima of Lemma 5.12 are IsLeast (attained), and "equality iff " reads as "iff is an eigenfunction for ", i.e. with . is . Norm convergence is .A complete development needs linear ODEs with a complex parameter and their analytic dependence on it, Green functions, an Arzelà–Ascoli argument in , and the spectral theorem for compact symmetric operators on an inner product space. The definitions RegularSL, SLOp, SLDomain, SLInner and SLWronskian are reusable for the oscillation and comparison theory (Theorems 5.17–5.25) in the rest of the chapter. Contributions connecting IsCompactOp to Mathlib's IsCompactOperator on the completion are welcome.
The -server problem is a basic model of on-line decision making. mobile servers move in a metric space, requests for points arrive one at a time, and each request has to be covered by a server before the next one arrives. The cost is the total distance the servers move. The problem includes paging, caching and disk-head scheduling as special cases (Manasse, McGeoch, Sleator 1990). An on-line algorithm is judged by its competitive factor: how much its cost can exceed that of an off-line algorithm that knows the whole request sequence in advance.
For randomized algorithms against an oblivious adversary (one that fixes the whole request sequence before the algorithm flips any coins), the best-understood case is paging, which is the -server problem on a uniform metric space. There the optimal factor is the harmonic number . Fiat et al. proved the lower bound (1991) and McGeoch and Sleator the matching upper bound (1991). Karlin, Manasse, McGeoch and Owicki (Algorithmica 11, 1994, §5) asked whether -competitive algorithms also exist when the metric space is not uniform. They answered no, already for two servers on three points: on certain triangles the optimal randomized factor is strictly larger than . This mission formalizes their Theorem 13, which gives the exact optimal factor on the triangle with edge lengths 3, 4 and 5.
Timeline:
Let be a metric space with exactly three points , where , and . A configuration gives the positions of two labelled servers in . A request sequence is a finite list of points of .
A deterministic on-line algorithm assigns to each prefix of a request sequence a configuration, in which the last request is covered. Its configuration after a prefix therefore cannot depend on later requests. Its initial configuration is the one it assigns to the empty prefix, and its cost on is the total distance its servers move while serving request by request.
The optimal off-line cost from an initial configuration is the infimum, over all schedules that start at and cover each request of in turn, of the total distance moved.
A randomized on-line algorithm is a probability distribution over deterministic on-line algorithms, all starting at . The cost on each fixed is required to be measurable in the random choice, and is the expected cost. is -competitive against an oblivious adversary if there is a constant such that for every request sequence ,
These are the definitions of p. 543 of the paper. They are the platform's published KServer_model and KServer_randomized, which this mission reuses unchanged: KServer.RandomizedAlgorithm 2 M and A.IsCompetitiveFrom C₀ ρ.
For every initial configuration of the two servers,
The first claim is quantified over all randomized algorithms, so it also covers deterministic ones (point masses). The second claim asks for one algorithm. Together they say that is the exact optimal randomized factor on this triangle.
Every real solution has . 2. The LP attainment (p. 568). The paper's printed probabilities lie in , and with suitable potentials they satisfy all twelve constraints at . 3. Theorem 13, first claim: the lower bound for every randomized algorithm. 4. Theorem 13, second claim: a -competitive randomized algorithm exists.
The result. Theorem 13 shows that the behaviour of randomized paging does not carry over to general metric spaces. Two servers on a three-point space already force a factor above . The value is exact, which makes this triangle a test case for any general theory of randomized -server algorithms on small metric spaces. With Theorem 12 (the isosceles triangles, a companion mission of this series), it is one of the few non-uniform metric spaces with a known optimal randomized factor.
Formalizing it. The result has been proved since 1994. To our knowledge there is no machine-checked proof. The paper derives both bounds from two framework theorems for phase-based algorithms: Theorem 3 (an LP lower bound for phase-based algorithms bounds every algorithm) and Theorem 2 (a lazy phase-based algorithm with LP bound is -competitive). The phase tables themselves (which phases can occur and what they cost) are stated without detailed proof. A formal proof has to supply both framework arguments for this space and verify the phase tables, as well as the finite linear algebra of milestones 1 and 2. The milestones isolate the exact-arithmetic core so that it can be closed independently of the probabilistic part.
The two LP milestones are finite exact-arithmetic facts. The hard part is linking them to Theorem 13.
For the lower bound, an algorithm need not be phase-based at all. Its probabilities may depend on the whole history, not only on the current phase, and it may leave the configuration of the off-line optimum at the end of a phase. The obvious attempt is to fix one hard request sequence and compare costs, but that cannot work: randomization defeats any single sequence. The reduction from arbitrary algorithms to phase-based ones (the paper's Theorem 3) is the substantive step.
For the upper bound, the printed probabilities describe the algorithm's marginal position after each prefix of a phase. They have to be realized as a single probability distribution over deterministic on-line algorithms that is lazy (it moves only to serve a request) and whose expected cost per phase equals the table's entry. On top of this, the LP accounting has to be turned into a bound on arbitrary request sequences, including partial phases and a start away from the optimum's configuration.
KServer_model and KServer_randomized are used unchanged. Servers are labelled (Config 2 M = Fin 2 → M). A deterministic algorithm is a function of the request prefix, which makes it on-line by construction. A randomized algorithm is a mixed strategy with a probability measure and a measurability field, and its expected cost is the lower Lebesgue integral of the nonnegative cost. The off-line optimum is a real infimum over schedules from ; the set is nonempty and bounded below by . Competitiveness allows any real additive constant.The k-server problem of Manasse, McGeoch and Sleator (J. Algorithms 11 (1990)) asks how mobile servers in a metric space should respond, on-line, to a sequence of requests at points of the space, each of which must be covered by a server. It is the central model of on-line computation: paging is the special case of a uniform metric, and many caching and scheduling problems reduce to it. For two servers the deterministic picture is complete: the optimal competitive ratio is on every metric space with at least three points.
Randomization changes the picture, and the smallest nontrivial case already shows how. On the equilateral triangle the optimal randomized ratio against an oblivious adversary is . Karlin, Manasse, McGeoch and Owicki (Algorithmica 11 (1994) 542–571) computed the exact optimal randomized ratio for several nonuniform triangles, where the distances differ, and showed that it depends on the geometry. Their Theorem 12 settles the whole family of isosceles triangles with edge lengths , , . These exact values are among the few known optimal randomized ratios for server problems.
Timeline:
Fix an integer . The isosceles triangle has three points , , with
A configuration places two labelled servers on points of . A deterministic on-line algorithm assigns to every finite request sequence a configuration, computed from alone and covering the last request; its value on the empty sequence is its initial configuration. Its cost is the total distance its servers move while serving request by request. The off-line optimum from an initial configuration is the least total movement of any schedule that starts at and covers each request in turn, knowing in advance.
A randomized algorithm is a probability distribution on deterministic on-line algorithms; its expected cost is . It is -competitive against an oblivious adversary from if every algorithm in its support starts at and there is a constant such that
The request sequence is fixed in advance and does not react to the algorithm's coin flips.
Write and
In Lean this is NonuniformCompetitive.Isosceles.isoscelesRatio d.
For every and every initial configuration :
The two claims are also milestones of their own (no_better_ratio, ratio_attained).
For free real and real with
one has (lp_lower_bound); and , is nondecreasing from to and makes every constraint an equality (lp_attained).
(ratio_increases_to_e_ratio).
The theorem gives an exact optimal randomized ratio for an infinite family of metric spaces. It shows that the optimal randomized two-server ratio is not a constant: it runs from on the equilateral triangle to as the triangle becomes long and thin, where the problem resembles ski rental. With the deterministic ratio , it quantifies exactly how much randomization gains on these spaces.
The results are proved in the paper; none is formalized on Prove2Me, and no machine-checked proof of them is known. A formal proof would require the paper's phase framework (Theorems 1–3 and the appendix's Theorem 15) for server problems, which this mission does not state separately, and a concrete randomized algorithm as a measurable mixed strategy. Both would be reusable for Theorem 13 (the 3-4-5 triangle) and for other exact ratios on small metric spaces.
The phase LP milestones are finite real arithmetic. The difficulty is the passage between them and the goal. The lower bound must hold for every randomized algorithm, not only phase-based lazy ones: an arbitrary algorithm may condition on the whole history, move non-lazily, and randomize in ways that do not reduce to the probabilities . The paper handles this with Theorem 3, which says that the LP bound of phase-based algorithms bounds the competitive factor of all algorithms; its proof uses an averaging argument over histories that must be made rigorous. The upper bound needs a mixed strategy over infinitely many phases, with measurable costs, an explicit additive constant covering the first partial phase from an arbitrary initial configuration, and an accounting of across phase boundaries.
The model is the platform's published KServer_model and KServer_randomized (reference items): labelled servers Fin 2 → M; a deterministic on-line algorithm as a map from request prefixes to configurations; a randomized algorithm as a probability measure over deterministic algorithms, with the cost of each fixed sequence measurable in the random outcome; expected cost as a lower Lebesgue integral in ; the off-line optimum as a real infimum over schedules from (nonempty and bounded below by ); and IsCompetitiveFrom A C₀ c with a real additive constant.
Committed conventions:
Without the measurability field of a randomized algorithm the lower integral would under-report expected cost and the attainment claim would become easier than the paper's; the published definition includes it. The lower bound is not vacuous: the triangle hypotheses are satisfiable for every .
Welcome contributions: a formal version of the phase framework (Theorems 1–3, 15) for finite metric spaces, reusable across missions III and IV; a measurable construction of phase-based randomized algorithms; and proofs of the LP milestones.
Almost every quantitative statement about an ordinary differential equation, from the stability of an equilibrium to the existence of a periodic orbit, presupposes that the equation has a solution through each initial point and, usually, that this solution is unique and depends continuously on the data. Chapter 2 of Gerald Teschl's graduate textbook Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012) establishes these facts for first-order systems in . It is the foundation for the rest of the series: the flows, limit sets, Poincaré maps and invariant manifolds of later chapters are all built on the existence, uniqueness and extension results proved here.
A short history. Local existence was first proved in the nineteenth century by polygonal approximation (Cauchy) under differentiability-type hypotheses. Lipschitz isolated the condition that bears his name. Picard and Lindelöf established existence and uniqueness by successive approximation, and Banach (1922) abstracted the argument into the contraction principle. Peano (1890) showed that continuity of the right-hand side alone suffices for existence, without uniqueness. Gronwall's inequality and its integral generalisations give the continuous dependence estimates. Teschl's chapter presents all of these in a uniform notation.
An initial value problem (IVP) is
where is a continuous map from an open set to and . Here is the Euclidean norm on . A solution on an interval is a function whose graph lies in and which is differentiable on (one-sidedly at an endpoint that belongs to ) with . Such a solution is automatically continuously differentiable.
The function is locally Lipschitz in the second argument, uniformly with respect to the first, if for every compact there is a constant with whenever (the book's (2.18)).
For let , where , let , and define the existence time
The chapter also works in a real Banach space , a complete normed real vector space, where a contraction of a closed set is a map with for some .
If is continuous on and , then there is a function with solving
and the analogous statement holds on with . No Lipschitz condition is assumed and the solution need not be unique.
Peano's theorem is the existence statement with the weakest regularity hypothesis on in the classical theory. It is what lets one speak of solutions of equations with non-Lipschitz right-hand sides, such as , and it is the starting point for the theory of non-unique solutions and differential inclusions. The explicit existence time is the quantitative form used whenever one needs a uniform lower bound on the lifetime of solutions starting in a compact set. Picard–Lindelöf, Gronwall and continuous dependence together make the IVP well posed. The global existence theorem under linear growth is used throughout the later chapters to define global flows.
Mathlib already contains a Picard–Lindelöf theorem (IsPicardLindelof), Gronwall's inequality in differential form, the Banach fixed point theorem for complete (extended) metric spaces, and an Arzelà–Ascoli theorem for bounded continuous functions. It does not contain Peano's theorem, the integral form of the generalised Gronwall inequality with variable , Weissinger's theorem, or global existence under linear growth. The statements here are phrased in the book's setting: one-sided intervals, the convention for , local Lipschitz conditions on an open set, -valued functions. Connecting them to the existing Mathlib results is part of the work.
For Peano's theorem the obvious approach, Picard iteration, does not apply. Without a Lipschitz condition the integral operator need not be a contraction on any ball, its fixed points need not be unique, and a sequence of approximate solutions need not converge. Any argument has to produce a solution without a uniqueness mechanism and still reach the full interval that the theorem specifies, not merely some shorter one. On the formal side, derivatives relative to closed intervals, the corner of , and passing between the differential and the integral form of the IVP all need care.
For Theorem 2.17 the difficulty is that "every solution is defined on all of " is a statement about maximal solutions, and the book defines these only through a gluing construction. Without a Lipschitz condition that construction is no longer unique. An a-priori bound on alone does not give extension beyond a finite endpoint.
EuclideanSpace ℝ (Fin n), so is the Euclidean norm. The right-hand side is a total function ; hypotheses restrict attention to or . Banach spaces are real normed spaces with CompleteSpace.IsSolutionOn U f I x: for every , and has derivative at relative to . Initial conditions are separate hypotheses.IsGreatest {|f(p)| : p ∈ V} M. is if M = 0 then T else min T (δ / M). "Some interval around " in Theorem 2.2 is with , and "unique" means uniqueness on every interval containing . In Theorem 2.8 the suprema , of (2.41) become arbitrary constants , bounding the same quantities, which is equivalent because the bound is monotone in both; the case uses the limit . In Theorem 2.17 the constants are existential inside , so they may depend on but not on . "All solutions are defined for all " means that every solution on an open interval extends to a solution on .A complete development needs derivatives within intervals, interval integrals, uniform convergence and compactness in . The definitions IsSolutionOn and LocallyLipschitzSecond are reused throughout the Teschl series. Contributions that connect these statements to Mathlib's IsPicardLindelof, ContractingWith and BoundedContinuousFunction.arzela_ascoli are welcome.
In spectral theory the resolvent of a self-adjoint operator is studied through scalar functions , defined for non-real . Each is holomorphic on the upper half plane and maps it into itself. The spectral theorem, in the form presented in G. Teschl's Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), comes down to the converse: a function of this kind with the right growth is the Cauchy–Stieltjes transform of a finite measure on , and that measure is the spectral measure of . In the other direction, the absolutely continuous, singularly continuous and pure point spectra of Schrödinger operators are identified by looking at the boundary values of on the real axis. This mission formalizes the appendix to Chapter 3 of Teschl's book (Section 3.4, The Herglotz theorem, pp. 106–110) and Theorem 3.10, the measure-theoretic layer that the rest of the book's spectral analysis stands on.
The representation goes back to G. Herglotz (1911) for the disc and R. Nevanlinna (1922) for the half plane. The inversion formula is due to T. J. Stieltjes (1894). The link between boundary values and the Lebesgue decomposition of the measure is classical harmonic analysis on the half plane (Fatou, de la Vallée Poussin) and is the tool behind the spectral-type results of Gilbert–Pearson subordinacy theory and Aronszajn–Donoghue rank-one perturbation theory.
Write . A Herglotz function
is a holomorphic map on with for every
(IsHerglotz).
For a Borel measure on , its Borel transform is
(borelTransform μ). The spectrum of is its set of growth points,
(measureSpectrum).
With and Lebesgue measure, the
upper and lower derivatives of are
and
,
values in (upperDeriv, lowerDeriv). The derivative is the limit
when it exists, possibly (HasMeasureDeriv μ x d).
A set is a support of if (IsSupport). A support
is a minimal support if every Borel with is Lebesgue-null
(IsMinimalSupport). The Lebesgue decomposition with respect to
Lebesgue measure refines to , where lives on the atoms of
. The absolutely continuous part and the singularly continuous part
are acPart μ and scPart μ.
If is a Herglotz function and for all , then there is a Borel measure on with and
Theorem 3.20 together with Theorem 3.10 is a bijection between finite Borel measures on and Herglotz functions of bounded growth . In Teschl's development it produces the spectral measures from the resolvent, and hence the projection-valued measure of an unbounded self-adjoint operator. Theorems 3.21–3.25 turn spectral questions into boundary-value questions. The later chapters on Sturm–Liouville operators and one-dimensional Schrödinger operators decide which spectral type an operator has by reading for the Weyl–Titchmarsh function.
These are textbook results with complete published proofs. Mathlib has the upper half plane as a type, Lebesgue decomposition, Radon–Nikodym derivatives and Vitali-family differentiation of measures, but it has no Borel (Cauchy–Stieltjes) transform of a measure on , no Herglotz representation on the half plane, and no Stieltjes inversion. The remaining work is to formalize the known proofs against Mathlib's measure theory and complex analysis. No machine-checked version of these statements is known to exist on Prove2Me.
For the goal, the measure has to be built: nothing in the hypothesis names it. A Herglotz function gives no measure directly, only a family of absolutely continuous approximations coming from the boundary values of slightly above the real axis. The difficulty is to pass to a limit that is only a measure (it may have atoms and singular parts), and to identify the limit's transform with itself, not just its imaginary part. The uniform bound is what makes the limit exist and keeps its mass at most . Without it the general Nevanlinna representation carries an extra linear term and a non-finite measure, and the statement here fails.
For the boundary-value theorems, the pointwise behaviour of the Poisson integral has to be compared with the symmetric derivatives of at each point, including points where is singular. The almost-everywhere statements for both and Lebesgue measure need the differentiation theory of measures in its singular form: the derivative is infinite -almost everywhere, not only finite Lebesgue-almost everywhere.
Measures are MeasureTheory.Measure ℝ on the Borel σ-algebra. Every theorem assumes
IsFiniteMeasure μ, except the goal, whose conclusion μ Set.univ ≤ ENNReal.ofReal M makes
μ finite. Functions on the half plane are ℂ → ℂ, constrained only on {z | 0 < z.im}. The
Borel transform is a Bochner integral. Every claim evaluates it where the integrand is bounded,
so Mathlib's convention that a non-integrable integral is never enters.
Limits as are taken along 𝓝[>] 0. The quantities that may be infinite
(derivatives of measures, boundary values of ) live in ℝ≥0∞, with
, which is nonnegative for , embedded
by ENNReal.ofReal. An infinite limit of itself is Tendsto … (Bornology.cobounded ℂ). The
lower and upper derivatives, the supports and the parts , are defined in
the mission's namespace exactly as in the book (Sec. A.8, Sec. 3.2).
Three readings of the printed text are fixed. Theorem 3.22 is stated for , which is what its proof estimates. Theorem 3.23's identity takes the factor once, consistent with Theorem 3.22. Theorem 3.10's Herglotz conclusion is stated for : the book's Herglotz functions map into the open half plane, and the zero measure's transform is identically zero.
A Herglotz function is defined analytically (holomorphic, positive imaginary part), never as "a Borel transform"; the latter would make the goal a tautology. No object is taken as data. The chunk uses no Hilbert space, no operator, and no projection-valued measure.
Useful infrastructure: UpperHalfPlane, Cauchy's integral formula on rectangles and
semicircles, weak compactness of finite measures on (Helly/Prokhorov), Mathlib's
VitaliFamily.ae_tendsto_rnDeriv and Measure.singularPart. A reusable Poisson-kernel library
for the half plane would be a welcome by-product, as would the vague-convergence lemmas of the
book's Appendix A.
Fictitious play is the oldest model of learning in games: each player repeatedly best-responds to the empirical frequencies of the opponents' past play. Stochastic fictitious play adds random payoff disturbances before each choice, so that players choose smoothed ("perturbed") best responses. It is a standard model in economics and in the study of learning in games (Fudenberg and Levine, 1998), and its long-run behavior is described through a deterministic mean dynamic, the perturbed best response dynamic, using stochastic approximation theory (Benaïm and Hirsch, 1999).
Supermodular games model strategic complementarities: the gain from moving to a higher strategy increases when opponents move to higher strategies. They arise in coordination, oligopoly and macroeconomic models (Milgrom and Roberts, 1990; Vives, 1990). Hofbauer and Sandholm (Econometrica 2002) show that in such games stochastic fictitious play converges almost surely whenever its mean dynamic has a unique rest point. This mission formalizes that result and the chain of lemmas behind it (Section 5 and the Appendix of the paper).
Timeline. Benaïm and Hirsch (1999) observed that supermodular games with exactly two strategies per player yield strongly monotone perturbed best response dynamics. Hofbauer and Sandholm (2002) extended this to any number of strategies by introducing stochastic dominance coordinates, and proved Theorem 6.1(iv). Benaïm (2000) supplied the low-dimensional convergence theorem used for the dimension ≤ 2 clause.
A player normal form game gives player an ordered finite strategy set and a utility on pure profiles. is the set of mixed profiles, and player 's payoff vector is .
The game is strictly supermodular if for all distinct players and all profiles with and , the difference is strictly increasing in .
Each player has a shock density on , strictly positive, whose choice function is continuously differentiable. The perturbed best response is , and the perturbed best response dynamic is
is its set of rest points in and its chain recurrent set.
In standard stochastic fictitious play the shocks have densities and are independent over time and across players. From an arbitrary initial pure profile , each player at time plays the pure strategy maximizing , where is the vector of empirical frequencies.
The stochastic dominance coordinates are , the mass on strategies above ; means each stochastically dominates . In these coordinates (P) becomes a dynamic (T) on .
For a strictly supermodular game with players and shock densities as above, if then
on every probability space, for every independent shock family with the given densities and every initial profile.
The result gives global almost-sure convergence of a stochastic learning process in a broad class of games with many strategies, where earlier results needed two strategies per player or specific payoff structures. It also shows which properties of the choice function matter: only eqs. (17)–(18), not the symmetry of its derivative used for potential and zero-sum games.
The paper's proof is complete but relies on outside results: stochastic approximation (Benaïm–Hirsch 1999, Benaïm 1999), monotone dynamical systems (Smith 1995), and the inclusion of the chain recurrent set in the global attractor (Robinson 1995). None of these, nor the Hofbauer–Sandholm theorem itself, is formalized in any proof assistant as far as known. The mission produces a machine-checked version of the theorem and of the Section 5 monotonicity theory.
The monotonicity lemmas are finite-dimensional calculus and summation by parts. The substantial steps are elsewhere. Strong monotonicity of a cooperative irreducible system (Corollary 5.5(i)) is a theorem of monotone dynamical systems that Mathlib does not have, and it must hold on the closed, non-open state space . The step from the ODE to the random process needs the stochastic approximation theorem: the empirical frequencies are an asymptotic pseudotrajectory of (P), and their limit set is almost surely internally chain transitive. Knowing that is globally asymptotically stable for (P) does not by itself give almost-sure convergence of . The limit set of the random process must be related to the chain recurrent set of (P), which is where Corollary 5.5(ii) enters.
Players are Fin p, strategies Fin (n α) (0-based, same order as the paper), with every . Mixed profiles live in the ambient space with the sup norm. The fields of (P) and (T) are defined on the whole ambient space, so partial derivatives are ordinary Fréchet derivatives. Densities are -valued. Solutions are forward solutions staying in the state space. The chain recurrent set quantifies over solutions, which are unique here because the fields are . The process is defined pathwise from the shocks, with ties in the argmax broken by the smallest index (a null event). Densities may differ across players.
A statement about the ODE (P), or about a single noise law such as logit, would be a different and much weaker theorem. The goal is about the random process , on every probability space carrying independent shocks with the given densities. Irreducibility and strong monotonicity additionally assume that two distinct players each have at least two strategies; when one player owns every stochastic dominance coordinate and has at least two of them, supermodularity holds vacuously while irreducibility fails.
A complete development needs: random utility choice functions and their derivatives; monotone and cooperative ODE theory on convex sets; the chain recurrent set and the global attractor; stochastic approximation for processes with step size . The last three are reusable well beyond this mission. Contributions to any milestone, and general-purpose lemmas on cooperative systems or stochastic approximation, are welcome.
This mission continues chapter 10's algorithmic account across its remaining two sections:
finishing the Iwata-Fleischer-Fujishige fixing algorithm for submodular minimization (§10.2.3's
tail), the steepest descent algorithm for L-convex function minimization (§10.3), and — the
capstone of chapter 10's account of the M-convex submodular flow problem (§10.4) — conjugate
scaling, the operation that finally makes the primal-dual algorithm run in polynomial time. As in
mission 34-ch10b-algorithms, most of this block's numbered results are asymptotic complexity
bounds; this mission places the results that are ordinary mathematical propositions.
The IFF fixing algorithm (mission 34-ch10b-algorithms) builds an acyclic graph D=(U,F)
and partition Z,H,Γ certifying the maximal minimizer of a submodular ρ once η≤0 (Eq.
(10.26)); this mission places the case-independent inequality its own legitimacy rests on, and
restates its correctness conclusion. The steepest descent algorithm for an L-convex function
g repeatedly minimizes the submodular set function ρ_p(X)=g(p+χ_X)-g(p) and moves to
p+χ_X for its minimal minimizer X (the tie-breaking rule (10.33)); this mission places the
resulting monotonicity fact and a domain-size bound for the L-convex adaptation.
Conjugate scaling replaces a dual-integral M-convex function's conjugate g with
g_α(p)=g(αp)/α, defining f⟨α⟩ via the resulting sup-formula (Eq. (10.77)) — a scaling
operation compatible with M-convexity where the naive ⌈f(·)/α⌉ is not.
For a dual-integral polyhedral M-convex function f (represented as the mixed real-primal/
integer-dual conjugate of an L-convex g), the conjugate scaling f⟨α⟩ is again
dual-integral M-convex, witnessed by g_α itself being L-convex, provided f⟨α⟩>-∞.
Chosen as goal: this is the fact the whole conjugate scaling algorithm — chapter 10's final and
most refined algorithm for the M-convex submodular flow problem — depends on, and the book's own
text singles it out as the "compatible scaling operation" that makes M-convex cost scaling work
where a naive approach provably does not.
Proposition 10.26 (the case-independent inequality underlying the IFF fixing algorithm's own
legitimacy) and Proposition 10.28 (that algorithm's correctness conclusion) close out mission
34-ch10b-algorithms's coverage of §10.2.3. Proposition 10.30 gives the steepest descent
algorithm's monotonicity property under its tie-breaking rule; Proposition 10.32 (found by direct
reading) bounds the L-convex adaptation's domain-size parameter in terms of the
original function's.
Conjugate scaling is chapter 10's demonstration that M-convexity, while a combinatorial rather
than a numeric-magnitude notion, still admits a genuine scaling technique compatible with its own
structure — completing the book's account of the M-convex submodular flow problem with an
algorithm whose polynomial running time depends on exactly this compatibility. Propositions
10.26/10.28 complete the correctness/legitimacy argument for the strongly polynomial submodular-
minimization algorithm mission 34-ch10b-algorithms began placing, and Propositions 10.30/10.32
are the analogous structural facts for L-convex function minimization, chapter 10's third major
algorithmic thread.
None of these results are open — they are Murota's own account of submodular-function- minimization (§10.2 continued), L-convex minimization (§10.3), and conjugate scaling (§10.4.5). What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Proposition 10.32) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).
As in mission 34-ch10b-algorithms, several numbered results in this block are excluded as
hard for being pure algorithmic-complexity bounds (Propositions 10.25, 10.27, 10.31); see
HARD.md. A further three (Propositions 10.37-10.39, on the primal-dual algorithm's maximum
submodular flow subproblem) are excluded for a distinct reason: the source text's own OCR
extraction demonstrably cannot distinguish the two visually different capacity-bound symbols
(c* overlined vs. underlined) central to their shared defining formula, confirmed directly
against the raw extracted bytes, making faithful reconstruction of that formula impossible from
the available text; see HARD.md.
Ground-set elements are a Fintype V with DecidableEq. All apparatus needed for Propositions
10.26/10.28 (Submodular, GammaSet, RhoTilde, ReachSet, Eta, IsMaximalMinimizer) is
redeclared fresh from mission 34-ch10b-algorithms, genericized over an arbitrary ground type
where the original was V-specific, since this draft cannot import that sibling. Proposition
10.26 is placed as the case-independent core inequality its own proof establishes, rather than by
replicating the three-case verification against Proposition 10.24's own internal proof objects
(Cases (i)-(iii)); see HARD.md. Proposition 10.30 omits its own trailing iteration-count
corollary (a pure complexity bound); see HARD.md. Six numbered results (Propositions 10.25,
10.27, 10.31, 10.37, 10.38, 10.39) are hard. Contributions completing any of the five sorrys
are welcome; the goal carries the most independent proof content (via the conjugacy theorem and
Theorem 7.10(2), both established elsewhere in this series).
34-ch10b-algorithms's own Proposition 10.24).In the capacitated vehicle routing problem (CVRP) a fleet of vehicles of capacity leaves a depot and serves customers; every customer is visited once, and the load of each route must not exceed . In practice customer demands are uncertain at planning time. The chance-constrained CVRP asks that each route respect the capacity with probability at least , but this presupposes a known demand distribution, which is rarely available. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) require the chance constraints to hold for every distribution in an ambiguity set built from the information that can actually be estimated: support, means and dispersion bounds.
Their branch-and-cut method separates rounded capacity inequalities whose right-hand side is the worst-case value-at-risk of the total demand of a customer set . This quantity is evaluated thousands of times during the search, so it matters whether it has a closed form or a small convex reformulation. This mission concerns the paper's covariance ambiguity sets (§5.2), which bound the whole covariance matrix of the demands and can therefore express that demands of nearby customers are correlated, as happens with geographically clustered demand. The covariance bound can be derived from data, for example analytically through McDiarmid's inequality (Delage and Ye, 2010) or by bootstrapping.
Customers are indexed by and their random demand vector is . Fix a box with , a mean vector in the interior of , and a symmetric positive definite matrix . The covariance ambiguity set is
where is the set of all probability distributions on and means that is positive semidefinite.
For a distribution and a real random variable , the value-at-risk at level , , is . For a customer set , the worst-case value-at-risk is . A route serving satisfies the chance constraint for every exactly when this number is at most .
Two componentwise bounds appear in the answer:
A route set is an ordered partition of the customers into nonempty ordered routes. It is feasible in the distributionally robust problem RVRP() if every route satisfies the chance constraint for every , and feasible in a deterministic instance with capacity and demands if every route's total demand is at most .
For every customer set ,
The right-hand side maximizes an affine function over the intersection of an ellipsoid and a box.
For a diagonal bound , program (17) collapses to a search over one parameter with :
over the for which the first bracket is nonnegative and the point of (17) that induces respects (see Formalization scope).
For some instance with the ambiguity set (16), no deterministic CVRP instance on the same customers and fleet has the same set of feasible route sets.
Theorem 7 makes the worst-case value-at-risk over (16) computable in polynomial time as a convex quadratically constrained program. With it, the rounded capacity inequalities of the two-index vehicle flow formulation can be separated for covariance information. Theorem 2 of the same paper shows that the resulting demand estimator is subadditive, so this formulation is exact. Corollary 4 gives a closed form for the diagonal case, which the paper uses to evaluate the estimator in time linear in after sorting. Theorem 6 explains why the paper needs this machinery: the robust feasible region cannot be reproduced by any deterministic demand vector and capacity.
The results are proved in the paper's online supplement. No part of them is formalized anywhere to our knowledge; the platform has no worst-case value-at-risk and no moment-based ambiguity set. A complete development would give machine-checked worst-case VaR bounds over moment sets with second-order information. These are used well beyond routing, in distributionally robust portfolio and inventory models.
The supremum ranges over an infinite-dimensional set of distributions, while (17) ranges over vectors. The inequality "" requires, for every feasible of (17), a sequence of distributions in (16) whose value-at-risk approaches . The value-at-risk is a lower quantile, so a distribution placing mass exactly on a high point does not attain the value: the construction has to be a limit. The inequality "" is harder. It must rule out every distribution, not only two-point ones, and a bound through the one-dimensional Chebyshev–Cantelli inequality for alone ignores the box: it yields , which is too large whenever the support bounds bind. The interaction between the Loewner constraint and the componentwise support bounds, which produces the unusual bound , is where the work lies. For Theorem 6 the difficulty is to exhibit the instance and to evaluate enough chance constraints exactly.
Customers are Fin n (0-based) and demand vectors are Fin n → ℝ. Distributions are measures on Fin n → ℝ. The set (16) is covarianceSet qlo qhi μ Sig: a probability measure with P (Set.Icc qlo qhi) = 1, coordinate means μ, and Sig - M positive semidefinite, where M is the matrix of integrals . The covariance bound is called Sig because Σ is Lean syntax. The side conditions , , (Sig.PosDef) and are hypotheses of every theorem. The value-at-risk is the published MultistageStochastic.valueAtRisk P Y (1 - ε). The worst-case value-at-risk is a real sSup over the image of the set. That image is nonempty (the Dirac measure at lies in (16)) and bounded (the box), so the supremum is genuine. "The optimal objective value" of a maximization is stated as a supremum; attainment is not part of any claim. is Mathlib's matrix inverse.
The paper states Theorem 7 and Corollary 4 with "-VaR" without a level; the level , used in the sentence introducing Theorem 7 and everywhere else, is read in. Corollary 4 as printed is false. It maximizes over every with a nonnegative bracket. For , every large then gives the value , which can exceed and hence every value-at-risk. The formal statement adds the condition that makes each a feasible point of (17): for , where is the first bracket. With this condition the statement is the diagonal case of Theorem 7.
A theorem about the Lean set is trivial if the set is empty or the supremum is a junk value. Neither happens here, and replacing the Loewner constraint by a scalar variance bound on would state a different theorem. The dual second-order cone program printed after Theorem 7 is not a target: as printed it has the all-ones vector where Lagrangian duality gives , and it has no multiplier for .
Needed infrastructure: quantiles of pushforward measures, the Loewner order on moment matrices, and finite-support (two-point) distributions. The value-at-risk lemmas and the moment-matrix lemmas are reusable beyond this mission, and contributions of either kind are welcome. Theorem 6 needs only the route-set layer defined here and one explicit instance.
In the capacitated vehicle routing problem (CVRP) a depot serves customers with vehicles of capacity , and every route must respect the capacity. When customer demands are uncertain, the distributionally robust chance-constrained CVRP of Ghosal and Wiesemann (Oper. Res. 68(3), 2020) requires every route to meet its capacity with probability at least under every distribution in an ambiguity set , a family of distributions consistent with what is known about the demands. Such constraints are handled in a branch-and-cut scheme through rounded capacity inequalities, whose right-hand sides require one quantity for each customer subset : the worst-case value-at-risk of the cumulative demand of .
For ambiguity sets that describe each customer separately (marginal moment sets), this quantity is additive over customers and the problem reduces to a deterministic CVRP. Such sets cannot express that the demands of customers in the same municipality, county or state vary jointly within limits. The first-order generic moment ambiguity set does express this: it bounds the mean absolute deviation of the cumulative demand of prescribed customer groups. The mean absolute deviation is a standard robust dispersion measure, less sensitive to outliers than the standard deviation (see Casella and Berger, Statistical Inference, 2002). This mission formalizes the paper's description of the worst-case value-at-risk over such sets.
Demands form a random vector on . The data are a support box with , a mean vector in the interior of , customer subsets and bounds . For , is its indicator vector. The first-order generic moment ambiguity set, Eq. (12) of the paper, is
where is the set of probability distributions on and acts componentwise. The subsets are arbitrary: they may overlap and need not cover .
For a risk level and a random variable , the value-at-risk is . For a customer subset the quantity of interest is
Write (componentwise) and for the componentwise positive part. A route set partitions into nonempty ordered routes. It is feasible in the deterministic CVRP with demands if for all , and feasible in the distributionally robust CVRP if for all and all .
For every customer subset ,
The right-hand side is the optimal value of the paper's problem (13). The statement holds for every family of subsets and all data satisfying the standing assumptions, so it is the general form of which the milestones are special cases.
If are pairwise disjoint and cover and , then
If , for and , then
For some instance with an ambiguity set of the form (12), no deterministic CVRP instance on the same customers and vehicles (capacity , demands ) has the same set of feasible route sets.
Theorem 5 makes the worst-case value-at-risk over (12) computable in polynomial time as the value of a nonsmooth convex problem over the nonnegative orthant, which the paper notes can be written as a linear program. This gives the right-hand sides of the rounded capacity inequalities in a branch-and-cut scheme for the distributionally robust CVRP. Corollaries 2 and 3 give closed forms for two structured families of groups, evaluable in time linear in . Theorem 4 shows the gain in modelling power has a cost: unlike the marginal case, the problem cannot in general be replaced by a deterministic CVRP with altered demands. With a single customer and , Theorem 5 reduces to the closed form for marginalized first-order sets, so it extends that single-customer formula to joint dispersion constraints.
All four results are proved in the paper's online supplement. As far as a platform search shows, none has been machine-checked. The mission produces checked proofs of the equality in Theorem 5, the two closed forms, and an explicit instance for Theorem 4.
The supremum ranges over an infinite-dimensional set of joint distributions, and the value-at-risk is neither convex nor concave in the distribution. Bounding the value-at-risk of each group separately and adding the bounds does not work when groups overlap, and it ignores the total-dispersion constraint. It gives only an upper bound, and in the setting of Corollary 2 that bound is strict whenever the total bound is the binding term. Showing that the infimum in (13) is attained in the limit needs distributions that saturate several overlapping dispersion constraints at once while keeping the mean fixed and the support inside the box. For Theorem 4, the witness must separate the feasible-route-set family of the robust instance from every family defined by a single linear capacity inequality with nonnegative weights.
Customers are Fin n (0-based), subsets are Sfam : Fin p → Finset (Fin n), and a distribution is a Measure (Fin n → ℝ) that is required to be a probability measure. Support is P (Set.Icc qlo qhi) = 1, the mean condition is ∫ q, q j ∂P = μ j, and the dispersion condition is ∫ q, ∑ j ∈ Sfam l, |q j - μ j| ∂P ≤ ν l. The integrability clauses stated alongside are automatic for measures carried by the box. The value-at-risk is the published MultistageStochastic.valueAtRisk P Y (1 - ε). The worst-case value-at-risk is the real sSup of its image over the set; under the standing assumptions this image is nonempty (the Dirac at lies in the set) and bounded (bounded support), so the real supremum is the paper's. The optimal value of (13) is the real sInf of the objective over , a nonempty set on which the objective is bounded below by . Attainment is not claimed. All statements carry the standing assumptions , , and . Corollary 2 writes with the last subset Sfam (Fin.last r). Corollary 3 indexes the singleton of customer by Fin.castSucc i. In Theorem 4 route sets are Fin m → List (Fin n) and only feasibility is modelled; costs play no role.
The theorems are not trivialized by an empty ambiguity set or a junk supremum: membership of the Dirac distribution at is checked locally with a sorry-free proof. Theorem 4 needs a genuinely separating instance: an instance in which no route set is robustly feasible, for example, is matched by a deterministic instance in which none is feasible either.
Needed infrastructure: two-point and finitely supported distributions on and their value-at-risk; weak duality for moment problems over the box; the positive-part calculus of (13). The value-at-risk lemmas for finitely supported measures are reusable in the sibling missions on this paper. Contributions of any of the milestones, of lemmas for these building blocks, or of either inequality of Theorem 5 on its own are welcome.
The capacitated vehicle routing problem (CVRP) assigns customers to a fleet of identical vehicles of capacity and orders each vehicle's visits so as to minimize transportation cost, subject to each vehicle's total load not exceeding . In practice the customers' demands are not known when the routes are planned. Two classical responses are the robust CVRP, which requires feasibility for every demand vector in an uncertainty set, and the chance-constrained CVRP, which requires each capacity constraint to hold with probability at least under a known demand distribution. The first ignores all distributional information; the second assumes a distribution that is rarely known and usually requires independent demands.
Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust chance-constrained CVRP, RVRP(), in which each capacity constraint must hold with probability at least under every distribution of an ambiguity set . Whether this problem can be solved with existing CVRP technology depends on how the worst-case value-at-risk of a customer set's total demand behaves as a set function. This mission formalizes §4 of the paper, which treats ambiguity sets that only constrain each customer's demand separately.
There are customers with random demand vector and a risk level . For a probability distribution and a real random variable , the value-at-risk is
For an ambiguity set and a customer subset , the worst-case value-at-risk of is .
Fix a support box with , a mean vector in the interior of , and for each customer a componentwise convex dispersion measure with bound . The marginalized moment ambiguity set (5) is
It constrains marginal moments only, and so contains joint distributions of every dependence structure, from independent to perfectly correlated demands. Three special cases have their own closed forms: the first-order set (6), where bounds the mean absolute deviation ; the variance set (8), where bounds ; and the semivariance set (10), where bound and .
A route set partitions the customers into nonempty ordered routes. It is feasible in RVRP() if for all and all , and feasible in the deterministic CVRP with demands if for all .
For every marginalized moment ambiguity set (5) and every nonempty ,
The dispersion measures are left arbitrary (convex, componentwise, any number of components), so the goal covers every set of the form (5).
Theorem 3 says that over (5) the worst case of a sum is the sum of the worst cases. Because the value-at-risk is not additive for a fixed distribution, and the online supplement exhibits distributions in such a set for which the individual values-at-risk are not additive, the statement is about the ambiguity set, not about any of its members. Its consequence, Corollary 1, is that RVRP() over (5) is a deterministic CVRP with inflated demands, so existing branch-and-cut and branch-and-cut-and-price codes solve it unchanged. Propositions 2–4 make those inflated demands explicit for three standard dispersion measures, so that the whole reduction is in closed form. The corollary also exposes a limitation: under (5) the worst-case distribution does not depend on the route set, and the model cannot represent known dependencies between customers.
The results are proved in the paper's online supplement; none has a machine-checked proof. A formalization produces a checked worst-case value-at-risk calculus over moment sets with support constraints, including sharp one-sided Chebyshev-type bounds under mean-absolute-deviation, variance and semivariance constraints, which are reusable in distributionally robust optimization beyond vehicle routing.
The value-at-risk is neither subadditive nor superadditive in general, so neither inequality of Theorem 3 follows from properties of a single distribution. The inequality "" requires combining near-worst-case distributions of the individual customers into one joint distribution in that is simultaneously near-worst for the sum; the inequality "" requires bounding the value-at-risk of the sum for an arbitrary joint law using only marginal information. In Propositions 2–4 the supremum is typically not attained: the distribution concentrating mass at the claimed worst-case value violates the mean constraint, and the value is reached only as a limit of distributions in . An argument that exhibits a single maximizer therefore fails, and the statements must be proved as equalities of suprema.
Customers are Fin n (0-based) and demand vectors are Fin n → ℝ. An ambiguity set is a set of measures on Fin n → ℝ, each required to be a probability measure; the support condition is P (Set.Icc qlo qhi) = 1 and expectations are Bochner integrals. The sets are sets of joint laws on , never products of marginals. In (5) each expectation is required to exist; this is automatic for convex on the bounded support. The value-at-risk is the published definition MultistageStochastic.valueAtRisk P Y (1 - ε), and the worst-case value-at-risk is the real supremum of its values over the ambiguity set; under the standing assumptions that set of values is nonempty (the Dirac law at belongs to ) and bounded (by the support), so the supremum is not a default value. The single-customer quantity is the case . The standing assumptions (, , convexity of , , , ) are explicit hypotheses. Routes are lists of customers; a route set has nonempty routes whose concatenation is a permutation of all customers. Costs are not formalized, since both routing problems minimize the same cost over their feasible route sets.
All targets are equalities or equivalences; a one-sided inequality, a statement asserting that some distribution attains the value, or a formulation over product measures is a different theorem and does not count.
Contributions welcome: the reduction of the chance constraint to a value-at-risk bound, the right-continuity lemmas for the value-at-risk of a measure on , two-point constructions in the ambiguity sets, and one-sided Chebyshev-type bounds with support constraints.
The capacitated vehicle routing problem (CVRP) asks for a set of minimum-cost routes by which a fleet of identical vehicles of capacity , based at a depot, serves every customer exactly once without any vehicle carrying more than its capacity. In practice customer demands are not known when routes are planned. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust CVRP: the demand vector is random, its distribution is known only to lie in an ambiguity set , and every route must respect its capacity with probability at least under every distribution in .
Exact CVRP solvers rely on compact two-index vehicle flow formulations strengthened by rounded capacity inequalities, which bound from below the number of vehicles entering any customer subset by a demand estimator . The paper shows (its Theorem 1) that the robust two-index formulation is exact whenever the demand estimator is subadditive and demands are nonnegative, and that this fails for some natural ambiguity sets: sets that fix the marginal distribution of each customer's demand violate it (Example 1). This mission formalizes the paper's positive result for the most widely used class of ambiguity sets, the moment ambiguity sets of distributionally robust optimization (see El Ghaoui et al. 2003, Delage and Ye 2010, Wiesemann et al. 2014).
There are customers, indexed ; the demand vector is . Fix
The moment ambiguity set is
where denotes all probability distributions on . The paper's standing assumptions are , each closed and convex, and .
For a distribution the value-at-risk of a random variable is , with risk level . The worst-case value-at-risk of a customer subset is , and the demand estimator (2) is
The Lean development names these momentAmbiguitySet qlo qhi μ φ σ, worstCaseVaR, demandEstimator and twoPointMeasure in the namespace DRCVRP.Moment.
For every moment ambiguity set satisfying the standing assumptions, every and every ,
This is condition (S) of the paper, stated for the rounded estimator (2) and for all pairs of subsets, overlapping or empty ones included.
For every customer subset there are two-point distributions with and such that
Combined with the paper's Theorem 1, Theorem 2 says that for every moment ambiguity set with nonnegative demands the robust CVRP can be solved through the compact two-index formulation with robust rounded capacity inequalities, i.e. by the branch-and-cut machinery of the deterministic CVRP. It also separates moment ambiguity sets from ambiguity sets built from marginal histograms, hypothesis tests, -divergences or Wasserstein balls, whose estimators can violate subadditivity. Proposition 1 describes the worst case: however many moment constraints the set contains, two demand scenarios suffice to approach the worst-case value-at-risk, strengthening the Richter–Rogosinski theorem for this functional.
Both results are proved in the paper's online supplement. They have not, to the best of current knowledge, been machine checked. This mission produces a checked statement and proof of both, together with a reusable encoding of moment ambiguity sets and of the worst-case value-at-risk over them. The companion missions of the series formalize the equivalence theorem (I) and the explicit worst-case VaR formulas for marginalized (III), first-order (IV) and covariance (V) ambiguity sets.
Value-at-risk is not subadditive for a single distribution, so the obvious route, subadditivity of the worst-case VaR followed by , needs an argument specific to the moment set; for the marginal-histogram set of Example 1 the worst-case VaR itself fails to be subadditive. The supremum over ranges over an infinite-dimensional set of distributions and is in general not attained, so an argument that picks a maximizer does not apply, and the classical finite-support reduction (Richter–Rogosinski) yields a number of support points that grows with the number of moment constraints, not two. The integer rounding and the must also be handled for all pairs of subsets, including overlapping ones.
Customers are Fin n (0-based) and customer subsets are Finset (Fin n). Distributions are measures on Fin n → ℝ; membership in the moment set requires a probability measure giving mass one to the closed box Set.Icc qlo qhi, integrable coordinates with ∫ q, q i ∂P = μ i (an equality), and integrable φ l with ∫ q, φ l q ∂P ≤ σ l. The integrability clauses hold automatically under the standing assumptions and do not shrink the set. The dispersion measure is an arbitrary real-valued function whose components are convex (convex real functions on are continuous, which covers "closed"); is allowed. The value-at-risk is the published platform definition MultistageStochastic.valueAtRisk at level . The worst-case VaR is a real sSup; over a moment set satisfying the standing assumptions the set of VaRs is nonempty (the Dirac measure at belongs to ) and bounded by the box, so this is the true supremum. The estimator is integer valued. Every standing assumption is a hypothesis of both theorems.
Neither statement can be satisfied trivially: the goal is about the rounded estimator of the true supremum over a nonempty set, not about subadditivity of an arbitrary set function, and the milestone requires the two-point laws to lie in and their VaRs to converge to the supremum, not to be attained. Extended-valued dispersion measures, such as the one expressing the covariance set of §5.2 as an instance of (4), are outside the scope of the real-valued encoding.
A complete development needs basic facts about quantiles of finitely supported measures, the structure of the moment set, and a duality or construction argument for the worst-case VaR. Lemmas about value-at-risk of two-point laws and about moment sets are reusable across the series. Proofs of the milestone, of the goal, and of intermediate lemmas are welcome.
Chapters 6 through 8 built M-convex and L-convex functions and their conjugacy theory as abstract combinatorial objects on the integer lattice. Chapter 9 grounds that theory in a setting every reader already knows: network flows. The chapter's throughline is that the classical minimum cost flow problem — flows bounded by simple arc capacities, with a single linear cost — is a shadow of a much richer submodular flow problem, in which the constraint on a flow's boundary is not "equal a fixed supply vector" but "lie in the base polyhedron of an arbitrary submodular set function." This mission formalizes the feasibility theory for both problems and its capstone: a max-flow min-cut theorem for submodular flows that specializes to the classical max-flow min-cut theorem exactly when the submodular function degenerates to a plain capacity function.
Let be a finite directed graph, with giving each arc's start and end vertex. The boundary of a flow is . For , and are the arcs leaving and entering . Given an upper capacity and lower capacity , the cut capacity function is . A submodular set function with plays the same structural role as but is arbitrary problem data rather than a derived quantity.
For a feasible maximum submodular flow problem on a specified arc : , a common value in ; if the data is integer valued and the value is finite, an integer-valued maximum flow exists.
Proposition 9.2: the cut capacity function is always submodular — the fact that lets the classical minimum cost flow problem's feasibility be phrased in exactly the same base- polyhedron language as the general submodular flow problem. Theorem 9.3: a flow meeting the capacity constraint with boundary exists if and only if for all and — the classical case, and the direct predecessor of the goal's feasibility side. Theorem 9.10: the submodular flow problem is feasible if and only if for all — obtained from Theorem 9.3 via Edmonds's intersection theorem in the book's own proof, and the feasibility half of the goal's own maximum-flow variant.
The result itself. Theorem 9.13 is a genuine generalization of the max-flow min-cut theorem — one of the most-cited results in combinatorial optimization — to a submodularly constrained setting where the classical single-source-single-sink cut structure is replaced by an arbitrary vertex subset scored by a submodular function rather than merely counted. It specializes to the classical theorem when is the indicator of a fixed boundary value and the graph carries a single source/sink; the book's own derivation (dividing the target arc and reducing to Theorem 9.10's feasibility criterion) is exactly the kind of "one shared mechanism explains two theorems" result this whole book is organized around.
Formalizing it. A prior-art search (GET /theorems?q=max-flow min-cut) found two existing
platform items for the classical theorem — LinearOptimization.max_flow_min_cut (Bertsimas &
Tsitsiklis, single source/sink, plain capacities) and menger_directed_max_flow (Ford-Fulkerson,
integer capacities) — both at a genuinely different, simpler generality (no lower capacity
bounds, no submodular vertex-cut function, a fixed source/sink rather than an arbitrary marked
arc). A further search (q=network flow) found a distinct mission formalizing Bertsimas &
Tsitsiklis's uncapacitated network flow LP theory (basic feasible solutions, tree solutions,
basis-matrix integrality) — a different technique (linear-algebraic, not cut-based) for a
different problem (no capacities at all). Neither family is reused; this mission gives the
first formal statement of submodular-flow feasibility and its max-flow min-cut theorem at the
book's own generality.
The obvious shortcut — state only the value equality of Theorem 9.13 and drop the integrality clause — would misrepresent the theorem's own content: the equality of the extremal values follows from ordinary LP duality on the polyhedron (arguably already within reach of chunk 04's Edmonds's intersection theorem machinery, as the book's own proof of the feasibility predecessor Theorem 9.10 uses exactly that), whereas the integer-flow existence half is the theorem's genuine combinatorial content, unique to the integer lattice. This chunk keeps both halves in every drafted theorem (Theorem 9.3, 9.10, and the goal) rather than only the polyhedral half.
A second, more structural difficulty governed this chunk's scope: BRIEF.md recommended
Theorem 9.4 (the potential-optimality criterion) and its M-convex-cost specialization Theorem
9.14 as milestones, but both need a polyhedral convexity hypothesis on real-valued (or
M-convex) functions over that this series has never built — the identical scope
boundary chunk 10 hit with Theorem 8.4. Rather than silently drop the polyhedral-convexity
hypothesis (which would make the drafted statement unsound, since the theorem's hard direction
genuinely needs it), this chunk selects only results — Proposition 9.2, Theorem 9.3, Theorem
9.10, Theorem 9.13 — that need no convexity apparatus of any kind, only the submodularity of
/ and elementary capacity-constraint feasibility.
and are Fintypes with DecidableEq V (and DecidableEq A where a Finset.erase is
needed); tail, head : A → V are plain functions, not a bundled graph structure. Every
capacity- and cut-related quantity is WithTop ℝ-valued (ℝ ∪ {+∞}) throughout, with no
EReal: a per-term check (documented in MODERATION_NOTES.md) confirms every subtraction this
chunk needs is really an addition of two terms each individually in , via a small new cast NegLowerToUpper : WithBot ℝ → WithTop ℝ. The base
polyhedron is stated by its defining inequalities rather than via a named polyhedral
object (chunk 04's BasePolyhedron is ℤ^V-domain and does not fit chapter 9's real-vector-
space setting). Not drafted: Theorem 9.4/9.14 (needs the real-domain polyhedral-convexity layer
above), Theorem 9.6 (needs a real-domain polyhedral L-convexity notion for its dual-integrality
half), Theorem 9.5/9.18/9.20/9.22 (negative-cycle criteria, an alternative non-potential
certificate family, checked against platform prior art and found adjacent only), Propositions
9.23–9.25 (supporting technical facts), and Theorems 9.26–9.28 (the separate network-
transformation technique of §9.6). A trivializing formalization would state Theorem 9.13's
value equality with the integrality clause dropped, or would silently allow / to range over all of EReal (permitting a nonsensical upper-
capacity-like lower bound); neither is done — both the integrality clause and the WithTop ℝ/WithBot ℝ type-level domain restriction are kept exactly as the book states them.
Several complex variables studies functions of that are holomorphic in every coordinate. It underlies complex geometry, the theory of analytic spaces, and parts of mathematical physics and harmonic analysis. Every later topic of the subject (domains of holomorphy, pseudoconvexity, the -problem, the Bergman kernel, analytic varieties) starts from the same foundation: a function that is holomorphic in each variable separately and locally bounded is jointly smooth and is locally the sum of a convergent power series. This mission formalizes that foundation as it appears in the first chapter of Jiří Lebl's textbook Tasty Bits of Several Complex Variables (jirka.org/scv).
Historically, the step from separate to joint regularity is due to Osgood (1899), who showed that a continuous (later: locally bounded) function that is holomorphic in each variable separately is holomorphic; Hartogs (1906) later removed the boundedness assumption altogether, a much harder theorem not covered here.
Points of are . For a center and a polyradius with every , the polydisc is
a product of open discs . Its distinguished boundary is the torus , and denotes the closed polydisc.
A function on an open set is holomorphic (the book's Definition 1.1.2) if it is locally bounded (every point of has a neighborhood on which is bounded) and complex-differentiable in each variable separately: for every and every , the one-variable limit
exists. A map is holomorphic if every component is.
A multi-index is , with , and . A power series is summed over all multi-indices; since has no natural order, convergence means absolute convergence, and the series converges uniformly absolutely on a set when converges uniformly for . The Wirtinger derivative is for , and applies exactly times for each .
Let be a polydisc. If is continuous and holomorphic in , then there are coefficients with
the series converging uniformly absolutely on every compact subset of . Conversely, a function defined on by such a series is holomorphic on . Both directions are part of the goal.
In attack order:
Theorem 1.2.1 is the statement that makes the theory of several complex variables possible: it identifies the book's elementary, one-variable-at-a-time definition of holomorphy with local representability by power series. Uniqueness of the coefficients, the Cauchy estimates, the identity theorem, the maximum principle, and holomorphy of compositions and of implicit functions all follow from it, and every later chapter of the book (Hartogs figures, pseudoconvexity, the Bergman kernel, Weierstrass preparation) uses it without comment.
Mathlib already develops complex analysis in several variables for Fréchet-differentiable maps: analyticity of DifferentiableOn ℂ functions, torusIntegral, Cauchy integrals over circles, and Osgood-type regularity for maps on are available or published on the platform. What this mission adds is the bridge from the weaker separate notion of holomorphy, with local boundedness, to these results, stated with multi-index power series and uniform absolute convergence on compact sets exactly as in the textbook. The results are classical and fully proved in the book; none has a machine-checked proof in this form.
The hypothesis controls only along complex lines parallel to the coordinate axes, plus a bound. Nothing in the definition says that is continuous, let alone jointly differentiable, so no joint limit, Fréchet derivative, or change of the order of integration is available at the start. Every tool that the one-variable theory and Mathlib's multivariable library supply presupposes joint regularity; the obstacle is to obtain it from separate information.
A second difficulty is bookkeeping: power series over have no natural order, so convergence must be handled as unconditional summation with a uniformity statement over compact sets, and iterated Wirtinger derivatives must be related to derivatives of the series term by term.
Fin n → ℂ; multi-indices are Fin n → ℕ. A polyradius is ρ : Fin n → ℝ with the hypothesis ∀ k, 0 < ρ k; the polydisc is defined coordinatewise (not Metric.ball, which only gives equal radii).IsHolomorphicOn f U: local boundedness plus complex differentiability at of (via Function.update). Openness of is a hypothesis wherever the book says "open". Maps into are holomorphic componentwise.DifferentiableOn ℂ. That makes Proposition 1.1.3 and the first half of the goal off-target (they would follow from existing library results) and is not the book's definition.closure (polydisc a ρ); "continuous on , holomorphic in " keeps both hypotheses.HasSum (unconditional summation) of the terms to , and uniform absolute convergence on a set means the finite partial sums of , directed by inclusion, converge uniformly on . Mathlib's HasFPowerSeriesOnBall is not used: its balls for the sup norm are equiradial polydiscs only.torusIntegral, whose parametrization includes the Jacobian and orients each circle positively. The integrands are continuous on the compact torus, so no integrability hypothesis is needed.deriv along and ); iterates it. is LinearMap.det of the real Fréchet derivative, which is basis independent.A complete development needs the one-variable Cauchy integral formula (in Mathlib), iterated circle integrals and torusIntegral, and summation over Fin n → ℕ. The regularity bridge from separate to joint holomorphy and the multi-index power-series API are reusable across the whole series of missions on this book; contributions of either as standalone lemmas are welcome.
Missions 29-ch08b-conjugacyduality and 30-ch08c-conjugacyduality built the M2-/L2-convex
function classes and proved their conjugacy correspondence is nearly complete. This mission
finishes that correspondence (Theorems 8.48-8.49) and then turns to chapter 8's capstone
application: a Lagrangian duality theory for integer programs, built entirely from the
M-/L-convexity machinery developed across the whole book. It develops the general
perturbation-based duality framework (mirroring Rockafellar's conjugate duality for nonlinear
programming), specializes it to M-convex programs via the perturbation , and proves the
strong duality theorem this specialization exists to deliver — together with its mirror
construction recovering the primal problem from the dual.
An M-convex program consists of a set satisfying (REG) — is an M-convex set — and an objective satisfying (OBJ) — is an M-convex function. The general duality framework embeds any in a family of perturbed problems via with , yielding an optimal-value function , a Lagrangian , and a dual objective . For M-convex programs the perturbation , for an M-convex regularizer with , makes this framework concrete; the case is written with subscript .
For a feasible, bounded-below M-convex program, , and . This is the theorem
mission 11-conjugacy-ii-lagrange's own STATUS.md explicitly deferred, noting it needs the
specific M-convex perturbation (Eq. (8.61)) and Propositions 8.55-8.56/Theorems 8.57-8.58 as
prerequisites — all built as milestones of this mission.
Theorem 8.48 completes the M2-/L2-convex conjugacy correspondence; Theorem 8.49 characterizes separable convex functions as exactly the M-and-L-convex functions. Theorem 8.53 (reduced to parts (1),(2),(4)) gives the general perturbation-independent duality identities: the dual objective is , weak duality's biconjugate form , and the equivalence of strong duality with biconjugate exactness. Proposition 8.55 shows the M-convex perturbation legitimately instantiates the general framework; Proposition 8.56 (reduced to part (1)) gives the closed form for the unregularized Lagrangian kernel via the conjugate of 's indicator function; Theorems 8.57 and 8.58 establish the resulting convexity/concavity of the kernel, the dual objective, and the optimal-value function in each of their arguments. Propositions 8.62-8.63 and Theorems 8.64-8.65 build and analyze the mirror construction — the dual perturbation , its optimal-value function , and the dual-of-dual reconstruction — showing that for bounded the process exactly recovers the primal problem and its own strong duality theorem.
This is chapter 8's payoff: a full nonlinear-integer-programming duality theory, built without any convexity assumption beyond M-/L-convexity, mirroring Rockafellar's classical conjugate duality approach line for line while replacing every continuous convexity argument with a discrete M-/L-convexity one. Theorem 8.59's proof is a two-line consequence of the machinery this mission assembles (Theorems 8.35, 8.53, 8.58), which is itself the point: the discrete theory's hard combinatorial work (Theorems 8.35, 8.36, 8.42 from prior missions) is what makes the strong duality theorem here nearly free, exactly as convex analysis makes classical Lagrangian duality nearly free once Fenchel duality is established. The bidirectional construction of Theorems 8.62-8.65 is the discrete analogue of the classical fact that Lagrangian duality is symmetric between primal and dual convex programs.
None of these results are open — they are Murota's own account of M2-/L2-conjugacy and
Lagrangian duality (section 8.3.3 and section 8.4), continuing chapter 8's duality program to its
conclusion. What this mission contributes is a faithful, machine-checked formal statement of each,
completing the platform's coverage of chapter 8's duality theorems begun in missions
10-conjugacy-i and 11-conjugacy-ii-lagrange; no comparable formalization exists on the
platform (see Formalization scope).
The EReal-valued () typing is essential and new to this mission:
unlike every prior mission in this series, the general framework's derived quantities
(, , , and their mirror-construction analogues , , ,
) are defined as infima/suprema over families that are not a priori bounded, so they can
genuinely equal or — a value WithTop ℝ cannot represent and whose sInf
instance would silently substitute a junk value (0) rather than correctly returning .
The book's own repeated " is convex (resp. concave), or , or "
disjunctive escape clauses (Theorems 8.57, 8.58, Propositions 8.63) are captured with two small
generic combinators, IsEmbedOf/IsNegOf, rather than restating the embedding by hand at each of
the roughly dozen occurrences.
Ground-set elements are a Fintype V with DecidableEq; the base M-/L-/M2-/L2-convexity
vocabulary is redeclared verbatim from missions 29-ch08b-conjugacyduality and
30-ch08c-conjugacyduality, since sibling drafts in this series cannot yet reference one another.
Two results carry a documented partial-coverage scope reduction (see HARD.md): Theorem 8.53 is
placed with only parts (1),(2),(4), the purely algebraic identities holding unconditionally for any
perturbation , omitting parts (3),(5),(6), which characterize under the
book's own biconjugacy hypothesis (8.55) — a hypothesis this mission's M-convex-specific Theorem
8.59 later establishes directly rather than invoking Theorem 8.53's general form; and Proposition
8.56 is placed with only part (1), the closed form, omitting part (2), the closed form
via the infimal convolution , not independently needed elsewhere in this
chunk. One numbered result nominally in this chunk's page range, Theorem 8.46, is not re-placed
here: it was already found and placed as a milestone in mission 30-ch08c-conjugacyduality, whose
own page range overlaps this chunk's by one page (PDF251/printed 233) — see HARD.md.
Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 8.57 carry
the most independent proof content.
Chapter 16 of Keller and Trotter's Applied Combinatorics (2017 Edition, CC BY-SA 4.0) is a survey of seven topics. Two of them are self-contained results with complete proofs on the page, and this mission formalizes both.
The first is the Lovász Local Lemma. It was introduced by Erdős and Lovász in 1975 to show that certain hypergraphs are 3-colourable (Erdős–Lovász 1975), and it has become a standard tool of the probabilistic method. The classical probabilistic argument shows that a random object has a property with probability close to one. The local lemma is different: it shows that a good object exists even when it is exceedingly rare, provided that each "bad" event depends on only a few of the others. It underlies lower bounds for Ramsey numbers such as , the subject of Section 16.8. It also underlies results on colouring, satisfiability and Latin transversals, and the algorithmic version of Moser–Tardos (2010).
The second is the Gale–Ryser Theorem, proved independently by Gale (1957) and Ryser (1957). It decides when a zero–one matrix with prescribed row and column sums exists. Equivalently, it decides when a pair of sequences is the degree sequence of a bipartite graph. Its condition is a comparison in the dominance order on integer partitions.
A finite probability space is a finite set with a function defined on all subsets, finitely additive, with and . Let be a finite family of events. For a subfamily write
the event that every event of fails; for it is . Fix, for each , a subfamily . The event is independent of any event not in if for every with and . In the formalization this condition is IndepOutside μ A N i, written as
A partition of a positive integer is a non-increasing string of positive integers with sum ; is the set of partitions of . It is partially ordered by iff is no longer than and every partial sum is at least (Dominates). covers when with nothing in between (Covers). The dual partition has entries, the -th being the number of with (dual). A zero–one matrix with row sum string and column sum string is an matrix with entries in whose row sums to and column to (IsZeroOneMatrixWithSums).
If and for every , then for every non-empty
If , , , and , then
If covers in , then arises from by moving one unit from a part to a later part (possibly a new part of size one), and all parts strictly between equal . For partitions of ,
The Erdős–Ko–Rado bound of Theorem 16.8 enters as the published reference FamousTheorems.erdos_ko_rado.
The local lemma is the entry point to the probabilistic method's rare-event side. A formal statement in the book's form — finite spaces and the book's conditional notion of independence — is a reusable interface for formalizing its applications: Ramsey lower bounds, hypergraph colouring and -SAT with bounded occurrences. The symmetric form is the version most applications call. Mathlib has no local lemma. The platform has a conditional-probability bound from an unrelated paper mission (Erdos390.WholePaper.finiteAsymmetricLocalLemma_conditionalBound), which bounds with and does not state the product lower bound for the joint failure.
Gale–Ryser is the prototype of margin problems for -matrices and of degree-sequence characterizations (compare Erdős–Gallai for graphs). Formalizing it produces the dominance order, conjugate partitions and covering relations on sorted lists of positive integers. Mathlib has Nat.Partition but no dominance order or conjugate. None of these results is formalized on the platform. The results themselves are classical and proved; the work is formalizing the proofs.
For the local lemma, the naive induction on fails. Conditioning on the joint failure of a subfamily requires that failure to have positive probability, and that is only known after the inductive bound has been proved for smaller subfamilies. The induction must therefore carry the lower bound and the positivity of every smaller joint failure at once. It must also split each conditioning family into the part inside and the part outside. The independence hypothesis controls only the part outside, and only through intersections of complements, not through arbitrary events.
For Gale–Ryser, necessity is an exchange argument, but sufficiency needs the fine structure of covers in the dominance order (Proposition 16.11): the case analysis of where the moved unit lands, including a new last part, and the fact that a maximal chain from down to exists. Converting the list-level statements into matrix constructions over Fin m × Fin n is the other main cost.
Fintype Ω with DiscreteMeasurableSpace Ω and a measure μ with IsProbabilityMeasure μ; every subset is an event and probabilities are μ.real, as in the book's finite probability spaces.A : ι → Set Ω over a Fintype ι, so repeated events are allowed. Neighbourhoods are N : ι → Finset ι with i ∉ N i.0 < x i < 1 is strict on both sides, as on the page.Fintype.card ι, together with positivity. Here and are real and is Real.exp 1.List ℕ, non-increasing with positive entries. Entries are 1-based through entry, and partial sums are (V.take j).sum.Matrix (Fin m) (Fin n) ℕ with entries in .Not included.
Welcome contributions. Reusable infrastructure: a finite-space conditional-probability API, and the dominance order as a PartialOrder on sorted partitions linked to Nat.Partition.
Mission 29-ch08b-conjugacyduality opened chapter 8's account of M2-convex functions — sums of
M-convex functions — proving their domains and minimizers are M2-convex and that they are
integrally convex. This mission completes that program and builds its exact mirror for L2-convex
functions (integer infimal convolutions of L-convex functions), the class that appears on the
opposite side of Edmonds's intersection theorem's min-max relation from M2-convexity. It proves
optimality and proximity theorems for both classes, shows their subdifferentials add (a discrete
analogue of the classical subdifferential sum rule), derives how the Legendre-Fenchel transform
interacts with the sum/infimal-convolution operation, and — the technically hardest result in the
whole cluster — establishes that L♮₂-convex functions are integrally convex, by a genuinely
different and more intricate argument than the M2-side analogue required.
Fix a finite ground set . A function is
L2-convex if , the integer infimal convolution
, of two L-convex functions
; L-convex if the summands are L-convex. An M2-convex
function is a sum of two M-convex functions (mission
29-ch08b-conjugacyduality). The integer subdifferential and
real subdifferential generalize the subgradient set to integer- and
real-valued perturbation directions respectively.
Every L-convex function is integrally convex, and in particular every L-convex set is integrally convex. The book's own proof is the most intricate argument in this cluster: given in the Minkowski sum of two L-convex sets, it constructs an explicit representation of as a convex combination of finitely many integer points of , all lying in 's own integral neighborhood, via the sorted fractional-part values of a chosen decomposition — a genuinely different technique from the M2-side analogue (Theorem 8.31), whose proof is a two-line consequence of convex extensibility.
Eleven further results build the M2-/L2-convex theory in parallel. Theorems 8.33-8.34 give the M2-optimality criterion (a nonnegative-sum condition over cyclic exchange families) and its scaling-based proximity theorem; Theorem 8.35 shows subdifferentials of a sum of M- convex functions add, and that subdifferentials of M2-/M-convex functions are L2-/L-convex; Theorem 8.36 computes the conjugate of a sum as the infimal convolution of conjugates, with biconjugacy recovering the original sum. Propositions 8.39-8.41 transfer L-(natural-)convexity from summands to the domain and minimizer set of an L2-convex function, and give the precise attainment condition under which a linearly-perturbed infimal convolution's minimizer set splits additively. Theorems 8.43-8.44 give the L2-optimality and L2-proximity theorems, the exact L-side mirrors of Theorems 8.33-8.34; Theorem 8.45 mirrors Theorem 8.35 for subdifferentials of an infimal convolution; and Theorem 8.46 (found by direct reading, immediately following 8.45 and explicitly named by the book as 8.36's counterpart) shows biconjugacy for L-convex infimal convolutions.
The M2-/L2-convex function classes are where discrete convex analysis's abstract machinery meets
concrete combinatorial optimization: Edmonds's matroid intersection theorem and its
generalizations are literally statements about M2-convex minimization, with the L2-convex side
supplying the dual bound. Theorem 8.35's subdifferential additivity is the discrete analogue of
the classical Moreau-Rockafellar sum rule, and its proof (via the M-convex intersection theorem,
already a milestone of mission 10-conjugacy-i) shows the sum rule holding without the
constraint-qualification technicalities the continuous theory needs — a case where the discrete
theory is cleaner than its continuous ancestor. Theorem 8.42's harder, dedicated proof technique
is itself informative: it demonstrates that L2-convexity's combinatorial structure is not a
routine transcription of the M2-convex case, foreshadowing the book's broader theme that M- and
L-convexity, while conjugate, are not interchangeable in how their proofs actually work.
None of these results are open — they are Murota's account of the sum/infimal-convolution closure
properties of M-convex and L-convex functions, continuing chapter 8's duality program into its
most combinatorially concrete corner. What this mission contributes is a faithful,
machine-checked formal statement of each, including one result (Theorem 8.46) the platform's own
automated extractor missed, extending the shared Lean vocabulary (InfConv, L2Convex,
M2ConvexSet) mission 29-ch08b-conjugacyduality began; no comparable formalization exists on
the platform (see Formalization scope).
The naive approach to the goal would try to adapt the M2-side integral-convexity proof (a direct appeal to convex extensibility) verbatim; the book's own proof shows this does not work, requiring instead a from-scratch construction: decompose , take fractional parts and , sort their combined distinct values, build threshold sets exactly as in the Lovász-extension construction, and verify each resulting integer point both lies in (via L-convex-set closure properties, Theorem 5.10) and in 's integral neighborhood (a case split on whether is itself an integer) — a genuinely multi-stage combinatorial argument with no single-inequality shortcut, unlike almost every other result in this mission.
Ground-set elements are a Fintype V with DecidableEq; M2-/L2-convex functions are
(V→ℤ)→WithTop ℝ. All twelve numbered results found in this chunk's page range are placed, with
no partial-coverage scope reduction needed — every clause of every result, including all three
parts of Theorems 8.35 and 8.45 and the full cyclic-exchange condition of Theorems 8.33-8.34, is
stated in full. One numbered result nominally in this chunk's page range, Theorem 8.32, is not
re-placed here: it was already found and placed as a milestone in mission
29-ch08b-conjugacyduality, whose own page range overlaps this chunk's by one page (PDF245) —
see HARD.md. "g1□g2 > −∞" hypotheses are omitted rather than translated, since WithTop ℝ
has no −∞ element to violate. This mission's base vocabulary is redeclared verbatim from
mission 29-ch08b-conjugacyduality rather than imported, since sibling drafts in this series
cannot yet reference one another; ConvexConjugate is redeclared from mission 10-conjugacy-i.
Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 8.35 carry
the most independent proof content.
Many counting questions ask for the number of objects up to symmetry: necklaces of coloured beads that may be rotated and flipped, musical scales up to transposition, chemical isomers up to the symmetries of a molecule, graphs on vertices up to relabelling. Counting all configurations and dividing by the number of symmetries fails, because some configurations are fixed by some symmetries. The standard tool for such questions is the enumeration theorem of Redfield (1927) and Pólya (1937), which turns the symmetry group into a generating function recording not only how many inequivalent configurations there are but how many use each colour a prescribed number of times.
This mission formalizes Chapter 15 of Keller and Trotter's Applied Combinatorics (2017 Edition), which develops the theorem from Burnside's Lemma for an undergraduate audience. The chapter's footnotes record the history: the orbit-counting lemma was known to Cauchy and Frobenius before it appeared in Burnside's book, and Redfield's paper anticipating Pólya's work was rediscovered only around 1960.
Let be a finite set with . A permutation group of is a set of bijections containing the identity and closed under composition and inverses. Every permutation splits into disjoint cycles; a fixed point is a cycle of length . Write for the number of cycles of length , so that . The cycle index of is the polynomial with rational coefficients
For the eight symmetries of a square, .
A coloring of with colours is a map ; denotes the set of all of them. A permutation acts on colorings by , and two colorings are equivalent when some carries one to the other. The weight of is the monomial in commuting variables, where counts the points coloured . The pattern inventory is the polynomial whose coefficient of is the number of equivalence classes of colorings using each exactly times.
More generally, for a finite group acting on a finite set , the orbit (equivalence class) of is , the stabilizer of is , and the fixed set of is .
For a finite group acting on a finite set and every ,
If is the number of equivalence classes of induced by the action, then
For a permutation group of with and colours ,
an identity of polynomials in with rational coefficients: substituting power sums of the colours into the cycle index yields the pattern inventory.
The result itself. The theorem reduces counting inequivalent configurations to a computation with the cycle structure of the symmetry group, which is usually available in closed form (cyclic, dihedral and symmetric groups, and the pair group acting on edges of a graph). Setting all gives the number of inequivalent colorings, ; reading off one coefficient answers refined questions such as the number of necklaces with a prescribed number of beads of each colour. The book applies it to musical scales, isomers of hydrocarbons and nonisomorphic graphs.
Formalizing it. Burnside's Lemma is in Mathlib (MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group), and so is the orbit–stabilizer theorem, so the two milestones are short; they are kept because they are the book's route to the goal. Mathlib has Equiv.Perm.cycleType but no cycle index and no pattern inventory, and no statement of Pólya's theorem was found on the platform (searches for Pólya, cycle index, pattern inventory, necklace and orbit counting, September 2026). The mission therefore produces the first machine-checked cycle index and Pólya enumeration theorem in this environment.
Burnside's Lemma counts orbits by fixed points; Pólya's theorem is a weighted Burnside lemma. Two steps separate them. First, the weight-enumerator of the colorings fixed by must be matched with the monomial of evaluated at power sums. This needs the cycles of as subsets of , including its fixed points, whereas Mathlib's cycleType records only the lengths of the nontrivial cycles. Second, the weighted orbit count needs the weight to be invariant under the action and Burnside's argument to be carried out inside a polynomial ring rather than in . Neither step is a direct instance of a Mathlib lemma. Proving the identity only after substituting integers for the does not suffice: it determines the number of classes, not the coefficient of each monomial.
Fintype with decidable equality, = Fintype.card S; a permutation group is a Subgroup (Equiv.Perm S), and = Nat.card G .cycleCount π k: the number of fixed points for and the multiplicity of in Equiv.Perm.cycleType for . is cycleIndex G : MvPolynomial (Fin r) ℚ, the variable with index standing for .Fin m, colorings are S → Fin m, and ; the induced relation is colorSetoid G m. Composing with instead of gives the same classes.patternInventory G m : MvPolynomial (Fin m) ℚ, the sum over the quotient of the weight of a representative (Quotient.out); that the weight is a class invariant is part of the theorem.MvPolynomial.bind₁ sending to .MulAction G 𝒞 with Fintype G and Fintype 𝒞; is the number of MulAction.orbitRel classes and the identity is stated in .Reusable beyond this mission: the cycle index of a permutation group and the pattern inventory, both needed for any later count of necklaces, graphs up to isomorphism, or de Bruijn's generalization with a group acting on the colours. Contributions of cycle indices of specific groups (cyclic, dihedral, symmetric) are welcome.
Moving as much as possible of something — freight, water, data — from an origin to a destination through connections of limited capacity is one of the basic problems of operations research. Its mathematical form, the maximum flow problem, was posed in the 1950s in work on rail networks and solved independently by Ford and Fulkerson (Maximal flow through a network, Canadian J. Math. 8 (1956)) and by Elias, Feinstein and Shannon (A note on the maximum flow through a network, IRE Trans. Inform. Theory 2 (1956)). The answer, the Max Flow–Min Cut Theorem, is a min–max duality: the largest amount that can be shipped equals the smallest total capacity whose removal disconnects the destination from the origin. It is a standard example of linear-programming duality with a combinatorial proof, and it is the source of Hall's matching theorem, Menger's theorem and Dilworth's theorem via network constructions.
This mission formalizes Chapter 13 of Keller and Trotter's Applied Combinatorics (2017 Edition), together with the two theorems of Chapter 14 that apply it, in the book's own model of a network.
A network consists of a finite vertex set , a set of directed edges , a source and a sink with , and a capacity (a real number) on each edge. The underlying directed graph is an oriented graph: for any two vertices at most one of , is an edge. Every edge at points away from and every edge at points into .
A flow is a function on the edges with , extended by on pairs that are not edges, satisfying the conservation laws
The value of is .
A cut is a partition with , . Its capacity is
summed over the edges directed from to only.
Given a flow , an edge is used if and has spare capacity if . An augmenting path is a sequence of distinct vertices from to such that each step either follows an edge with spare capacity (a forward edge) or traverses a used edge backwards (a backward edge). Its augmentation amount is , where is the least spare capacity of a forward edge and the least flow on a backward edge ( when there is no backward edge).
For Chapter 14: in a finite simple graph with bipartition , a matching is a set of edges no two of which share an endpoint; it saturates a vertex that is an endpoint of one of its edges; and is the set of neighbors of the vertices in .
For every network there is a real number with
that is, is attained by some flow and bounds every flow value from above, and is attained by some cut and bounds every cut capacity from below.
The result. Theorem 13.10 turns every maximum-flow computation into a certified one: a flow and a cut of equal value prove each other optimal, and Theorem 13.4 shows no certificate can do better. Together with the integrality theorem 14.1 it is the engine behind the combinatorial applications of Chapter 14: maximum matchings in bipartite graphs, Hall's theorem, and the computation of the width of a poset with a minimum chain partition. Beyond the book, the same duality underlies Menger's theorem, König's theorem, the analysis of image segmentation by graph cuts, and the combinatorial theory of totally unimodular linear programs.
Formalizing it. The results are classical and proved. Mathlib has no theory of network flows. The platform has a Max-Flow Min-Cut theorem in the model of Bertsimas and Tsitsiklis (a general digraph on Fin n with capacities in , value compared in EReal), which does not cover the book's networks with zero capacities and is stated for a different encoding. This mission produces the theory in the book's model: finite oriented networks with real non-negative capacities, flows as functions on vertex pairs, cuts as vertex subsets, and the augmenting-path step that the Ford–Fulkerson labeling algorithm iterates. Hall's theorem is in Mathlib in its indexed-family form; the graph form stated here is new to the platform.
Theorem 13.4 is a finite-sum rearrangement. The difficulty of the goal is the existence of a maximum flow. The textbook argument runs the labeling algorithm until it halts, then reads off a cut from the labeled vertices. With real capacities this algorithm need not halt: with badly chosen augmenting paths and irrational capacities the flow values can converge to a limit strictly below the maximum, so "repeat until no augmenting path exists" does not by itself produce a maximum flow. The existence of an optimal flow is therefore not a by-product of the algorithm's description; it has to be established in its own right before the absence of augmenting paths can be turned into a cut of equal capacity. A formalization that assumes a maximum flow exists proves a strictly weaker statement. Proposition 13.7 is elementary but bookkeeping-heavy: backward edges subtract flow, and conservation must be checked at every interior vertex of the path.
The vertex set is a type V with [Fintype V] [DecidableEq V]. A network (AppliedComb.Flows.Network) bundles an edge relation adj, the source S and sink T with S ≠ T, and a real capacity function cap, together with the axioms of an oriented graph, the orientation of edges at S and T, and 0 ≤ cap x y on edges. Flows are functions ϕ : V → V → ℝ satisfying IsFlow, which includes off the edges and keeps the first conservation law as part of the definition, as on the page. The value is . A cut is its part L : Finset V with S ∈ L, T ∉ L. Augmenting paths are injective maps Fin (m + 1) → V, and are computed in WithTop ℝ so that an empty minimum is and when there is no backward edge. Hall's theorem uses Mathlib's SimpleGraph with a given bipartition into two Finsets and matchings as sets of Sym2 V edges.
No explicit constants arise: the chapter has no asymptotic or approximate statements.
The book's sentence of Theorem 13.10 reads "if is the maximum value of a flow and the minimum capacity of a cut, then ". A formalization that takes and as hypothetical extrema of possibly empty or unattained sets would be trivial or vacuous; the goal here asserts the existence of a maximum flow and a minimum cut at the same number, and the existence of a maximum flow for real capacities is part of what must be proved.
Needed infrastructure: finite-sum manipulation over Finset (reindexing, splitting over L and Lᶜ), existence of maximizers of a linear function over the set of flows, and, for Theorem 14.1, control of integrality. The definitions of networks, flows, cuts and augmenting paths are reusable for Menger's theorem, König's theorem and the chain-partition network of Section 14.3. Contributions of alternative proofs (via linear-programming duality) are welcome.
Ramsey theory studies the principle that complete disorder is impossible: every sufficiently large structure contains a large, perfectly uniform substructure. Its most familiar instance concerns graphs. In any graph on six vertices there are three vertices that are pairwise adjacent or three that are pairwise non-adjacent, and the same phenomenon persists at every scale. The quantity that measures it, the Ramsey number , is one of the most studied and least understood functions in combinatorics. Only a handful of values are known exactly (, ), while is only known to lie between 43 and 49 (Radziszowski, Small Ramsey Numbers).
The subject has a short, well-documented history. F. P. Ramsey proved the general theorem in 1930 as a lemma in decidability (Ramsey 1930). Erdős and Szekeres (1935) gave the upper bound (Erdős–Szekeres 1935). In 1947 Erdős proved an exponential lower bound for the diagonal numbers by counting graphs (Erdős 1947); this argument is now regarded as the origin of the probabilistic method. In 1959 Erdős used the same method to show that graphs of large girth and large chromatic number exist (Erdős 1959). For decades the exponential bases and stood essentially unchanged; the upper base was lowered below only in 2023 (Campos–Griffiths–Morris–Sahasrabudhe).
This mission formalizes these results as presented in Chapter 11 of Keller and Trotter, Applied Combinatorics (2017 Edition).
A graph is a finite simple graph: a finite vertex set with a symmetric, irreflexive adjacency relation (no loops, no multiple edges). A complete subgraph on vertices is a set of pairwise adjacent vertices; an independent set of size is a set of pairwise non-adjacent vertices.
A non-negative integer is a Ramsey bound for if every graph with at least vertices contains a complete subgraph on vertices or an independent set of size . The Ramsey number is the least positive Ramsey bound. In Lean these are AppliedComb.Ramsey.IsRamseyBound m n N and AppliedComb.Ramsey.ramseyNumber m n.
More generally, write and for the family of -element subsets of . For a string , the number is the least positive such that for every and every colouring some colour has a set of size all of whose -subsets receive colour (hypergraphRamseyNumber s r h).
The girth of a graph is the smallest number of vertices on a cycle, and infinite for a forest; the chromatic number is the least number of colours in a proper vertex colouring.
For every positive integer ,
Equivalently, below this threshold there is a graph on each number of vertices with neither a complete subgraph on vertices nor an independent set of size . The statement is for every , with no asymptotic slack.
A further item, not a milestone because the book does not number it, records the bound that the proof of Theorem 11.2 establishes: every graph with at least vertices has a complete subgraph on vertices or an independent set of size .
The goal is the diagonal lower bound that every later improvement is measured against. With the upper bound from the proof of Theorem 11.2 it shows that grows exponentially, with base between and . No explicit construction is known to give for any constant . Theorem 11.7 is the standard example of a statement whose only known proofs for decades were probabilistic, and it shows that chromatic number is not a local property.
On the formal side, Mathlib has cliques, independent sets, girth and chromatic number, but no Ramsey numbers, no Erdős lower bound and no high-girth theorem. The platform already has weaker or differently shaped relatives, all checked for this mission. Erdos1947.ramsey_lower_bound gives a graph on vertices without monochromatic -sets, a weaker bound than the goal's. BookSixth.high_girth_chromatic is a single-parameter form of Theorem 11.7 in another Lean environment. ramsey_theory_upper_bound is a diagonal bound. The goal statement carries the constant exactly, which requires an explicit, non-asymptotic lower bound for where the book writes "Stirling's approximation".
The obvious route to the goal is to count graphs with a large clique or independent set and compare the result with the total number of graphs. Two steps of that route do not go through as written in the text. First, the book replaces by its Stirling approximation, which is only asymptotic; a statement for every needs an inequality valid for all , and the constant leaves no room for a cruder estimate such as alone. Second, the counting argument yields a graph on each below the threshold, whereas is defined as a least threshold over all graphs with at least that many vertices; the two have to be connected.
Theorem 11.7 needs random graphs with edge probability depending on , a first-moment bound on short cycles and on independent sets, and a deletion step. The book states Theorem 11.6 without proof.
SimpleGraph V on a finite type V : Type (Theorems 11.1, 11.2, 11.4) or on Fin N (Theorem 11.7). Cliques and independent sets are SimpleGraph.IsNClique and SimpleGraph.IsNIndepSet on a Finset.IsRamseyBound m n N quantifies over every graph with at least vertices, as the book does; ramseyNumber m n is the sInf of the positive Ramsey bounds. Theorem 11.2 is stated as IsLeast {N | 0 < N ∧ IsRamseyBound m n N} (ramseyNumber m n), so its content is the nonemptiness of that set. The same pattern is used for Theorem 11.6.(n : ℝ) / (Real.exp 1 * Real.sqrt 2) * (2 : ℝ) ^ ((n : ℝ) / 2) ≤ (ramseyNumber n n : ℝ), with a real power. Explicit constant: the book says "use the Stirling approximation … after some algebra"; the statement keeps the book's constant and holds for every with no threshold.ramseyNumber, so it cannot hold through an empty defining set.SimpleGraph.egirth (valued in , for forests), not SimpleGraph.girth, which is on forests. Chromatic number is SimpleGraph.chromaticNumber in . The parameter of Theorem 11.7 is a natural number; negative is trivial.Fin n, with colours in Fin r.IsRamseyBound/ramseyNumber, the hypergraph version, an all- lower bound for , and counting over the labelled graphs on vertices. Proofs of any milestone are welcome contributions.Linear recurrences with constant coefficients are among the first tools of enumerative combinatorics and the analysis of algorithms: the Fibonacci numbers, the number of binary strings avoiding a pattern, the running time of a divide-and-conquer loop and the number of tilings of a strip all satisfy relations of the form . Chapter 9 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org) treats such relations as linear equations in an operator, the advancement operator, in direct analogy with linear differential equations with constant coefficients. The chapter's Principal Theorem says that the solution set of such an equation is a vector space whose dimension equals the order of the recurrence; everything else in the chapter (general solutions for distinct and repeated roots, and the reduction of nonhomogeneous equations to homogeneous ones) is organised around it.
This mission formalizes that theorem, in the book's model of functions on all of , together with the numbered lemmas of Section 9.5 on which its outline rests.
Let be the real vector space of all functions , with pointwise addition and scalar multiplication. The advancement operator is
a linear operator with for . For a nonnegative integer and real constants , the advancement operator polynomial is
so that . The solution space of the homogeneous equation is
the kernel of , a linear subspace of . In Lean, is AppliedComb.Recurrence.advance : Module.End ℝ (ℤ → ℝ), is opPoly k c for a coefficient vector c : Fin (k + 1) → ℝ with c i multiplying , and is solutionSpace k c := LinearMap.ker (opPoly k c). A factor is advance - r • 1.
For a positive integer and real constants with and ,
for some real constants .
The result itself. Theorem 9.18 is what justifies the standard recipe for solving a recurrence: once linearly independent solutions are found, every solution is a linear combination of them, and initial values pin down a unique solution. Theorems 9.21 and 9.22 name those solutions when the characteristic polynomial splits over , and Lemma 9.20 reduces nonhomogeneous recurrences, the ones arising from counting problems with a forcing term, to one particular solution plus the homogeneous space.
Formalizing it. The book states Theorem 9.18 without a full proof ("we won't prove the full result") and leaves Lemma 9.22 as an exercise, so a formalization supplies arguments the source omits. Mathlib's LinearRecurrence develops the -indexed, monic version (LinearRecurrence.solSpace_rank); the bi-infinite, two-sided setting of the book, in which the constant term must be nonzero, is not in Mathlib or on the platform as of this mission.
The subspace part of Theorem 9.18 is immediate; the content is the dimension count, in both directions. On a solution must extend to negative indices as well as positive ones, so an argument that works for sequences indexed by does not transfer: there the constant term plays no role and the dimension is whatever the constant term, while on a vanishing changes the answer. The outline in the book proceeds through factorisations of , which over need not exist (complex roots), so the goal cannot be obtained by combining Theorems 9.21 and 9.22 alone. Lemma 9.22 requires showing that the functions solve and that they exhaust its solutions, for ranging over all integers.
zpow), always of a nonzero base.Module.rank ℝ (solutionSpace k c) = k, a cardinal equality, so it also asserts finite-dimensionality.c : Fin (k + 1) → ℝ; c 0 is the leading coefficient and c (Fin.last k) the constant term .iff.Needed infrastructure: linear operators on the function space ℤ → ℝ, powers and products in Module.End, Module.rank/Module.finrank, and finite sums; Mathlib's LinearRecurrence may be adapted for the forward half. The definitions advance, opPoly and solutionSpace are reusable for any later mission on recurrences or on generating functions for bi-infinite sequences. Contributions of the milestone lemmas, of a proof of the goal that avoids factorisation over , and of a complex-valued variant are welcome.
Mathlib/Algebra/LinearRecurrence.lean (ℕ-indexed linear recurrences, LinearRecurrence.solSpace_rank). Mathlib docsChunk 10 formalized the discrete conjugacy theorem — the Legendre-Fenchel transform's bijection between the classes of M-convex and L-convex functions — and, along the way, a function-level generalization of Edmonds's intersection theorem. Section 8.4 turns that machinery toward a different question: not "how are two convexity classes related," but "when does a discrete optimization problem have a dual that meets it with equality." The classical route to such strong-duality results in continuous convex programming — Lagrangian relaxation, an embedding of the problem in a family of perturbed problems, and a saddle-point characterization of when primal and dual values coincide — has a discrete analogue that needs no continuity, no differentiability, and no convexity in the classical sense at all: only the elementary fact that the Legendre-Fenchel transform, once discretized, is still an involution on the right class of functions. This mission formalizes that discrete Lagrangian duality framework and its central saddle-point theorem, in full generality — before the book specializes it, in the section that follows, to the specific M-convex perturbation that gives the chapter's headline strong-duality result for M-convex programs.
Let and be finite ground sets. A perturbation of an optimization problem
is a function such that for all (Eq. (8.54)) and, for each
fixed , is self-biconjugate:
under the discrete Legendre-Fenchel transform of chunk 10 (Eq. (8.55)). The Lagrangian
function is (Eq. (8.58)),
valued in (formalized in EReal, since both the infimum and the
supremum below can be genuinely unbounded). The dual objective is (Eq. (8.60)). Writing , ,
, , the primal problem is to minimize over and the dual problem
is to maximize over .
Assuming is self-biconjugate (Eq. (8.55)): both and are finite and if and only if there exist , with finite and for all — a saddle point of the Lagrangian kernel. When this holds, and .
Theorem 8.52 (weak duality): always, with no biconjugacy hypothesis on at all — the baseline the saddle-point theorem sharpens to equality. Proposition 8.51(1)-(2): under self-biconjugacy, the perturbation (and hence the primal objective ) is itself recoverable from the Lagrangian kernel by a supremum, and — the algebraic identity the saddle-point theorem's proof turns on directly.
The result itself. The saddle-point theorem is the general-purpose engine behind every strong-duality result the book proves for specific classes of discrete optimization problems: the book's own next section specializes it (via a particular choice of built from an M-convex regularizer ) to obtain strong duality for M-convex programs, but the theorem itself needs no M-convexity, no submodularity, and no exchange axiom — only the elementary self-biconjugacy of a perturbation under the discrete Legendre-Fenchel transform. It is, in that sense, the most general and most reusable strong-duality statement in the book: any future mission proving strong duality for a specific class of discrete programs (M-convex, M2-convex, network flow, or otherwise) by exhibiting a self-biconjugate perturbation can cite this theorem directly rather than reproving the saddle-point argument from scratch.
Formalizing it. No matching item exists on the platform for a discrete Lagrangian saddle-
point theorem, discrete weak duality, or this perturbation-based duality framework. (A prior-art
search turned up an unrelated continuous Lagrangian saddle-point theorem for convex cones,
Luenberger's Chapter 8 §8.4, formalized as VectorSpaceOpt.lagrangian_saddle_sufficient_pointed
— a genuinely different setting: no discreteness, no biconjugacy hypothesis, and a one-directional
sufficiency statement rather than this mission's iff. Not reused.) This mission gives the first
formal statement of discrete Lagrangian duality, and directly reuses chunk 10's ConvexConjugate
apparatus (self-biconjugacy is stated using chunk 10's own conjugate-of-conjugate composition),
demonstrating exactly the kind of shared-substrate payoff the discrete conjugacy theorem was
built to provide.
The saddle-point theorem's "only if" direction is not a routine unwinding of definitions: given at finite common value, one must construct the saddle point — the book's proof takes , (which exist because the infimum/supremum are attained at a finite optimum) and verifies the sandwiching inequality using Proposition 8.51(2)'s identity together with weak duality, rather than by any direct algebraic manipulation of alone. Skipping straight to a "trivial" biconditional that never invokes Proposition 8.51 would misrepresent the actual proof structure the book relies on for exactly this direction.
are Fintype ground types; LagrangianKernel, DualObjective, InfP, SupD are
EReal-valued to keep both the defining infima/suprema total (a complete lattice) without an
artificial finiteness side-condition; OptP, OptD compare PrimalValue/DualObjective
against InfP/SupD after casting through chunk 10's ToEReal, mirroring that chunk's own
round-trip convention. "Finite" throughout is formalized as ≠ ⊤ ∧ ≠ ⊥ in EReal. The
perturbation itself is left fully abstract (an arbitrary function satisfying the
self-biconjugacy hypothesis where needed) — this mission does not draft the specific M-convex
perturbation (Eq. (8.61)) that the book's next subsection (§8.4.3) uses to specialize this
framework to M-convex programs, nor Theorem 8.59 (the resulting M-convex strong-duality
theorem) itself, which needs that specific perturbation plus its own regularity conditions
(REG)/(OBJ) and a chain of M-convex-specific propositions (8.55–8.58) beyond what the general
framework built here provides. A trivializing formalization would state the saddle-point
theorem's sandwiching inequality with a weaker order (e.g., only one of the two directions) or
would omit the "" consequence
clause; neither is done — both inequalities and the full consequence clause are included exactly
as the book states them.
Generating functions are the standard device of enumerative combinatorics for turning a counting sequence into a single algebraic or analytic object: a sequence is recorded as the power series , and operations on series (products, powers, derivatives) become operations on the counts. Chapter 8 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org), an open textbook used in undergraduate combinatorics courses, develops the method up to one of its classical applications: extending the binomial theorem to real exponents, as Newton did, and reading off an identity about central binomial coefficients that is awkward to prove by direct counting.
The identity in question,
appears in standard collections of binomial identities such as Graham, Knuth and Patashnik's Concrete Mathematics (1994).
For a real number and a nonnegative integer , the book defines a number by the recursion
so that with no requirement . The generalized binomial coefficient is
For integers this is the usual binomial coefficient; for integers it is ; for other real it is in general nonzero for every . In the Lean development is AppliedComb.GenFun.fallingP p k and is AppliedComb.GenFun.binomReal p k.
The generating function of a real sequence is the formal power series , in Lean PowerSeries.mk a : PowerSeries ℝ. When a closed-form function such as or is called the generating function of a sequence, the statements below read this as convergence of to the function's value on an explicit real interval around .
The central binomial coefficients are :
For every integer ,
stated as an identity of natural numbers.
The first five follow the chapter's own chain toward the goal; Theorem 8.16 is the chapter's other main result and is included as a reference.
Corollary 8.14 says that the sequence of central binomial coefficients convolved with itself is the sequence ; equivalently, the generating function of is a square root of . Central binomial coefficients count lattice paths with up-steps and down-steps, and the identity says that the pairs consisting of a balanced path of length and one of length , summed over , are equinumerous with all strings over a four-letter alphabet. The same generating function reappears in the book's Section 9.7, and Newton's theorem with exponent or is the standard route to closed forms for Catalan-type sequences.
On the formalization side, Mathlib has the central binomial coefficient (Nat.centralBinom), formal power series, and Newton's series in the complex-analytic form Complex.one_add_cpow_hasFPowerSeriesOnBall_zero, which is also published on the platform as FamousTheorems.newton_binomial_series_6b and included in this mission as a reference. It does not contain the convolution identity of Corollary 8.14, and it does not contain the book's recursive or the closed form of . The mission produces a machine-checked version of the chapter's chain from the book's own definitions to the identity.
The identity is not a special case of the Vandermonde convolution : both factors depend on the summation index in their upper argument as well as their lower one. Induction on does not close directly, since the sum for is not a simple combination of the sum for . A counting proof is possible but not obvious, which is why the chapter's route goes through a generating function with a non-integer exponent. That route passes from formal power series to real analysis: is a real function, and the passage from an identity of functions on an interval to an identity of coefficients requires the uniqueness of power series coefficients on an open interval and the product of two convergent series. The book asserts Newton's theorem without proof.
AppliedComb.GenFun.binomReal. Mathlib's descPochhammer and Ring.choose compute the same values; they are not used in the statements so that Lemma 8.11 is a statement about the book's recursion rather than a definitional unfolding.Real.rpow of a positive base on the left and HasSum (unconditional convergence of the series) on the right. The book's hypothesis is kept. No other explicit constants replace informal ones: the chapter's statements contain no , "" or "sufficiently large".PowerSeries ℝ with the sum written as over Finset.range (n + 1).ℕ with Nat.choose; the subtractions and occur only for and are exact. A statement asserting only that the square of the formal power series equals , or a purely formal version of Theorem 8.13, would hide the identity in a coefficient comparison and is not the book's statement; the goal is the explicit sum identity.FamousTheorems.card_odds_eq_card_distincts, stated for all with Mathlib's Nat.Partition, whose partitions are multisets of positive integers, as in the book (p. 168); the case it adds is immediate.A complete development needs real power series on an interval (Cauchy products, identity theorem for coefficients), the real power function, and elementary manipulation of binomial coefficients; the identification of binomReal with Ring.choose is reusable for any later statement using the generalized binomial coefficient. Proofs of any milestone are welcome independently, and so is a direct proof of Corollary 8.14 that bypasses the analytic chain.
Complex.one_add_cpow_hasFPowerSeriesOnBall_zero (Newton's binomial series). https://github.com/leanprover-community/mathlib4This mission completes chapter 7's L-convex function theory and closes the book on it. It first
finishes the theory of positively homogeneous L-convex functions — showing they coincide exactly
with the classical Lovász extensions of submodular set functions, a one-to-one correspondence
that recognizes forty years of submodular-optimization machinery as a special case of L-convex
function theory. It then proves the L-side capstone this series has been building toward since
mission 26-ch07b-lconvexfunctions: polyhedral L-convexity is characterized simultaneously by
directional derivatives, subdifferentials, and weighted-minimizer polyhedra — the exact mirror of
what mission 24-ch06d-mconvexfunctions proved for M-convex functions. Finally it develops quasi
L-convex functions, the L-side analogue of mission 25-ch06e-mconvexfunctions's quasi M-convex
functions, ending exactly where chapter 7 itself ends.
Fix a finite ground set . The class consists of polyhedral L-convex functions that are positively homogeneous; , its integer-valued integer-domain analogue. A positively homogeneous L-convex function induces a submodular set function ; conversely the Lovász extension of a submodular set function is positively homogeneous L-convex. The base polyhedron of a submodular is always an M-convex polyhedron. A function is quasi submodular (QSB) if or for all ; the weaker (QSBw) requires only .
For a polyhedral convex function with : is
L-convex if and only if every directional derivative is , if and only if every subdifferential is an M-convex polyhedron,
if and only if every weighted minimizer set is an L-convex polyhedron. Not present in this
chunk's own extraction table (its label opens mid-paragraph, missed by the same extractor failure
already documented for mission 25-ch06e-mconvexfunctions's Theorem 6.68), found by direct
reading and chosen as goal because it is the exact L-side mirror of mission
24-ch06d-mconvexfunctions's own milestone Theorem 6.63, and its proof is assembled entirely from
results already in this series (Theorem 7.43, Proposition 7.34, Theorem 7.40).
Fifteen further results build the two remaining pieces of chapter 7's theory. Propositions
7.37-7.39 and Theorem 7.40 establish the one-to-one correspondence between positively homogeneous
L-convex functions and submodular set functions via the Lovász extension; Proposition 7.41 gives
a minimizer-polyhedron characterization of this class, and Proposition 7.42 shows directional
derivatives of L-convex functions automatically land in it. Theorem 7.43 — the L-side mirror of
mission 24-ch06d-mconvexfunctions's own goal, Theorem 6.61 — proves the directional-
derivative/subdifferential correspondence via the induced submodular set function's base
polyhedron; Proposition 7.44 checks consistency at integer points, and Theorem 7.46 refines
Theorem 7.45 to the integral case. Theorem 7.49 (also missed by the extractor) gives the
quasi-submodularity implication hierarchy and its perturbation-equivalence capstone, mirroring
mission 25-ch06e-mconvexfunctions's Theorem 6.68 exactly. Proposition 7.50 and Theorems
7.51-7.52 build the level-set/perturbation machinery quasi submodularity needs; Theorems 7.53-7.54
(both missed by the extractor, the latter's full statement requiring one page beyond this
chunk's nominal range, at the very end of chapter 7) give the quasi L-optimality and quasi
L-proximity theorems.
The 0L/submodular correspondence (Theorem 7.40) is the precise sense in which L-convex function theory generalizes submodular set function theory rather than merely resembling it: every submodular set function is literally the restriction to of a positively homogeneous L-convex function, and every algorithm for one transfers to the other through this exact dictionary. The goal, Theorem 7.45, completes the parallel structure this series has built since chapter 6: M-convexity and L-convexity are now each characterized in the same four convex-analytic vocabularies, setting up chapter 8's conjugacy theorem, which will show these two characterizations are not merely analogous but literally dual to each other under the Legendre-Fenchel transform. The quasi-submodularity results matter for the same reason as their M-side counterparts: chapter 10's algorithms for L-convex-function minimization remain correct under nonlinear rescalings that destroy L-convexity itself but preserve quasi submodularity.
None of these results are open — they are Murota's account of how far L-convex function theory
extends beyond the polyhedral case (to positive homogeneity and its submodular-function
incarnation) and how far its exchange-style inequality can be relaxed while preserving
optimization theory (to quasi submodularity), mirroring chapter 6's identical two-part program for
M-convex functions. What this mission contributes is a faithful, machine-checked formal statement
of each, including four theorems (7.45, 7.49, 7.53, 7.54) the platform's own automated extractor
missed entirely — one of them requiring a page beyond this chunk's own nominal range to complete,
since chapter 7 ends there and this is the last mission covering it — extending the shared Lean
vocabulary (ZeroLR, BasePolyhedron, QSBw) this series builds on; no comparable formalization
exists on the platform (see Formalization scope).
The naive approach to the goal would try to prove all six pairwise implications among its four
conditions independently; the book's own proof instead chains through results already
established: (a)⇒(b) is Proposition 7.42, (a)⇒(c) is Theorem 7.43, (a)⇒(d) is Proposition 7.34,
(b)⇔(c) uses the 0L/M0[R] correspondence, and (d)⇒(b) is the genuinely hard direction, requiring
Proposition 7.41 applied to the directional derivative itself (showing
is an L-convex cone by an explicit description via the admissible-potential set of the distance
function underlying ). The remaining combinatorial difficulty in this block is in
Theorem 7.43's proof: identifying with the base polyhedron
requires the L-optimality criterion (Theorem 7.33, mission 27-ch07c-lconvexfunctions) applied
pointwise, a chain of logical equivalences with no single-step shortcut, exactly mirroring how
mission 24-ch06d-mconvexfunctions's Theorem 6.61 needed the M-optimality criterion.
Ground-set elements are a Fintype V with DecidableEq; L-convex functions are
(V→ℝ)→WithTop ℝ (polyhedral) or (V→ℤ)→WithTop ℝ (integer-domain). All sixteen numbered
results found in this chunk's page range — the twelve in BRIEF.md's own table plus four the
extractor missed (Theorems 7.45, 7.49, 7.53, 7.54) — are placed, with two documented,
content-preserving scope decisions: Theorem 7.43 omits the dual-integral refinement clauses for
L[R→R|Z]/L[Z→Z] (the same decision mission 24-ch06d-mconvexfunctions's Theorem 6.61 made),
and Proposition 7.50 states the general inequalities without restating their "In particular"
specializations, which add no independent content — see HARD.md. "" is
replaced by the equivalent (ArgMinR ...).Nonempty hypothesis throughout, matching mission
25-ch06e-mconvexfunctions's identical substitution. This mission's base vocabulary is
redeclared from missions 20-ch04b-mconvexsets, 21-ch05b-lconvexsets,
23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since
sibling drafts in this series cannot yet reference one another. Contributions completing any of
the sixteen sorrys are welcome; the goal and Theorem 7.43 carry the most independent proof
content.