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?
Partially ordered sets model precedence: tasks that must wait for other tasks, versions that supersede others, files nested in directories, alternatives ranked by several criteria at once. Two questions about such a structure recur in scheduling and in the design of algorithms. How many sequential "threads" are needed so that every item lies on a thread in which all items are mutually comparable? How many "rounds" are needed so that no round contains two comparable items? Dilworth's theorem answers the first and its dual, due to Mirsky, answers the second: in both cases the obvious lower bound, given by one large set of mutually incomparable (resp. comparable) items, is attained.
This mission formalizes Chapter 6 of Keller and Trotter's open textbook Applied Combinatorics (2017 Edition, appliedcombinatorics.org), whose capstone is Dilworth's theorem, together with the chapter's other three proved theorems on the same objects.
Timeline. Sperner (1928, doi:10.1007/BF01171114) showed that the largest family of subsets of a -set in which no member contains another has members. Dilworth (1950, doi:10.2307/1969503) proved that a finite poset whose largest antichain has elements can be partitioned into chains. Mirsky (1971, doi:10.2307/2316481) recorded the dual statement for antichain partitions. Fishburn (1970, doi:10.1016/0022-2496(70)90062-3) characterized the posets that arise from comparing real intervals as those with no subposet .
A poset is a set with a reflexive, antisymmetric and transitive relation . Here is finite and is represented by a finite type with a partial order. A subset is a chain if every two distinct points of are comparable; a subset is an antichain if every two distinct points of are incomparable. The empty set is both.
The width of is the largest size of an antichain, and the height the largest size of a chain:
A chain partition of into parts is a family of pairwise disjoint chains with union ; an antichain partition is defined the same way with antichains.
The subset lattice is the family of all subsets of a -element set, ordered by inclusion.
A poset is an interval order if each point can be assigned a closed real interval , degenerate intervals allowed, such that exactly when . The poset consists of two disjoint two-element chains with no comparabilities between them, and excludes if no four points of induce a copy of it.
For every finite poset with ,
The milestones stand on the same definitions as the goal (width, height, chain and antichain partitions, subposets) and are ordered from the one closest to the goal's statement to the one furthest from it.
The result itself. Dilworth's theorem is a min–max theorem: a minimum over covers equals a maximum over obstructions. It is equivalent to König's theorem on bipartite matchings and to Hall's marriage theorem, and it underlies the computation of minimum chain covers by bipartite matching and network flows (Chapter 14 of the same book). The dual theorem gives the layer decomposition used in scheduling with precedence constraints. Sperner's theorem is the first result of extremal set theory, and Fishburn's theorem is the basic structure theorem for interval orders, which model preferences with thresholds of indifference.
Formalizing it. All four results are classical and proved. In Mathlib at the environment revision of this mission there is no Dilworth or Mirsky theorem; Sperner's inequality (the upper bound on antichains in a Boolean lattice) is available through the LYM inequality, and there is no theory of interval orders. The Prove2Me library holds the easy half of Dilworth (an antichain is no larger than any chain partition) in a different Mathlib environment and over a different chain-partition structure. The mission asks for complete machine-checked statements of the book's four theorems over one common set of definitions.
For Dilworth's theorem the lower bound is a pigeonhole argument; the content is the existence of a partition into exactly chains. Greedy constructions fail: removing a longest chain, or a maximal chain through a chosen point, can leave a poset whose width has not decreased, so a partition built by repeatedly peeling chains may use more than of them. No local rule visible from a single chain decides whether its removal keeps the count at .
For Sperner's theorem the lower bound (the middle rank is an antichain) is immediate and the upper bound needs a counting argument over maximal chains; both halves are required, since the target is an equality. For Fishburn's theorem one direction is a four-line contradiction; the other requires constructing real intervals from nothing but the absence of .
The ground set is a type α with [PartialOrder α] [Fintype α]. Chains and antichains are
Mathlib's IsChain (· ≤ ·) and IsAntichain (· ≤ ·). width α and height α are
maxima of Finset.card over all antichains (resp. chains) of α; the family is never empty,
since the empty set qualifies, so both are well defined and equal for the empty poset.
Width is defined from antichains, not as the least number of chains in a partition; a
definition of the latter kind would make the goal true by definition and is ruled out. Chain and
antichain partitions are families indexed by Fin k of pairwise disjoint Finsets whose union
is all of α; empty parts are not excluded, which does not change either theorem. The "no fewer"
clauses quantify over every k and every such family. The subset lattice is
Finset (Fin t) ordered by inclusion, is t / 2 in ℕ, and Sperner's
theorem keeps the book's hypothesis . An interval representation is a pair of maps
a b : α → ℝ with a x ≤ b x; is Fin 2 ⊕ Fin 2 with the disjoint-sum
order, and "excludes" means there is no order embedding of it into α. Fishburn's theorem is
stated for finite posets: the book's construction of a representation is finite, and the
equivalence fails for some uncountable posets.
No statement contains an asymptotic bound, so no explicit constant is instantiated.
A complete development needs finite-poset combinatorics (induction on the ground set, subposets
as subtypes, maximal and minimal elements), which is reusable across order theory; results
proving the definitions agree with Mathlib's notions of chains in Finset lattices are
welcome, as is an alternative proof of Dilworth via Hall's theorem, which Mathlib has.
L-convex functions were defined purely combinatorially, on the integer lattice. Chapter 6's
M-convex theory showed that combinatorial definition always extends to a genuine convex function
on real space (missions 23-ch06c-mconvexfunctions/24-ch06d-mconvexfunctions); this mission
carries out the identical program for the L side. It first shows L-convexity is
exactly integral convexity plus ordinary submodularity — a clean synonym that also explains why
submodular set functions are a natural special case — then builds the entire polyhedral
(real-variable) theory of L-convex functions: the axioms (SBF[R])/(TRF[R]), two practical local
criteria for verifying submodularity without checking every pair of points, the fact that the
classical Lovász extension of a submodular set function is itself a polyhedral L-convex function,
the six-operation closure toolkit, and — this mission's goal — the L-optimality criterion in its
full polyhedral generality, characterizing global optimality by finitely many directional
derivatives.
Fix a finite ground set . A polyhedral convex function with nonempty effective domain is polyhedral L-convex, , if it satisfies (SBF[R]): , and (TRF[R]): , for all , ; it is polyhedral L-convex if its lift to one extra real coordinate is polyhedral L-convex. A function is integrally convex if its convex closure agrees, at every real point, with the closure taken using only that point's integral neighborhood. The Lovász extension of a submodular set function is the piecewise-linear interpolation built from the sorted distinct components of . The directional derivative is .
For a polyhedral L-convex function and : for all if and only if for every and ; for polyhedral L-convex , the criterion simplifies to
for every . This is the direct L-side mirror of mission 24-ch06d-mconvexfunctions's
M-optimality criterion (Theorem 6.52) and the polyhedral generalization of mission
08-lconvex-functions-i's integer-domain L-optimality criterion (Theorem 7.14): checking global
optimality against exponentially many points reduces to (or ) directional-derivative
inequalities.
Twelve further results build the polyhedral theory from the ground up. Theorems 7.20-7.21
identify L-convexity with the conjunction of ordinary submodularity and integral
convexity — a genuinely different, function-analytic characterization from the exchange-axiom-
style definitions used so far. Propositions 7.23-7.24 give two practical sufficient conditions
for verifying (SBF[R]) locally, at a single scale, rather than globally. Proposition 7.25 shows
the Lovász extension of any submodular set function is automatically polyhedral L-convex — not
in this chunk's own extraction table (its label is preceded by an unlabeled restatement of the
same fact, which evidently confused the extractor), found and placed by direct reading. Theorem
7.26 shows an L-convex function's convex extension, when polyhedral, inherits polyhedral
L-convexity, continuing mission 26-ch07b-lconvexfunctions's Theorem 7.19. Theorems 7.28-7.32
restate the discrete theory's core equivalences (translation submodularity, the L/L
correspondence, the six basic operations, restrictions) in the polyhedral setting, and Proposition
7.34 shows minimizer sets of linearly-perturbed polyhedral L-convex functions are themselves
L-convex polyhedra — flagged by the book itself as a partial result whose full converse
characterization (Theorem 7.45) lies beyond this chunk's range.
Theorems 7.20-7.21's synonym is structurally important: it means every algorithm and theorem already known for submodular-function minimization over -type domains applies, after a midpoint-convexity check, to the vastly larger class of integer-lattice L-convex functions, with no new proof technique required. Proposition 7.25 is the bridge that lets the combinatorial Lovász extension — the workhorse of submodular optimization for forty years — be recognized as a special case of the polyhedral L-convex function theory this mission builds, explaining why algorithms for one transfer so readily to the other. The goal, Theorem 7.33, is the precise tool chapter 10's continuous-relaxation algorithms for L-convex-function minimization actually verify against: a scaling algorithm's claimed optimum is confirmed correct exactly by checking the criterion's finitely many directional-derivative inequalities.
None of these results are open — they are Murota's account of how the integer-lattice theory of
L-convexity survives, result by result, the passage to polyhedral convex functions on , mirroring chapter 6's identical program for M-convexity. What this mission contributes is a
faithful, machine-checked formal statement of each, including one result (Proposition 7.25) the
platform's own automated extractor missed, extending the shared Lean vocabulary (SBFR, TRFR,
LovaszExtension, DirDeriv) this series builds on; no comparable formalization exists on the
platform (see Formalization scope).
The naive approach to the goal would try to verify directly against every ; the book's actual proof instead reduces this to the finite family of directional derivatives via Theorem 7.20's integral-convexity fact (an L-convex function's local behavior determines its global behavior) applied to the polyhedral setting through Theorem 3.21's general optimality criterion for integrally convex functions — a two-layer reduction (polyhedral integral-convexity finite local check) with no direct one-step argument. The genuine combinatorial content in this block is in Proposition 7.25's proof: showing the Lovász extension is submodular requires the finite-valued case (a direct calculation split on whether the two perturbed coordinates land in the same or different threshold sets) and then a limiting argument over a sequence of finite-valued truncations for the general, possibly-infinite case — a genuine two-step argument, not a single inequality chase.
Ground-set elements are a Fintype V with DecidableEq; polyhedral L-(natural-)convex
functions are (V→ℝ)→WithTop ℝ. All thirteen numbered results found in this chunk's page range
are placed, with one documented scope reduction: Proposition 7.24 states only part (1) (the
unconditional-on-magnitude sufficient condition), not part (2)'s sharper, sorted-index-restricted
version, which needs the same SortedValues apparatus a second time for no other result's
benefit — see HARD.md. "" and its variants are replaced by the equivalent
(DomR ...).Nonempty hypothesis throughout, matching mission 24-ch06d-mconvexfunctions's
identical substitution. "Domain is closed"/"domain is an interval" (Propositions 7.23-7.24) are
stated via Mathlib's IsClosed and Set.OrdConnected respectively, the latter being the precise
order-theoretic notion of "interval" in a pointwise-ordered space. This mission's base vocabulary
is redeclared from missions 08-lconvex-functions-i, 20-ch04b-mconvexsets (for the Lovász
extension machinery), 21-ch05b-lconvexsets, 23-ch06c-mconvexfunctions/
24-ch06d-mconvexfunctions, and 26-ch07b-lconvexfunctions rather than imported, since sibling
drafts in this series cannot yet reference one another. Contributions completing any of the
thirteen sorrys are welcome; the goal and Proposition 7.25 carry the most independent proof
content.
Chapter 5 characterized L-convex sets — sublattice-closed, translation-periodic subsets of
— and showed they interact cleanly with integral convexity. Chapter 7 asks the
functional analogue: which functions on the integer lattice deserve to be called convex in the
"L" sense, and how do they relate back to L-convex sets? This mission (continuing mission
08-lconvex-functions-i, which built the axioms (SBF[Z])/(TRF[Z])/(SBF[Z]) and proved
the L-optimality and L-proximity theorems) answers the second question at its sharpest: an
L-convex function is exactly a function whose every weighted-minimizer set is an L-convex
polyhedron — the discrete analogue of the fact that a convex function is determined by the convex
geometry of its sublevel sets. Along the way it settles the chapter's basic toolkit: operations
that preserve L-convexity, the local nature of submodularity, the correspondence with ordinary
submodular set functions, and the first two structural facts about the convex extension every
L-convex function admits.
Fix a finite ground set . A function with nonempty effective domain is L-convex, , if it satisfies submodularity (SBF[Z]): , and translation invariance (TRF[Z]): , for all . It is L-convex if its lift to one extra coordinate (Eq. (7.2)) is L-convex. A set function is submodular if ; it corresponds to an L-convex function supported on via (Eq. (7.5)). The convex closure of is its extension to by finite convex combinations.
For with bounded nonempty effective domain:
is L-convex if and only if is an L-convex set for every ;
the L analogue holds with L-convex sets. This is the direct mirror of
mission 23-ch06c-mconvexfunctions's own goal (Theorem 6.43, characterizing M-convex functions
via M-convex weighted-minimizer polyhedra) — the book's text calls it exactly "how the concept of
L-convex functions can be defined from that of L-convex sets."
Eleven further results build the chapter's basic vocabulary. Theorem 7.2 strengthens translation submodularity to allow negative shifts; Theorem 7.3 places L-convexity inside L- convexity; Proposition 7.4 identifies submodular set functions with a subclass of L-convex functions via the indicator embedding, and Theorem 7.15 derives the classical submodular-minimizer local-optimality criterion as its corollary; Proposition 7.5 shows submodularity is a local property, needing only unit-distance pairs; Proposition 7.8 transfers L-(natural-)convexity from functions to their effective domains; Proposition 7.9 and Theorem 7.10–7.11 give the chapter's basic examples (univariate and pairwise-difference functions) and its six-operation closure toolkit (scaling, affine reparametrization, linear perturbation, projection, infimal convolution with a separable function, and sums), both for L-convex and L- convex functions, the latter also admitting interval and coordinate restrictions; Proposition 7.16 shows minimizer sets of L-convex functions are themselves L-convex, the special case () the goal generalizes to every linear perturbation; Theorem 7.19 begins the convex-extension program this chapter's next chunk completes, establishing that the convex closure agrees with on and inherits its translation constant.
The goal is significant for the same structural reason as its M-side counterpart: it says
L-convexity is not merely a combinatorial condition on lattice differences but is equivalent to
a purely polyhedral-geometric one, closing the loop between chapters 5 and 7 the way Theorem 6.43
closes the loop between chapters 4 and 6. Theorem 7.15's corollary status is itself instructive:
the well-known fact that a submodular set function's global minimizer needs only local
verification against comparable sets — the theoretical basis of every submodular-minimization
algorithm in chapter 10 — falls out of the L-optimality criterion (mission
08-lconvex-functions-i's Theorem 7.14) applied to the indicator embedding, rather than needing
an independent proof. Theorem 7.10–7.11's six operations are the toolkit every later construction
in this chapter and chapter 9's network transformations builds new L-convex functions from old.
None of these results are open — they are Murota's account of the basic function-level theory of
L-convexity, mirroring chapter 6's M-convex function theory chunk-by-chunk. What this mission
contributes is a faithful, machine-checked formal statement of each, extending the shared Lean
vocabulary (SBF, TRF, LNaturalConvex, LConvexSet) that missions 08-lconvex-functions-i
and 21-ch05b-lconvexsets began; no comparable formalization exists on the platform (see
Formalization scope).
The naive approach to the goal would try to verify L-convexity's submodularity inequality directly against the definition of an L-convex set applied to each minimizer family; the book's actual proof instead routes through Theorem 7.10 (3)'s closure of L-convexity under linear perturbation and Proposition 7.16's minimizer-is-L-convex-set fact for the forward direction, and defers the converse entirely to a later note (Note 7.47, outside this chunk and mission 08's combined range) proved via the integral-convexity machinery of section 7.7 onward. The genuine combinatorial difficulty in this block is upstream, in Theorem 7.10 (5)'s infimal-convolution operation: proving L-convexity of the perturbed function requires a four-term submodularity inequality assembled from the separable function's own convexity and 's submodularity applied at the optimal simultaneously — a genuine two-hypothesis combination with no single-inequality shortcut.
Ground-set elements are a Fintype V with DecidableEq; L-(natural-)convex functions are
(V→ℤ)→WithTop ℝ. All twelve numbered results found in this chunk's page range are placed, with
one documented scope reduction: Theorem 7.19 states only parts (3)-(4) (that the convex closure
agrees with on and inherits its translation constant), not the explicit
Lovász-extension-formula construction of parts (1)-(2) and (5), which needs a sorted-distinct-
component apparatus no other result in this chunk requires — see HARD.md. "" and
its variants are replaced by the equivalent (DomZ ...).Nonempty hypothesis throughout, matching
mission 24-ch06d-mconvexfunctions's identical substitution (WithTop ℝ has no
element). This mission's base vocabulary (SBF, TRF, LNaturalConvex, etc.) is redeclared
verbatim from mission 08-lconvex-functions-i rather than imported, since sibling drafts in this
series cannot yet reference one another; LConvexSet is likewise redeclared from mission
21-ch05b-lconvexsets. Contributions completing any of the twelve sorrys are welcome; the goal
and Theorem 7.10 carry the most independent proof content.
Bernoulli's law of large numbers says that the relative frequency of a single event in independent trials converges in probability to . Statistics and learning theory need more: the probabilities of a whole class of events are judged from one and the same sample, so the frequencies must converge uniformly over the class. Uniform convergence can fail even for simple classes (all open subsets of ), so one needs a criterion that says when it holds and how fast.
Vapnik and Chervonenkis gave the first distribution-free answer in On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities (Theory Probab. Appl. 16 (1971) 264–280, doi:10.1137/1116025). Its Theorem 2, now called the VC inequality, bounds the probability of a uniform deviation larger than by a combinatorial quantity of the class times an exponentially small factor.
Timeline:
Let be a probability space and a collection of measurable events , with probabilities . A sample of size is a sequence of points of drawn independently with law , so the sample has the product law on . The relative frequency of in the sample is , where is the number of sample terms in . The uniform deviation is
Each induces in a sample the subsample of terms lying in . The index is the number of different subsamples so induced (at most ), and the growth function is over all samples of size .
For a double sample let and be the frequencies of in the two semi-samples and , and let
Following the paper, and are assumed to be measurable functions of the sample for every .
For every and every ,
The constants and and the growth function at are the paper's.
The bound holds for every distribution and depends on the class only through . Together with the paper's Theorem 1 (the growth function is either for every or bounded by ), it shows that every class whose growth function is not identically enjoys uniform convergence at an exponential rate in probability and almost surely. The Glivenko–Cantelli theorem is the special case of rays on the line. The inequality underlies sample-complexity bounds for empirical risk minimization, the "finite VC dimension implies learnability" direction of the fundamental theorem of statistical learning, and the theory of empirical processes indexed by sets.
The result has been proved for more than fifty years; what is missing is a machine-checked proof of it in its original form. Formal libraries contain Hoeffding-type inequalities for independent variables and textbook uniform-convergence statements with other constants, stated for hypothesis classes and loss functions. This mission produces the 1971 statement itself, with its constants and its sequence-based index, together with the combinatorial tail bound for sampling without replacement that the paper states without proof.
The obvious argument applies Hoeffding's inequality to each and takes a union bound. This fails as soon as is infinite, and the classes of interest are uncountable. The growth function can only enter after the probabilities have been removed from the event, because only then does the event depend on the finitely many subsamples that induces on a finite sample. Lemma 2 does this at the price of the condition and a factor .
The second difficulty is combinatorial. Under a random rearrangement of a fixed double sample, the number of points of an event that fall into the first half is hypergeometric, not binomial. The paper states the required tail bound and omits the "simple but long computation". Mathlib has no tail bound for sampling without replacement.
Samples are functions Fin l → X with 0-based positions; repetitions are allowed. The subsample induced by is the set of positions {i | x i ∈ A}, so the index counts distinct sets of positions and the growth function maximizes over sequences, not finite point sets (the paper's model; the two differ when has fewer than points). The sample law is Measure.pi (fun _ : Fin l => P). The double sample is Fin (l + l) → X, read through Fin.castAdd and Fin.natAdd, and is growth S (2 * l). Suprema are real suprema over the events of (values in ; for ). Probabilities are values in and the bounds enter through ENNReal.ofReal. Theorem 3 uses the infinite product Measure.infinitePi and evaluates on the first coordinates.
The measurability of (p. 265) and of (p. 268) are the paper's own assumptions and are carried as hypotheses. Without them Theorem 2 can fail for uncountable classes; replacing them by a stronger condition such as countability of would weaken the theorem.
A trivializing formalization is ruled out as follows: is stated, which forces and so avoids the value of the frequency. The supremum runs over the events of , not over all subsets. The index counts distinct subsamples, not sets.
Corrections of the printed text:
Needed infrastructure:
Measure.pi under permutations of coordinates;Fin (l + l) into two halves under the product measure;The last two are reusable beyond this mission. Proofs of any milestone are welcome.
Milgrom and Shannon's theory of quasi-supermodularity, developed for monotone comparative statics in economics, showed that many of the consequences of lattice submodularity survive under a much weaker, purely ordinal relaxation of the defining inequality. Chapter 7's final section imports this idea into discrete convex analysis: does L-convexity's optimality and proximity theory survive when the additive submodularity inequality is relaxed to an ordinal condition on the sign pattern of the two relevant differences, rather than their sum? This mission formalizes the chapter's answer for the strongest of the relevant relaxations, (SSQSB) (semistrict quasi submodularity): yes, and the class is large enough to include every strictly increasing rescaling of an L-convex function — exactly mirroring chunk 07's result for the M-convex side, and completing the "quasi" theory on both halves of the exchange-axiom framework before chapter 8 unifies them under conjugacy.
Let be a finite ground set and . Building on chunk 08's submodularity axiom (SBF[Z]), this section introduces four ordinal relaxations. is quasi submodular, satisfying (QSB), if for every , or . is semistrictly quasi submodular, satisfying (SSQSB), if additionally and symmetrically. The weak variants (QSBw) and (SSQSBw) restrict attention to points of the effective domain and compare against directly, with (SSQSBw) additionally allowing the four-way tie . The linear perturbation of by is .
Let satisfy (SSQSB) and for all , , a positive integer. If satisfies for all , then and there is with the componentwise bound — verbatim the same conclusion, and the same exact bound, as chunk 08's Theorem 7.18(1), now established for the strictly larger class satisfying (SSQSB) rather than (SBF[Z]).
Theorem 7.49: the full nesting chain (SBF[Z]) (SSQSB) (QSB), (SSQSB) (SSQSBw) (QSBw), together with the collapse theorem that (SBF[Z]) holds if and only if every linear perturbation of satisfies (QSBw) — precisely quantifying how weak (QSBw) is pointwise and how the classes reunite under universal perturbation. Theorem 7.53 (the quasi L-optimality criterion): the direct analogue of chunk 08's Theorem 7.14, showing that global (or, for the weaker (QSBw) case, unique-up-to-translation) optimality still reduces to a purely local check against the nontrivial sign-pattern neighbors .
The result itself. As with the M-convex case (chunk 07), the proximity theorem is what algorithms actually need: an L-convex-flavored objective transformed by any strictly increasing scalar rescaling (a common device — expressing a network-flow cost in a different currency, or applying a monotone risk adjustment) retains a scaling algorithm's correctness guarantee with exactly the same distance bound, even though the rescaled function is generally no longer L-convex itself.
Formalizing it. No matching item exists on the platform for quasi submodularity or quasi L-convexity in any form. Together with chunk 07 (the M-side quasi-convexity theory), this mission completes the "quasi" relaxation on both halves of the exchange-axiom framework the book develops, immediately before chapter 8 unifies M-convexity and L-convexity under a single conjugacy relationship.
As with chunk 07's quasi M-proximity theorem, the temptation is to imitate chunk 08's L-proximity proof line by line. The overall architecture does survive — translate so , find a lattice-minimal sufficiently-good point, and bound the gap using submodularity — but chunk 08's proof uses (SBF[Z])'s additive inequality directly to compare four function values at once, while this proof must instead route every such comparison through (SSQSB)'s two one-directional implications (Proposition 7.50's quasi-version of the same two-sided inequality), which only ever license moving in one direction at a time depending on which side of a comparison is tight. The book's proof handles this by working with the specific implications (7.43)–(7.44) in place of the L♮-approach property used in chunk 08's proof — an ordinal substitute for the same additive step, at the cost of a case analysis chunk 08's proof did not need.
This mission builds directly on chunk 08's published items (SBF, DomZ, ArgMin,
IndicatorVec), per the platform's textbook convention that a later chapter section of the same
book imports an earlier one's definitions; its own namespace
DiscreteConvex.LConvexFunctions.Quasi nests under chunk 08's DiscreteConvex.LConvexFunctions
accordingly. Note the sign convention of the linear perturbation here, , is the opposite of the M-side's
(chunks 06–07) — verified against the book's own formula rather than assumed by analogy.
A trivializing formalization of the goal would silently strengthen (SSQSB) back to plain
(SBF[Z]) (making this mission redundant with chunk 08's Theorem 7.18) or loosen the exact bound
; neither is done. Only (QSB), (SSQSB), (QSBw), (SSQSBw) are drafted, matching
exactly what the chosen three items need; the polyhedral L-convex-function bridge (§7.8–7.9,
Theorems 7.40–7.46) and the level-set characterizations (Theorems 7.51–7.52) are left for a
follow-on mission. Contributions building the 0L ↔ S correspondence (Theorem 7.40, a bridge
back to chunk 04's submodular-set-function vocabulary) or the scaled quasi L-minimizer-cut
analogue are welcome.
Every characterization of M-convexity so far in this series — the exchange axiom, the
optimality criterion, convex extensibility, the directional-derivative/subdifferential
correspondence — has been an equivalence with M-convexity itself: a function either is M-convex
or it is not. Section 6.14 asks a different question: what happens when the exchange axiom's
defining inequality is relaxed to only the sign patterns it actually forces? The answer is a
hierarchy of "quasi M-convex" conditions — weaker than M-convexity, strong enough to keep the
optimality criterion and the proximity/minimizer-cut theorems intact — and, at the top of that
hierarchy, a genuinely new characterization of M-convexity itself: a function is M-convex if and
only if every one of its linear perturbations is quasi M-convex in the weakest sense. This
mission formalizes that entire hierarchy and its capstone, plus two further characterizations of
polyhedral M-convexity (via directional derivatives, subdifferentials, and weighted-minimizer
polyhedra) that complete the real-variable theory chunk 24-ch06d-mconvexfunctions began.
Fix a finite ground set and . Write
. Relaxing the exchange axiom's inequality
to the sign patterns it forces gives quasi
M-convexity (QM) and semistrict quasi M-convexity (SSQM), and requiring only some pair
rather than every gives their weaker variants (QMw), (SSQMw); the minimization-only
variants (SSQM), (SSQM) replace "" with "". The set-level analogue (Q-EXC)/(Q-EXCw) relaxes the M-convex-set exchange axiom
the same way. For , the level set . A polyhedral convex function is (real-variable) M-convex, , if it satisfies the
real exchange axiom (M-EXC[R]) from chunk 24-ch06d-mconvexfunctions; denotes
polyhedra realized as for a triangle-inequality distance function , and
denotes real M-convex polyhedral cones.
For : (1) the implication diagram (M-EXC[Z]) (SSQM) (QM), (M-EXCw[Z]) (SSQMw) (QMw), (M-EXC[Z]) (M-EXCw[Z]), (SSQM) (SSQMw), (QM) (QMw); (2) satisfies (M-EXC[Z]) if and only if satisfies (QMw) for every . This theorem is not named in the chunk's own extraction table — the automated extractor, which requires a result's label to start a text line, misses it because it opens mid-paragraph directly after an ASCII-rendered implication diagram — but it is the capstone of the section: its own proof is "combining Theorems 6.72 and 6.74," both formalized here as milestones, and part (2) answers exactly the question a reader of this stretch would ask: what does the entire apparatus of quasi M-convexity ultimately say about M-convexity itself?
Fourteen further results build the hierarchy and complete the real-variable theory. Proposition
6.62 checks the two halves of chunk 24-ch06d-mconvexfunctions's Theorem 6.61 agree at integer
points. Theorems 6.63–6.64 add two more characterizations of polyhedral M-convexity — via
positively homogeneous directional derivatives and -valued subdifferentials, and
via /-valued weighted-minimizer polyhedra — to the
convex-extensibility characterization chunk 23-ch06c-mconvexfunctions proved. Theorem 6.67 gives
two equivalent reformulations of (QMw) as pointwise inequalities; Propositions 6.69–6.70 and
Theorems 6.72–6.74 build the level-set/perturbation machinery the goal needs. Theorem 6.75 is the
(SSQM) analogue of Theorem 6.67. Theorem 6.76 is the quasi M-optimality criterion
(optimality still characterized by local non-improvement, under only the weak quasi-convexity
hypotheses). Theorems 6.77–6.79 show the M-minimizer-cut and M-proximity theorems (from missions
06-mconvex-functions-i and 23-ch06c-mconvexfunctions) hold verbatim under the strictly weaker
(SSQM) hypothesis.
The hierarchy's practical payoff is immediate: Theorems 6.77–6.79 mean the algorithms of chapter
10 that rely on minimizer cuts and proximity bounds do not actually need the full exchange axiom
to run correctly on nonlinearly rescaled M-convex functions (Example 6.66 shows any nondecreasing
scaling of an M-convex is quasi M-convex, yet nonlinear scalings are common in
practice and destroy M-convexity itself). The goal, Theorem 6.68, is significant independently:
it says the exchange axiom — a condition that looks irreducibly combinatorial, quantifying over
pairs of points and directions — is equivalent to a purely ordinal, perturbation-based
condition (every linear tilt of has no strict local improvement that a level set can't
witness), giving a genuinely different lens on why M-convexity is the right discrete analogue of
convexity. Theorems 6.63–6.64 close out chunk 24-ch06d-mconvexfunctions's program of
characterizing polyhedral M-convexity in every classical convex-analytic vocabulary at once
(directional derivatives, subdifferentials, weighted minimizers), completing the bridge to
Chapter 8's duality theory that chunk builds toward.
None of these results are open — they are Murota's account of how far the exchange axiom's
defining inequality can be relaxed while keeping optimization theory intact. What this mission
contributes is a faithful, machine-checked formal statement of each, including four theorems
(6.68, 6.76, 6.77, 6.78) the platform's own automated extractor missed entirely, extending the
shared Lean vocabulary (DeltaF, QMw, LevelSet) the Discrete Convex Analysis series builds
on; no comparable formalization exists on the platform (see Formalization scope).
The naive approach to the goal would try to prove the implication diagram's six arrows and the perturbation equivalence as six independent facts; the book's own proof of part (2) instead derives it in one step from Theorems 6.72 and 6.74 — themselves nontrivial (Theorem 6.74's proof strengthens the local exchange axiom equivalence (Theorem 6.4) to hold whenever the domain merely satisfies (Q-EXCw), then runs a bipartite-matching argument on a 4-point neighborhood to verify the resulting local condition). The difficulty is genuinely upstream of the goal's own statement: everything the goal needs is already proved by the time Theorem 6.68 is reached, so the formalization work is in stating the sixteen distinct axioms and their level-set reformulations precisely enough that "combining 6.72 and 6.74" is literally how a Lean proof would proceed.
Ground-set elements are a Fintype V with DecidableEq; integer-domain functions are
(V→ℤ)→WithTop ℝ, real-domain ones (V→ℝ)→WithTop ℝ. All fifteen numbered results — including
the four (6.68, 6.76, 6.77, 6.78) the automated extractor missed because their labels open
mid-paragraph — are placed as milestone or goal, and every clause of every one is stated in
full; no partial-coverage scope reduction was needed in this chunk (contrast chunks
22-ch06b-mconvexfunctions/24-ch06d-mconvexfunctions, which restated 4-of-8-part operations
theorems). Two formalization choices are recorded in HARD.md/MODERATION_NOTES.md: "" is replaced by the equivalent (ArgMinOn ...).Nonempty hypothesis (WithTop ℝ
has no element), matching mission 23-ch06c-mconvexfunctions's identical substitution;
and / are realized via the book's own
indicator-function device rather than a freestanding cone axiom. This mission's definitions are
redeclared from chunks 06-mconvex-functions-i, 22–24-ch06*-mconvexfunctions rather than
imported, since sibling drafts in this series cannot yet reference one another. Contributions
completing any of the fifteen sorrys are welcome; the goal and Theorem 6.74 carry the most
independent proof content.
Second-order elliptic equations in divergence form, such as , model steady diffusion, electrostatics in inhomogeneous media and linear elasticity. They are also the stationary part of every parabolic and hyperbolic problem studied later in the same notes. When the coefficients are only bounded and measurable, classical solutions need not exist. The modern theory replaces them by weak solutions in the Sobolev space and settles existence, uniqueness and solvability by Hilbert-space methods. This mission formalizes that theory as presented in Chapter 4 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014). The chapter follows the standard development of Evans, Partial Differential Equations, Chapter 6, and of Gilbarg–Trudinger, Chapter 8.
Timeline. Riesz (1907) and Fréchet represented bounded functionals on Hilbert spaces. Fredholm (1903) proved the alternative for integral equations of the second kind, and Riesz (1918) extended it to compact operators. Lax and Milgram (1954) removed the symmetry assumption from the Riesz approach, and Gårding (1953) proved the coercivity estimate for elliptic forms. Together these give the existence and Fredholm theory for the Dirichlet problem stated here.
Let be open. A test function is a smooth with compact support in . The space is the closure of the test functions in the norm ; each element carries a function and a weak gradient , both square-integrable. is the space of bounded linear functionals on , and acts on it by .
Given coefficients with , the operator is
It is uniformly elliptic if for some , almost every and every . Its bilinear form on is
and the formal adjoint has the form . For , is a weak solution of with on if and for all . The resolvent maps to that solution.
A bounded operator on a Hilbert space is Fredholm if its kernel is finite-dimensional and its range is closed with finite-dimensional orthogonal complement. Its index is .
For bounded, uniformly elliptic and , exactly one of the following holds:
with non-unique solutions in case (2). Every kernel and equation is meant in the weak sense on .
The Fredholm alternative is the complete linear solvability theory of the Dirichlet problem for general elliptic operators on bounded domains. Uniqueness for the homogeneous problem is equivalent to existence for all data. When uniqueness fails, the obstruction is a finite set of orthogonality conditions given by the adjoint problem. This feeds directly into the spectral theory of Theorem 4.25, into eigenfunction expansions, and into the existence theory for parabolic and hyperbolic equations (Galerkin approximation in later chapters). Nonlinear elliptic problems are routinely reduced to it through linearization and the implicit function theorem.
Mathlib has Lax–Milgram for continuous coercive forms, compact operators, the Riesz representation theorem and the spectral theorem for compact self-adjoint operators. It does not have Sobolev spaces with zero boundary values as used here, elliptic bilinear forms, Fredholm operators or their index. As far as a search of the platform shows, none of these results has a machine-checked statement for elliptic operators with coefficients. The mission would give formal statements, and eventually proofs, of textbook results that are fully proved on paper.
The abstract functional analysis is close to the library. The difficulty lies in connecting it to the PDE objects. Gårding's inequality needs pointwise uniform ellipticity turned into an integral bound on the weak gradient, with the non-symmetric first-order term controlled explicitly enough to reach the stated . Compactness of the resolvent needs the Rellich–Kondrachov theorem: embeds compactly in for bounded , which is not in Mathlib in this form. The goal then relates the weak problem on to operator statements on in both directions, including the solution spaces and the adjoint's kernel. A proof that argues only on , without tracking that the solutions lie in and satisfy the weak identity for every test function, does not reach the stated result.
EuclideanSpace ℝ (Fin n) with Lebesgue measure. Coordinates are 0-based.H10 n Ω) is modelled by jets. It is the closure, in , of the pairs for smooth compactly supported with support in . Its norm is exactly the standard norm, and it is a Hilbert space. is StrongDual ℝ (H10 n Ω).Coeffs n. Admissible is membership plus a.e. symmetry. Uniform ellipticity carries .Lp ℝ 2 on .Module.finrank and is only used for Fredholm operators.finrank equality between two infinite-dimensional spaces (both in Lean) cannot stand in for the book's claim.Needed infrastructure, reusable beyond this mission: the jet model of and its Poincaré inequality, Gårding-type estimates, a Rellich–Kondrachov compactness theorem for , and Fredholm operators with index on Hilbert spaces. Contributions of any of these as separate lemmas are welcome.
Two problems in this mission, both about markets that do not behave the way the textbook Black–Scholes market does, and both solved by the same technique.
The first is portfolio choice in a pure jump market. Prices move by jumps at the epochs of a Poisson process, not by continuous Brownian fluctuation. This is not a technical variation: the market is incomplete, there is no replicating portfolio, and the machinery of stochastic analysis that makes the diffusion case tractable is unavailable. What is available instead is that the wealth process is piecewise deterministic — between jumps it follows an ODE, and all the randomness is in when the jumps happen and how big they are. Chapter 8's technique embeds such a process in its jump chain and turns the continuous-time control problem into a discrete-time Markov Decision Model with infinite horizon; Chapter 7's contracting theory then solves that.
The second is trade execution in an illiquid market. An agent must sell a large block of shares by a deadline. Placing the whole order at once moves the price against them, and in a traditional order book other participants can see the intention and trade against it — so the order goes to a dark pool, where there is no order book and matches arrive at random. The agent can only sell when a counterparty happens to appear, and whatever is unsold at the deadline must be dumped on the traditional market at once. The question is how much to offer at each opportunity.
The two problems have opposite curvature — the first is a concave maximisation of utility, the second a convex minimisation of cost — and the section is a good demonstration that the same embedding technique handles both, with each problem's structure entering only through which set of functions the value function is sought in.
The jump market (§9.3). The bond is S⁰_t = e^{ρt}; the risky assets follow
dS^k_t = S^k_{t-}(μ_k dt + dC^k_t) where C_t = Σ_{n≤N_t} Y_n is a compound Poisson process of
intensity λ whose jumps Y_n are supported in (-1,∞)^d, which keeps prices positive.
Short-sellings are prohibited, so the admissible fractions of wealth form the compact set
𝒰 = {u ≥ 0, u·e ≤ 1}, and the wealth follows
The investor maximises E^π_{tx}[U(X_T)] for a strictly increasing, strictly concave U.
The embedded model's state is (t,x) — a jump time and the wealth just after it — and its
action is a whole control path α : [0,T] → 𝒰, followed until the next jump. Between jumps
the wealth is φ^α_t(x) = x exp(∫₀^t (ρ + α_s·(μ-ρe))ds) (9.13), and the transition kernel is
substochastic: with probability e^{-λ(T-t)} no further jump arrives before the horizon, and
the reward r(t,x,α) = e^{-λ(T-t)}U(φ^α_{T-t}(x)) is collected instead.
The trade execution model (§9.4). A Poisson process of intensity λ delivers the trading
epochs; selling a shares costs C(a) with C strictly increasing and strictly convex (the
discrete form (9.19)), C(0) = 0; the inventory X_t = x₀ - ∫₀^t π_s dN_s is what remains, and
C(X_T) is the terminal dump. Here the flow is uncontrolled — the inventory does not move
between epochs — which makes the embedded model simpler.
The goal is Theorem 9.3.4, the main result for the terminal wealth problem, in all six of
its parts: the value function is the limit of the value iteration and lies in IM_cv; it is the
unique fixed point of the dynamic programming operator there; value iteration converges at the
explicit geometric rate α_b^n/(1-α_b); there exists an optimal Markov portfolio strategy given by
a single decision rule; policy iteration holds; and Howard's policy improvement algorithm holds.
Parts a)–c) describe the value; parts d)–f) produce the strategy, and a formalization of the
first three alone would omit the entire control half of the theorem.
The seven milestones are the rest of §9.3–9.4: the reduction from continuous to discrete time, the bounding function and its explicit contraction modulus, the invocation of Chapter 7's Structure Theorem, the iff-characterization of when holding only the bond is optimal, the stability of the value and of the optimal policies under perturbation of the utility, and then the trade execution problem's own bounding function and its monotone, unit-Lipschitz optimal execution rate.
Two formalization conventions run through everything here. The operator of §9.3 is a supremum
over a space of control paths, and since Mathlib's sSup of a set unbounded above is 0 — with
an unbounded reward that is a live risk, not a formality — it is carried as a relation defined by
least upper bounds against explicit sets of achievable values, with its iterates a chain of such
relations. And the continuous-time side is built, not assumed: Theorem 9.3.1 is the
identification of the continuous-time value with the discrete-time one, so the law of the embedded
jump chain is pinned by the one-step conditional law the book displays, and the terminal wealth is
read off that chain.
Convexity on the integer lattice cannot be defined by the classical secant-line inequality alone: a function can be midpoint-convex along every line and still admit no useful global optimality theory, because integer points off a chosen line are invisible to it. M-convex functions, introduced by Murota, resolve this by replacing the secant condition with an exchange axiom directly generalizing the basis-exchange property of matroids and the convex-hull structure of network flows: a function on the integer lattice is M-convex if, whenever two points can be improved by moving one coordinate up and a compensating coordinate down, at least one such move weakly improves the sum of the two function values. This single axiom turns out to be equivalent to several strikingly different-looking properties — invariance under a wide family of domain operations, supermodularity in the M♮ (translation-invariant) case, and, most importantly, a local-to-global optimality principle: a point is a global minimizer of an M-convex function if and only if no single coordinate exchange improves it. This mission develops the algebraic core of that theory — the exchange axiom's basic consequences, its equivalent local and dynamic reformulations, and the operations that preserve it — building toward the theorem that recasts M-convexity itself as an algorithmically meaningful local-search guarantee.
Companion mission 06-mconvex-functions-i (Discrete Convex Analysis V) covers this chapter's
own primary line of development: the equivalence of M-convexity and M♮-convexity with their
respective exchange axioms (Theorem 6.2), the M-optimality criterion (Theorem 6.26), a
minimizer-cut lemma (Theorem 6.28), and the M-proximity theorem (Theorem 6.37, its goal). This
mission builds the vocabulary those results also need (redeclared here, since sibling drafts
cannot yet import one another) and proves the results that chapter leaves for a second pass:
the domain structure of M- and M♮-convex functions, worked examples (quadratic forms,
quasi-separable functions), the operations that preserve M-convexity, supermodularity of the
M♮-convex case, the descent-direction property, and — this mission's goal — the equivalence of
the exchange axiom with a dynamic sequential-improvement property.
Fix a finite ground set . A function with nonempty effective domain is M-convex if it satisfies the exchange axiom (M-EXC[Z]): for and (coordinates where exceeds ), there is with
Writing when and otherwise (a lift to one extra coordinate), is M-convex if is M-convex; M♮-convexity is a genuine generalization of M-convexity (every M-convex function is M♮-convex, but not conversely) and coincides with it exactly when lies on a single hyperplane. The linear-weighted function (for ) is the standard device for testing local optimality under an arbitrary reweighting.
with the analogous statement for M♮-convexity (Theorem 6.24). This is the weakest stable form: it makes no reference to a specific algorithm, only to the existence of an improving single exchange whenever the current point is suboptimal under any linear reweighting — a property a faster algorithm could exploit without invalidating the characterization itself.
Eleven further results build the vocabulary and toolkit this goal draws on: the domain structure of M-convex and M♮-convex functions (Propositions 6.1, 6.7), the equivalence of the exchange axiom with a local, bounded-distance version (Theorem 6.4), worked examples establishing M-convexity for quadratic forms, univariate, conservation-law, and quasi-separable functions (Propositions 6.8-6.9), the domain and range operations preserving M-convexity (Theorem 6.13, Proposition 6.14), supermodularity of the M♮-convex case (Theorem 6.19), the descent-direction property (Proposition 6.23) that Theorem 6.24 generalizes, and a discrete subgradient inequality (Proposition 6.25).
Theorem 6.24 is the bridge between the static exchange axiom (a property of function values at pairs of points) and the dynamic behavior of local-search algorithms: it says a greedy single-coordinate-exchange step, applied to any linearly reweighted version of an M-convex function, always finds a strict improvement when one exists. This is exactly the guarantee that makes steepest-descent-type algorithms for M-convex function minimization correct, and it is the theorem chapter 10's algorithmic analysis (Schrijver-type methods) relies on implicitly whenever it argues that local exchange steps make global progress. The descent-direction property (Proposition 6.23) is the special case , isolating the core combinatorial fact before the reweighting machinery is added. The operations catalog (Theorem 6.13) is the practical toolkit that lets later chapters build complex M-convex functions (network flow costs, matroid rank functions composed with linear maps) from simple pieces without re-verifying the exchange axiom from scratch each time.
None of these results are open — they are Murota's own systematic development of the exchange-
axiom theory, with worked examples drawn from classical quadratic and separable function theory.
What this mission contributes is a faithful, machine-checked formal statement of each, sharing
the Lean vocabulary (MExchangeAxiom, MNaturalConvex, LinearWeight) the rest of the
Discrete Convex Analysis series builds on; no comparable formalization exists on the platform
(see Formalization scope).
The forward direction of Theorem 6.24 (M-convex sequential improvement) follows in one step from Proposition 6.23 applied to , itself M-convex by Theorem 6.13(3) — routine once those two pieces are in hand. The converse is the substantial direction: it must derive the full static exchange axiom from a property that only ever exhibits some improving exchange at some linear weighting, for every pair of suboptimal points — the proof constructs an explicit adversarial weighting designed so that failure of the local exchange step at that specific forces the domain itself to be M-convex (via Theorem 4.3) and then forces the local exchange axiom (M-EXCloc[Z]) via a bipartite-matching argument on the coordinates that differ, finally invoking Theorem 6.4 to lift locality to the full exchange axiom. No shortcut bypasses this two-stage reduction (domain structure, then local exchange) — attempting to verify (M-EXC[Z]) directly from (M-SI[Z]) without first pinning down that is M-convex fails because the exchange axiom's own statement presupposes a well-structured domain.
Ground-set elements are a Fintype V with DecidableEq; functions are
(V → ℤ) → WithTop ℝ. SuppPos/SuppNeg are Finset V (not Set V), matching how the
(M-SI[Z])/(M♮-SI[Z]) axioms and the descent-direction property use Finset.inf, whose value on
an empty index set is ⊤ — exactly the book's own stated convention for an empty minimum. No
Module ℝ or ConvexOn machinery is used for WithTop ℝ-valued arithmetic; scalar actions by
positive reals (PosScalarMul, Theorem 6.13(1)) and by naturals (FCheck's flow coefficients,
Proposition 6.25) are built directly from the native order and AddMonoid structure. No
numeric constants are hard-coded anywhere in this mission (rule 7 is vacuous); Proposition 6.8's
quadratic-form conditions are stated with the book's own literal coefficients (, and the
min/≥ structure of Eq. (6.25)-(6.28)), not a special case. Theorem 6.13's parts (7)
(aggregation) and (8) (integer infimal convolution) are not restated here since the book itself
proves them only later via Chapter 9's network-transformation machinery — see the Difficulty
note and MODERATION_NOTES.md; this is not a trivializing omission, since the six operations
that are included already exercise every domain- and range-transformation technique this
mission's goal needs. This mission's definitions (MExchangeAxiom, MNaturalConvex, CharVec,
DomZ, SuppPos, SuppNeg, CharVecOpt) are redeclared from chunk 06-mconvex-functions-i
rather than imported, since sibling drafts in this series cannot yet reference one another.
Contributions completing any of the twelve sorrys are welcome; the goal's converse direction
and Theorem 6.13's operations are the two with the most independent proof content.
Financial regulators and risk managers summarise the loss distribution of a position by a single number, the capital that must be held against it. The two standards in practice are Value-at-Risk (VaR), a quantile of the loss, and expected shortfall (ES), an average of the upper quantiles; ES is the standard of the Basel framework. Both depend on the position only through its probability law, a property called law invariance, which is what allows them to be estimated from data.
The axiomatic theory of risk measures, starting with Artzner, Delbaen, Eber and Heath (1999) and Föllmer and Schied (2002), centres on convex risk measures. VaR is not convex, however, and neither are its robust variants used in practice: the maximum or the median of VaR over a set of scenario models, or the benchmark-loss VaR of Bignozzi, Burzoni and Munari (2020). Castagnoli, Cattelan, Maccheroni, Tebaldi and Wang (Operations Research 70(5), 2022) propose star-shapedness as the common property of all of these measures: doubling the exposure to a risky position at least doubles the required capital. Their Section 7 identifies exactly which law-invariant risk measures are star-shaped.
Timeline:
Let be a probability space with atomless: every event of positive probability contains an event of strictly smaller positive probability. A position is a bounded measurable function , read as a loss: is money lost in state . The positions form a linear space that contains the constants and carries the pointwise order .
A risk measure is a function that is monotone (), translation invariant ( for real ) and normalized (). It is star-shaped if for all and all , and law-invariant if and with the same law under satisfy . Its acceptance set is . A set in a vector space is star-shaped if whenever and .
For the Value-at-Risk of is
Write . A loss first-order stochastically dominates , written , if pointwise, so is the smaller loss.
For a function the following are equivalent:
The goal fixes neither nor any constant. The paper's "Moreover" clause, closure of the class under the operations of Theorem 1, is excluded: its proof is a citation of Liu et al. (2020, Theorem 2) plus "the rest is straightforward".
Theorem 5 says that the star-shaped law-invariant risk measures are exactly the robustifications of VaR: each benchmark in gives a capital requirement , and takes the most favourable benchmark. The class contains VaR, ES, their scenario-based maxima and the benchmark-loss VaR. The theorem parallels Theorem 4 of the same paper, derived from Mao and Wang (2020), in which ES replaces VaR and SSD-consistency replaces law invariance. Together the two results separate the two classes: VaR is star-shaped and law-invariant but not SSD-consistent. Section 7 also records that star-shaped law-invariant measures are in general not minima of law-invariant convex risk measures, which is why a representation specific to VaR is needed.
On the formal side, the result is proved in the paper; no machine-checked proof is known. The mission yields a Lean library of law-invariant risk measures on bounded measurable positions, a quantile-based Value-at-Risk with its basic order properties, and the FSD-consistency of monotone law-invariant functionals on atomless spaces. That last statement is the probabilistic core that other law-invariant representation theorems reuse.
The direction (ii) ⇒ (i) is a direct computation. The direction (i) ⇒ (ii) rests on FSD consistency. The obvious argument writes as and applies monotonicity, but first-order dominance compares only laws, and two positions ordered in law need not be ordered state by state. One must construct positions with the laws of and that are ordered pointwise, and this uses atomlessness in an essential way: on a space with atoms, the construction can fail. The remaining steps are bookkeeping of extended-real infima and suprema, including levels near where may diverge.
Positions are the bounded measurable functions (a Submodule ℝ (Ω → ℝ), definition Positions) with the pointwise order, rather than equivalence classes in . For a law-invariant the two readings agree: almost surely equal positions have the same law, and a position that dominates another almost surely has a pointwise modification with the same law that dominates it everywhere. Atomlessness is defined locally (IsAtomless), because Mathlib's NoAtoms only states that singletons are null, which is weaker. Law invariance compares push-forward measures P.map X; measurability is part of Positions, so these are never degenerate.
VaR is an sInf of reals and is applied only to bounded positions at levels in , where the infimum is over a nonempty set that is bounded below. In (25) each function has domain exactly , "increasing" means weakly increasing, and is stated as in the extended reals. Both sides of (25) are compared in the extended reals, since the inner supremum can be . The minimum in Eq. (7) is an attained minimum (IsLeast), and the supremum condition on acceptance sets is a least upper bound (IsLUB).
These choices rule out the trivialising formalizations of (25). A real-valued supremum would read an unbounded supremum as . Dropping monotonicity of or the condition describes a larger class that includes non-normalized functionals. Allowing is excluded because the left side of (25) is a real number and the right side would be .
The following are not part of the mission: the "Moreover" clause of Theorem 5, Theorem 4 (its main direction is Mao and Wang 2020, Theorem 3.1), and Proposition 7 (ES as the smallest SSD-consistent risk measure dominating ), which would need second-order dominance and ES as additional definitions.
Reusable infrastructure: VaR on bounded measurable functions and its homogeneity and translation properties; the equivalence (A.1); existence of a uniform random variable on an atomless probability space and the quantile coupling it provides. Proofs of these as separate lemmas are welcome.
A risk measure turns the random loss of a financial position into a single number: the amount of capital a regulator or a risk manager requires to hold the position. Two families of risk measures dominate practice and theory. Value-at-Risk (VaR), a quantile of the loss distribution, is used in banking and insurance regulation; it is positively homogeneous but not convex, so it can penalize diversification. Convex risk measures (Föllmer and Schied 2002; Frittelli and Rosazza Gianini 2002), and their positively homogeneous subclass of coherent risk measures (Artzner, Delbaen, Eber and Heath 1999), reward diversification and come with a duality theory, but they exclude VaR and many of its robust variants.
Castagnoli, Cattelan, Maccheroni, Tebaldi and Wang (Operations Research 70(5), 2022) study the class that contains both: star-shaped risk measures, those for which increasing the exposure to a position never decreases the risk per unit of exposure. The class is closed under the aggregation operations used in practice (averages across models, worst cases across scenarios, medians, risk sharing), which convexity is not. It contains VaR, Expected Shortfall, their scenario-based robustifications such as , the benchmark-loss VaR of Bignozzi et al. (2020), and utility-based shortfall risk for utilities with the Landsberger–Meilijson property.
Timeline. Artzner et al. (1999) axiomatize coherent risk measures. Föllmer and Schied (2002) and Frittelli and Rosazza Gianini (2002) introduce convex ones. Föllmer and Schied (2016, Proposition 4.47) show that VaR is the minimum of the convex risk measures dominating it. Castagnoli et al. (2015) state the representation below without proof. The 2022 paper proves it for every star-shaped risk measure, and shows that the property characterizes the class.
Fix a set of states. The space of positions is a linear space of bounded functions containing every constant function; the constant is identified with the position that pays in every state. A value is a loss. No probability measure is fixed. is ordered pointwise: means for every .
A risk measure is a function that is monotone (), translation invariant ( for all real ) and normalized (). It is
The acceptance set of is . More generally, an acceptance set is a subset with that is closed downwards (, imply ). It is convex if convex and coherent if a convex cone, and it generates . A set is star-shaped if for all and .
In the Lean development the space of positions is PositionSpace Ω, positions are elements of 𝒳.carrier, and the predicates are IsRiskMeasure, IsStarShaped, IsConvexRiskMeasure, IsCoherentRiskMeasure, acceptanceSet, IsAcceptanceSet, IsConvexAcceptanceSet.
For a risk measure , the following are equivalent:
Moreover, for star-shaped , may be taken to be the set of all convex risk measures , and the family to be their acceptance sets. The minima are attained. The goal fixes no particular , or .
Theorem 2 identifies star-shaped risk measures as exactly the lower envelopes of convex risk measures. Consequences drawn in the paper: minimizing a star-shaped risk measure over a set of positions reduces to a family of convex risk-minimization problems (Corollary 1, Proposition 6), each convex risk measure in the envelope carries its dual representation (Proposition 5), and VaR-type measures inherit a tractable structure without being convex. The positively homogeneous case gives the analogous statement for VaR-like measures in terms of coherent ones, generalizing Föllmer–Schied Proposition 4.47.
The paper proves these results; the mission adds a machine-checked proof on a general space of bounded positions, with the attainment of every minimum made explicit. No formalization of star-shaped risk measures is known to exist. The platform mission Coherent Measures of Risk formalizes the Artzner et al. axioms on finitely many states with a gain convention; its definitions are not reused here. The definitions of this mission (risk measures on a space of bounded functions, acceptance sets, the aggregation operations) are reusable by any later development of monetary risk measures without a reference probability.
The equivalence (2)⇔(3) and the direction (2)⇒(1) reduce to closure properties of the class; the content is (1)⇒(2) together with the "Moreover" clause. The obvious first idea, taking the convex hull or convex envelope of or of , fails: the convex hull of generates a convex risk measure below , not above it, and a single convex risk measure cannot equal a non-convex . What is needed is, for each position, a convex risk measure that dominates everywhere and touches it at that position, and it must be monotone, translation invariant and normalized, not merely a convex functional. Attainment of the minimum, rather than an infimum, is part of the claim.
Submodule ℝ (Ω → ℝ) containing the constants whose elements are bounded, bundled as PositionSpace Ω. It is not specialised to all bounded functions, and no measurability or probability is imposed; positive values are losses.IsLeast (attained). The acceptance-set axiom is IsLUB, not sSup … = 0. uses the real sInf, which is genuine for acceptance sets on bounded positions.Contributions welcome: proofs of any milestone, and in particular general lemmas on risk measures on a space of bounded functions (the bounds , properties of , convexity of for convex ), which are reusable across risk-measure missions.
Chunk 07a built the general theory of infinite-horizon Markov Decision Processes and its
sharpest special case, contracting models, where Banach's fixed point theorem delivers existence,
uniqueness, and an explicit convergence rate all at once. That theory answers "does an optimal
policy exist, and can I compute it by iterating a fixed point equation?" This mission answers the
two questions a practitioner asks next: what happens when the reward's negative part, rather
than its positive part, is the one that needs controlling (positive models, §7.4), and — more
strikingly — can finding an optimal policy be reduced to solving a genuine linear program, the
single most heavily-optimized computational primitive in all of operations research (§7.5)?
A positive Markov Decision Model is the mirror image of chunk 07a's general setup: instead of
bounding the reward's positive part with an upper bounding function, the negative part is bounded
by an integrability quantity , and the roles of "largest subharmonic" and "smallest
superharmonic" swap accordingly. The computational sections build on chunk 07a's contracting
theory directly: Howard's policy improvement algorithm iteratively replaces a decision rule with
a strict pointwise improvement; the linear-programming approach recasts the entire optimization
problem — the value function and the optimal policy — as a primal/dual pair of linear programs,
not over finite vectors but over an infinite-dimensional space of measurable functions () and finitely-additive-in-spirit measures (); and state-space discretization
approximates an infinite (Borel) state space by a finite grid, with an explicit, computable bound
on the resulting numerical error.
The goal, Theorem 7.5.8 (Strong Duality), is the section's deepest result: under chunk 07a's
contracting Structure Theorem's own hypotheses, the primal linear program is solved
exactly by the true optimal value function , the dual program is solved by the
occupation measure of any optimal stationary policy, and the two optimal values coincide. The
milestones build up to it in three groups: the positive-model mirror theory (Lemmas 7.4.1-7.4.2,
Theorems 7.4.3 and 7.4.5); Howard's policy improvement and its termination guarantee (Theorem
7.5.1, Corollary 7.5.3); and the linear-programming machinery itself (weak duality, complementary
slackness, and the finite-state specialization that recovers an ordinary finite linear program,
Theorems 7.5.6, 7.5.7, 7.5.9) together with the discretization error bounds that make the whole
theory numerically usable (Proposition 7.5.11, Theorem 7.5.12).
The strong duality theorem is genuinely new content relative to what is already on the platform:
the existing finite-dimensional LP duality missions (SmaleNinth.lp_strong_duality,
LinearOptimization.lp_general_weak_duality, and others in the linear-optimization field) all
operate over -valued vectors, while this theorem's primal and dual variables are a
measurable function on a general Borel space and a measure on a general Borel space respectively
— an infinite-dimensional linear program in the fullest sense. Theorem 7.5.9, the finite-state
specialization, is the one point of genuine hypothesis-for-hypothesis contact with that prior art
(checked directly; see STATUS.md for why it was drafted fresh rather than cited as a reference
item), and it is exactly there that the reduction to an ordinary finite LP — with the platform's
familiar vertex/extreme-point vocabulary — becomes visible.
Constructing the occupation measure without a canonical infinite-horizon
path measure is the central technical challenge: it must be a genuine Measure (E × A), not
merely a real-valued functional, since the dual program optimizes over a space of such measures.
This mission builds it from iterated Measure.bind (pushing the initial law forward through
the model's kernel under a fixed stationary decision rule) combined with a countable
Measure.sum of -scaled terms — a construction that stays entirely within Mathlib's
existing measure-theoretic vocabulary without needing an Ionescu–Tulcea-style infinite product.
A second, different difficulty is the state-space discretization section's grid interpolation,
which presupposes a convex-combination structure ( for grid points )
on the state space that a general Borel space does not carry; this mission represents the grid
operator and grid bounding function as data satisfying exactly the structural properties their
two target theorems' own proofs use, rather than reconstructing the literal interpolation scheme
— a deliberate, documented scope decision (see MODERATION_NOTES.md), not an approximation of
either theorem's mathematical content.
Every operator and value-function construction restates chunk 07a's own vocabulary (per this
series' file-ownership convention, an independent copy in this chunk's own namespace), extended
by the positive-model integrability bound , the occupation-measure/linear-program
apparatus of §7.5.2, and the grid-approximation data of §7.5.3. The primal/dual optimal values
/ are kept EReal-valued rather than real-valued specifically
so that Theorem 7.5.6's own finiteness claims (, ) remain genuine, checkable content rather than being trivialized by a real-valued
sInf/sSup's always-finite convention. Theorem 7.5.9's "optimal vertex" is stated via an
explicit convex-combination (extreme-point) characterization using ENNReal weights, since
Measure does not carry the module structure Mathlib's own Set.extremePoints requires.
A closed set is flow-invariant for a dynamical system when every trajectory that starts in stays in . Invariance of sets underlies state constraints in optimal control, safety certificates for controlled systems, comparison and maximum principles for differential equations, and the positivity of solutions of kinetic and population models. The question is always the same: which infinitesimal condition at the points of is equivalent to the global statement that trajectories cannot leave ?
For a smooth vector field and a smooth boundary the answer is that the field must not point strictly outward. For a nonsmooth set, such as a polyhedron, the positive orthant or a set with inward cusps, "pointing inward" must be made precise through a notion of tangent vector that works at corners. Frank H. Clarke's 1975 paper introduces the generalized gradient of a Lipschitz function and derives from it a normal cone and a tangent cone for arbitrary closed sets. Its Theorem (4.4) shows that this tangent cone is exactly the right notion: for a Lipschitz differential inclusion , a closed set is flow-invariant if and only if is contained in the tangent cone at each point of the set.
Timeline:
Throughout, carries the Euclidean inner product and norm .
Generalized gradient. For Lipschitz on bounded sets, is the convex hull of all limits with and differentiable at each (Definition (1.1)). The generalized directional derivative is (Definition (1.3)).
Distance function. For a nonempty closed , . It is Lipschitz with constant . A point with is a closest point to ; it exists but need not be unique.
Normal and tangent cones. For , the cone of normals is
and the tangent cone is its dual,
Differential inclusions. A multifunction assigns to each a set ; standing assumption of §4: every is nonempty and compact. A trajectory is an absolutely continuous with for almost every ((4.1)). is Lipschitz if there is such that for all and some has ((4.2)). A closed set is flow-invariant for if every trajectory with has for all ((4.3)).
Let be a Lipschitz multifunction with nonempty compact values and a nonempty closed subset of . Then
The result. Theorem (4.4) turns a statement about all trajectories of a set-valued dynamical system into a pointwise geometric condition on that can be checked without solving anything. It is the prototype of the strong invariance theorems of nonsmooth control theory, later developed in viability theory and in the monograph of Clarke, Ledyaev, Stern and Wolenski, and it is the tool behind state-constrained optimal control and Lyapunov-type arguments for nonsmooth systems. Its corollaries recover the Bony and Brezis theorems for Lipschitz vector fields. The companion milestones (2.5), (3.2) and (3.7) are standalone facts of nonsmooth geometry: the Clarke normal cone is generated by limits of proximal normals, and Clarke tangency can be tested along rays from nearby points of the set.
Formalizing it. The result is proved in the paper and has been reproved in textbooks; to the best of our knowledge it has no machine-checked proof. Mathlib contains Rademacher's theorem, absolutely continuous functions on intervals and the Bouligand tangent cone, but no Clarke generalized gradient, no Clarke normal or tangent cone, and no theory of differential inclusions. A complete development supplies a first nonsmooth-analysis layer on top of Mathlib and a first existence theorem for Lipschitz differential inclusions.
The direction (2) (1) looks like a Gronwall argument for , but is not differentiable, is only absolutely continuous, and the closest point to can jump. The step that must be controlled is the comparison between , a nearby admissible velocity at the closest point, and the normal ; this is where Proposition (3.2) enters, and it is why the Clarke cone, rather than a weaker cone, is needed.
The direction (1) (2) needs a trajectory through an arbitrary whose initial velocity is a prescribed . For a nonconvex multifunction this is Filippov's theorem [7, Theorem 5], which the paper cites and does not prove. A solver must prove it, or an equivalent existence result for Lipschitz inclusions with compact values, from scratch in Lean. The Clarke tangent cone and the more familiar Bouligand (contingent) cone differ pointwise at nonconvex corners, so a statement written with Mathlib's tangentConeAt is a different theorem from (4.4). That the two universal conditions " for all " are equivalent for Lipschitz is a later, separate result and cannot be assumed.
EuclideanSpace ℝ (Fin n); is Metric.infDist · E; " is a closest point to " is e ∈ E ∧ dist x e = infDist x E.DifferentiableAt, because Mathlib's gradient is off the differentiability set. is a real limsup, and every theorem using it carries the §1 Lipschitz hypothesis.tangentConeAt.x : ℝ → ℝⁿ with AbsolutelyContinuousOnInterval x 0 1 and, for almost every , ∃ w ∈ X (x t), HasDerivAt x w t. Values outside are irrelevant.deriv in (4.1), using a punctured filter in (3.7), which would make (3.7)(2) hold at isolated points, and assuming Filippov's theorem as a hypothesis of (4.9) or of the goal.norm_le_gronwallBound_of_norm_deriv_right_le for the differentiable case), and Filippov's existence theorem. The generalized gradient, cones and trajectory notions are reusable by any nonsmooth-optimization or control mission. Contributions of any of these as separate lemmas are welcome.Shortest-path distances and network potentials are among the oldest objects in combinatorial
optimization: a directed graph with arc lengths, its shortest-path distances, and the "feasible
potentials" (vertex labels consistent with those lengths) underlie duality in min-cost flow,
scheduling, and difference-constraint systems. Murota's Discrete Convex Analysis (SIAM, 2003)
isolates the abstract structure behind these objects — distance functions satisfying the
triangle inequality, and their associated sets of admissible potentials — and shows it is
governed by exactly the same discrete-convexity machinery as submodular set functions: a
one-to-one correspondence with a second family of well-behaved integer point sets, the
L-convex sets. Where an M-convex set (chapter 4) is defined by an exchange axiom generalizing
matroid base exchange, an L-convex set is defined by closure under coordinatewise lattice
operations (∨, ∧) and translation by the all-ones vector — a genuinely different axiom
system that nonetheless produces a parallel structural theory: hole-freeness, a polyhedral
description via an induced distance function, and integral convexity.
Companion mission 05-lconvex-sets (Discrete Convex Analysis IV) covers this chapter's other
half: the hole-free property (Theorem 5.2), the one-to-one correspondence between L-convex sets
and integer-valued triangle-inequality distance functions (Theorem 5.5), the intersection
properties (Theorem 5.7), and the chapter's discrete separation theorem (Theorem 5.9, its goal).
This mission builds the vocabulary those results also need (redeclared here, since sibling
drafts cannot yet import one another) and proves the results the chapter leaves for its second
half: the fundamental facts connecting a distance function to its admissible potentials
(Proposition 5.1), the two-way polyhedral correspondence's supporting propositions (5.3-5.4),
Minkowski-sum convexity (Theorem 5.8), and — this mission's goal — the explicit description of
an L-convex set's convex hull that establishes its integral convexity (Theorem 5.10).
Fix a finite ground set . A distance function is a map with ; it may take negative finite values and need not be symmetric. It defines a directed graph with , arc having length . Write for the shortest-path length from to in ( if none exists); is well defined ( finite-valued wherever a path exists) exactly when has no negative cycle. The triangle inequality defines the class (or when integer-valued). A vector is an admissible potential of if for all ; write for the set of all such potentials.
A nonempty set is L-convex if it satisfies (SBS[Z]): (coordinatewise max/min), and (TRS[Z]): . A set is integrally convex if every point of its convex hull lies in the convex hull of restricted to that point's integral neighborhood — a strong, local form of "no holes" saying every real point of the hull is explained by nearby integer points alone.
For an L-convex set , writing for the fractional part of , for the distinct nonzero values of , and (with ):
This is the weakest stable form available: it exhibits an explicit, finite set of at most integer witnesses for every point of the hull, which is what "integrally convex" asserts abstractly, rather than a numerical bound that a sharper construction could later shrink.
Four further results build the correspondence this goal uses: the basic duality between a distance function's admissible potentials, its shortest-path closure, and negative-cycle freedom (Prop. 5.1); the induced-distance-function construction recovering a triangle-inequality distance function from any integer point set, and the convex hull of an L-convex set as its associated polyhedron (Prop. 5.3); the converse construction recovering an L-convex set from an integer-valued distance function (Prop. 5.4); and convexity in Minkowski sum (Thm. 5.8).
Theorem 5.10 is what makes "L-convex" a genuinely convex-analytic notion rather than a combinatorial curiosity: it shows the convex hull of an L-convex set is not merely a polyhedron (already known from the chapter's polyhedral-description results) but one with the strongest local integrality property discrete convex analysis considers, integral convexity — every real point's hull membership is certified by a small, explicitly constructed set of nearby lattice points, uniformly across the whole set. This is the L-convex counterpart of the corresponding M-convex fact (chapter 4's Theorem 4.24) and is used later in the book wherever L-convex functions (chapter 7) need their epigraphs' local structure. Proposition 5.1 is the combinatorial engine underneath: it is exactly the LP-duality statement between shortest paths and feasible potentials that appears, in various guises, throughout network flow theory, made precise here as the base case the L-convex correspondence rests on.
None of these results are open — Murota presents them as, in his own words, "fundamental facts
well known in network flow theory" (Proposition 5.1) systematized into the discrete convex
analysis framework. What this mission contributes is a faithful, machine-checked formal
statement of each, in the shared Lean vocabulary (LConvexSet, AdmissiblePotentials,
ShortestDist) the rest of the Discrete Convex Analysis series can build on; no comparable
formalization exists on the platform (see Formalization scope).
The shortest-path closure is not a bookkeeping convenience but genuinely graph-theoretic content: proving Proposition 5.1 requires constructing an admissible potential from a shortest-path labeling and, conversely, deriving the negative-cycle-freeness of from the mere existence of one admissible potential — a min-cost-flow-style LP duality argument, not a direct combinatorial check. Theorem 5.10's difficulty sits in a different place: the naive approach to " is integrally convex" would attempt an inductive argument peeling off one coordinate at a time, but the actual proof constructs a single, uniform family of witness points from the sorted fractional values of — a Carathéodory-style representation (Eq. (5.11)) that must simultaneously stay inside the integral neighborhood and land in itself via the triangle inequality of 's induced distance function, a construction with no one-coordinate-at-a-time shortcut.
Ground-set elements are a Fintype V with DecidableEq; L-convex sets are Set (V → ℤ);
distance functions are V → V → WithTop ℝ; admissible-potential sets are Set (V → ℝ). The
shortest-path closure is formalized directly from finite walks (Fin (k+1) → V) rather than via
a graph-library shortest-path predicate, matching the book's own construction. The Eq. (5.11)
witnesses are built exactly as the book describes them — sorted distinct nonzero fractional
values and their level sets — mirroring the Lovász-extension construction of the companion
mission 20-ch04b-mconvexsets. No numeric constants are hard-coded anywhere in this mission
(rule 7 is vacuous). The goal's explicit witness set (at most points) is not a
trivializing special case: it holds for every L-convex set and every point of its hull, with no
extra hypothesis narrowing the class. This mission's definitions
(LConvexSet, AdmissiblePotentials, DistanceFunction, IsIntegrallyConvex) are redeclared
from chunk 05-lconvex-sets (and, for IsIntegrallyConvex/IntegralNeighborhood, from chapter
3's own definitions) rather than imported, since sibling drafts in this series cannot yet
reference one another; a later, published version of this book's namespace should consolidate
them. Contributions completing any of the five sorrys are welcome; Proposition 5.1's LP-duality
argument and the goal's Carathéodory-style construction are the two with the most independent
proof content.
Submodular set functions are the combinatorial stand-in for convexity: a function on the subsets of a finite ground set is submodular if , and this single diminishing-returns inequality drives an enormous range of combinatorial optimization — matroid rank functions, graph cut capacities, entropy, coverage functions, and the max-flow min-cut theorem all arise as special or dual cases (Edmonds 1970; Lovász 1983; Fujishige 2005). M-convex sets are the "vector" incarnation of the same idea: subsets of satisfying an exchange axiom that generalizes the basis-exchange property of matroids to sets of integer points lying on a common hyperplane. Murota's Discrete Convex Analysis (SIAM, 2003) develops both sides of this correspondence and proves they coincide exactly: M-convex sets are precisely the integer points of the base polyhedra of integer-valued submodular functions. This mission covers the second half of that development — the structural theory (integrality, holes, Minkowski sums) that turns the correspondence into a working calculus, and its capstone, a discrete separation theorem for two disjoint M-convex sets whose separating hyperplane is forced to have - or -valued coefficients.
Companion mission 04-mconvex-sets (Discrete Convex Analysis III) covers the same chapter's
foundational results: the equivalence of the exchange-axiom variants, the one-to-one
correspondence between M-convex sets and integer submodular functions (Theorem 4.15), Edmonds's
intersection theorem (Theorem 4.18), and Frank's discrete separation theorem for submodular/
supermodular pairs (Theorem 4.17). This mission builds on that vocabulary (redeclared here,
since draft missions in the same series cannot yet import one another) and proves the results
the chapter leaves for its second half.
Fix a finite ground set . A vector assigns an integer to each ; write for . For , the positive support and negative support record where exceeds, and falls short of, . A nonempty set is M-convex if it satisfies the exchange axiom (B-EXC[Z]): for all and , some has both and , where is the characteristic vector of .
A set function with and is submodular (the class , or when integer-valued) if for all . Its base polyhedron is . The Lovász extension linearly interpolates off : sorting the distinct values of as and setting , it is .
for M-convex sets (Theorem 4.21). This is the weakest stable form of the result — it asserts only the existence of a combinatorially special separator, not any bound tied to or a particular construction, so it is not invalidated by a sharper algorithm for finding .
Eleven further results build the calculus this goal rests on: the hyperplane property of M-convex sets (Prop. 4.1), an equivalent one-sided exchange axiom (Prop. 4.2), nonemptiness and the support-function identity for (Props. 4.4-4.5), integrality of for integer-valued (Prop. 4.6), the hole-free property identifying an M-convex set with the integer points of its own convex hull (Thm. 4.12), the two-way polyhedral description of M-convex sets via induced submodular functions (Props. 4.13-4.14), the equivalence of submodularity with convexity of the Lovász extension (Thm. 4.16, due to Lovász), integrality of the intersection of M-convex sets (Thm. 4.22), and Minkowski-sum identities for base polyhedra and M-convex sets (Thm. 4.23).
The discrete separation theorem is what makes M-convexity discrete rather than merely a
polyhedral fact: ordinary separation of two disjoint convex sets by a hyperplane is classical,
but here the separator is forced into — a purely combinatorial
object — with no loss of strength. This is the mechanism behind integrality results across
combinatorial optimization (e.g., that the intersection of two integral base polyhedra is
integral, Theorem 4.22, used pervasively in matroid intersection and submodular flow
algorithms). The structural results (holes, Minkowski sums, the Lovász-extension convexity
equivalence) are the working toolkit every later use of M-convexity in the book — proximity
theorems for M-convex functions (chunks 06+), the discrete conjugacy theorem, submodular
flows — draws on without restating.
None of these results are open: Murota attributes the exchange-axiom theory to the matroid and
submodular-function literature it systematizes, citing Edmonds, Frank, and Lovász by name for
the specific theorems. What this mission produces is a machine-checked formal statement of each
result exactly as the book states it, in a shared Lean vocabulary (ExchangeAxiomB,
BasePolyhedron, LovaszExtension) that the rest of the Discrete Convex Analysis series
builds on; no result here has a prior formalization on the platform (see Formalization scope).
The separation theorem is not proved by convex separation directly — the whole point is that the
naive proof (apply the ordinary hyperplane separation theorem to the convex hulls of , then argue the separator can be taken -valued) does not go through, because
convex separation alone gives no control over the separator's coefficients. The book instead
derives it from Edmonds's intersection theorem (Theorem 4.18, chunk 04-mconvex-sets) applied
to a submodular/supermodular pair built from 's associated set functions (Theorem
4.15), routed through Frank's discrete separation theorem (Theorem 4.17) — a genuine two-step
reduction, not a direct argument. A second, independent difficulty sits in the supporting
results: the hole-free property (Theorem 4.12) requires an explicit induction reducing an
arbitrary convex combination representing an integer point to a single element of , a
combinatorial exchange argument with no shortcut through general polyhedral theory.
Ground-set elements are a Fintype V with DecidableEq; M-convex sets are Set (V → ℤ);
submodular/supermodular functions are Finset V → WithTop ℝ / WithBot ℝ; base polyhedra are
Set (V → ℝ). The Lovász extension is formalized directly from the book's own sorted-values
construction (SortedValues, LevelSet, Eq. (4.4)-(4.6)), not via an equivalent closed form.
Since WithTop ℝ carries no Module ℝ structure, convexity for Theorem 4.16 is stated via a
bespoke nonnegative-scalar action (ScalarWithTop) rather than Mathlib's ConvexOn — this
changes no mathematical content, only its packaging (see MODERATION_NOTES.md). No numeric
constants are hard-coded anywhere in this mission (rule 7 is vacuous). The goal's hypothesis
(ExchangeAxiomB plus Nonempty on each ) is exactly the book's own definition of
M-convexity — no weaker substitute (e.g. requiring a specific witness in the hypothesis
rather than deriving one, or dropping the constraint on in favor of a
generic separator) would be faithful, and both trivializations are ruled out by construction.
This mission's definitions (ExchangeAxiomB, BasePolyhedron, SubmodularSetFunction,
LovaszExtension) are redeclared from chunk 04-mconvex-sets rather than imported, since
sibling drafts in this series cannot yet reference one another; a later, published version of
this book's namespace should consolidate them. Contributions completing any of the twelve
sorrys are welcome; the hole-free property (Theorem 4.12) and the goal are the two with the
most independent proof content.
In quantum field theory a Ward–Takahashi identity is an identity between correlation functions that follows from a global or gauge symmetry of the theory. In quantum electrodynamics it was used by Ward (1950) and Takahashi (1957) to relate the wave-function renormalization of the electron to its vertex renormalization, and it is described in the source article as "the quantum version of classical current conservation associated to a continuous symmetry by Noether's theorem". In the path-integral formulation the identities are a reflection of the invariance of the functional measure under the symmetry; when the measure is not invariant one obtains the anomalous Ward–Takahashi identity (e.g. the chiral anomaly).
The continuum path integral of interacting QED is not a mathematically defined object, so the identities cannot be formalized literally. This mission formalizes the path-integral derivation in the setting where every step is rigorous: a finite lattice, where the functional measure is Lebesgue measure on a finite-dimensional space.
A field configuration of a complex scalar field on sites is . The global symmetry acts by . The local generator at site is , and the local variation of a real-differentiable functional is . An action is -invariant if for all . The (unnormalised, Euclidean) path integral of an observable is
For invariant , is the lattice divergence of the Noether current.
For a , -invariant action with the moment conditions and : current conservation , and for all sites
The goal is the lattice version of the statement that the divergence of the current inserted into a charged correlation function produces only contact terms — the structure of the QED identity in the source, whose right-hand side consists of amplitudes with shifted external momenta. The milestones isolate the three ingredients of the textbook derivation: invariance of the measure, Noether current conservation, and integration by parts; the anomalous version identifies the anomaly with the Jacobian (trace) of the transformation. The results are classical; to the drafter's knowledge they are not available in Mathlib in this form.
The identities are elementary on paper; the work is analytic bookkeeping. Integration by parts must be justified on the non-compact space with non-constant vector fields or , so the "surface terms vanish" step of the physics derivation has to be replaced by explicit integrability hypotheses, and products with complex conjugates require real (not complex) differentiability throughout.
Fields are Fin N → ℂ with the sup norm and the product Lebesgue measure; derivatives are real Fréchet derivatives (fderiv ℝ); integrals are Bochner integrals, which take the value on non-integrable integrands. The weight is Euclidean, , and all identities are stated for unnormalised integrals (normalised expectations are ratios by ). Hypotheses are satisfiable: e.g. any Gaussian action is -invariant and satisfies all moment conditions, so the goal is not vacuous. Continuum QED, renormalization and the S-matrix Ward identity are out of scope.
A classical convex function's global minimality is equivalent to its local minimality — the single fact that makes convex optimization tractable, since checking a small neighborhood suffices to certify a global guarantee. The discrete analogue is not automatic: a function on the integer lattice can fail to have any well-behaved "local" notion at all, and even when a discrete convexity-like property is imposed, the naive candidate (a function's values agreeing with its own convex-hull interpolation) does not by itself guarantee that local optimality implies global optimality. Murota's Discrete Convex Analysis (SIAM, 2003) isolates exactly the extra condition — integral convexity — that restores this guarantee, and shows it is general enough to contain every other discrete convexity notion the book studies (M-convex, L-convex, and their variants), making it the common ancestor of the book's entire hierarchy of classes. This mission completes the chapter's account of integral convexity: how it behaves under sums, restrictions, and linear perturbations, how it transfers between a function and its domain or minimizer sets, and a companion fact about hole-freeness under intersection and Minkowski sums that motivates why integral convexity, not mere hole-freeness, is the right notion to use.
For with nonempty effective domain , the convex closure is . The integral neighborhood of is , and the local convex extension replaces "for all " in 's definition with "for all ". A function is integrally convex if everywhere on . A set is integrally convex if its indicator function is; it is hole free if , where is the real convex hull of . The discrete Minkowski sum is . A function is separable convex if for univariate functions satisfying the discrete convexity inequality . For , and is its minimizer set.
Goal (Theorem 3.29). For with nonempty bounded effective domain,
This leaves the characterization at the level of the two named properties (integral convexity of the function versus of every minimizer set), the strongest statement of this kind that holds without extra hypotheses beyond boundedness of the domain.
Supporting milestones. Proposition 3.17 (four basic containment/equality relations between hole-free sets' intersections, Minkowski sums, and their real closures); Proposition 3.22 (for a periodic integrally convex function, global optimality reduces to a one-sided local check); Proposition 3.24 (an integrally convex function plus a separable convex function is integrally convex); Proposition 3.25 (separable convex functions are integrally convex, and integral convexity survives linear perturbation); Proposition 3.26 (an integrally convex set is hole free); Proposition 3.28 (the effective domain and every minimizer set of an integrally convex function are integrally convex sets — the forward direction of the goal); and Proposition 3.30 (for integer-valued integrally convex functions, a finite infimum is always attained).
Theorem 3.29 turns a statement about a function on all of (integral convexity, a condition on and that is a priori about uncountably many points) into a statement about a countable family of discrete sets (the minimizer sets ), giving a genuinely different and often more tractable way to certify or refute integral convexity. Propositions 3.24–3.25 are the closure properties that make integral convexity useful in practice: without them, verifying integral convexity of a function built from simpler pieces (a sum with a separable cost, a linearly reweighted objective) would require re-deriving the property from scratch each time. Proposition 3.17, by contrast, is a cautionary result: Note 3.27 and Example 3.15 (the two hole-free sets whose Minkowski sum has a hole) show that hole-freeness alone does not inherit good behavior under set operations, which is exactly the gap integral convexity's stronger, locally-checkable condition is built to close — this mission's Proposition 3.17 documents the "obvious"/general-purpose relations that hold regardless, so that the reader can see precisely which inclusion is automatic and which requires more.
The naive approach to Theorem 3.29's converse direction (integral convexity of every minimizer set implies integral convexity of ) tries to check directly at an arbitrary ; this is circular, since and are themselves defined via suprema over affine minorants, not via minimizer sets. The book's actual proof instead sets up a primal-dual pair of linear programs whose optimal solutions witness and respectively, uses LP duality's complementary slackness to show the dual optimal solution can be chosen supported inside , and only then concludes — routing the entire argument through the integral convexity of the specific minimizer set at the optimal dual price . This is why Theorem 3.29's proof needs LP duality (Theorem 3.10, formalized in the previous mission in this series) as an ingredient, not just the closure-property machinery of Propositions 3.24–3.28.
All apparatus (ConvexClosure, IntegralNeighborhood, LocalConvexExtension,
IntegrallyConvex, ArgMinPerturbed, HoleFree, IntegrallyConvexSet, SeparableConvex,
MinkowskiSumZ) is redeclared fresh in DiscreteConvex.IntegralConvexityC, mirroring chunk
03-integral-convexity's already-established constructions (Fin n-indexed, WithTop ℝ-valued
functions, EReal-valued convex closures via sSup), since a draft mission cannot import
another draft's definitions. IntegrallyConvexSet is defined via the book's own primary
definition (indicator function integrally convex) rather than either of its two stated
equivalent reformulations, since no result in this mission needs those forms as a named
predicate. An integer-valued function (Proposition 3.30) is represented as Zⁿ → WithTop ℤ and
cast to WithTop ℝ via a small casting map wherever the real-valued apparatus is needed — a
faithful embedding. Boundedness of a discrete set is containment in a finite integer interval.
The formalization does not trivialize: Theorem 3.29's hypothesis is exactly "nonempty bounded
effective domain", not further restricted to, say, a fixed small dimension or a finite ground
set with a fixed cardinality bound, and every milestone is stated at the same generality as
Propositions 3.24–3.28 and 3.30 give it (arbitrary , arbitrary integrally convex function).
Infrastructure needed beyond Mathlib: all definitions are fresh; a contribution completing any
milestone, or the LP-duality-based proof of Theorem 3.29's converse direction, would be a
natural entry point, alongside chunk 03's Theorem 3.21 as background.
Two of the oldest simplifying assumptions in portfolio theory are that trading is frictionless
and that risk means variance. Neither survives contact with practice: every real market charges
a transaction cost proportional to the size of a trade, and variance penalizes upside deviations
exactly as much as downside ones, which is not what an investor actually fears. Bäuerle and
Rieder's §4.5 reopens the multiperiod terminal-wealth problem of chunk 04a with proportional
transaction costs added to every trade, and finds that the qualitative shape of the solution
survives — a buy/hold/sell rule with explicit thresholds, still obtained from the Structure
Theorem of chunk 02a. Their §4.6 then leaves expected-utility maximization altogether and
solves the classical Markowitz mean-variance problem in its genuinely dynamic, multiperiod form:
choose a self-financing trading strategy that attains a target expected terminal wealth
while minimizing the variance of that terminal wealth. This is Markowitz's one-period portfolio
selection problem (H. Markowitz, Portfolio Selection, Journal of Finance, 1952) transplanted
into a stage-by-stage trading horizon, and it earns its own solution technique: the objective is
not linear in the underlying probability measure, so no direct Bellman equation applies, and the
chapter instead builds a Lagrangian-embedding argument from scratch. Section §4.7 closes the
chapter by replacing variance with the Average-Value-at-Risk, an axiomatically better-behaved
risk measure (P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk,
Mathematical Finance, 1999), and solves the resulting mean-risk problem in the binomial model by
the same Lagrangian route.
The transaction-cost model (§4.5): state (bond and stock holdings), action (the stock holding chosen after the trade), bond holding after the trade if and if , for a proportional cost rate ; transition ; terminal reward for a utility homogeneous of degree .
The mean-variance model (§4.6): state (wealth), action (amounts invested in risky assets, short-selling allowed), transition . Writing for the terminal wealth reached from under a strategy , the problem is
Because is not linear in the law of , (MV) is solved via the Lagrangian , whose saddle points give (MV)'s value and optimizer, reduced in turn to the tractable auxiliary quadratic problem : minimize , a stochastic linear-quadratic control problem.
The mean-risk model (§4.7): the binomial (Cox–Ross–Rubinstein) market with one bond (interest rate ) and one stock with relative return w.p. or w.p. ; the Average-Value-at-Risk at level , ; the problem subject to , solved via the same Lagrangian route through an auxiliary problem .
where is a recursively-defined sequence in (Lemma 4.6.4) built from the one-period return moments . This closes the loop the chapter opens: it is the exact value and optimal strategy of the dynamic mean-variance problem, obtained by specializing the auxiliary problem 's closed-form solution (Theorem 4.6.5) at the Lagrange multiplier that Lemma 4.6.2's saddle-point argument selects.
The Lagrangian route itself: the equivalence of (MV) and its equality-constrained form (Lemma 4.6.1), the saddle-point value identity (Lemma 4.6.2), the reduction of the Lagrange problem to (Lemma 4.6.3), the boundedness of (Lemma 4.6.4), and 's own explicit solution (Theorem 4.6.5) — the four-step argument the goal theorem is the payoff of. Upstream of §4.6: the transaction-cost model's upper bounding function (Proposition 4.5.1), its Structure Assumption via buy/hold/sell decision rules (Proposition 4.5.2), and the resulting explicit three-region optimal policy (Theorem 4.5.4). Downstream: the Two-Fund Theorem (Corollary 4.6.7), and the parallel mean-risk development — the auxiliary problem 's solution (Theorem 4.7.1), the binomial value of (Proposition 4.7.2), and the mean-risk problem's own explicit solution in both orderings of and (Theorems 4.7.3 and 4.7.4).
Theorem 4.6.6 is the multiperiod extension of the single most-used result in portfolio theory: the mean-variance efficient frontier, here derived stage by stage rather than assumed static, and it recovers the classical Two-Fund Theorem (every investor holds the same risky portfolio, scaled by wealth) as an immediate corollary rather than a separate argument. The transaction-cost results answer a standing objection to frictionless portfolio theory by showing that its qualitative conclusions — a threshold trading rule derived from a value function via the same abstract Structure Theorem — survive costs, with the thresholds now depending on the current value function rather than being fixed. The mean-risk results extend the whole technique to a risk measure that, unlike variance, is coherent in the sense of Artzner et al., showing the Lagrangian-embedding method is not an accident of the quadratic case.
None of this chapter's results have machine-checked proofs on Prove2Me at the time of writing
(the platform's saddle-point sufficiency results, VectorSpaceOpt.lagrangian_saddle_sufficient_pointed
and ConvexOptimization.lagrangian_saddle_iff_strong_duality, are stated over a closed convex
cone in a normed vector space, not over the finite-horizon admissible-policy space that
Lemma 4.6.2 needs, and were checked and ruled out as reusable for this mission). Formalizing this
chapter means building the Lagrangian-embedding argument for a dynamic (rather than static)
optimization problem from scratch: no existing platform infrastructure covers a saddle point of
a Lagrangian defined over a sequence of Markov policies.
The obvious first attempt at (MV) is to apply the Structure Theorem of chunk 02a directly to
the variance objective, exactly as chunk 04a does for expected utility. This fails outright:
is not
additive over time and has no Bellman recursion of the usual form, because the square of an
expectation over the whole horizon cannot be decomposed into a sum of one-period rewards. The
chapter's actual route — Lagrangian relaxation to , then a further reduction to the
quadratic (and hence tractable) — is not a shortcut around this obstacle but the only way
the mean-variance problem admits a Markov Decision Process reformulation at all. A correct
formalization of the goal theorem must go through this exact chain (saddle_point_value,
plambda_implies_qp, qp_solution), not around it.
The financial market and the four named optimization problems (MV), (MV=), ,
are formalized as explicit structures and Prop-valued predicates in MDPFinance.MeanVariance
(none of them is a numbered definition in the book — each is introduced only in prose — so each
gets its own precise Lean definition rather than being left implicit). Wealth is real-valued,
policies are sequences of measurable Markov maps , and values that can be in the book (the value of , of
, and of (MR) itself) are typed EReal rather than ℝ, matching the book's own use
of infinite values as legitimate outcomes rather than failure states. A formalization that solved
the goal theorem by first proving a Bellman equation for directly
would not be proving Theorem 4.6.6 — no such recursion exists — and the goal statement is phrased
purely in terms of IsOptimalMV, varXN, and meanXN, independent of any intermediate value
function, precisely so that only the actual saddle-point argument can discharge it. The
transaction-cost model's buy/hold/sell threshold functions are
represented by their defining maximizing property rather than a closed form, since the book
itself only pins them down as an argmax. Reusable beyond this mission: the MVMarket/
MeanRiskMarket structures and the Lagrangian-saddle-point machinery are natural substrate for
any later mission that needs a dynamic risk-constrained portfolio problem. Contributions
completing any milestone's sorry are welcome, particularly a sorry-free proof of Lemma 4.6.2
(the saddle-point value identity), since it is the one genuinely general technique this mission
introduces.
In economics, a pair of goods are substitutes if raising the price of one increases demand for the other, and complements if it decreases it; formally, a utility or value function is submodular in the substitutes case and supermodular in the complements case. A natural question is which of these two regimes a given optimization problem's value function falls into, and whether the answer depends on the underlying combinatorial structure of the problem rather than being a coincidence of the particular numbers involved. Murota's Discrete Convex Analysis (SIAM, 2003) answers this question for the maximum-weight circulation problem in a directed network: the value function is submodular in some coordinates and supermodular in others, purely as a consequence of a graph-theoretic distinction — whether the arcs involved are parallel or series — and this chapter shows the distinction is explained precisely by the dual pair of discrete convexity notions (L-natural-convexity and M-natural-convexity) developed elsewhere in the book. This mission also completes the quadratic-forms thread the previous mission in this series (Discrete Convex Analysis XV) began, by formalizing its natural generalization to functions that may take the value .
Let be a directed graph with vertex set and arc set ; write , for the initial and terminal vertex of arc . For a flow , its boundary is , the net flow leaving . Given a capacity , is a feasible circulation for if for every arc and for every vertex. For a weight , is the maximum-weight circulation value, and is optimal for (with capacity ) if it is feasible and attains this maximum. A simple cycle is an alternating sequence of pairwise distinct vertices and arcs with (indices mod ) and . Two arcs are parallel if every simple cycle containing both of them orients them oppositely, and series if every such cycle orients them the same way; a set of arcs is parallel (series) if its arcs are pairwise parallel (series). A circuit is a -valued with whose support forms a simple cycle. For , , . A function is submodular if , supermodular with the reverse inequality, and has translation submodularity (is L-natural-convex) if the stronger inequality holds for every . A function has the M-natural exchange property (is M-natural-convex) if for there exist and with for ; a function is M-natural-concave or L-natural-concave if its negation is M-natural- or L-natural-convex.
Goal (Theorem 2.23). For a parallel arc set and a series arc set,
where , denote 's dependence on the coordinates of , indexed by (resp. ) with the remaining coordinates held fixed. This is the mission's capstone: it upgrades the plain submodularity/supermodularity split of Theorem 2.22 to the sharper pair of combinatorial convexity classes that explains it.
Supporting milestones. Proposition 2.21 (the classical fact that is convex in and concave in , with no combinatorial content — the baseline against which Theorem 2.23's sharper claim is measured); Theorem 2.16 (the general, possibly--valued extension of the quadratic-form conjugacy from Discrete Convex Analysis XV's Theorem 2.11, to functions restricted to a linear subspace); Theorem 2.22 (plain submodularity/supermodularity of in and , the result Theorem 2.23 strengthens); and Propositions 2.24–2.28 (the graph-theoretic lemmas — sparse intersection of a circuit's support with a parallel or series arc set, merging two circuits along a series set, and three existence statements for optimality-preserving perturbations — that the book's own proof of Theorem 2.23 is built from).
Theorem 2.23 gives a structural explanation, rather than a case-by-case verification, for a phenomenon well known in network flow theory: that convexity/concavity and submodularity/supermodularity are independent properties, appearing in all four combinations depending on which side of the problem (weights or capacities) and which graph-theoretic role (parallel or series) is varied. Without it, (2.55)'s four combinations would be four separate facts with no common cause; with it, they are corollaries of two applications of a single pair of dual discrete-convexity notions, the same notions the book uses throughout to unify matroid theory, submodular optimization, and convex analysis. Formalizing this mission produces, so far as a platform search shows, the first Lean statement of a combinatorial-convexity classification result for a network optimization value function, together with the graph-theoretic vocabulary (simple cycles, parallel/series arcs, circuits) needed to state it — infrastructure with no prior formalized counterpart on the platform that a later mission on network flows or matroid union could reuse.
The naive approach to Theorem 2.23 tries to verify translation submodularity or the exchange property directly from the linear-programming definition of as a maximum over a polytope, treating as an abstract convex-piecewise-linear function; this loses the graph structure entirely and gives at best the plain submodularity of Theorem 2.22, not the sharper L-natural/M-natural classification, because submodularity alone does not distinguish a combinatorially meaningful discrete convexity from an arbitrary submodular function. The book's actual route instead works with explicit optimal circulations for the two perturbed weight vectors and reconstructs a feasible pair achieving the target inequality by rerouting flow along a circuit — and the existence of a usable circuit (one that touches the perturbed arcs in a way compatible with the parallel or series structure) is exactly what Propositions 2.24–2.28 supply via the conformal decomposition of a difference of two circulations into elementary circuits. This is why those five propositions, although individually narrow existence lemmas, are included as milestones: they are the load-bearing combinatorial content the naive convex-analytic argument cannot reach.
The graph is {V A : Type*} with src dst : A → V rather than a bundled structure, matching
the book's own notation directly. is a real sSup over feasible
circulations' weights (existence of a maximizer is not asserted, since no proof is attempted this
pass); IsOptimalCirc is a separate, directly-stated primitive for " is optimal for ",
matching the book's own working vocabulary in the propositions that need it. A simple cycle is
formalized as an injective cyclically-indexed vertex sequence together with a matching arc
sequence, exactly as the book's own footnote defines it; parallel and series arcs are defined by
quantifying over every such representation of every simple cycle containing the two arcs, which
is checked to be independent of which of a cycle's two traversal directions or starting vertex is
chosen. Viewing as a function of alone extends a partial vector by a fixed background
vector on the complement of , the same partial-application device the book uses informally.
M-natural- and L-natural-concavity are recorded as the corresponding convexity property of the
negated function, the standard convention. The formalization does not trivialize: parallel and
series arc sets are genuine graph-theoretic hypotheses (not, e.g., specialized to or a
graph with no simple cycles, which would make the parallel/series distinction vacuous), and
Theorem 2.23's four conclusions are stated with the same combinatorial-convexity predicates
(TranslationSubmodular, MNatExchangeR) used for the book's sharpest discrete convexity
classes, not weakened to plain submodularity/supermodularity. Theorem 2.16 additionally needs
Set (V → ℝ)-valued subspaces K, H (following the book's own set-builder notation for ker M
and X⊥ rather than bundling them as Mathlib Submodules) and a WithTop ℝ-valued Legendre-
Fenchel conjugate. Infrastructure needed beyond Mathlib: all graph, circulation, and
combinatorial-convexity vocabulary is defined fresh in DiscreteConvex.CombinatorialC; a
contribution proving any of the five graph-theoretic lemmas (Propositions 2.24–2.28) or the
convex/concave halves of Proposition 2.21 independently would be a natural entry point.
Once a finite-horizon Markov Decision Model (MDM) is known to admit an optimal policy — the existence theory of continuity/compactness models — a natural next question is qualitative: does the optimal value function inherit structural properties (monotonicity, concavity, convexity) of the model's own data, and are the resulting optimal actions themselves monotone in the state? These questions matter beyond aesthetics. A value function known in advance to be concave in wealth, say, restricts the search for an optimizer to a much smaller, better-behaved class of candidates, simplifies numerical solution (dynamic programming over convex functions can exploit shape-preserving approximation schemes), and is often the only handle available for comparative-statics questions — e.g. "if the model's transition mechanism becomes riskier, does the decision-maker's value go down?" — the kind of question that drives applications in inventory theory, insurance, and portfolio choice. The general theory traces to Topkis's lattice-programming approach to comparative statics (Topkis, Supermodularity and Complementarity, Princeton University Press, 1998) and to the stochastic-orders literature (Müller and Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002); Bäuerle and Rieder's Chapter 2, §2.4.4-2.4.5 specializes both to the Borel-space finite-horizon Markov Decision Model of their own Definition 2.1.1.
Fix a (non-stationary) Markov Decision Model as in Definition 2.1.1: , measurable spaces, the admissible state-action pairs, the transition kernel, the one-stage reward, the terminal reward. Write . An upper bounding function (Definition 2.4.1) is a measurable function for which constants exist with , , and for all admissible and all ; is the set of measurable with for some . The two central operators are and ; a decision rule is a maximizer of at time if for every . The Structure Assumption (SAN) on families and of decision rules says: ; implies ; and every has a maximizer in . It is the single hypothesis from which the whole finite-horizon theory — a well-defined Bellman recursion, an optimal policy built rule-by-rule — follows (established elsewhere in this mission series).
For this section only, and carry the usual componentwise order, and the same spaces are given a real vector-space structure when convexity statements are in play; denotes has property for . A set is completely monotone (Definition 2.4.15) if with , forces . A function on a lattice is supermodular (Definition A.3.1) if for all . The comparison theorem below additionally uses three orders between probability measures: the usual stochastic order ( for every bounded increasing , Definition B.3.2/Theorem B.3.3(ii)), the convex order (same, for convex , Definition B.3.9a), and its concave-function dual (matching ; see the Formalization scope section on how the book's own, non-monotone "cv" differs from the increasing-concave order it also uses elsewhere, e.g. in Definition B.3.9c).
This is the weakest stable statement: it names exactly the compatibility conditions between the kernel, reward, and terminal payoff that propagate convexity through , without committing to any particular model beyond them.
Six further results of the same section are formalized as milestones on the way to, or alongside, the goal: the monotone (increasing) analogue (Theorem 2.4.14), the accompanying result that a largest maximizer under a supermodular on a completely monotone is itself weakly increasing (Proposition 2.4.16), the concavity-preservation step for and its structure theorem (Proposition 2.4.18, Theorem 2.4.19), the convexity-preservation step together with the existence of a bang-bang maximizer when is a polytope (Proposition 2.4.21), and the comparison theorem for two models whose kernels are ordered (Theorem 2.4.23).
Theorems 2.4.14/2.4.19/2.4.22 give three parallel, reusable templates: once a modeler checks three or four structural conditions on , , , individually — never on the recursively-defined value function itself, which is usually inaccessible in closed form — the corresponding shape of the value function is guaranteed for every horizon, with no further induction needed by the modeler. This is what makes results like the concavity of the optimal consumption-investment value function (used in later chapters of this book) checkable from the market model alone. Proposition 2.4.16's comparative-statics conclusion (optimal actions inherit monotonicity in the state) is the Markov-decision-process incarnation of Topkis's monotone comparative statics, and Theorem 2.4.23 formalizes the intuitive but non-trivial fact that making the transition mechanism "worse" in a precise stochastic-order sense can only lower the optimal value — a comparison that requires the compatibility between the order and the very shape (monotonicity/concavity/convexity) the Structure Assumption already pins down.
All of these results, including the goal, are unformalized on the platform prior to this
mission: no result matching "supermodular", "completely monotone", "comparative statics", or a
Borel-space convex Markov decision model was found in a platform search at drafting time. The
proofs themselves are short (Bäuerle and Rieder give complete, self-contained arguments for
every result in this section), so what this mission contributes is the formal statement —
getting the exact quantifiers and hypothesis set right in a general Borel/vector-space setting —
rather than a technically deep proof; the sorry-free companion proofs are left as the
formalization task.
The obvious first idea for the goal is to prove convexity of by convexity of a supremum of convex functions — true only when does not itself depend on in a way that mixes domains under a convex combination. The book's own hypothesis (i), (constant), is exactly what rules out the general case and makes the argument work: for a genuinely -dependent , a convex combination need not even have its action component available at the combined state, so "supremum of convex functions is convex" does not apply termwise. A second trap is treating (closed under concave, not-necessarily-increasing ) as if it required the stronger increasing-concave order that the appendix's Definition B.3.9c actually names — the two are different relations, and only the plain "concave-test-function" order is compatible with as stated (see Formalization scope).
Because Mathlib's ConvexOn/ConcaveOn require a Module ℝ structure on the codomain, and
EReal (needed for value functions that may equal ) carries no such structure, this
mission introduces ConvexOnEReal/ConcaveOnEReal: the same defining inequality with the real
convex-combination coefficients cast into EReal and multiplied there (EReal does carry a
Mul). Real-valued convexity/concavity of and uses Mathlib's own ConvexOn/
ConcaveOn directly. "Vertex of a polytope" (Proposition 2.4.21) is formalized via Mathlib's
Set.extremePoints, and " is a polytope" as compact, convex, with finitely many extreme
points. The comparison theorem's order has no verbatim numbered
definition in the book: Appendix B.3 defines the stochastic order
(Definition B.3.2, via CDFs, with the increasing-test-function characterization given as an
equivalent condition, Theorem B.3.3(ii)) and the convex order (Definition
B.3.9a, directly via for convex ), but never a bare
"" — only the increasing-concave order (Definition
B.3.9c). This mission defines as the direct concave-test-function analogue
of ( for every concave ), matching the
book's own (plain concavity, not required to be increasing) and
consistent with the standard "st/cv/cx" triple of Müller and Stoyan (2002), the reference the
book cites for this whole appendix section. Likewise is formalized directly
via Theorem B.3.3(ii)'s functional characterization (bounded increasing test functions) rather
than the CDF definition, since Theorem 2.4.23 compares kernels on a general rather than real-valued random variables. The value function used only in the
comparison theorem is given by its recursive characterization (, ,
established as this series' Theorem 2.3.8) rather than by re-deriving the sup-over-policies
primitive definition and its supporting history/policy machinery, which is not otherwise needed
in this mission.
A trivializing formalization is ruled out: taking throughout would make
hypothesis (i) (" is convex") vacuously true and hide the genuinely restrictive role
plays in the proof; this mission keeps (and ) as general real vector
spaces (with a Preorder added only where monotonicity, rather than convexity, is at stake),
so the convexity hypotheses carry their full content. Reusable infrastructure:
ConvexOnEReal/ConcaveOnEReal (any later chunk needing shape-preservation results for
EReal-valued value functions can reuse the same pattern, restated per this series' convention),
and the LEStochasticOrder/LEConcaveOrder/LEConvexOrder triple (reused, restated, by
mission 04b's Theorems 4.4.4-4.4.5 and mission 05b's Definition 5.4.9, which need the same or
a closely related order). sorry-free proofs of the milestones (all short in the book) are
welcome contributions.
Newton's method converges quadratically near a non-degenerate minimum, but on its own it has no global guarantee: far from a minimum the Newton step may not exist or may increase the objective. Nesterov and Polyak (Math. Program. 108 (2006) 177–205) replaced the Newton step by the minimizer of a cubic-regularized second-order model. The resulting method has global complexity bounds on non-convex problems, which the other missions of this series formalize. This mission formalizes the complementary local result, Theorem 3 of the paper. Close to a non-degenerate local minimum, a relaxed version of the method keeps the quadratic rate of the classical Newton method. It no longer needs the safeguards (a lower bound on the regularization parameter and a descent test) that the global analysis relies on.
The cubic-regularized step later became the basis of adaptive cubic regularization (Cartis, Gould and Toint, Math. Program. 127 (2011)). Local quadratic convergence is the property that makes such second-order methods worth their per-iteration cost.
Let and let be twice differentiable, with gradient and Hessian . The Hessian is assumed Lipschitz continuous with constant in the spectral norm (Assumption 1 of the paper):
Eigenvalues of a symmetric operator are numbered decreasingly, so is the smallest eigenvalue, and means .
For , the cubic model of at is
and the cubic-regularized Newton step is any global minimizer of (Eq. (2.4)). Its length is .
The relaxed method (3.5) starts at and sets
Unlike the globally convergent scheme (3.3), it imposes no lower bound and no acceptance test . The local progress measure is
If and , the whole sequence converges to a point with and that is a local minimum of . Moreover, for every ,
Theorem 3 shows that the cubic-regularized scheme does not lose Newton's local behaviour. Once the iterates enter the region , any choice gives a doubly exponential decrease of the gradient norm. The theorem thus supplies the final phase of the paper's complexity estimate (6.1) (Section 6), which counts the iterations until is reached and then adds a last phase of order steps.
On the formal side, the result is proved in the literature but, as far as a search of the platform shows, not formalized. A complete development yields a machine-checked local convergence theorem for a regularized Newton method under a Lipschitz Hessian. The ingredients include the Taylor bound (2.2), the stationarity system (2.5) of the cubic model, and eigenvalue perturbation bounds for Lipschitz Hessians, and they are reusable for other second-order methods. The published proof of (3.8) contains a gap in its constant (see Difficulty), so a formal proof would also certify the printed constant.
The obvious argument treats as a Newton step with a small perturbation and invokes the classical Kantorovich-type analysis. That analysis assumes the regularization vanishes. Here can be as large as , and the step solves a nonlinear system (2.5) in which the step length appears in the operator. The proof must control three coupled quantities at once: the gradient, the smallest Hessian eigenvalue, and the step length. The eigenvalue lower bound has to survive infinitely many steps, so the per-step losses of curvature must be summable, and positive definiteness at the next iterate has to be established before is even defined.
The printed proof of (3.8) is not immediate from (3.6). It states , but (3.6) as printed only gives , which is too weak for the constant . A proof of (3.8) as stated cannot rest on (3.6) alone.
EuclideanSpace ℝ (Fin n) with . The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every point; the operator norm is the spectral norm.IsCubicStep). Every result holds for every such choice, matching the paper's "Arg min". A merely stationary point of the model is not a step.lamMin A, the infimum of over the unit sphere. It equals the smallest eigenvalue for self-adjoint , and is 0 < lamMin (H x).x 0. The ranges are as printed: in (3.6)–(3.7) and in (3.8). "Converges quadratically" is rendered by the paper's own quantitative clause (3.8), together with existence of the limit, , and IsLocalMin f x*.The theorem assumes positivity of the Hessian and only at . A formalization that assumes strongly convex, everywhere, or for all , or that imports the lower bound or the descent test of method (3.3), proves a different theorem and is excluded.
Needed infrastructure: the Taylor bound with Lipschitz Hessian, first-order optimality of the non-smooth-looking but cubic model, perturbation bounds for lamMin under operator-norm changes, and the inverse bound . These are reusable well beyond this mission. Contributions welcome: proofs of the milestones, and a proof of (3.8) with the printed constant.
Maximizing a nonnegative submodular set function without constraints contains Max Cut, Max Directed Cut and facility-location problems as special cases. In the value-oracle model an algorithm knows nothing about the function except the values of the sets it queries, and it is judged by the number of queries it makes. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave constant-factor algorithms in this model and matching limits on what any algorithm can do. For symmetric functions, such as cut functions of undirected graphs, a uniformly random set already achieves of the optimum in expectation (Theorem 2.1 of the paper). The question this mission formalizes is whether any algorithm can do better, and the answer given by Theorem 4.5 is: not without exponentially many value queries. The same factor was later shown to be achievable for general (non-symmetric) nonnegative submodular functions by Buchbinder, Feldman, Naor and Schwartz (FOCS 2012 / SIAM J. Comput. 2015), so the bound of Theorem 4.5 is the tight limit of the whole problem in the value-oracle model.
Timeline:
Let be the ground set, with even. A set function is submodular if for all , symmetric if for all , and .
Fix an integer with and write , so that is an integer. For integers put
For a set with and , the hard instance is . The cut function of the complete graph is , with maximum . A set is balanced for if ; on balanced sets .
A deterministic adaptive -query algorithm chooses each query from the answers received so far, and after answers outputs a set when run against an oracle . A randomized algorithm is a distribution over deterministic ones, with expected value .
For every such :
Hence the ratio attained is at most .
The theorem shows that the factor for symmetric submodular maximization, and hence for unconstrained submodular maximization in general, cannot be improved by any algorithm that uses a subexponential number of value queries, whatever its running time. It is an information-theoretic bound and needs no complexity assumption. Along with the later matching -approximation, it settles the value-oracle approximability of the problem. The construction, a function equal to a symmetric function on "balanced" sets and larger elsewhere, is the prototype of the symmetry-gap technique used for many later oracle lower bounds.
The result is proved in the paper. No machine-checked version is known to exist: the platform has no value-oracle or query-lower-bound statement. Formalizing it requires a precise model of adaptive randomized query algorithms, a concentration bound for the hypergeometric distribution, and a finite verification of submodularity of an explicit two-regime function, and it fixes the constants that the printed statement leaves as terms.
Two steps of the printed argument do not go through as written. First, the proof bounds the probability that a fixed query is unbalanced by citing the Chernoff bound for independent variables, but for a uniformly random half-size set the count is hypergeometric, and the summands are not independent. A bound for sampling without replacement is needed instead. Replacing the balanced partition by independent coin flips is not an option: then in general, and the function is no longer the paper's instance.
Second, the argument counts only the queries, but the value an algorithm receives is of its output, which equals of the output only if the output is balanced as well. That event has to be controlled too.
Finally, submodularity of must be checked across the boundary between the two regimes, where the formula changes.
Fin n with even; is an integer with and , following the paper's "assume that is an integer". Sets are Finset (Fin n), and all values are real.Finset.sup' over all subsets. There is no junk value.n/2-subsets divided by , written multiplied out.query, output : List ℝ → Finset (Fin n) making exactly adaptive queries with arbitrary real answers. A randomized algorithm is a PMF over deterministic algorithms, which covers every randomization with countable support. The algorithm sees only through query answers; it never receives .PMF of algorithms. The algorithm model and the hypergeometric bound are reusable for other oracle lower bounds. Proofs of any milestone, and alternative derivations of the balance bound, are welcome.Many polytopes that arise in combinatorial optimization, such as the matching, cut, stable set and travelling salesman polytopes, have exponentially many facets, yet some of them can be written as the linear projection of a polyhedron with far fewer facets. The smallest number of facets of such a lift decides whether the polytope admits a compact linear-programming formulation. Yannakakis (Expressing combinatorial optimization problems by linear programs, J. Comput. System Sci. 43 (1991)) showed that this number equals the nonnegative rank of the polytope's slack matrix, turning a question about formulations into a question about matrix factorizations. Gouveia, Parrilo and Thomas (arXiv:1111.3164v2) extended this correspondence from polytopes and nonnegative orthants to arbitrary convex bodies and closed convex cones.
Exact nonnegative rank is NP-hard to compute (Vavasis, SIAM J. Optim. 20 (2009)), so lower bounds matter. The oldest ones are combinatorial: they see only which entries of the slack matrix are zero. Goemans (Smallest compact formulation for the permutahedron, Math. Program. 153 (2015)) observed that a polytope with faces needs a lift with at least facets. Section 4.2 of Gouveia–Parrilo–Thomas recasts these support-based bounds through the face lattice and derives, alongside Goemans' bound, a sharper antichain bound. This mission formalizes that chain of results.
Write for Euclidean space with inner product . A polytope is the convex hull of finitely many points; as throughout the paper, the origin is assumed to lie in its interior. The polar of is
Let be the set of extreme points of (its vertices). The slack operator is the function on . The extreme points of correspond to the facets of , the facet of being , so is the canonical vertex–facet slack matrix of and is nonnegative.
An -factorization of consists of maps and with . The nonnegative rank is the least such , and if there is none.
The support is the matrix with a one where . A Boolean factorization of it of intermediate dimension assigns subsets with ; the least such is the Boolean rank.
A face of is the empty set or a set of maximizers in of a linear functional; itself is a face. The face lattice is the set of faces ordered by inclusion, and the Boolean lattice is the set of subsets of ordered by inclusion. An embedding satisfies .
For a polytope :
for every antichain of faces of (no face contained in another), and
where is the number of faces of , including and .
Both bounds depend only on the combinatorial type of the polytope. For a square they give and ; for a three-dimensional cube and (p. 16). For the regular -gon, whose slack matrices all have rank , the face-count bound gives , which is of the optimal order (Example 4.14). Theorem 4.11 is the statement that the Boolean rank of a slack matrix, also known as its rectangle covering number, is an invariant of the face lattice; the rectangle-covering version is phrased as Theorem 2.9 of Fiorini, Kaibel, Pashkovich and Theis (Combinatorial bounds on nonnegative rank and extended formulations, arXiv:1111.0444), as cited by the paper.
The results are proved in the paper. The formalization provides machine-checked definitions of the polar, the slack operator of a polytope, its nonnegative and Boolean ranks and its face lattice, reusable for later work on extension complexity (for instance, rectangle-covering lower bounds for specific polytopes). No formal proof of these statements is known to exist in Lean or on this platform.
Milestone 1 and the passage from Corollary 4.12 to Corollary 4.13 are short: Sperner's theorem is available in Mathlib as IsAntichain.sperner, and an embedding of into is injective. The weight lies in Theorem 4.11, which needs facts about polytopes that Mathlib does not state in this form: every vertex is an exposed point, each extreme point of the polar cuts out a face, every face of a polytope is the convex hull of the vertices it contains, and every proper face is the intersection of the facets containing it, with those facets indexed by . The last fact is where the origin-in-the-interior assumption and the polar enter, and it fails for faces described by an arbitrary list of inequalities that is not the facet description. A second, smaller difficulty is finiteness: the face-count bound needs the set of faces of a polytope to be finite.
is EuclideanSpace ℝ (Fin n) with the Euclidean inner product. The polar is the one-sided polar above, not Mathlib's absolute polar. A polytope is the convex hull of a Finset with the origin in its interior; is allowed (), and all targets hold there. Faces are Mathlib's exposed faces (IsExposed ℝ C F), which include and , as the paper's counts do; for a polytope these are all faces. The factorization maps are total functions on constrained only on extreme points. The nonnegative rank is valued in ℕ∞, the infimum of the empty family being ; part (2) of the goal is stated for every finite value of the rank. Part (1) is stated for every antichain of faces, equivalent to the paper's "largest antichain". "Smallest " is sInf of a set of naturals that is nonempty in each case (the set of with , and the set of admitting an embedding of the finite lattice ).
The paper says "lattice embedding". Its proof of Theorem 4.11 constructs, and uses, only a map that preserves and reflects inclusion, and need not preserve joins or meets; the formalization reads "lattice embedding" as an order embedding (Face C ↪o Finset (Fin k)) throughout.
Trivializing formalizations are ruled out: the rank is not a natural-number infimum (which would be when no factorization exists); faces are not arbitrary subsets of ; and an embedding is order-reflecting, not merely monotone (every poset maps monotonically into ).
Welcome contributions: a proof of milestone 1; a library of polytope facts (vertices are exposed points, faces are convex hulls of their vertices, finiteness of the face lattice, facets from the polar), which is reusable well beyond this mission; then Theorem 4.11 and the corollaries.
Many optimization problems ask for a subset of a finite ground set that maximizes a submodular function, a set function with diminishing marginal returns. Max Cut and Max Directed Cut in graphs, facility location with fixed costs, and the maximization of mutual information or entropy of a subset of random variables are all of this form. Unlike the monotone case, where a greedy algorithm achieves , a general nonnegative submodular function may decrease when elements are added, and the empty set and the full set can both be poor. The question is how large a constant fraction of the optimum a polynomial-time algorithm can guarantee when the function is given only through an oracle that returns for a queried set .
Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor algorithms for this problem. A uniformly random set achieves of the optimum, a deterministic local search achieves , and a randomized smooth local search achieves . The last result is the paper's best approximation for general nonnegative submodular functions (Table 1, p. 1136), and it is the subject of this mission.
Timeline. Feige, Mirrokni and Vondrák: , and (FOCS 2007; journal version 2011). Gharan and Vondrák (SODA 2011): about by simulated annealing. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015): a randomized double greedy algorithm achieving , which matches the hardness in the value oracle model proved in the same paper by Feige, Mirrokni and Vondrák.
Let be a finite ground set with elements and a function with for all and
Write . The multilinear extension of is
the expected value of on a random set containing each independently with probability .
For and , the random set is sampled with bias based on : each element of is included independently with probability , each element of with probability . The potential is and the smoothed marginal value of is
Algorithm SLS starts from . At each iteration it obtains estimates within of . If some has it adds ; otherwise, if some has it removes ; otherwise it stops and returns a random set .
With , and with probability or with probability : for every run from whose estimates are all accurate and which has terminated at ,
and, for every , every run of iterations with accurate estimates has (fewer than for ).
The bound showed that local search on a smoothed objective, the multilinear extension restricted to points with two coordinate values, beats both uniform sampling and plain local search for non-monotone submodular maximization. The multilinear extension later became the standard tool for submodular maximization under constraints, through continuous greedy methods, contention resolution schemes and the analysis of randomized rounding. Display (∗) and Lemma 2.2 are the basic sampling inequalities for submodular functions and are reused throughout that literature.
The result is proved in the paper; it has been superseded in ratio by later algorithms reaching . To our knowledge none of it is machine-checked: Mathlib has no multilinear extension and no submodular maximization results. This mission produces a checked form of the analysis with every constant explicit: the as , "polynomial time" as iterations, and the dependence on the accuracy of the sampled estimates as an explicit hypothesis.
The iteration bound and the increment identity are routine once the multilinear extension is set up. The substance lies in the lower bounds. The returned set is random, so the comparison with the optimal set cannot be made through a single local-optimality inequality as in deterministic local search; and approximate local optimality holds only for the smoothed marginals , which are averages over the random set, not for at any fixed set. Sampling inequalities such as (∗) are stated for independent samples of arbitrary, possibly overlapping sets, and their expectations are sums over products of subsets; the bookkeeping of such sums is the main formalization burden. The constants must also balance exactly: with the ths add up so that the mixture yields . A different split or a different gives a different constant.
The ground set is a Fintype X with decidable equality; sets are Finset X; is real valued, with nonnegativity and submodularity as hypotheses. The standing assumptions of the paper are made explicit: (§3), value-oracle access (modelled by itself), , and (Nonempty X), so that and are not Lean's junk value of division by zero. is Finset.sup' over all subsets, which has no junk value. Every expectation over independently sampled sets is an exact finite sum: the multilinear extension for , and iterated sums over subsets for the several independent samples in Lemma 2.2 and (∗). Sampling probabilities carry .
The algorithm is a relation, not a choice: any element meeting the step-3 condition may be added, and removal is allowed only when no addition applies. The goal quantifies over every run from , every choice of accurate estimates, recomputed at every iteration, and every termination point. Accuracy is non-strict ("within "); the thresholds are strict. The thresholds and accuracy use itself, as the proof does, although step 1 of the algorithm says an estimate of is used. The sampling that produces the estimates and its "with high probability" are not modelled, and the goal is conditional on accurate estimates. The value of the branch is written as , which equals .
A statement "every satisfying the terminal conditions gives " would be the final milestone plus arithmetic and is not the goal. The goal fixes the start at , the thresholds, the step order, the accuracy of every estimate, termination and the mixture.
A complete development needs basic calculus of the multilinear extension: affinity in one coordinate, translation and restriction , and splitting a sample into disjoint pieces. These lemmas are reusable for any work on submodular maximization, and contributions of them as separate theorems are welcome. The golden-ratio variant (proof omitted in the paper), the tight example and the hardness results of §4 are out of scope.
Many data sets are large matrices of which only a small fraction of the entries is observed, and of which the underlying object is believed to have low rank: user–item rating tables in collaborative filtering, distance matrices in sensor-network localization, and measurement matrices in structure-from-motion. Matrix completion asks when the missing entries can be recovered exactly. Rank minimization subject to the observed entries is intractable in general. Its convex relaxation, nuclear-norm minimization, is a semidefinite program, and the question is how many randomly placed entries it needs.
Timeline:
Fix of rank with singular value decomposition , where and , are orthonormal. Let , , and let be the sign matrix. The tangent space at is the image of the projection
and .
obeys the strong incoherence property with parameter if every entry of and is within of the corresponding entry of , and every entry of is at most in absolute value.
An observation set is either a uniformly random -subset (the uniform model) or contains each entry independently with probability (the Bernoulli model). keeps the entries in and zeroes the rest. The program is
where is the sum of the singular values.
The analysis uses the centered operators and , where and . It also uses the random matrices , where the operator is applied to from the right. denotes the spectral norm.
There is an absolute constant such that, for every fixed as above and uniformly sampled entries,
The constant is not fixed; the goal asserts only its existence.
provided the right-hand side is below . 3. Lemma 8.1. An exact expansion of in powers of with explicit recursive coefficients. 4. Lemma 8.2. The coefficients are at most , with . 5. Lemma 3.3. On the event , the same terms with obey the bound with an extra factor . 6. Theorem 3.6 (Moment bound II). Let and . Then
Theorem 1.2 shows that a polynomial-time convex program recovers an incoherent low-rank matrix from a number of entries that is linear in and within a polylogarithmic factor of what any method requires. It turned nuclear-norm minimization from a heuristic into a method with near-optimal guarantees, and much of the later work on low-rank recovery, robust PCA and phase retrieval uses its framework of dual certificates, tangent spaces and incoherence.
The theorem is proved; formalizing it is the remaining work here. None of these results has a machine-checked proof. The platform already has the Candès–Recht definitions (nuclear norm, SVD data, Bernoulli model, tangent projection), the deterministic Lemma 3.1, and the Bernoulli-to-uniform transfer. This mission adds:
Shorter later proofs (Gross, Recht) use a different incoherence condition. A formal proof of the goal along either route is welcome, provided it proves the statement as given.
The obvious approach bounds each term of the Neumann series for the certificate separately, using noncommutative Khintchine inequalities and decoupling. This is what Candès and Recht did, and it fails beyond small : the entries of these matrices are coupled through the same random indicators, and the bounds degrade with . That is where their comes from.
The moment method avoids this but has its own obstruction. Taking absolute values inside the expansion of loses a factor of , which gives the quadratic dependence of Theorem 1.1. The linear bound needs sign cancellations among the coefficients of to be tracked through a nested induction over "generalized spider" configurations (Section VI). Replacing by (Lemma 3.3) is necessary for those cancellations. Without it the diagonal coefficients are of size instead of .
Matrix (Fin n) (Fin n) ℝ (MatrixCompletion.RealMatrix). The SVD is the platform structure SVD M r. Logarithms are natural. Probabilities are the platform's finite sums: successProb (uniform -subsets), bernoulliEventProb and bernoulliExpectation. The spectral norm is spectralNorm. The definitions of matrix_completion_{basic,svd,bernoulli,tangent} are reused, not restated.successProb is for ; it does not exclude any case the paper covers. The failure probability stays and is not traded for a constant. The constant may not depend on , , or , so it cannot be chosen to make (I.12) unsatisfiable. For fixed , (I.12) is satisfiable with for every large and every .