Convex Optimization

Motivation

Chunk 10 formalized the discrete conjugacy theorem — the Legendre-Fenchel transform's bijection between the classes of M-convex and L-convex functions — and, along the way, a function-level generalization of Edmonds's intersection theorem. Section 8.4 turns that machinery toward a different question: not "how are two convexity classes related," but "when does a discrete optimization problem have a dual that meets it with equality." The classical route to such strong-duality results in continuous convex programming — Lagrangian relaxation, an embedding of the problem in a family of perturbed problems, and a saddle-point characterization of when primal and dual values coincide — has a discrete analogue that needs no continuity, no differentiability, and no convexity in the classical sense at all: only the elementary fact that the Legendre-Fenchel transform, once discretized, is still an involution on the right class of functions. This mission formalizes that discrete Lagrangian duality framework and its central saddle-point theorem, in full generality — before the book specializes it, in the section that follows, to the specific M-convex perturbation that gives the chapter's headline strong-duality result for M-convex programs.

Setting

Let $V$ and $U$ be finite ground sets. A perturbation of an optimization problem $\min\{f(x) : x \in \mathbb Z^V\}$ is a function $F : \mathbb Z^V \times \mathbb Z^U \to \mathbb Z \cup \{+\infty\}$ such that $F(x,0) = f(x)$ for all $x$ (Eq. (8.54)) and, for each fixed $x$, $F(x,\cdot)$ is self-biconjugate: $F(x,\cdot)^{\bullet\bullet} = F(x,\cdot)$ under the discrete Legendre-Fenchel transform of chunk 10 (Eq. (8.55)). The Lagrangian function is $K(x,y) = \inf\{F(x,u) + \langle u,y\rangle : u \in \mathbb Z^U\}$ (Eq. (8.58)), valued in $\mathbb Z \cup \{\pm\infty\}$ (formalized in EReal, since both the infimum and the supremum below can be genuinely unbounded). The dual objective is $g(y) = \inf\{K(x,y) : x \in \mathbb Z^V\}$ (Eq. (8.60)). Writing $\inf(P) = \inf_x f(x)$, $\sup(D) = \sup_y g(y)$, $\operatorname{opt}(P) = \{x : f(x) = \inf(P)\}$, $\operatorname{opt}(D) = \{y : g(y) = \sup(D)\}$, the primal problem $P$ is to minimize $f$ over $\mathbb Z^V$ and the dual problem $D$ is to maximize $g$ over $\mathbb Z^U$.

Formalization targets

Goal: Theorem 8.54 (the saddle-point theorem)

Assuming $F$ is self-biconjugate (Eq. (8.55)): both $\inf(P)$ and $\sup(D)$ are finite and $\min(P) = \max(D)$ if and only if there exist $\bar x \in \mathbb Z^V$, $\bar y \in \mathbb Z^U$ with $K(\bar x,\bar y)$ finite and $K(x,\bar y) \le K(\bar x,\bar y) \le K(\bar x,y)$ for all $x,y$ — a saddle point of the Lagrangian kernel. When this holds, $\bar x \in \operatorname{opt}(P)$ and $\bar y \in \operatorname{opt}(D)$.

Milestones: Theorem 8.52, Proposition 8.51(1)-(2)

Theorem 8.52 (weak duality): $\inf(P) \ge \sup(D)$ always, with no biconjugacy hypothesis on $F$ at all — the baseline the saddle-point theorem sharpens to equality. Proposition 8.51(1)-(2): under self-biconjugacy, the perturbation $F$ (and hence the primal objective $f$) is itself recoverable from the Lagrangian kernel $K$ by a supremum, $F(x,u) = \sup_y\{K(x,y) - \langle u,y\rangle\}$ and $f(x) = \sup_y K(x,y)$ — the algebraic identity the saddle-point theorem's proof turns on directly.

Significance

The result itself. The saddle-point theorem is the general-purpose engine behind every strong-duality result the book proves for specific classes of discrete optimization problems: the book's own next section specializes it (via a particular choice of $F$ built from an M-convex regularizer $r$) to obtain strong duality for M-convex programs, but the theorem itself needs no M-convexity, no submodularity, and no exchange axiom — only the elementary self-biconjugacy of a perturbation under the discrete Legendre-Fenchel transform. It is, in that sense, the most general and most reusable strong-duality statement in the book: any future mission proving strong duality for a specific class of discrete programs (M-convex, M2-convex, network flow, or otherwise) by exhibiting a self-biconjugate perturbation can cite this theorem directly rather than reproving the saddle-point argument from scratch.

Formalizing it. No matching item exists on the platform for a discrete Lagrangian saddle- point theorem, discrete weak duality, or this perturbation-based duality framework. (A prior-art search turned up an unrelated continuous Lagrangian saddle-point theorem for convex cones, Luenberger's Chapter 8 §8.4, formalized as VectorSpaceOpt.lagrangian_saddle_sufficient_pointed — a genuinely different setting: no discreteness, no biconjugacy hypothesis, and a one-directional sufficiency statement rather than this mission's iff. Not reused.) This mission gives the first formal statement of discrete Lagrangian duality, and directly reuses chunk 10's ConvexConjugate apparatus (self-biconjugacy is stated using chunk 10's own conjugate-of-conjugate composition), demonstrating exactly the kind of shared-substrate payoff the discrete conjugacy theorem was built to provide.

Difficulty

The saddle-point theorem's "only if" direction is not a routine unwinding of definitions: given $\min(P) = \max(D)$ at finite common value, one must construct the saddle point $(\bar x,\bar y)$ — the book's proof takes $\bar x \in \operatorname{opt}(P)$, $\bar y \in \operatorname{opt}(D)$ (which exist because the infimum/supremum are attained at a finite optimum) and verifies the sandwiching inequality using Proposition 8.51(2)'s identity $f(x) = \sup_y K(x,y)$ together with weak duality, rather than by any direct algebraic manipulation of $K$ alone. Skipping straight to a "trivial" biconditional that never invokes Proposition 8.51 would misrepresent the actual proof structure the book relies on for exactly this direction.

Formalization scope

$V, U$ are Fintype ground types; LagrangianKernel, DualObjective, InfP, SupD are EReal-valued to keep both the defining infima/suprema total (a complete lattice) without an artificial finiteness side-condition; OptP, OptD compare PrimalValue/DualObjective against InfP/SupD after casting through chunk 10's ToEReal, mirroring that chunk's own round-trip convention. "Finite" throughout is formalized as ≠ ⊤ ∧ ≠ ⊥ in EReal. The perturbation $F$ itself is left fully abstract (an arbitrary function satisfying the self-biconjugacy hypothesis where needed) — this mission does not draft the specific M-convex perturbation $F_r$ (Eq. (8.61)) that the book's next subsection (§8.4.3) uses to specialize this framework to M-convex programs, nor Theorem 8.59 (the resulting M-convex strong-duality theorem) itself, which needs that specific perturbation plus its own regularity conditions (REG)/(OBJ) and a chain of M-convex-specific propositions (8.55–8.58) beyond what the general framework built here provides. A trivializing formalization would state the saddle-point theorem's sandwiching inequality with a weaker order (e.g., only one of the two directions) or would omit the "$\bar x \in \operatorname{opt}(P), \bar y \in \operatorname{opt}(D)$" consequence clause; neither is done — both inequalities and the full consequence clause are included exactly as the book states them.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.

Motivation

This mission completes chapter 7's L-convex function theory and closes the book on it. It first finishes the theory of positively homogeneous L-convex functions — showing they coincide exactly with the classical Lovász extensions of submodular set functions, a one-to-one correspondence that recognizes forty years of submodular-optimization machinery as a special case of L-convex function theory. It then proves the L-side capstone this series has been building toward since mission 26-ch07b-lconvexfunctions: polyhedral L-convexity is characterized simultaneously by directional derivatives, subdifferentials, and weighted-minimizer polyhedra — the exact mirror of what mission 24-ch06d-mconvexfunctions proved for M-convex functions. Finally it develops quasi L-convex functions, the L-side analogue of mission 25-ch06e-mconvexfunctions's quasi M-convex functions, ending exactly where chapter 7 itself ends.

Setting

Fix a finite ground set $V$. The class $0L[\mathbb R \to \mathbb R]$ consists of polyhedral L-convex functions that are positively homogeneous; $0L[\mathbb Z \to \mathbb Z]$, its integer-valued integer-domain analogue. A positively homogeneous L-convex function $g$ induces a submodular set function $\rho_g(X) = g(\chi_X)$; conversely the Lovász extension $\hat\rho$ of a submodular set function is positively homogeneous L-convex. The base polyhedron $B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ \forall X,\ x(V) = \rho(V)\}$ of a submodular $\rho$ is always an M-convex polyhedron. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is quasi submodular (QSB) if $g(p\wedge q) \le g(p)$ or $g(p\vee q) \le g(q)$ for all $p,q$; the weaker (QSBw) requires only $\max\{g(p),g(q)\} \ge \min\{g(p\wedge q), g(p\vee q)\}$.

Formalization targets

Goal: the four characterizations of polyhedral L-convexity (Theorem 7.45)

For a polyhedral convex function $g$ with $\operatorname{dom}_{\mathbb R} g \ne \emptyset$: $g$ is L-convex if and only if every directional derivative $g'(p;\cdot)$ is $0L[\mathbb R \to \mathbb R]$, if and only if every subdifferential $\partial_{\mathbb R} g(p)$ is an M-convex polyhedron, if and only if every weighted minimizer set is an L-convex polyhedron. Not present in this chunk's own extraction table (its label opens mid-paragraph, missed by the same extractor failure already documented for mission 25-ch06e-mconvexfunctions's Theorem 6.68), found by direct reading and chosen as goal because it is the exact L-side mirror of mission 24-ch06d-mconvexfunctions's own milestone Theorem 6.63, and its proof is assembled entirely from results already in this series (Theorem 7.43, Proposition 7.34, Theorem 7.40).

Supporting structural targets

Fifteen further results build the two remaining pieces of chapter 7's theory. Propositions 7.37-7.39 and Theorem 7.40 establish the one-to-one correspondence between positively homogeneous L-convex functions and submodular set functions via the Lovász extension; Proposition 7.41 gives a minimizer-polyhedron characterization of this class, and Proposition 7.42 shows directional derivatives of L-convex functions automatically land in it. Theorem 7.43 — the L-side mirror of mission 24-ch06d-mconvexfunctions's own goal, Theorem 6.61 — proves the directional- derivative/subdifferential correspondence via the induced submodular set function's base polyhedron; Proposition 7.44 checks consistency at integer points, and Theorem 7.46 refines Theorem 7.45 to the integral case. Theorem 7.49 (also missed by the extractor) gives the quasi-submodularity implication hierarchy and its perturbation-equivalence capstone, mirroring mission 25-ch06e-mconvexfunctions's Theorem 6.68 exactly. Proposition 7.50 and Theorems 7.51-7.52 build the level-set/perturbation machinery quasi submodularity needs; Theorems 7.53-7.54 (both missed by the extractor, the latter's full statement requiring one page beyond this chunk's nominal range, at the very end of chapter 7) give the quasi L-optimality and quasi L-proximity theorems.

Significance

The 0L/submodular correspondence (Theorem 7.40) is the precise sense in which L-convex function theory generalizes submodular set function theory rather than merely resembling it: every submodular set function is literally the restriction to $\{0,1\}^V$ of a positively homogeneous L-convex function, and every algorithm for one transfers to the other through this exact dictionary. The goal, Theorem 7.45, completes the parallel structure this series has built since chapter 6: M-convexity and L-convexity are now each characterized in the same four convex-analytic vocabularies, setting up chapter 8's conjugacy theorem, which will show these two characterizations are not merely analogous but literally dual to each other under the Legendre-Fenchel transform. The quasi-submodularity results matter for the same reason as their M-side counterparts: chapter 10's algorithms for L-convex-function minimization remain correct under nonlinear rescalings that destroy L-convexity itself but preserve quasi submodularity.

None of these results are open — they are Murota's account of how far L-convex function theory extends beyond the polyhedral case (to positive homogeneity and its submodular-function incarnation) and how far its exchange-style inequality can be relaxed while preserving optimization theory (to quasi submodularity), mirroring chapter 6's identical two-part program for M-convex functions. What this mission contributes is a faithful, machine-checked formal statement of each, including four theorems (7.45, 7.49, 7.53, 7.54) the platform's own automated extractor missed entirely — one of them requiring a page beyond this chunk's own nominal range to complete, since chapter 7 ends there and this is the last mission covering it — extending the shared Lean vocabulary (ZeroLR, BasePolyhedron, QSBw) this series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to prove all six pairwise implications among its four conditions independently; the book's own proof instead chains through results already established: (a)⇒(b) is Proposition 7.42, (a)⇒(c) is Theorem 7.43, (a)⇒(d) is Proposition 7.34, (b)⇔(c) uses the 0L/M0[R] correspondence, and (d)⇒(b) is the genuinely hard direction, requiring Proposition 7.41 applied to the directional derivative itself (showing $\arg\min(g'(p;\cdot)[-x])$ is an L-convex cone by an explicit description via the admissible-potential set of the distance function underlying $\arg\min g[-x]$). The remaining combinatorial difficulty in this block is in Theorem 7.43's proof: identifying $\partial_{\mathbb R} g(p)$ with the base polyhedron $B(\rho_{g,p})$ requires the L-optimality criterion (Theorem 7.33, mission 27-ch07c-lconvexfunctions) applied pointwise, a chain of logical equivalences with no single-step shortcut, exactly mirroring how mission 24-ch06d-mconvexfunctions's Theorem 6.61 needed the M-optimality criterion.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; L-convex functions are (V→ℝ)→WithTop ℝ (polyhedral) or (V→ℤ)→WithTop ℝ (integer-domain). All sixteen numbered results found in this chunk's page range — the twelve in BRIEF.md's own table plus four the extractor missed (Theorems 7.45, 7.49, 7.53, 7.54) — are placed, with two documented, content-preserving scope decisions: Theorem 7.43 omits the dual-integral refinement clauses for L[R→R|Z]/L[Z→Z] (the same decision mission 24-ch06d-mconvexfunctions's Theorem 6.61 made), and Proposition 7.50 states the general inequalities without restating their "In particular" specializations, which add no independent content — see HARD.md. "$\inf g[-x]>-\infty$" is replaced by the equivalent (ArgMinR ...).Nonempty hypothesis throughout, matching mission 25-ch06e-mconvexfunctions's identical substitution. This mission's base vocabulary is redeclared from missions 20-ch04b-mconvexsets, 21-ch05b-lconvexsets, 23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the sixteen sorrys are welcome; the goal and Theorem 7.43 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota and A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research, 24 (1999), pp. 95-105 [152] (the polyhedral theory Theorems 7.26-7.46 are drawn from).
• P. Milgrom and C. Shannon, "Monotone comparative statics," Econometrica, 62 (1994), pp. 157-180 [129] (the origin of the quasi-submodularity condition (SSQSB)).

Motivation

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$^\natural$-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.

Setting

Fix a finite ground set $V$. A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain is polyhedral L-convex, $g \in L[\mathbb R \to \mathbb R]$, if it satisfies (SBF[R]): $g(p)+g(q) \ge g(p\vee q)+g(p\wedge q)$, and (TRF[R]): $\exists r \in \mathbb R$, $g(p+\alpha\mathbf 1) = g(p)+\alpha r$ for all $p \in \mathbb R^V$, $\alpha \in \mathbb R$; it is polyhedral L$^\natural$-convex if its lift to one extra real coordinate is polyhedral L-convex. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ 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 $\hat\rho$ of a submodular set function $\rho$ is the piecewise-linear interpolation built from the sorted distinct components of $p \in \mathbb R^V$. The directional derivative $g'(p;d)$ is $\inf_{t>0}(g(p+td)-g(p))/t$.

Formalization targets

Goal: the polyhedral L-optimality criterion (Theorem 7.33)

For a polyhedral L-convex function $g$ and $p \in \operatorname{dom}_{\mathbb R} g$: $g(p) \le g(q)$ for all $q$ if and only if $g'(p;\chi_Y) \ge 0$ for every $Y \subseteq V$ and $g'(p;\mathbf 1)=0$; for polyhedral L$^\natural$-convex $g$, the criterion simplifies to $g'(p;\pm\chi_Y) \ge 0$ for every $Y$. 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 $|V|+1$ (or $2|V|$) directional-derivative inequalities.

Supporting structural targets

Twelve further results build the polyhedral theory from the ground up. Theorems 7.20-7.21 identify L$^\natural$-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$^\natural$ 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.

Significance

Theorems 7.20-7.21's synonym is structurally important: it means every algorithm and theorem already known for submodular-function minimization over $\{0,1\}^V$-type domains applies, after a midpoint-convexity check, to the vastly larger class of integer-lattice L$^\natural$-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 $\mathbb R^V$, 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).

Difficulty

The naive approach to the goal would try to verify $g(p) \le g(q)$ directly against every $q \in \mathbb R^V$; 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$^\natural$-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 $\to$ integral-convexity $\to$ 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 $\rho_k \to \rho$ for the general, possibly-infinite case — a genuine two-step argument, not a single inequality chase.

Formalization scope

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. "$g_U > -\infty$" 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.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota and A. Shioura, "Extreme points of a generalized polymatroid," Discrete Applied Mathematics, 152 (2005), pp. 268-278 [152] (the polyhedral L-convex function theory this mission's real-variable results are drawn from).

Motivation

Chapter 5 characterized L-convex sets — sublattice-closed, translation-periodic subsets of $\mathbb Z^V$ — 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$^\natural$[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.

Setting

Fix a finite ground set $V$. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain is L-convex, $g \in L[\mathbb Z \to \mathbb R]$, if it satisfies submodularity (SBF[Z]): $g(p)+g(q) \ge g(p\vee q) + g(p\wedge q)$, and translation invariance (TRF[Z]): $\exists r \in \mathbb R$, $g(p+\mathbf 1) = g(p) + r$ for all $p$. It is L$^\natural$-convex if its lift to one extra coordinate (Eq. (7.2)) is L-convex. A set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ is submodular if $\rho(X)+\rho(Y) \ge \rho(X\cup Y) + \rho(X\cap Y)$; it corresponds to an L$^\natural$-convex function supported on $\{0,1\}^V$ via $g(\chi_X) = \rho(X)$ (Eq. (7.5)). The convex closure $\bar g$ of $g$ is its extension to $\mathbb R^V$ by finite convex combinations.

Formalization targets

Goal: L-convexity via minimizer polyhedra (Theorem 7.17)

For $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with bounded nonempty effective domain: $g$ is L-convex if and only if $\arg\min g[-x]$ is an L-convex set for every $x \in \mathbb R^V$; the L$^\natural$ analogue holds with L$^\natural$-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."

Supporting structural targets

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$^\natural$- convexity; Proposition 7.4 identifies submodular set functions with a subclass of L$^\natural$-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$^\natural$- 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 ($x=0$) 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 $g$ on $\mathbb Z^V$ and inherits its translation constant.

Significance

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).

Difficulty

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 $g$'s submodularity applied at the optimal $q_1,q_2$ simultaneously — a genuine two-hypothesis combination with no single-inequality shortcut.

Formalization scope

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 $g$ on $\mathbb Z^V$ 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. "$g_U > -\infty$" and its variants are replaced by the equivalent (DomZ ...).Nonempty hypothesis throughout, matching mission 24-ch06d-mconvexfunctions's identical substitution (WithTop ℝ has no $-\infty$ 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.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313–371 (the original account of L-convex functions this chapter's basic theory is drawn from).

Motivation

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.

Setting

Let $V$ be a finite ground set and $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$. Building on chunk 08's submodularity axiom (SBF[Z]), this section introduces four ordinal relaxations. $g$ is quasi submodular, satisfying (QSB), if for every $p, q \in \mathbb Z^V$, $g(p \wedge q) \le g(p)$ or $g(p \vee q) \le g(q)$. $g$ is semistrictly quasi submodular, satisfying (SSQSB), if additionally $g(p \vee q) \ge g(q) \implies g(p \wedge q) \le g(p)$ and symmetrically. The weak variants (QSBw) and (SSQSBw) restrict attention to points of the effective domain and compare $\max(g(p), g(q))$ against $\min(g(p \wedge q), g(p \vee q))$ directly, with (SSQSBw) additionally allowing the four-way tie $g(p) = g(q) = g(p\wedge q) = g(p \vee q)$. The linear perturbation of $g$ by $x : V \to \mathbb R$ is $g[x](p) = g(p) + \langle p, x \rangle$.

Formalization targets

Goal: Theorem 7.54 (the quasi L-proximity theorem)

Let $g$ satisfy (SSQSB) and $g(p) = g(p + \mathbf 1)$ for all $p$, $n = |V|$, $\alpha$ a positive integer. If $p_\alpha \in \operatorname{dom} g$ satisfies $g(p_\alpha) \le g(p_\alpha + \alpha \chi_Y)$ for all $Y \subseteq V$, then $\arg\min g \ne \emptyset$ and there is $p^* \in \arg\min g$ with the componentwise bound $p_\alpha \le p^* \le p_\alpha + (n-1)(\alpha-1) \mathbf 1$ — 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]).

Milestones: Theorems 7.49, 7.53

Theorem 7.49: the full nesting chain (SBF[Z]) $\Rightarrow$ (SSQSB) $\Rightarrow$ (QSB), (SSQSB) $\Rightarrow$ (SSQSBw) $\Rightarrow$ (QSBw), together with the collapse theorem that (SBF[Z]) holds if and only if every linear perturbation of $g$ 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 $2^n - 2$ nontrivial sign-pattern neighbors $p + \chi_X$.

Significance

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.

Difficulty

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 $p_\alpha = 0$, 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.

Formalization scope

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, $g[x](p) = g(p) + \langle p,x\rangle$, is the opposite of the M-side's $f[p](x) = f(x) - \langle p,x\rangle$ (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 $(n-1)(\alpha-1)$; 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.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• P. Milgrom, C. Shannon, "Monotone comparative statics," Econometrica, 62(1), 1994, pp. 157–180.

Motivation

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.

Setting

Fix a finite ground set $V$ and $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$. Write $\Delta f(z;v,u) = f(z + \chi_v - \chi_u) - f(z)$. Relaxing the exchange axiom's inequality $\Delta f(x;v,u) + \Delta f(y;u,v) \le 0$ to the sign patterns it forces gives quasi M-convexity (QM) and semistrict quasi M-convexity (SSQM), and requiring only some pair $(u,v)$ rather than every $u$ gives their weaker variants (QMw), (SSQMw); the minimization-only variants (SSQM$\ne$), (SSQM$\ne_w$) replace "$x,y \in \operatorname{dom} f$" with "$f(x) \ne f(y)$". The set-level analogue (Q-EXC)/(Q-EXCw) relaxes the M-convex-set exchange axiom the same way. For $\alpha \in \mathbb R$, the level set $L(f,\alpha) = \{x \in \mathbb Z^V : f(x) \le \alpha\}$. A polyhedral convex function $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (real-variable) M-convex, $f \in M[\mathbb R \to \mathbb R]$, if it satisfies the real exchange axiom (M-EXC[R]) from chunk 24-ch06d-mconvexfunctions; $L_0[\mathbb R]$ denotes polyhedra realized as $D(\gamma)$ for a triangle-inequality distance function $\gamma$, and $M_0[\mathbb R]$ denotes real M-convex polyhedral cones.

Formalization targets

Goal: the quasi M-convexity hierarchy (Theorem 6.68)

For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$: (1) the implication diagram (M-EXC[Z]) $\Rightarrow$ (SSQM) $\Rightarrow$ (QM), (M-EXCw[Z]) $\Rightarrow$ (SSQMw) $\Rightarrow$ (QMw), (M-EXC[Z]) $\Leftrightarrow$ (M-EXCw[Z]), (SSQM) $\Rightarrow$ (SSQMw), (QM) $\Rightarrow$ (QMw); (2) $f$ satisfies (M-EXC[Z]) if and only if $f[p]$ satisfies (QMw) for every $p \in \mathbb R^V$. 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?

Supporting structural targets

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 $L_0[\mathbb R]$-valued subdifferentials, and via $M_0[\mathbb R]$/$M_0[\mathbb Z|\mathbb R]$-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$\ne_w$) 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$\ne$) hypothesis.

Significance

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 $\phi \circ f$ of an M-convex $f$ 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 $f$ 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).

Difficulty

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.

Formalization scope

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: "$\inf f[-p] > -\infty$" is replaced by the equivalent (ArgMinOn ...).Nonempty hypothesis (WithTop ℝ has no $-\infty$ element), matching mission 23-ch06c-mconvexfunctions's identical substitution; and $M_0[\mathbb R]$/$M_0[\mathbb Z|\mathbb R]$ 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.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• M. Avriel, W. E. Diewert, S. Schaible, and I. Zang, Generalized Concavity, Plenum Press, 1988 (the continuous quasi-convexity theory this chapter's discrete analogue generalizes).

Motivation

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:

• 1999: Artzner et al. introduce coherent risk measures and show that ES-type measures dominate VaR (doi:10.1111/1467-9965.00068).
• 2002: Föllmer and Schied introduce convex risk measures.
• 2020: Mao and Wang characterise the risk measures consistent with second-order stochastic dominance as infima of ES-based functionals.
• 2022: Castagnoli et al. prove Theorem 5, the corresponding characterisation of star-shaped law-invariant risk measures through VaR.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space with $P$ atomless: every event of positive probability contains an event of strictly smaller positive probability. A position is a bounded measurable function $X:\Omega\to\mathbb R$, read as a loss: $X(\omega)>0$ is money lost in state $\omega$. The positions form a linear space $\mathcal X$ that contains the constants and carries the pointwise order $X\geqq Y$.

A risk measure is a function $\rho:\mathcal X\to\mathbb R$ that is monotone ($X\geqq Y\Rightarrow\rho(X)\ge\rho(Y)$), translation invariant ($\rho(X-m)=\rho(X)-m$ for real $m$) and normalized ($\rho(0)=0$). It is star-shaped if $\rho(\lambda X)\ge\lambda\rho(X)$ for all $X$ and all $\lambda>1$, and law-invariant if $X$ and $Y$ with the same law under $P$ satisfy $\rho(X)=\rho(Y)$. Its acceptance set is $\mathcal A_\rho=\{X\mid\rho(X)\le 0\}$. A set $S$ in a vector space is star-shaped if $\lambda s\in S$ whenever $s\in S$ and $\lambda\in[0,1]$.

For $\alpha\in(0,1)$ the Value-at-Risk of $X$ is

$$\mathrm{VaR}_\alpha(X)=\inf\{x\in\mathbb R : P(X>x)\le 1-\alpha\}.$$

Write $F_X(x)=P(X\le x)$. A loss $X$ first-order stochastically dominates $Y$, written $X\succsim_{\mathrm{FSD}}Y$, if $F_X\ge F_Y$ pointwise, so $X$ is the smaller loss.

Formalization targets

Goal: Theorem 5, (i) ⇔ (ii)

For a function $\rho:\mathcal X\to\mathbb R$ the following are equivalent:

1. $\rho$ is a star-shaped and law-invariant risk measure;
2. there is a star-shaped set $\mathcal G$ of increasing functions $g:(0,1)\to\mathbb R$ with $g(0+)\le 0$ such that

$$\rho(X)=\inf_{g\in\mathcal G}\ \sup_{\alpha\in(0,1)}\ \{\mathrm{VaR}_\alpha(X)-g(\alpha)\}\qquad X\in\mathcal X.\tag{25}$$

The goal fixes neither $\mathcal G$ 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".

Milestones

• Eq. (7): $\rho(X)=\min\{m\in\mathbb R\mid X-m\in\mathcal A_\rho\}$ for every risk measure.
• Proposition 2: for a risk measure $\rho$, the following are equivalent: $\rho$ is star-shaped; $\mathcal A_\rho$ is star-shaped; $\rho=\rho_{\mathcal A}$ for a star-shaped acceptance set $\mathcal A$.
• Eq. (A.1): $F_X\ge F_Y$ if and only if $\mathrm{VaR}_\alpha(X)\le\mathrm{VaR}_\alpha(Y)$ for all $\alpha\in(0,1)$.
• FSD consistency (proof of Theorem 5): if $P$ is atomless and $\rho$ is monotone and law-invariant, then $X\succsim_{\mathrm{FSD}}Y\Rightarrow\rho(X)\le\rho(Y)$.

Significance

Theorem 5 says that the star-shaped law-invariant risk measures are exactly the robustifications of VaR: each benchmark $g$ in $\mathcal G$ gives a capital requirement $\sup_\alpha\{\mathrm{VaR}_\alpha(X)-g(\alpha)\}$, and $\rho$ 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.

Difficulty

The direction (ii) ⇒ (i) is a direct computation. The direction (i) ⇒ (ii) rests on FSD consistency. The obvious argument writes $X\succsim_{\mathrm{FSD}}Y$ as $X\le Y$ 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 $X$ and $Y$ 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 $\alpha$ near $0$ where $g$ may diverge.

Formalization scope

Positions are the bounded measurable functions $\Omega\to\mathbb R$ (a Submodule ℝ (Ω → ℝ), definition Positions) with the pointwise order, rather than equivalence classes in $L^\infty(\Omega,\mathcal F,P)$. For a law-invariant $\rho$ 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 $(0,1)$, where the infimum is over a nonempty set that is bounded below. In (25) each function $g$ has domain exactly $(0,1)$, "increasing" means weakly increasing, and $g(0+)\le 0$ is stated as $\inf_{\alpha\in(0,1)}g(\alpha)\le 0$ in the extended reals. Both sides of (25) are compared in the extended reals, since the inner supremum can be $+\infty$. 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 $0$. Dropping monotonicity of $g$ or the condition $g(0+)\le 0$ describes a larger class that includes non-normalized functionals. Allowing $\mathcal G=\emptyset$ is excluded because the left side of (25) is a real number and the right side would be $+\infty$.

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 $\mathrm{VaR}_\alpha$), 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.

Selected references

• E. Castagnoli, G. Cattelan, F. Maccheroni, C. Tebaldi, R. Wang, Star-Shaped Risk Measures, Operations Research 70(5):2637–2654, 2022. https://doi.org/10.1287/opre.2022.2303
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, 4th ed., De Gruyter, 2016. https://doi.org/10.1515/9783110463453
• T. Mao, R. Wang, Risk Aversion in Regulatory Capital Principles, SIAM Journal on Financial Mathematics 11(1):169–200, 2020 (cited as Mao and Wang 2020 in the source paper).
• V. Bignozzi, M. Burzoni, C. Munari, Risk Measures Based on Benchmark Loss Distributions, Journal of Risk and Insurance, 2020 (cited as Bignozzi et al. 2020 in the source paper).

Motivation

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 $\mathrm{MaxVaR}$, 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.

Setting

Fix a set $\Omega$ of states. The space of positions $\mathcal X$ is a linear space of bounded functions $X:\Omega\to\mathbb R$ containing every constant function; the constant $m$ is identified with the position that pays $m$ in every state. A value $X(\omega)>0$ is a loss. No probability measure is fixed. $\mathcal X$ is ordered pointwise: $X\geqq Y$ means $X(\omega)\ge Y(\omega)$ for every $\omega$.

A risk measure is a function $\rho:\mathcal X\to\mathbb R$ that is monotone ($X\geqq Y\Rightarrow\rho(X)\ge\rho(Y)$), translation invariant ($\rho(X-m)=\rho(X)-m$ for all real $m$) and normalized ($\rho(0)=0$). It is

• star-shaped if $\rho(\lambda X)\ge\lambda\rho(X)$ for all $X$ and all $\lambda>1$;
• convex if $\rho(\lambda X+(1-\lambda)Y)\le\lambda\rho(X)+(1-\lambda)\rho(Y)$ for all $X,Y$ and all $\lambda\in(0,1)$;
• positively homogeneous if $\rho(\lambda X)=\lambda\rho(X)$ for all $\lambda>0$;
• coherent if it is positively homogeneous and subadditive, $\rho(X+Y)\le\rho(X)+\rho(Y)$.

The acceptance set of $\rho$ is $\mathcal A_\rho=\{X\in\mathcal X\mid\rho(X)\le0\}$. More generally, an acceptance set is a subset $\mathcal A\subseteq\mathcal X$ with $\sup\{m\in\mathbb R\mid m\in\mathcal A\}=0$ that is closed downwards ($X\in\mathcal A$, $Y\leqq X$ imply $Y\in\mathcal A$). It is convex if convex and coherent if a convex cone, and it generates $\rho_{\mathcal A}(X)=\inf\{m\mid X-m\in\mathcal A\}$. A set $S$ is star-shaped if $\lambda s\in S$ for all $s\in S$ and $\lambda\in[0,1]$.

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.

Formalization targets

Goal: Theorem 2 (p. 2643)

For a risk measure $\rho$, the following are equivalent:

1. $\rho$ is star-shaped;
2. there is a set $\Gamma$ of convex risk measures with

$$\rho(X)=\min_{\gamma\in\Gamma}\gamma(X)\qquad\text{for all }X\in\mathcal X;$$

3. there is a family $\{\mathcal A_\beta\}_{\beta\in B}$ of convex acceptance sets with

$$\rho(X)=\min\{m\in\mathbb R\mid X-m\in\mathcal A_\beta\text{ for some }\beta\in B\}\qquad\text{for all }X\in\mathcal X.$$

Moreover, for star-shaped $\rho$, $\Gamma$ may be taken to be the set of all convex risk measures $\gamma\geqq\rho$, and the family to be their acceptance sets. The minima are attained. The goal fixes no particular $\Omega$, $\mathcal X$ or $\Gamma$.

Milestones

• Proposition 1 (p. 2642): star-shapedness is equivalent to $\rho(\alpha X)\le\alpha\rho(X)$ for $\alpha\in(0,1)$, and to the risk-to-exposure ratio $\beta\mapsto\rho(\beta X)/\beta$ being increasing on $(0,\infty)$.
• Eq. (7) (p. 2642): $\rho(X)=\min\{m\mid X-m\in\mathcal A_\rho\}$.
• Proposition 2 (p. 2642): $\rho$ is star-shaped iff $\mathcal A_\rho$ is star-shaped iff $\rho=\rho_{\mathcal A}$ for a star-shaped acceptance set $\mathcal A$.
• Theorem 1 (p. 2643), in four parts: the infimum, supremum, $\mu$-average and inf-convolution of star-shaped risk measures are star-shaped risk measures.
• Proposition 3 (p. 2642): for subadditive risk measures, star-shaped, positively homogeneous and convex coincide.
• Theorem 2, positively homogeneous case: the same equivalence with "positively homogeneous", "coherent risk measures" and "coherent acceptance sets".
• Corollary 1 (p. 2645): $\inf_{X\in\mathcal Y}\rho(X)=\inf_{\gamma\in\Gamma}\inf_{X\in\mathcal Y}\gamma(X)$ for any $\mathcal Y\subseteq\mathcal X$.

Significance

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.

Difficulty

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 $\rho$ or of $\mathcal A_\rho$, fails: the convex hull of $\mathcal A_\rho$ generates a convex risk measure below $\rho$, not above it, and a single convex risk measure cannot equal a non-convex $\rho$. What is needed is, for each position, a convex risk measure that dominates $\rho$ 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.

Formalization scope

• $\mathcal X$ is any 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.
• "min" is always IsLeast (attained). The acceptance-set axiom $\sup\{m\mid m\in\mathcal A\}=0$ is IsLUB, not sSup … = 0. $\rho_{\mathcal A}$ uses the real sInf, which is genuine for acceptance sets on bounded positions.
• Every $\gamma\in\Gamma$ is a full risk measure: monotone, translation invariant, normalized and convex. A representation of $\rho$ as a minimum of arbitrary, non-normalized convex functionals holds for every monotone translation-invariant map and is not this theorem; such a formalization is ruled out.
• The family in (3) is a set of subsets of $\mathcal X$, with no finiteness or nonemptiness assumption.
• A coherent acceptance set is convex and closed under multiplication by every $t>0$.
• Theorem 1 adds the hypotheses the page leaves implicit: a nonempty index set for supremum and infimum; the power-set σ-algebra and a countably additive probability measure for the average (the paper's proof also covers capacities with Choquet integrals, which are not stated here); $n\ge1$ and the normality condition (10) for the inf-convolution.
• Corollary 1 computes infima in the extended reals, so the set $\mathcal Y$ may be empty and the infima may be $-\infty$.

Contributions welcome: proofs of any milestone, and in particular general lemmas on risk measures on a space of bounded functions (the bounds $\inf X\le\rho(X)\le\sup X$, properties of $\rho_{\mathcal A}$, convexity of $\rho_{\mathcal A}$ for convex $\mathcal A$), which are reusable across risk-measure missions.

Selected references

• E. Castagnoli, G. Cattelan, F. Maccheroni, C. Tebaldi, R. Wang, Star-Shaped Risk Measures, Operations Research 70(5):2637–2654, 2022. https://doi.org/10.1287/opre.2022.2303
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072
• M. Frittelli, E. Rosazza Gianin, Putting order in risk measures, Journal of Banking & Finance 26(7):1473–1486, 2002. https://doi.org/10.1016/S0378-4266(02)00270-4
• H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, 4th ed., De Gruyter, 2016. https://doi.org/10.1515/9783110463453

Motivation

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).

Setting

Fix a finite ground set $V$. A distance function is a map $\gamma : V \times V \to \mathbb R \cup \{+\infty\}$ with $\gamma(v,v) = 0$; it may take negative finite values and need not be symmetric. It defines a directed graph $G_\gamma = (V, A_\gamma)$ with $A_\gamma = \{(u,v) : \gamma(u,v) < +\infty\}$, arc $(u,v)$ having length $\gamma(u,v)$. Write $\bar\gamma(u,v)$ for the shortest-path length from $u$ to $v$ in $G_\gamma$ ($+\infty$ if none exists); $\gamma$ is well defined ($\bar\gamma$ finite-valued wherever a path exists) exactly when $G_\gamma$ has no negative cycle. The triangle inequality $\gamma(v_1,v_2) + \gamma(v_2,v_3) \ge \gamma(v_1,v_3)$ defines the class $T[\mathbb R]$ (or $T[\mathbb Z]$ when integer-valued). A vector $p \in \mathbb R^V$ is an admissible potential of $\gamma$ if $p(v) - p(u) \le \gamma(u,v)$ for all $u \ne v$; write $D(\gamma)$ for the set of all such potentials.

A nonempty set $D \subseteq \mathbb Z^V$ is L-convex if it satisfies (SBS[Z]): $p, q \in D \implies p \vee q,\ p \wedge q \in D$ (coordinatewise max/min), and (TRS[Z]): $p \in D \implies p \pm \mathbf 1 \in D$. A set $S \subseteq \mathbb Z^V$ is integrally convex if every point of its convex hull $\overline S$ lies in the convex hull of $S$ restricted to that point's integral neighborhood $N(p) = \{y \in \mathbb Z^V : \lfloor p \rfloor \le y \le \lceil p \rceil\text{ coordinatewise}\}$ — a strong, local form of "no holes" saying every real point of the hull is explained by nearby integer points alone.

Formalization targets

Goal: integral convexity of L-convex sets

For an L-convex set $D \subseteq \mathbb Z^V$, writing $a = p - \lfloor p \rfloor$ for the fractional part of $p \in \mathbb R^V$, $\alpha_1 > \cdots > \alpha_m$ for the distinct nonzero values of $a$, and $U_i(p) = \{v : a(v) \ge \alpha_i\}$ (with $U_0 = \emptyset$):

$$\overline D = \{p \in \mathbb R^V : \lfloor p \rfloor + \chi_{U_i(p)} \in D\ \ (i = 0, 1, \ldots, m)\}, \qquad \text{hence } D \text{ is integrally convex}.$$

This is the weakest stable form available: it exhibits an explicit, finite set of at most $|V|+1$ 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.

Supporting structural targets

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).

Significance

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).

Difficulty

The shortest-path closure $\bar\gamma$ 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 $G_\gamma$ 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 "$D$ 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 $m+1$ witness points from the sorted fractional values of $p$ — a Carathéodory-style representation (Eq. (5.11)) that must simultaneously stay inside the integral neighborhood $N(p)$ and land in $D$ itself via the triangle inequality of $D$'s induced distance function, a construction with no one-coordinate-at-a-time shortcut.

Formalization scope

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 $|V|+1$ 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.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• A. J. Hoffman, "On abstract dual linear programs," Naval Research Logistics Quarterly, 10 (1963), pp. 369-373 (feasible-potential duality in network flow theory).