Operations Research

Completed

Convex Optimization Discrete Geometry Optimization·Captain: Shuze Chen

Discrete Convex Analysis VIII: Quasi L-Convex Functions and the Quasi-Proximity TheoremTextbook

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.

8 thms3 active usersReviewed

Completed

Convex Optimization Discrete Geometry Optimization·Captain: Shuze Chen

Discrete Convex Analysis XXIV: Quasi M-Convex FunctionsTextbook

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

56 thms3 active usersReviewed

Convex Optimization Functional Analysis Optimization+1·Captain: mikedeng1

Dual Stochastic Dominance and Related Mean-Risk Models 2: Mean–Gini Optimal Portfolios Exist and Are SSD-EfficientResearch Paper

Motivation

Portfolio selection and other decisions under risk are routinely solved as mean–risk models: maximize the expected outcome minus a multiple of a risk measure over the feasible set. Such a model is computationally convenient, but it is only defensible if its answers agree with the preferences of risk-averse decision makers. The standard formal expression of those preferences is second-degree stochastic dominance (SSD): a random outcome $X$ dominates $Y$ when every nondecreasing concave utility prefers $X$ . A mean–risk model whose optimal solution may be SSD-dominated by another feasible decision recommends something every risk-averse investor would reject; the classical mean–variance model has exactly this defect.

Ogryczak and Ruszczyński (SIAM J. Optim. 13 (2002) 60–78) characterize SSD through the absolute Lorenz curve (the second quantile function) and use this dual view to study risk measures defined from quantiles: the vertical diameter of the dual dispersion space, the tail Gini measure and the Gini mean difference. Their §5 shows that the mean–Gini model, with trade-off coefficient at most one, has optimal solutions and that all of them are SSD-efficient. This mission formalizes that result together with the lemmas it rests on. A companion mission of this series formalizes the dual characterization of SSD itself (the paper's Theorems 3.1–3.2).

Timeline. Yitzhaki (1982) showed the mean–Gini necessary condition for SSD for bounded distributions; Ogryczak and Ruszczyński proved SSD consistency of mean-semideviation models (Eur. J. Oper. Res. 116 (1999)) and, in the present paper, extended the analysis to quantile-based and Gini-type risk measures for general integrable outcomes, with existence and efficiency of optimal solutions over sets in $L_q$ .

Setting

Let $(\Omega,\mathcal B,P)$ be a probability space and $X:\Omega\to\mathbb R$ an integrable random variable with mean $\mu_X=E X$ and distribution function $F_X(\eta)=P\{X\le\eta\}$ . The second performance function is

F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}F_X(\xi)\,d\xi ,

and $X\succeq_{SSD}Y$ means $F_X^{(2)}(\eta)\le F_Y^{(2)}(\eta)$ for all $\eta\in\mathbb R$ . Strict dominance is $X\succ_{SSD}Y$ iff $X\succeq_{SSD}Y$ and not $Y\succeq_{SSD}X$ . For a set $Q$ of random variables, $X\in Q$ is SSD-efficient in $Q$ if no $Y\in Q$ satisfies $Y\succ_{SSD}X$ .

The left quantile function is $F_X^{(-1)}(p)=\inf\{\eta:F_X(\eta)\ge p\}$ for $0<p\le1$ ; a number $q$ is a $p$ -quantile if $P\{X<q\}\le p\le P\{X\le q\}$ . The absolute Lorenz curve is $F_X^{(-2)}(p)=\int_0^pF_X^{(-1)}(\alpha)\,d\alpha$ on $[0,1]$ . From it the paper defines

the vertical diameter $h_X(p)=\mu_Xp-F_X^{(-2)}(p)$ , $p\in[0,1]$ (eq. (3.6));
the Gini mean difference $\Gamma_X=2\int_0^1(\mu_Xp-F_X^{(-2)}(p))\,dp$ (eq. (3.8));
the tail Gini measure $G_X(p)=\frac{2}{p^2}\int_0^p(\mu_X\alpha-F_X^{(-2)}(\alpha))\,d\alpha$ , $p\in(0,1]$ (eq. (4.8)), so that $\Gamma_X=G_X(1)$ .

The optimization problem is

\max_{X\in Q}\ (\mu_X-\lambda r_X),\tag{5.1}

with $\lambda>0$ , $r_X$ one of these dual risk measures, and $Q$ a convex, closed, bounded subset of $L_q(\Omega,P)$ for some $q>1$ .

Formalization targets

Goal: Theorem 5.3

For $1<q<\infty$ , a nonempty convex bounded closed $Q\subseteq L_q$ , $r_X=\Gamma_X$ and every $\lambda\in(0,1]$ :

\operatorname*{arg\,max}_{X\in Q}(\mu_X-\lambda\Gamma_X)\neq\emptyset\quad\text{and every } X\in\operatorname*{arg\,max}_{X\in Q}(\mu_X-\lambda\Gamma_X)\text{ is SSD-efficient in }Q.

Milestones

Lemma 3.4: for $p\in(0,1)$ , $h_X(p)=\min_{\xi\in\mathbb R}E\{\max(p(X-\xi),(1-p)(\xi-X))\}$ , attained at any $p$ -quantile.
Lemma 5.1: $X\mapsto h_X(p)$ is convex and positively homogeneous on $L_1$ for $p\in[0,1]$ .
Lemma 5.2: $X\mapsto G_X(p)$ is convex and positively homogeneous on $L_1$ for $p\in(0,1]$ .
(4.1): $X\succeq_{SSD}Y\Rightarrow\mu_X\ge\mu_Y$ .
Proposition 4.5: $X\succeq_{SSD}Y\Rightarrow\mu_X-\Gamma_X\ge\mu_Y-\Gamma_Y$ and $X\succ_{SSD}Y\Rightarrow\mu_X-\Gamma_X>\mu_Y-\Gamma_Y$ .

Companion: Theorem 5.4

For $r_X=h_X(p)/p$ with $p\in(0,1)$ and $\lambda\in(0,1]$ , the optimal set $Q^*$ is nonempty and each $X\in Q^*$ has an SSD-efficient $X^*\in Q^*$ with $\mu_{X^*}=\mu_X$ and $h_{X^*}(p)=h_X(p)$ .

Significance

Theorem 5.3 certifies the mean–Gini model as a safe decision rule: whatever trade-off $\lambda\in(0,1]$ is chosen, the model returns a decision that no feasible alternative dominates for all risk-averse utilities, and such a decision exists under assumptions natural for portfolio sets in $L_q$ . Theorem 5.4 gives the weaker but still usable guarantee for the tail-value-at-risk type measure $h_X(p)/p$ , for which non-efficient optima can occur. Lemma 3.4 is the bridge to computation: it turns $h_X(p)$ into an expected piecewise-linear loss minimized over a scalar, which is how these models become linear programs over scenarios (§6 of the paper).

On the formalization side, the results are proved in the paper but, as far as a search of the platform shows, not machine-checked anywhere. A complete development produces reusable infrastructure: quantile functions and their integrals for integrable random variables, convexity of law-invariant functionals on $L_1$ , the Gini mean difference, and an existence argument for concave maximization over weakly compact subsets of $L_q$ .

Difficulty

The existence half needs weak compactness of $Q$ in the reflexive space $L_q$ and weak upper semicontinuity of $\mu_X-\lambda\Gamma_X$ . The functional is defined through quantiles, which are not linear in $X$ , so neither its concavity nor its continuity is visible from the definition. Closedness of $Q$ in the norm topology must be upgraded to weak closedness, which uses convexity. The efficiency half needs the strict inequality (4.7): a strict SSD relation must produce a strict gap in the integrated absolute Lorenz curves, and the pointwise inequality of $F^{(2)}$ alone does not give strictness in $\Gamma$ . The obvious attempt to argue efficiency from (4.6) alone fails: it yields only a weak inequality, which is compatible with an optimum being strictly dominated.

Formalization scope

One probability space $(\Omega,P)$ with IsProbabilityMeasure P; random variables are functions Ω → ℝ, and all random variables compared by $\succeq_{SSD}$ live on it.
$F_X^{(2)}$ is the Bochner integral of P.real {X ≤ ξ} over $(-\infty,\eta]$ ; $\mu_X$ is ∫ X ∂P. Every statement about general random variables assumes Integrable X P (the paper's standing $E|X|<\infty$ ).
$F_X^{(-1)}$ uses the real sInf; its junk value at $p=1$ does not enter any integral and is never used pointwise. $F_X^{(-2)}$ is used only on $[0,1]$ , so it is real-valued here; the extended-real version with $+\infty$ off $[0,1]$ belongs to the companion mission.
$\Gamma_X$ is defined by the area formula (3.8), not by the double-integral formula that the paper cites; $h_X$ is defined by (3.6), not by the minimum (3.7), so Lemma 3.4 is a genuine statement.
$L_q$ is Mathlib's Lp ℝ q P with 1 < q and q ≠ ∞ (the paper's $q$ is a real number $>1$ ); the functionals are applied to the function of an $L_q$ element, and SSD-efficiency in $Q$ refers to the image of $Q$ in functions. Positive homogeneity is stated for the $L_1$ element $c\cdot X$ .
Added hypothesis: $Q$ is nonempty. The paper does not write it, and without it the optimal set is empty.
Optimal solutions are maximizers in $Q$ , not a supremum value. The trade-off coefficient is lam because λ is a Lean keyword; the range $\lambda\in(0,1]$ is kept exactly.
A trivializing formalization is ruled out: the weak relation $\succeq_{SSD}$ must not replace the strict relation in SSD-efficiency (every $X$ weakly dominates itself), and $\Gamma$ must not be a hand-chosen closed form.

Needed infrastructure: quantile functions and the identity $\int_0^1F_X^{(-1)}=\mu_X$ ; the minimum representation of Lemma 3.4; convexity of law-invariant functionals on Lp; weak compactness of bounded closed convex sets in reflexive Lp. Contributions of general lemmas about quantiles and Lorenz curves are welcome and reusable beyond this mission.

Selected references

W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13(1) (2002) 60–78. https://doi.org/10.1137/S1052623400375075
W. Ogryczak, A. Ruszczyński, From stochastic dominance to mean-risk models: semideviations as risk measures, Eur. J. Oper. Res. 116 (1999) 33–50. https://doi.org/10.1016/S0377-2217(98)00167-2
S. Yitzhaki, Stochastic dominance, mean variance, and Gini's mean difference, Amer. Econ. Rev. 72 (1982) 178–185. https://www.jstor.org/stable/1808584

10 thms3 active usersReviewed

Combinatorics Convex Optimization Discrete Geometry+1·Captain: Shuze Chen

Discrete Convex Analysis XXI: The Exchange Axiom as Local OptimalityTextbook

Motivation

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.

Setting

Fix a finite ground set $V$ . A function $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain $\operatorname{dom} f$ is M-convex if it satisfies the exchange axiom (M-EXC[Z]): for $x, y \in \operatorname{dom} f$ and $u \in \operatorname{supp}^+(x-y)$ (coordinates where $x$ exceeds $y$ ), there is $v \in \operatorname{supp}^-(x-y)$ with

f(x) + f(y) \ge f(x - \chi_u + \chi_v) + f(y + \chi_u - \chi_v).

Writing $\tilde f(x_0, x) = f(x)$ when $x_0 = -x(V)$ and $+\infty$ otherwise (a lift to one extra coordinate), $f$ is M $^\natural$ -convex if $\tilde f$ 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 $\operatorname{dom} f$ lies on a single hyperplane. The linear-weighted function $f[p](x) = f(x) - \langle p, x \rangle$ (for $p \in \mathbb R^V$ ) is the standard device for testing local optimality under an arbitrary reweighting.

Formalization targets

Goal: the exchange axiom as sequential improvement

f \text{ is M-convex} \iff \forall p \in \mathbb R^V,\ \forall x, y \in \operatorname{dom} f,\ f[p](x) > f[p](y) \implies f[p](x) > \min_{u \in \operatorname{supp}^+(x-y)}\ \min_{v \in \operatorname{supp}^-(x-y)} f[p](x - \chi_u + \chi_v),

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.

Supporting structural targets

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

Significance

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 $p=0$ , 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).

Difficulty

The forward direction of Theorem 6.24 (M-convex $\implies$ sequential improvement) follows in one step from Proposition 6.23 applied to $f[p]$ , 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 $p$ designed so that failure of the local exchange step at that specific $p$ 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 $\operatorname{dom} f$ is M-convex fails because the exchange axiom's own statement presupposes a well-structured domain.

Formalization scope

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 ( $0$ , 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.

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 exchange axiom and its equivalent local/dynamic reformulations).

38 thms3 active usersReviewed

Completed

Convex Optimization Probability·Captain: mikedeng1

Star-Shaped Risk Measures 2: law-invariant star-shaped risk measures as robustified Value-at-RiskResearch Paper

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:

$\rho$ is a star-shaped and law-invariant risk measure;
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).

7 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Star-Shaped Risk Measures 1: star-shaped risk measures are the minima of convex risk measuresResearch 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:

$\rho$ is star-shaped;
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;

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

14 thms3 active usersReviewed

Completed

Dynamic Programming Linear Optimization Optimization+1·Captain: Shuze Chen

Markov Decision Processes XIV: Positive Models and Linear Programming Duality for MDPsTextbook

Motivation

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

Setting

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 $\varepsilon$ , 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 ( $v \in IM$ ) and finitely-additive-in-spirit measures ( $\mu \in M_b$ ); and state-space discretization approximates an infinite (Borel) state space by a finite grid, with an explicit, computable bound on the resulting numerical error.

Formalization targets

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 $(P)$ is solved exactly by the true optimal value function $J_\infty$ , the dual program $(D)$ 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).

Significance

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 $\mathbb R^n$ -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.

Difficulty

Constructing the occupation measure $\mu^{f^\infty}_p$ 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 $p$ forward through the model's kernel under a fixed stationary decision rule) combined with a countable Measure.sum of $\beta^k$ -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 ( $x = \sum_k\lambda_kx_k$ for grid points $x_k$ ) 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.

Formalization scope

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 $\varepsilon$ , the occupation-measure/linear-program apparatus of §7.5.2, and the grid-approximation data of §7.5.3. The primal/dual optimal values $\mathrm{val}(P)$ / $\mathrm{val}(D)$ are kept EReal-valued rather than real-valued specifically so that Theorem 7.5.6's own finiteness claims ( $-\infty < \mathrm{val}(D)$ , $\mathrm{val}(P) < \infty$ ) 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.

Selected references

N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960 (the policy improvement algorithm this section names after him).
E. V. Denardo, "On linear programming in a Markov decision problem," Management Science, 1970 (the classical finite-state linear-programming formulation this section generalizes).
W. J. Heilmann, "A note on the dual of a linear program with infinitely many constraints," cited by the book's own Remark 7.5.5 for the finitely-additive treatment the restricted dual $(D)$ over $M_b$ sidesteps.

17 thms3 active usersReviewed

Analysis Control Theory Dynamical Systems+1·Captain: mikedeng1

Generalized Gradients and Applications II: Flow-Invariant Sets of Lipschitz Differential InclusionsResearch Paper

Motivation

A closed set $F\subseteq\mathbb R^n$ is flow-invariant for a dynamical system when every trajectory that starts in $F$ stays in $F$ . 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 $F$ is equivalent to the global statement that trajectories cannot leave $F$ ?

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 $\dot x\in X(x)$ , a closed set is flow-invariant if and only if $X(x)$ is contained in the tangent cone at each point of the set.

Timeline:

1942. Nagumo characterizes invariance for continuous ODEs with unique solutions by a condition on the distance function (Proc. Phys.-Math. Soc. Japan 24).
1969. Bony proves an invariance theorem for Lipschitz vector fields, stated through exterior normals, in the course of a maximum principle for degenerate elliptic operators (Bony 1969).
1970. Brezis characterizes flow-invariant closed sets of a locally Lipschitz vector field by $\lim_{\delta\downarrow0} d_F(y+\delta X(y))/\delta=0$ (Brezis 1970).
1972. Redheffer gives simplified proofs of the Bony and Brezis theorems under weaker "uniqueness function" hypotheses (Amer. Math. Monthly 79, 740–747).
1975. Clarke extends the characterization to Lipschitz multifunctions with nonempty compact values, with tangency in the sense of his new tangent cone, and recovers Bony and Brezis as corollaries (Clarke 1975, Theorem (4.4), Corollaries (4.10), (4.12)).

Setting

Throughout, $\mathbb R^n$ carries the Euclidean inner product $\zeta\cdot v$ and norm $|\cdot|$ .

Generalized gradient. For $f:\mathbb R^n\to\mathbb R$ Lipschitz on bounded sets, $\partial f(x)$ is the convex hull of all limits $\lim_i\nabla f(x+h_i)$ with $h_i\to0$ and $f$ differentiable at each $x+h_i$ (Definition (1.1)). The generalized directional derivative is $f^\circ(x;v)=\limsup_{h\to0,\ \delta\downarrow0}[f(x+h+\delta v)-f(x+h)]/\delta$ (Definition (1.3)).

Distance function. For a nonempty closed $E\subseteq\mathbb R^n$ , $d_E(x)=\min\{|x-e|:e\in E\}$ . It is Lipschitz with constant $1$ . A point $e\in E$ with $|x-e|=d_E(x)$ is a closest point to $x$ ; it exists but need not be unique.

Normal and tangent cones. For $e\in E$ , the cone of normals is

N_E(e)=\operatorname{cl}\{p:\ s\,p\in\partial d_E(e)\text{ for some }s>0\}\qquad\text{(Definition (3.1))},

and the tangent cone is its dual,

T_E(e)=\{\zeta:\ \zeta\cdot v\le0\text{ for all }v\in N_E(e)\}\qquad\text{(Definition (3.6))}.

Differential inclusions. A multifunction $X$ assigns to each $x\in\mathbb R^n$ a set $X(x)\subseteq\mathbb R^n$ ; standing assumption of §4: every $X(x)$ is nonempty and compact. A trajectory is an absolutely continuous $x:[0,1]\to\mathbb R^n$ with $\dot x(t)\in X(x(t))$ for almost every $t$ ((4.1)). $X$ is Lipschitz if there is $K$ such that for all $x_1,x_2$ and $v_1\in X(x_1)$ some $v_2\in X(x_2)$ has $|v_1-v_2|\le K|x_1-x_2|$ ((4.2)). A closed set $F$ is flow-invariant for $X$ if every trajectory with $x(0)\in F$ has $x(t)\in F$ for all $t\in[0,1]$ ((4.3)).

Formalization targets

Goal: Theorem (4.4)

Let $X$ be a Lipschitz multifunction with nonempty compact values and $F$ a nonempty closed subset of $\mathbb R^n$ . Then

F\text{ is flow-invariant for }X\iff X(x)\subseteq T_F(x)\ \text{ for every }x\in F.

Milestones, in the order the proof uses them

Proposition (1.4). $f^\circ(x;v)=\max\{\zeta\cdot v:\zeta\in\partial f(x)\}$ for locally Lipschitz $f$ .
Proposition (2.4). If $\nabla d_E(x)$ exists and is nonzero, then $x\notin E$ , $x$ has a unique closest point $e$ , and $\nabla d_E(x)=(x-e)/|x-e|$ .
Corollary (2.5). For $e\in E$ , $\partial d_E(e)=\operatorname{co}\{0,\lim (x_i-e_i)/|x_i-e_i|\}$ over $x_i\notin E$ , $x_i\to e$ , $e_i$ closest to $x_i$ .
Proposition (3.2). $N_E(e)=\operatorname{cl}\operatorname{co}\{\lim s_i(x_i-e_i)\}$ over $s_i\ge0$ , $x_i\to e$ , $e_i$ closest to $x_i$ .
Inequality (4.8). If $X(y)\subseteq T_F(y)$ on $F$ and $x$ is a trajectory, then $f(t)=d_F(x(t))$ satisfies $f'(t)\le Kf(t)$ almost everywhere.
Limit (4.9). If $F$ is flow-invariant, then $d_F(y+\delta v)/\delta\to0$ as $\delta\downarrow0$ for every $y\in F$ and $v\in X(y)$ .
Proposition (3.7). $v\in T_E(e_0)$ iff $\lim_{e\to e_0,\,e\in E}\liminf_{\delta\downarrow0} d_E(e+\delta v)/\delta=0$ .

Significance

The result. Theorem (4.4) turns a statement about all trajectories of a set-valued dynamical system into a pointwise geometric condition on $F$ 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.

Difficulty

The direction (2) $\Rightarrow$ (1) looks like a Gronwall argument for $f(t)=d_F(x(t))$ , but $d_F$ is not differentiable, $x$ is only absolutely continuous, and the closest point to $x(t)$ can jump. The step that must be controlled is the comparison between $\dot x(t)$ , a nearby admissible velocity at the closest point, and the normal $x(t)-y$ ; this is where Proposition (3.2) enters, and it is why the Clarke cone, rather than a weaker cone, is needed.

The direction (1) $\Rightarrow$ (2) needs a trajectory through an arbitrary $y\in F$ whose initial velocity is a prescribed $v\in X(y)$ . 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 " $X(x)\subseteq T_F(x)$ for all $x\in F$ " are equivalent for Lipschitz $X$ is a later, separate result and cannot be assumed.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $d_E$ is Metric.infDist · E; " $e$ is a closest point to $x$ " is e ∈ E ∧ dist x e = infDist x E.
$\partial f$ and $f^\circ$ follow Definitions (1.1) and (1.3). The gradient limits carry DifferentiableAt, because Mathlib's gradient is $0$ off the differentiability set. $f^\circ$ is a real limsup, and every theorem using it carries the §1 Lipschitz hypothesis.
$N_E$ and $T_E$ are defined from $\partial d_E$ as in (3.1) and (3.6). The tangent cone is not Mathlib's tangentConeAt.
A trajectory is x : ℝ → ℝⁿ with AbsolutelyContinuousOnInterval x 0 1 and, for almost every $t\in[0,1]$ , ∃ w ∈ X (x t), HasDerivAt x w t. Values outside $[0,1]$ are irrelevant.
Standing assumptions made explicit: $X(x)$ nonempty and compact for every $x$ (§4, p. 259); $E$ , $F$ nonempty and closed and $e\in E$ (§3, p. 254); $f$ Lipschitz on bounded sets (§1, p. 247). The Lipschitz constant of (4.2) is global.
Ruled out: dropping absolute continuity (Cantor-type curves would leave $F$ ), using 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.
Needed infrastructure: the Clarke calculus for $d_E$ , a chain-rule-type estimate for $d_F\circ x$ along absolutely continuous curves, a Gronwall lemma for absolutely continuous functions (Mathlib has 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.
The §1 definitions duplicate those of the companion mission Generalized Gradients and Applications I; the two missions were drafted at the same time.

Selected references

F. H. Clarke, Generalized gradients and applications, Trans. Amer. Math. Soc. 205 (1975), 247–262. https://doi.org/10.1090/s0002-9947-1975-0367131-6
A. F. Filippov, Classical solutions of differential equations with multivalued right-hand side, SIAM J. Control 5 (1967), 609–621. https://doi.org/10.1137/0305040
H. Brezis, On a characterization of flow-invariant sets, Comm. Pure Appl. Math. 23 (1970), 261–263. https://doi.org/10.1002/cpa.3160230211
J. M. Bony, Principe du maximum, inégalité de Harnack et unicité du problème de Cauchy pour les opérateurs elliptiques dégénérés, Ann. Inst. Fourier 19 (1969), 277–304. https://doi.org/10.5802/aif.319
R. M. Redheffer, The theorems of Bony and Brezis on flow-invariant sets, Amer. Math. Monthly 79 (1972), 740–747. MR 46 #2166.
F. H. Clarke, Yu. S. Ledyaev, R. J. Stern, P. R. Wolenski, Nonsmooth Analysis and Control Theory, Graduate Texts in Mathematics 178, Springer, 1998. https://doi.org/10.1007/b97650

16 thms3 active usersReviewed

Completed

Combinatorics Convex Optimization Discrete Geometry+1·Captain: Shuze Chen

Discrete Convex Analysis XX: Integral Convexity of L-Convex SetsTextbook

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

23 thms3 active usersReviewed

Combinatorics Convex Optimization Discrete Geometry+1·Captain: Shuze Chen

Discrete Convex Analysis XIX: Discrete Separation for M-Convex SetsTextbook

Motivation

Submodular set functions are the combinatorial stand-in for convexity: a function $\rho : 2^V \to \mathbb R$ on the subsets of a finite ground set $V$ is submodular if $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$ , 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 $B$ of $\mathbb Z^V$ 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 $\{0,1\}$ - or $\{0,-1\}$ -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.

Setting

Fix a finite ground set $V$ . A vector $x \in \mathbb Z^V$ assigns an integer $x(v)$ to each $v \in V$ ; write $x(X) = \sum_{v \in X} x(v)$ for $X \subseteq V$ . For $x, y \in \mathbb Z^V$ , the positive support $\operatorname{supp}^+(x-y) = \{v : x(v) > y(v)\}$ and negative support $\operatorname{supp}^-(x-y) = \{v : x(v) < y(v)\}$ record where $x$ exceeds, and falls short of, $y$ . A nonempty set $B \subseteq \mathbb Z^V$ is M-convex if it satisfies the exchange axiom (B-EXC[Z]): for all $x, y \in B$ and $u \in \operatorname{supp}^+(x-y)$ , some $v \in \operatorname{supp}^-(x-y)$ has both $x - \chi_u + \chi_v \in B$ and $y + \chi_u - \chi_v \in B$ , where $\chi_u$ is the characteristic vector of $u$ .

A set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ with $\rho(\emptyset) = 0$ and $\rho(V) < +\infty$ is submodular (the class $S[\mathbb R]$ , or $S[\mathbb Z]$ when integer-valued) if $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$ for all $X, Y$ . Its base polyhedron is $B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ (\forall X),\ x(V) = \rho(V)\}$ . The Lovász extension $\hat\rho : \mathbb R^V \to \mathbb R \cup \{\pm\infty\}$ linearly interpolates $\rho$ off $\{0,1\}^V$ : sorting the distinct values of $p \in \mathbb R^V$ as $\hat p_1 > \cdots > \hat p_m$ and setting $U_i = \{v : p(v) \ge \hat p_i\}$ , it is $\hat\rho(p) = \sum_{i=1}^{m-1}(\hat p_i - \hat p_{i+1})\rho(U_i) + \hat p_m \rho(U_m)$ .

Formalization targets

Goal: discrete separation for M-convex sets

B_1 \cap B_2 = \emptyset \implies \exists\, p^* \in \{0,1\}^V \cup \{0,-1\}^V,\quad \inf_{x \in B_1}\langle p^*, x\rangle - \sup_{x \in B_2}\langle p^*, x\rangle \ge 1,

for M-convex sets $B_1, B_2 \subseteq \mathbb Z^V$ (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 $|V|$ or a particular construction, so it is not invalidated by a sharper algorithm for finding $p^*$ .

Supporting structural targets

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 $B(\rho)$ (Props. 4.4-4.5), integrality of $B(\rho)$ for integer-valued $\rho$ (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).

Significance

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 $\{0,1\}^V \cup \{0,-1\}^V$ — 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).

Difficulty

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 $B_1, B_2$ , then argue the separator can be taken $\{0,1\}$ -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 $B_1, B_2$ '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 $B$ , a combinatorial exchange argument with no shortcut through general polyhedral theory.

Formalization scope

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 $B_i$ ) is exactly the book's own definition of M-convexity — no weaker substitute (e.g. requiring a specific $\rho$ witness in the hypothesis rather than deriving one, or dropping the $\{0,1\}/\{0,-1\}$ constraint on $p^*$ 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.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
J. Edmonds, "Submodular functions, matroids, and certain polyhedra," in Combinatorial Structures and Their Applications, 1970, pp. 69-87.
A. Frank, "An algorithm for submodular functions on graphs," Annals of Discrete Mathematics, 16 (1982), pp. 97-120.
L. Lovász, "Submodular functions and convexity," in Mathematical Programming: The State of the Art, Springer, 1983, pp. 235-257.

29 thms3 active usersReviewed

Convex Optimization Discrete Geometry Optimization·Captain: Shuze Chen

Discrete Convex Analysis XVIII: Integral Convexity of Minimizer SetsTextbook

Motivation

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.

Setting

For $f : \mathbb Z^n \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain $\operatorname{dom}_{\mathbb Z} f$ , the convex closure is $\bar f(x) = \sup_{p,\alpha} \{\langle p,x\rangle + \alpha : \langle p,y\rangle+\alpha \le f(y)\ \forall y \in \mathbb Z^n\}$ . The integral neighborhood of $x \in \mathbb R^n$ is $N(x) = \{y \in \mathbb Z^n : \lfloor x_i \rfloor \le y_i \le \lceil x_i \rceil\}$ , and the local convex extension $\tilde f$ replaces "for all $y \in \mathbb Z^n$ " in $\bar f$ 's definition with "for all $y \in N(x)$ ". A function is integrally convex if $\tilde f = \bar f$ everywhere on $\mathbb R^n$ . A set $S \subseteq \mathbb Z^n$ is integrally convex if its indicator function is; it is hole free if $S = \bar S \cap \mathbb Z^n$ , where $\bar S$ is the real convex hull of $S$ . The discrete Minkowski sum is $S_1+S_2 = \{x_1+x_2 : x_1 \in S_1, x_2 \in S_2\}$ . A function is separable convex if $f(x) = \sum_i f_i(x(i))$ for univariate functions $f_i$ satisfying the discrete convexity inequality $f_i(t-1)+f_i(t+1) \ge 2f_i(t)$ . For $p \in \mathbb R^n$ , $f[-p] (x) = f(x) - \langle p,x \rangle$ and $\arg\min f[-p]$ is its minimizer set.

Formalization targets

Goal (Theorem 3.29). For $f$ with nonempty bounded effective domain,

f \text{ is integrally convex} \iff \arg\min f[-p] \text{ is an integrally convex set for every } p \in \mathbb R^n.

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

Significance

Theorem 3.29 turns a statement about a function on all of $\mathbb R^n$ (integral convexity, a condition on $\tilde f$ and $\bar f$ that is a priori about uncountably many points) into a statement about a countable family of discrete sets (the minimizer sets $\arg\min f[-p]$ ), 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.

Difficulty

The naive approach to Theorem 3.29's converse direction (integral convexity of every minimizer set implies integral convexity of $f$ ) tries to check $\tilde f(x) = \bar f(x)$ directly at an arbitrary $x \in \operatorname{dom} f$ ; this is circular, since $\tilde f$ and $\bar f$ 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 $\bar f(x)$ and $\tilde f(x)$ respectively, uses LP duality's complementary slackness to show the dual optimal solution can be chosen supported inside $N(x)$ , and only then concludes $\tilde f(x) = \bar f(x)$ — routing the entire argument through the integral convexity of the specific minimizer set $S = \arg\min f[-p^*]$ at the optimal dual price $p^*$ . 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.

Formalization scope

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 $n$ , 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.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 3.
K. Murota, A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research 24 (1999), 95–105 (Lemma 6.13, cited for Proposition 3.30).

28 thms3 active usersReviewed

Completed

Dynamic Programming Optimization Probability·Captain: Shuze Chen

Markov Decision Processes VIII: Transaction Costs and the Dynamic Mean-Variance ProblemTextbook

Motivation

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 $\mu$ 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.

Setting

The transaction-cost model (§4.5): state $(x_0,x_1)\in E:=\mathbb{R}_{\ge0}^2$ (bond and stock holdings), action $a\in[0,x_1+x_0/(1+c)]$ (the stock holding chosen after the trade), bond holding after the trade $h(x_0,x_1,a) := x_0+(1-c)(x_1-a)$ if $a\le x_1$ and $x_0+(1+c)(x_1-a)$ if $a>x_1$ , for a proportional cost rate $c\in[0,1)$ ; transition $T_n((x_0,x_1),a,z) := (h(x_0,x_1,a)(1+i_{n+1}),\,az)$ ; terminal reward $U(x_0+x_1)$ for a utility $U$ homogeneous of degree $\gamma$ .

The mean-variance model (§4.6): state $E:=\mathbb{R}$ (wealth), action $A:=\mathbb{R}^d$ (amounts invested in $d$ risky assets, short-selling allowed), transition $T_n(x,a,z) := (1+i_{n+1})(x+a\cdot z)$ . Writing $X_N$ for the terminal wealth reached from $x_0$ under a strategy $\pi$ , the problem is

\mathrm{(MV)}\qquad \mathrm{Var}_{x_0}^\pi[X_N] \to \min \quad\text{subject to}\quad \mathbb{E}_{x_0}^\pi[X_N] \ge \mu, \ \ \pi \text{ admissible.}

Because $\mathrm{Var}$ is not linear in the law of $X_N$ , (MV) is solved via the Lagrangian $L_{x_0}(\pi,\lambda) := \mathrm{Var}_{x_0}^\pi[X_N] + 2\lambda(\mu-\mathbb{E}_{x_0}^\pi[X_N])$ , whose saddle points give (MV)'s value and optimizer, reduced in turn to the tractable auxiliary quadratic problem $QP(b)$ : minimize $\mathbb{E}_{x_0}^\pi[(X_N-b)^2]$ , a stochastic linear-quadratic control problem.

The mean-risk model (§4.7): the binomial (Cox–Ross–Rubinstein) market with one bond (interest rate $0$ ) and one stock with relative return $u-1$ w.p. $p$ or $d-1$ w.p. $1-p$ ; the Average-Value-at-Risk at level $\gamma$ , $\mathrm{AVaR}_\gamma(X) := \inf_{b\in\mathbb{R}} [b+\frac{1}{1-\gamma}\mathbb{E}[(X+b)^-]]$ ; the problem $\mathrm{(MR)}: \mathrm{AVaR}_\gamma(X_N)\to\min$ subject to $\mathbb{E}_{x_0}^\pi[X_N]\ge\mu$ , solved via the same Lagrangian route through an auxiliary problem $P(\lambda,b)$ .

Formalization targets

Goal — Theorem 4.6.6 (the mean-variance problem)

\mathrm{Var}_{x_0}^{\pi^*}[X_N] = \frac{d_0}{1-d_0}\big(\mathbb{E}_{x_0}^{\pi^*}[X_N] - x_0S^0_N\big)^2, \qquad \mathbb{E}_{x_0}^{\pi^*}[X_N] = \mu,

f_n^*(x) = \Big(\frac{\mu-d_0x_0S^0_N}{1-d_0}\cdot\frac{S^0_n}{S^0_N} - x\Big)\, C_{n+1}^{-1}\,\mathbb{E}[R_{n+1}],

where $(d_n)$ is a recursively-defined sequence in $(0,1)$ (Lemma 4.6.4) built from the one-period return moments $C_n,\mathbb{E}[R_n]$ . 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 $QP(b)$ 's closed-form solution (Theorem 4.6.5) at the Lagrange multiplier that Lemma 4.6.2's saddle-point argument selects.

Supporting milestones

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 $P(\lambda)$ to $QP(b)$ (Lemma 4.6.3), the boundedness of $(d_n)$ (Lemma 4.6.4), and $QP(b)$ '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 $P(\lambda,b)$ 's solution (Theorem 4.7.1), the binomial value of $P(\lambda)$ (Proposition 4.7.2), and the mean-risk problem's own explicit solution in both orderings of $p$ and $q$ (Theorems 4.7.3 and 4.7.4).

Significance

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 $F^N$ 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.

Difficulty

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: $\mathrm{Var}_{x_0}^\pi[X_N] = \mathbb{E}_{x_0}^\pi[X_N^2] - (\mathbb{E}_{x_0}^\pi[X_N])^2$ 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 $P(\lambda)$ , then a further reduction to the quadratic (and hence tractable) $QP(b)$ — 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.

Formalization scope

The financial market and the four named optimization problems (MV), (MV=), $P(\lambda)$ , $QP(b)$ 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 $\mathbb{N}\to\mathbb{R}\to(\mathrm{Fin}\ d\to \mathbb{R})$ , and values that can be $\pm\infty$ in the book (the value of $P(\lambda,b)$ , of $P(\lambda)$ , 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 $\mathrm{Var}_{x_0}^\pi[X_N]$ 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 $q^-(V_{n+1}),q^+(V_{n+1})$ 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.

Selected references

H. Markowitz, Portfolio Selection, The Journal of Finance 7(1), 1952, https://doi.org/10.2307/2975974
P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk, Mathematical Finance 9(3), 1999, https://doi.org/10.1111/1467-9965.00068
N. Bäuerle, U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011, https://doi.org/10.1007/978-3-642-18324-9, Chapter 4, §§4.5-4.7

23 thms3 active usersReviewed

Convex Optimization Discrete Geometry Optimization·Captain: Shuze Chen

Discrete Convex Analysis XVI: Substitutes and Complements in Network FlowsTextbook

Motivation

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

Setting

Let $G=(V,A)$ be a directed graph with vertex set $V$ and arc set $A$ ; write $\partial^+a$ , $\partial^-a$ for the initial and terminal vertex of arc $a$ . For a flow $\xi:A\to\mathbb R$ , its boundary is $\partial\xi(v)=\sum_{a:\partial^+a=v}\xi(a)-\sum_{a:\partial^-a=v}\xi(a)$ , the net flow leaving $v$ . Given a capacity $c:A\to\mathbb R_{\ge0}$ , $\xi$ is a feasible circulation for $c$ if $0\le\xi(a)\le c(a)$ for every arc and $\partial\xi(v)=0$ for every vertex. For a weight $w:A\to\mathbb R$ , $F(w,c)=\max\{\langle w,\xi\rangle : \xi\text{ feasible for }c\}$ is the maximum-weight circulation value, and $\xi$ is optimal for $w$ (with capacity $c$ ) if it is feasible and attains this maximum. A simple cycle is an alternating sequence of pairwise distinct vertices $v_0,\dots,v_{k-1}$ and arcs $a_1,\dots,a_k$ with $\{\partial^+a_i,\partial^-a_i\}=\{v_{i-1},v_i\}$ (indices mod $k$ ) and $v_0=v_k$ . 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 $\{0,\pm1\}$ -valued $\pi:A\to\mathbb R$ with $\partial\pi=0$ whose support forms a simple cycle. For $x\in\mathbb R^n$ , $\operatorname{supp}^+(x)=\{i:x_i>0\}$ , $\operatorname{supp}^-(x)=\{i:x_i<0\}$ . A function $g:\mathbb R^n\to\mathbb R$ is submodular if $g(p)+g(q)\ge g(p\vee q)+g(p\wedge q)$ , supermodular with the reverse inequality, and has translation submodularity (is L-natural-convex) if the stronger inequality $g(p)+g(q)\ge g((p-\alpha\mathbf1)\vee q)+g(p\wedge(q+\alpha\mathbf1))$ holds for every $\alpha\ge0$ . A function $f$ has the M-natural exchange property (is M-natural-convex) if for $i\in\operatorname{supp}^+(x-y)$ there exist $j\in \operatorname{supp}^-(x-y)\cup\{0\}$ and $\alpha_0>0$ with $f(x)+f(y)\ge f(x-\alpha(\chi_i-\chi_j))+f(y+\alpha(\chi_i-\chi_j))$ for $\alpha\in[0,\alpha_0]$ ; a function is M-natural-concave or L-natural-concave if its negation is M-natural- or L-natural-convex.

Formalization targets

Goal (Theorem 2.23). For $P$ a parallel arc set and $S$ a series arc set,

F\text{ is L-natural-convex in }w_P\text{ and M-natural-concave in }c_P,

F\text{ is M-natural-convex in }w_S\text{ and L-natural-concave in }c_S,

where $w_P$ , $c_P$ denote $F$ 's dependence on the coordinates of $w$ , $c$ indexed by $P$ (resp. $S$ ) 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 $F$ is convex in $w$ and concave in $c$ , with no combinatorial content — the baseline against which Theorem 2.23's sharper claim is measured); Theorem 2.16 (the general, possibly- $+\infty$ -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 $F$ in $w_P,c_P$ and $w_S,c_S$ , 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).

Significance

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.

Difficulty

The naive approach to Theorem 2.23 tries to verify translation submodularity or the exchange property directly from the linear-programming definition of $F$ as a maximum over a polytope, treating $w_P\mapsto F(w,c)$ 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.

Formalization scope

The graph is {V A : Type*} with src dst : A → V rather than a bundled structure, matching the book's own $\partial^+,\partial^-$ notation directly. $F(w,c)$ 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 " $\xi$ is optimal for $w$ ", 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 $F$ as a function of $w_P$ alone extends a partial vector by a fixed background vector on the complement of $P$ , 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 $|P|=1$ 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.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 2.
K. Murota, A. Shioura, "Conjugacy relationship between M-convex and L-convex functions in continuous variables," Mathematical Programming 101 (2004), 415–433.
R. T. Rockafellar, Network Flows and Monotropic Optimization, Wiley, 1984.

41 thms3 active usersReviewed

Completed

Dynamic Programming Optimization Probability·Captain: Shuze Chen

Markov Decision Processes III: Monotonicity and Convexity of the Value FunctionTextbook

Motivation

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.

Setting

Fix a (non-stationary) Markov Decision Model $(E, A, D_n, Q_n, r_n, g_N)_{n=0,\dots,N-1}$ as in Definition 2.1.1: $E$ , $A$ measurable spaces, $D_n \subseteq E \times A$ the admissible state-action pairs, $Q_n(\cdot\mid x,a)$ the transition kernel, $r_n$ the one-stage reward, $g_N$ the terminal reward. Write $D_n(x) := \{a \in A : (x,a) \in D_n\}$ . An upper bounding function $b : E \to \mathbb{R}_{\geq 0}$ (Definition 2.4.1) is a measurable function for which constants $c_r, c_g, \alpha_b \geq 0$ exist with $r_n^+(x,a) \leq c_r\, b(x)$ , $g_N^+(x) \leq c_g\, b(x)$ , and $\int b(x')\,Q_n(dx'\mid x,a) \leq \alpha_b\, b(x)$ for all admissible $(x,a)$ and all $n$ ; $\mathbb{I\!B}_b^+$ is the set of measurable $v : E \to [-\infty,\infty)$ with $v^+ \leq c\, b$ for some $c \geq 0$ . The two central operators are $(L_n v)(x,a) := r_n(x,a) + \int v(x')\,Q_n(dx'\mid x,a)$ and $(T_n v)(x) := \sup_{a \in D_n(x)} (L_n v)(x,a)$ ; a decision rule $f_n$ is a maximizer of $v$ at time $n$ if $(L_n v)(x, f_n(x)) = (T_n v)(x)$ for every $x$ . The Structure Assumption (SAN) on families $(\mathrm{I\!M}_n)_{n \leq N} \subseteq \mathrm{I\!M}(E)$ and $(\Delta_n)_{n<N}$ of decision rules says: $g_N \in \mathrm{I\!M}_N$ ; $v \in \mathrm{I\!M}_{n+1}$ implies $T_n v \in \mathrm{I\!M}_n$ ; and every $v \in \mathrm{I\!M}_{n+1}$ has a maximizer in $\Delta_n$ . 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, $E \subseteq \mathbb{R}^d$ and $A \subseteq \mathbb{R}^m$ carry the usual componentwise order, and the same spaces are given a real vector-space structure when convexity statements are in play; $\mathbb{I\!M}_n^{\diamond}$ denotes $\{v \in \mathbb{I\!B}_b^+ : v$ has property $\diamond\}$ for $\diamond \in \{\text{increasing}, \text{concave}, \text{convex}\}$ . A set $D \subseteq E \times A$ is completely monotone (Definition 2.4.15) if $(x,a'), (x',a) \in D$ with $x \leq x'$ , $a \leq a'$ forces $(x,a), (x',a') \in D$ . A function $f$ on a lattice is supermodular (Definition A.3.1) if $f(x) + f(y) \leq f(x \wedge y) + f(x \vee y)$ for all $x,y$ . The comparison theorem below additionally uses three orders between probability measures: the usual stochastic order $\mu \leq_{\mathrm{st}} \nu$ ( $\int f\,d\mu \leq \int f\,d\nu$ for every bounded increasing $f$ , Definition B.3.2/Theorem B.3.3(ii)), the convex order $\mu \leq_{\mathrm{cx}} \nu$ (same, for convex $f$ , Definition B.3.9a), and its concave-function dual $\mu \leq_{\mathrm{cv}} \nu$ (matching $\mathrm{I\!M}_n^{\mathrm{cv}}$ ; see the Formalization scope section on how the book's own, non-monotone "cv" differs from the increasing-concave order $\leq_{\mathrm{icv}}$ it also uses elsewhere, e.g. in Definition B.3.9c).

Formalization targets

Goal — Theorem 2.4.22 (the convex structure theorem)

\begin{aligned} &\text{If } E \text{ is convex}, D_n = E \times A, \text{ and for every } n: \\ &\quad\text{(ii) } x \mapsto \textstyle\int v(x')\,Q_n(dx'\mid x,a) \text{ is convex for every convex } v \in \mathbb{I\!B}_b^+, a \in A,\\ &\quad\text{(iii) } x \mapsto r_n(x,a) \text{ is convex for every } a, \quad \text{(iv) } g_N \text{ convex},\\ &\quad\text{(v) every convex } v \in \mathbb{I\!B}_b^+ \text{ has a maximizer in } \Delta_n,\\ &\text{then } \bigl(\mathrm{I\!M}_n^{\mathrm{cx}}\bigr)_{n \leq N} \text{ and } (\Delta_n)_{n<N} \text{ satisfy (SAN).} \end{aligned}

This is the weakest stable statement: it names exactly the compatibility conditions between the kernel, reward, and terminal payoff that propagate convexity through $T_n$ , 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 $L_n v$ on a completely monotone $D_n$ is itself weakly increasing (Proposition 2.4.16), the concavity-preservation step for $T_n$ 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 $A$ is a polytope (Proposition 2.4.21), and the comparison theorem for two models whose kernels are ordered (Theorem 2.4.23).

Significance

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 $D_n$ , $Q_n$ , $r_n$ , $g_N$ 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.

Difficulty

The obvious first idea for the goal is to prove convexity of $T_n v$ by convexity of a supremum of convex functions — true only when $D_n(x)$ does not itself depend on $x$ in a way that mixes domains under a convex combination. The book's own hypothesis (i), $D_n := E \times A$ (constant), is exactly what rules out the general case and makes the argument work: for a genuinely $x$ -dependent $D_n(x)$ , a convex combination $\alpha(x,a) + (1-\alpha)(x',a')$ 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 $\mathrm{I\!M}_n^{\mathrm{cv}}$ (closed under concave, not-necessarily-increasing $v$ ) as if it required the stronger increasing-concave order $\leq_{\mathrm{icv}}$ 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 $\mathrm{I\!M}_n^{\mathrm{cv}}$ as stated (see Formalization scope).

Formalization scope

Because Mathlib's ConvexOn/ConcaveOn require a Module ℝ structure on the codomain, and EReal (needed for value functions that may equal $-\infty$ ) 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 $r_n$ and $g_N$ uses Mathlib's own ConvexOn/ ConcaveOn directly. "Vertex of a polytope" (Proposition 2.4.21) is formalized via Mathlib's Set.extremePoints, and " $A$ is a polytope" as compact, convex, with finitely many extreme points. The comparison theorem's order $\leq_{\mathrm{cv}}$ has no verbatim numbered definition in the book: Appendix B.3 defines the stochastic order $\leq_{\mathrm{st}}$ (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 $\leq_{\mathrm{cx}}$ (Definition B.3.9a, directly via $\mathbb{E}f(X) \leq \mathbb{E}f(Y)$ for convex $f$ ), but never a bare " $\leq_{\mathrm{cv}}$ " — only the increasing-concave order $\leq_{\mathrm{icv}}$ (Definition B.3.9c). This mission defines $\leq_{\mathrm{cv}}$ as the direct concave-test-function analogue of $\leq_{\mathrm{cx}}$ ( $\mathbb{E}f(X) \leq \mathbb{E}f(Y)$ for every concave $f$ ), matching the book's own $\mathrm{I\!M}_n^{\mathrm{cv}}$ (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 $\leq_{\mathrm{st}}$ 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 $E \subseteq \mathbb{R}^d$ rather than real-valued random variables. The value function $V_n$ used only in the comparison theorem is given by its recursive characterization ( $V_N = g_N$ , $V_n = T_n V_{n+1}$ , 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 $E := \mathbb{R}$ throughout would make hypothesis (i) (" $E$ is convex") vacuously true and hide the genuinely restrictive role $D_n = E \times A$ plays in the proof; this mission keeps $E$ (and $A$ ) 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.

Selected references

N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. https://doi.org/10.1007/978-3-642-18324-9
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998.
A. Müller and D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002.
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete Time Case, Academic Press, 1978.

18 thms3 active usersReviewed

Completed

Optimization·Captain: mikedeng1

Cubic Regularization of Newton Method and Its Global Performance IV: Local Quadratic Convergence to a Non-degenerate MinimumResearch Paper

Motivation

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.

Setting

Let $n \ge 1$ and let $f:\mathbb{R}^n\to\mathbb{R}$ be twice differentiable, with gradient $f'(x)$ and Hessian $f''(x)$ . The Hessian is assumed Lipschitz continuous with constant $L > 0$ in the spectral norm (Assumption 1 of the paper):

\|f''(x) - f''(y)\| \le L\|x - y\| \qquad \forall x, y \in \mathbb{R}^n .

Eigenvalues of a symmetric operator are numbered decreasingly, so $\lambda_n(A)$ is the smallest eigenvalue, and $A \succ 0$ means $\lambda_n(A) > 0$ .

For $M > 0$ , the cubic model of $f$ at $x$ is

m_{M,x}(y) = \langle f'(x), y - x\rangle + \tfrac12\langle f''(x)(y - x), y - x\rangle + \tfrac M6\|y - x\|^3 ,

and the cubic-regularized Newton step $T_M(x)$ is any global minimizer of $m_{M,x}$ (Eq. (2.4)). Its length is $r_M(x) = \|x - T_M(x)\|$ .

The relaxed method (3.5) starts at $x_0$ and sets

x_{k+1} = T_{M_k}(x_k), \qquad M_k \in (0, 2L], \qquad k \ge 0 .

Unlike the globally convergent scheme (3.3), it imposes no lower bound $M_k \ge L_0 > 0$ and no acceptance test $f(x_{k+1}) \le \bar f_{M_k}(x_k)$ . The local progress measure is

\delta_k = \frac{L\,\|f'(x_k)\|}{\lambda_n^2(f''(x_k))} .

Formalization targets

Goal: Theorem 3, item 3

If $f''(x_0) \succ 0$ and $\delta_0 \le 1/4$ , the whole sequence $\{x_k\}$ converges to a point $x^*$ with $f'(x^*) = 0$ and $f''(x^*) \succ 0$ that is a local minimum of $f$ . Moreover, for every $k \ge 1$ ,

\|f'(x_k)\| \le \lambda_n^2(f''(x_0))\,\frac{9e^{3/2}}{16L}\left(\frac12\right)^{2^k}. \tag{3.8}

Milestones

Lemma 1, (2.2): $\|f'(y) - f'(x) - f''(x)(y - x)\| \le \tfrac12 L\|y - x\|^2$ .
Eq. (2.5): $f'(x) + f''(x)(T - x) + \tfrac12 M\|T - x\|(T - x) = 0$ for $T = T_M(x)$ .
Lemma 3, (2.9): $\|f'(T_M(x))\| \le \tfrac12(L + M)r_M^2(x)$ .
Eq. (3.9): if $f''(x) \succ 0$ then $r_M(x) \le \|f'(x)\|/\lambda_n(f''(x))$ .
Theorem 3, item 1, (3.6): every $\delta_k$ is well defined, and

\delta_{k+1} \le \tfrac32\Big(\frac{\delta_k}{1-\delta_k}\Big)^2 \le \tfrac83\delta_k^2 \le \tfrac23\delta_k .

Theorem 3, item 2, (3.7): $e^{-1}\lambda_n(f''(x_0)) \le \lambda_n(f''(x_k)) \le e^{3/4}\lambda_n(f''(x_0))$ for all $k \ge 0$ .

Significance

Theorem 3 shows that the cubic-regularized scheme does not lose Newton's local behaviour. Once the iterates enter the region $\{f'' \succ 0,\ \delta \le 1/4\}$ , any choice $M_k \in (0, 2L]$ 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 $\delta \le 1/4$ is reached and then adds a last phase of order $\log\log(1/\epsilon)$ 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.

Difficulty

The obvious argument treats $x_{k+1}$ as a Newton step with a small perturbation and invokes the classical Kantorovich-type analysis. That analysis assumes the regularization vanishes. Here $M_k$ can be as large as $2L$ , 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 $\delta_{k+1}$ is even defined.

The printed proof of (3.8) is not immediate from (3.6). It states $\delta_{k+1} \le \delta_k^2/(1-\delta_0)^2 \le \tfrac{16}{9}\delta_k^2$ , but (3.6) as printed only gives $\tfrac83\delta_k^2$ , which is too weak for the constant $\tfrac{9}{16}(\tfrac12)^{2^k}$ . A proof of (3.8) as stated cannot rest on (3.6) alone.

Formalization scope

Space. $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$ . 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.
Domain. The paper works on a closed convex set $F$ . Because method (3.5) has no descent test that keeps the iterates inside a smaller set, this mission takes $F = \mathbb{R}^n$ : $f$ is twice differentiable and Assumption 1 holds on all of $\mathbb{R}^n$ . Lemma 3's hypothesis $T_M(x) \in F$ is then automatic.
The step. $T_M(x)$ is represented by an arbitrary global minimizer of the cubic model (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.
Eigenvalues. $\lambda_n(A)$ is lamMin A, the infimum of $\langle Av, v\rangle$ over the unit sphere. It equals the smallest eigenvalue for self-adjoint $A$ , and $f''(x) \succ 0$ is 0 < lamMin (H x).
Indices. The index is 0-based and $x_0$ is x 0. The ranges are as printed: $k \ge 0$ in (3.6)–(3.7) and $k \ge 1$ in (3.8). "Converges quadratically" is rendered by the paper's own quantitative clause (3.8), together with existence of the limit, $f'(x^*) = 0$ , $\lambda_n(f''(x^*)) > 0$ and IsLocalMin f x*.
Constants. All constants ( $\tfrac14$ , $\tfrac32$ , $\tfrac83$ , $\tfrac23$ , $e^{-1}$ , $e^{3/4}$ , $\tfrac{9e^{3/2}}{16L}$ ) are the printed ones.

The theorem assumes positivity of the Hessian and $\delta \le 1/4$ only at $x_0$ . A formalization that assumes $f$ strongly convex, $f''(x) \succ 0$ everywhere, or $\delta_k \le 1/4$ for all $k$ , or that imports the lower bound $L_0$ 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 $C^1$ cubic model, perturbation bounds for lamMin under operator-norm changes, and the inverse bound $\|(A + cI)^{-1}\| \le 1/(\lambda_n(A) + c)$ . These are reusable well beyond this mission. Contributions welcome: proofs of the milestones, and a proof of (3.8) with the printed constant.

Selected references

Yu. Nesterov and B. T. Polyak, Cubic regularization of Newton method and its global performance, Math. Program., Ser. A 108 (2006) 177–205. https://doi.org/10.1007/s10107-006-0706-8
C. Cartis, N. I. M. Gould and Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Math. Program. 127 (2011) 245–295. https://doi.org/10.1007/s10107-009-0286-5

12 thms3 active usersReviewed

Completed

Combinatorics Complexity Theory Optimization+2·Captain: mikedeng1

Maximizing Non-Monotone Submodular Functions V: Beating 1/2 for Symmetric Functions Requires Exponentially Many Value QueriesResearch Paper

Motivation

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 $f(S)$ of the sets $S$ 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 $\tfrac12$ 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 $\tfrac12$ 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:

2007 (FOCS) / 2011 (SIAM J. Comput.): Feige, Mirrokni and Vondrák prove that no algorithm with subexponentially many value queries achieves $(\tfrac12 + \epsilon)$ of the optimum on symmetric nonnegative submodular functions, and give $\tfrac25$ for general functions.
2011: Vondrák's symmetry-gap framework (SIAM J. Comput. 42(1), 2013) generalizes the construction to constrained problems.
2012: Buchbinder, Feldman, Naor and Schwartz give a randomized $\tfrac12$ -approximation for general nonnegative submodular functions, matching the bound.

Setting

Let $[n] = \{0, \dots, n-1\}$ be the ground set, with $n$ even. A set function $f : 2^{[n]} \to \mathbb{R}$ is submodular if $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$ for all $S, T$ , symmetric if $f([n]\setminus S) = f(S)$ for all $S$ , and $\mathrm{OPT}(f) = \max_{S} f(S)$ .

Fix an integer $m$ with $1 \le m \le n/2$ and write $\epsilon = m/n$ , so that $\epsilon n$ is an integer. For integers $k, \ell$ put

f(k,\ell) = \begin{cases} (k+\ell)(n-k-\ell) & |k-\ell| \le m,\\ k(n-2\ell) + (n-2k)\ell + m^2 - 2m|k-\ell| & |k-\ell| > m. \end{cases}

For a set $C \subseteq [n]$ with $|C| = n/2$ and $D = [n] \setminus C$ , the hard instance is $f_C(S) = f(|S\cap C|, |S\cap D|)$ . The cut function of the complete graph is $g(S) = |S|(n-|S|)$ , with maximum $\tfrac14 n^2$ . A set $Q$ is balanced for $C$ if $\bigl||Q\cap C| - |Q\cap D|\bigr| \le m$ ; on balanced sets $f_C = g$ .

A deterministic adaptive $q$ -query algorithm $A$ chooses each query from the answers received so far, and after $q$ answers outputs a set $A(h)$ when run against an oracle $h$ . A randomized algorithm is a distribution $\mu$ over deterministic ones, with expected value $\mathbb{E}_{A\sim\mu}[h(A(h))]$ .

Formalization targets

Goal: Theorem 4.5 with the constants of its proof

For every such $n, m$ :

every $f_C$ with $|C| = n/2$ is nonnegative, symmetric and submodular, with

\mathrm{OPT}(f_C) = \tfrac12 n^2 (1 - 2\epsilon + 2\epsilon^2);

for every $q < e^{\epsilon^2 n/8}$ and every randomized $q$ -query algorithm $\mu$ there is a $C$ with $|C| = n/2$ and

\mathbb{E}_{A\sim\mu}\bigl[f_C(A(f_C))\bigr] \le \tfrac14 n^2 + \bigl(2e^{-\epsilon^2 n/8} + 2e^{-\epsilon^2 n/4}\bigr)\,\mathrm{OPT}(f_C).

Hence the ratio attained is at most $\frac{1}{2(1-2\epsilon+2\epsilon^2)} + 4e^{-\epsilon^2 n/8} = \tfrac12 + \epsilon + O(\epsilon^2) + 4e^{-\epsilon^2 n/8}$ .

Milestones

Theorem 1.2, the Chernoff bound for independent variables in $[-1,1]$ .
Submodularity of $f_C$ .
The value $\mathrm{OPT}(f_C) = \tfrac12 n^2(1 - 2\epsilon + 2\epsilon^2)$ , attained at $S = C$ .
A fixed query is unbalanced for at most a $2e^{-\epsilon^2 n/4}$ fraction of the half-size sets $C$ .
If all queries are balanced, the algorithm cannot distinguish $f_C$ from $g$ .
The deterministic case of the bound, averaged over $C$ .

Significance

The theorem shows that the factor $\tfrac12$ 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 $\tfrac12$ -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 $O(\cdot)$ terms.

Difficulty

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 $C$ the count $|Q\cap C|$ 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 $|C| \ne n/2$ 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 $f_C$ of its output, which equals $g$ of the output only if the output is balanced as well. That event has to be controlled too.

Finally, submodularity of $f_C$ must be checked across the boundary $|k-\ell| = \epsilon n$ between the two regimes, where the formula changes.

Formalization scope

The ground set is Fin n with $n$ even; $\epsilon n$ is an integer $m$ with $1 \le m$ and $2m \le n$ , following the paper's "assume that $\epsilon n$ is an integer". Sets are Finset (Fin n), and all values are real.
$\mathrm{OPT}$ is Finset.sup' over all subsets. There is no junk value.
The partition $(C, D)$ is uniform over half-size sets; probabilities over it are counts of n/2-subsets divided by $\binom{n}{n/2}$ , written multiplied out.
A deterministic algorithm is a pair of decision rules query, output : List ℝ → Finset (Fin n) making exactly $q$ 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 $f$ only through query answers; it never receives $C$ .
Pinned-down constants. The printed theorem, "fewer than $e^{\epsilon^2 n/8}$ queries" and "expected value at least $(\tfrac12+\epsilon)\mathrm{OPT}$ ", is not what the proof gives for one and the same $\epsilon$ . On the proof's instances $\mathrm{OPT} = \tfrac12 n^2(1-2\epsilon+2\epsilon^2)$ , and the ratio held is $\frac{1}{2(1-2\epsilon+2\epsilon^2)} > \tfrac12 + \epsilon$ . The formal goal states the explicit bound the proof establishes. The literal printed pair, stated for the proof's family with the same $\epsilon$ , is false: the zero-query algorithm that outputs a fixed half-size set gets at least $\tfrac14 n^2 > (\tfrac12+\epsilon)\mathrm{OPT}$ .
Added term. The error term $2e^{-\epsilon^2 n/4}$ for the output set is added to the paper's $2e^{-\epsilon^2 n/8}$ .
Ruled-out trivializations. A restricted algorithm class (non-adaptive, deterministic, or one that must return a queried set) would give a different, weaker theorem. So would a bound that lets the algorithm read $C$ , which would make the statement false. Both the instance's properties (nonnegativity, symmetry, submodularity, the value of OPT) and the bound are part of the goal, so an empty or degenerate family cannot satisfy it. The quantifier order is: for every algorithm there is an instance.
Needed infrastructure: a value-oracle algorithm model; tail bounds for the hypergeometric distribution (Hoeffding's inequality for sampling without replacement), which Mathlib lacks; averaging over a 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.

Selected references

U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
N. Alon, J. H. Spencer, The Probabilistic Method, Wiley (source of Theorem 1.2).
W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, J. Amer. Statist. Assoc. 58(301):13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830
J. Vondrák, Symmetry and Approximability of Submodular Maximization Problems, SIAM J. Comput. 42(1):265–304, 2013. https://doi.org/10.1137/110832318
N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

12 thms3 active usersReviewed

Completed

Combinatorics Convex Optimization Discrete Geometry+1·Captain: mikedeng1

Lifts of Convex Sets and Cone Factorizations II: Antichain and Face-Count Lower Bounds on the Nonnegative Rank of a PolytopeResearch Paper

Motivation

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 $n_C$ faces needs a lift with at least $\log_2 n_C$ 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.

Setting

Write $\mathbb{R}^n$ for Euclidean space with inner product $\langle\cdot,\cdot\rangle$ . A polytope $C \subseteq \mathbb{R}^n$ is the convex hull of finitely many points; as throughout the paper, the origin is assumed to lie in its interior. The polar of $C$ is

C^\circ = \{\, y \in \mathbb{R}^n : \langle x, y\rangle \le 1 \text{ for all } x \in C \,\}.

Let $\operatorname{ext}(C)$ be the set of extreme points of $C$ (its vertices). The slack operator $S_C$ is the function $S_C(x, y) = 1 - \langle x, y\rangle$ on $\operatorname{ext}(C) \times \operatorname{ext}(C^\circ)$ . The extreme points of $C^\circ$ correspond to the facets of $C$ , the facet of $y$ being $\{x \in C : \langle x, y\rangle = 1\}$ , so $S_C$ is the canonical vertex–facet slack matrix of $C$ and is nonnegative.

An $\mathbb{R}^k_+$ -factorization of $S_C$ consists of maps $A : \operatorname{ext}(C) \to \mathbb{R}^k_+$ and $B : \operatorname{ext}(C^\circ) \to \mathbb{R}^k_+$ with $S_C(x, y) = \langle A(x), B(y)\rangle$ . The nonnegative rank $\operatorname{rank}_+(C)$ is the least such $k$ , and $+\infty$ if there is none.

The support $\operatorname{supp}(S_C)$ is the $0/1$ matrix with a one where $S_C(x,y) \ne 0$ . A Boolean factorization of it of intermediate dimension $k$ assigns subsets $A(x), B(y) \subseteq [k] = \{1,\dots,k\}$ with $S_C(x,y) \ne 0 \iff A(x) \cap B(y) \ne \emptyset$ ; the least such $k$ is the Boolean rank.

A face of $C$ is the empty set or a set of maximizers in $C$ of a linear functional; $C$ itself is a face. The face lattice $L(C)$ is the set of faces ordered by inclusion, and the Boolean lattice $2^{[k]}$ is the set of subsets of $[k]$ ordered by inclusion. An embedding $\varphi : L(C) \to 2^{[k]}$ satisfies $H \subseteq F \iff \varphi(H) \subseteq \varphi(F)$ .

Formalization targets

Goal: Corollary 4.13 (p. 16)

For a polytope $C$ :

\text{(1)}\quad \operatorname{rank}_+(C) \ \ge\ \min\Big\{ k : p \le \tbinom{k}{\lfloor k/2 \rfloor} \Big\}

for every antichain of $p$ faces of $C$ (no face contained in another), and

\text{(2)}\quad \operatorname{rank}_+(C) \ \ge\ \log_2 n_C ,

where $n_C$ is the number of faces of $C$ , including $\emptyset$ and $C$ .

Milestones

§4.2, p. 15. For a nonnegative matrix $M$ , $\operatorname{rank}_B(M) \le \operatorname{rank}_+(M)$ : a nonnegative factorization of intermediate dimension $k$ yields a Boolean factorization of $\operatorname{supp}(M)$ of the same dimension.
Theorem 4.11, p. 15. $\operatorname{supp}(S_C)$ has a Boolean factorization of intermediate dimension $k$ if and only if $L(C)$ embeds into $2^{[k]}$ .
Corollary 4.12, p. 15. $\operatorname{rank}_+(C) \ge \min\{k : L(C) \text{ embeds into } 2^{[k]}\}$ .

Significance

Both bounds depend only on the combinatorial type of the polytope. For a square they give $\operatorname{rank}_+ \ge \log_2 10 \approx 3.32$ and $\operatorname{rank}_+ \ge 4$ ; for a three-dimensional cube $\log_2 28 \approx 4.81$ and $6$ (p. 16). For the regular $n$ -gon, whose slack matrices all have rank $3$ , the face-count bound gives $\operatorname{rank}_+ \ge \log_2 n$ , 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.

Difficulty

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 $L(C)$ into $2^{[k]}$ 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 $\operatorname{ext}(C^\circ)$ . 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.

Formalization scope

$\mathbb{R}^n$ 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; $n = 0$ is allowed ( $C = \{0\}$ ), and all targets hold there. Faces are Mathlib's exposed faces (IsExposed ℝ C F), which include $\emptyset$ and $C$ , as the paper's counts do; for a polytope these are all faces. The factorization maps are total functions on $\mathbb{R}^n$ constrained only on extreme points. The nonnegative rank is valued in ℕ∞, the infimum of the empty family being $+\infty$ ; 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 $k$ " is sInf of a set of naturals that is nonempty in each case (the set of $k$ with $p \le \binom{k}{\lfloor k/2\rfloor}$ , and the set of $k$ admitting an embedding of the finite lattice $L(C)$ ).

The paper says "lattice embedding". Its proof of Theorem 4.11 constructs, and uses, only a map that preserves and reflects inclusion, and $\varphi(F) = \bigcup_{v \in F} A(v)$ 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 $0$ when no factorization exists); faces are not arbitrary subsets of $C$ ; and an embedding is order-reflecting, not merely monotone (every poset maps monotonically into $2^{[0]}$ ).

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.

Selected references

J. Gouveia, P. A. Parrilo, R. R. Thomas, Lifts of Convex Sets and Cone Factorizations, Math. Oper. Res. 38(2):248–264, 2013; arXiv:1111.3164v2. https://arxiv.org/abs/1111.3164
M. Yannakakis, Expressing combinatorial optimization problems by linear programs, J. Comput. System Sci. 43(3):441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
M. X. Goemans, Smallest compact formulation for the permutahedron, Math. Program. 153:5–11, 2015. https://doi.org/10.1007/s10107-014-0757-1
S. Fiorini, V. Kaibel, K. Pashkovich, D. O. Theis, Combinatorial bounds on nonnegative rank and extended formulations, Discrete Math. 313(1):67–83, 2013; arXiv:1111.0444. https://arxiv.org/abs/1111.0444
S. A. Vavasis, On the complexity of nonnegative matrix factorization, SIAM J. Optim. 20(3):1364–1377, 2009. https://doi.org/10.1137/070709967

10 thms3 active usersReviewed

Completed

Combinatorics Optimization Probability+1·Captain: mikedeng1

Maximizing Non-Monotone Submodular Functions IV: Smooth Local Search Achieves 2/5 of the OptimumResearch Paper

Motivation

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 $1 - 1/e$ , 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 $f(S)$ for a queried set $S$ .

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 $1/4$ of the optimum, a deterministic local search achieves $1/3 - \epsilon/n$ , and a randomized smooth local search achieves $2/5 - o(1)$ . 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: $1/4$ , $1/3$ and $2/5$ (FOCS 2007; journal version 2011). Gharan and Vondrák (SODA 2011): about $0.41$ by simulated annealing. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015): a randomized double greedy algorithm achieving $1/2$ , which matches the $1/2$ hardness in the value oracle model proved in the same paper by Feige, Mirrokni and Vondrák.

Setting

Let $X$ be a finite ground set with $n = |X| \ge 1$ elements and $f : 2^X \to \mathbb{R}$ a function with $f(S) \ge 0$ for all $S$ and

f(S \cup T) + f(S \cap T) \le f(S) + f(T) \quad (S, T \subseteq X).

Write $OPT = \max_{S \subseteq X} f(S)$ . The multilinear extension of $f$ is

F(x) = \sum_{S \subseteq X} f(S) \prod_{i \in S} x_i \prod_{j \notin S} (1 - x_j),

the expected value of $f$ on a random set containing each $i$ independently with probability $x_i$ .

For $A \subseteq X$ and $\delta \in [-1,1]$ , the random set $\mathcal{R}(A,\delta)$ is sampled with bias $\delta$ based on $A$ : each element of $A$ is included independently with probability $p = (1+\delta)/2$ , each element of $B = X \setminus A$ with probability $q = (1-\delta)/2$ . The potential is $\Phi(A) = \mathbf{E}[f(\mathcal{R}(A,\delta))]$ and the smoothed marginal value of $x$ is

\omega_{A,\delta}(x) = \mathbf{E}[f(\mathcal{R}(A,\delta) \cup \{x\})] - \mathbf{E}[f(\mathcal{R}(A,\delta) \setminus \{x\})].

Algorithm SLS starts from $A = \emptyset$ . At each iteration it obtains estimates $\tilde\omega_{A,\delta}(x)$ within $\pm\frac{1}{n^2}OPT$ of $\omega_{A,\delta}(x)$ . If some $x \notin A$ has $\tilde\omega_{A,\delta}(x) > \frac{2}{n^2}OPT$ it adds $x$ ; otherwise, if some $x \in A$ has $\tilde\omega_{A,\delta}(x) < -\frac{2}{n^2}OPT$ it removes $x$ ; otherwise it stops and returns a random set $\mathcal{R}(A, \delta')$ .

Formalization targets

Goal: Theorem 3.6 in the explicit form of its proof

With $\delta = 1/3$ , and $\delta' = 1/3$ with probability $0.9$ or $\delta' = -1$ with probability $0.1$ : for every run from $\emptyset$ whose estimates are all accurate and which has terminated at $A$ ,

\tfrac{9}{10}\,\mathbf{E}[f(\mathcal{R}(A,\tfrac13))] + \tfrac{1}{10}\,f(X \setminus A) \ge \Big(\frac{2}{5} - \frac{9}{5n}\Big) OPT,

and, for every $\delta \in (0,1]$ , every run of $k$ iterations with accurate estimates has $k < n^2/\delta$ (fewer than $3n^2$ for $\delta = 1/3$ ).

Milestones, in attack order

Lemma 2.2: $\mathbf{E}[g(A(p))] \ge (1-p)g(\emptyset) + p\,g(A)$ .
Display (∗): for three independently sampled sets, $\mathbf{E}[f(A_1(p_1) \cup A_2(p_2) \cup A_3(p_3))] \ge \sum_{I \subseteq \{1,2,3\}} \prod_{i\in I} p_i \prod_{i \notin I}(1-p_i) f(\bigcup_{i \in I} A_i)$ .
The increment identity $\Phi(A \cup \{x\}) - \Phi(A) = \delta\,\omega_{A,\delta}(x)$ for $x \notin A$ , and its removal counterpart.
$0 \le \Phi(A) \le OPT$ .
The terminal upper estimates $\mathbf{E}[f(R \cup (B\cap C))],\ \mathbf{E}[f(R \cap (B \cup C))] \le \mathbf{E}[f(R)] + \frac{2}{n}OPT$ .
The two lower bounds in $27$ ths on the same two expectations.
The final chain $\mathbf{E}[f(R)] + \frac19 f(B) + \frac2n OPT \ge \frac49 OPT$ .

Significance

The $2/5$ 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 $1/2$ . 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 $o(1)$ as $\frac{9}{5n}$ , "polynomial time" as $n^2/\delta$ iterations, and the dependence on the accuracy of the sampled estimates as an explicit hypothesis.

Difficulty

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 $R$ is random, so the comparison with the optimal set $C$ cannot be made through a single local-optimality inequality as in deterministic local search; and approximate local optimality holds only for the smoothed marginals $\omega_{A,\delta}$ , which are averages over the random set, not for $f$ 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 $\delta = 1/3$ the $27$ ths add up so that the $\frac{9}{10}/\frac{1}{10}$ mixture yields $2/5$ . A different split or a different $\delta$ gives a different constant.

Formalization scope

The ground set is a Fintype X with decidable equality; sets are Finset X; $f$ is real valued, with nonnegativity and submodularity as hypotheses. The standing assumptions of the paper are made explicit: $f \ge 0$ (§3), value-oracle access (modelled by $f$ itself), $n = |X|$ , and $n \ge 1$ (Nonempty X), so that $\frac{1}{n^2}$ and $\frac{9}{5n}$ are not Lean's junk value of division by zero. $OPT$ 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 $\mathcal{R}(A,\delta)$ , and iterated sums over subsets for the several independent samples in Lemma 2.2 and (∗). Sampling probabilities carry $0 \le p \le 1$ .

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 $\emptyset$ , every choice of accurate estimates, recomputed at every iteration, and every termination point. Accuracy is non-strict ("within $\pm$ "); the thresholds are strict. The thresholds and accuracy use $OPT$ itself, as the proof does, although step 1 of the algorithm says an estimate of $OPT$ 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 $\delta' = -1$ branch is written as $\mathbf{E}[f(\mathcal{R}(A,-1))]$ , which equals $f(X \setminus A)$ .

A statement "every $A$ satisfying the terminal conditions gives $2/5 - 9/(5n)$ " would be the final milestone plus arithmetic and is not the goal. The goal fixes the start at $\emptyset$ , the thresholds, the step order, the accuracy of every estimate, termination and the $0.9/0.1$ mixture.

A complete development needs basic calculus of the multilinear extension: affinity in one coordinate, translation $f(\cdot \cup D)$ and restriction $f(\cdot \cap D)$ , 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 $\delta = \delta'$ (proof omitted in the paper), the tight example and the hardness results of §4 are out of scope.

Selected references

U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
S. O. Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011. https://doi.org/10.1137/1.9781611973082.83
N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205
G. Calinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a Monotone Submodular Function Subject to a Matroid Constraint, SIAM J. Comput. 40(6):1740–1766, 2011. https://doi.org/10.1137/080733991

14 thms3 active usersReviewed

Completed

Dynamic Programming Optimization Probability·Captain: Shuze Chen

Markov Decision Processes I: Markov Decision Models and the Bellman EquationTextbook

Motivation

A Markov Decision Model (MDM) formalizes sequential decision-making under uncertainty: a controller observes the current state of a system, chooses an action, receives a reward, and the system moves to a new (random) state whose law depends on the current state and action. This framework underlies dynamic programming across operations research, economics, and engineering — inventory control, sequential portfolio choice, queueing control, and reinforcement learning are all instances of it. The finite-horizon theory developed here is the foundation on which every later chapter of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) builds, including the infinite-horizon, partially observed, and optimal-stopping variants treated later in the book.

The classical treatment of dynamic programming for finite state and action spaces goes back to Bellman (1957) and is standard textbook material (see e.g. Puterman, Markov Decision Processes, 1994). The generalization to Borel state and action spaces — needed as soon as a state variable is continuous, as in almost every financial application — requires genuine measure-theoretic care: suprema over an infinite (even uncountable) action set need not be attained, and the resulting value function need not be measurable. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete Time Case (1978) is the classical reference for this general theory; Bäuerle and Rieder's treatment isolates the exact abstract hypothesis — the Structure Assumption (SAN) below — under which the finite-horizon theory goes through cleanly, separating the recursive (Bellman) machinery from the case-by-case verification of when it applies.

Setting

A Markov Decision Model with planning horizon $N \in \mathbb{N}$ consists of a state space $E$ and action space $A$ (measurable spaces), and, for each stage $n = 0,\dots,N-1$ : a measurable set $D_n \subseteq E \times A$ of admissible state-action pairs (containing the graph of some measurable selection $E \to A$ ); a stochastic transition kernel $Q_n(\cdot \mid x,a)$ giving the law of the next state; a measurable one-stage reward $r_n : D_n \to \mathbb{R}$ ; and a terminal reward $g_N : E \to \mathbb{R}$ .

A decision rule at time $n$ is a measurable $f_n : E \to A$ with $f_n(x) \in D_n(x) := \{a : (x,a) \in D_n\}$ for every $x$ ; an $N$ -stage policy $\pi = (f_0,\dots,f_{N-1})$ is a sequence of such rules. Given $\pi$ and an initial state $x$ at time $n$ , the process evolves as a (non-stationary) Markov chain, and the value of $\pi$ is the expected total reward

V_n^\pi(x) := \mathbb{E}^\pi_{n,x}\!\left[\sum_{k=n}^{N-1} r_k\bigl(X_k, f_k(X_k)\bigr) + g_N(X_N)\right],

with value function $V_n(x) := \sup_\pi V_n^\pi(x)$ , the best attainable expected reward. A policy is optimal if $V_0^\pi = V_0$ . Write $\mathrm{IM}(E)$ for the measurable functions $E \to [-\infty,\infty)$ (never $+\infty$ ), and define, for $v \in \mathrm{IM}(E)$ , the one-step operators $L_n v(x,a) := r_n(x,a) + \int v(x')\, Q_n(dx' \mid x,a)$ , $T_n^f v(x) := L_n v(x, f(x))$ , and $T_n v(x) := \sup_{a \in D_n(x)} L_n v(x,a)$ . A decision rule $f$ is a maximizer of $v$ at time $n$ if $T_n^f v = T_n v$ .

Formalization targets

Goal: Theorem 2.3.8 (the Structure Theorem)

Under the Structure Assumption (SAN) — the existence of sets $\mathrm{IM}_n \subseteq \mathrm{IM}(E)$ , $\Delta_n \subseteq F_n$ with $g_N \in \mathrm{IM}_N$ , $T_n$ mapping $\mathrm{IM}_{n+1}$ into $\mathrm{IM}_n$ , and every $v \in \mathrm{IM}_{n+1}$ admitting a maximizer in $\Delta_n$ — the value function satisfies the Bellman equation $V_n = T_n V_{n+1}$ (with $V_n \in \mathrm{IM}_n$ ), and every sequence of maximizers of $V_1,\dots,V_N$ defines an optimal policy. This is the weakest level at which the theorem holds: it names an abstract structural hypothesis rather than a specific sufficient condition (e.g. compactness plus semicontinuity, treated in a later mission), so any future refinement of sufficient conditions for (SAN) leaves this statement untouched.

Significance

Reducing an $N$ -stage optimization over an infinite-dimensional policy space to $N$ one-stage optimizations — literally the content of the Bellman equation — is what makes dynamic programming computationally and theoretically tractable at all. For finite state and action spaces this reduction is elementary (a supremum over a finite set is always attained); the content of the Structure Theorem is doing this correctly when $E$ , $A$ are general Borel spaces, where existence of the supremum and of a measurable maximizing selection are not automatic and must be assumed abstractly.

Formalizing this theorem produces machine-checked statements of the finite-horizon Bellman equation and verification theorem in the generality actually used throughout the book's finance applications (wealth is real-valued, portfolios are vector-valued — never finite sets). The statement, proof, and every hypothesis are original to this textbook chapter; no formalized version of this general-Borel-space theory exists on the platform. The closest prior art, finite state-and-action-space Bellman equations and verification theorems (e.g. discounted infinite-horizon and stochastic-shortest-path theorems for finite MDPs), is a strictly weaker special case in which the Structure Assumption's existence-of-maximizer clause is automatic; this mission's goal is not restated as a reference to that prior art; the generalization is exactly the mission's content.

Difficulty

The obvious first attempt — prove $V_n = T_n V_{n+1}$ directly from the definitions of $V_n$ and $V_n^\pi$ — runs into two separate obstructions that (SAN) is built to bypass simultaneously. First, $\sup_\pi V_n^\pi(x)$ and $\sup_{a \in D_n(x)} L_n V_{n+1}(x,a)$ are a priori different suprema (over policies versus over actions), and showing they agree requires that the pointwise supremum over decision rules $f \in F_n$ of $L_n V_{n+1}(x, f(x))$ equals the supremum over bare actions $a \in D_n(x)$ — which needs a measurable selection achieving (or approaching) the action-wise optimum, not just its existence pointwise. Second, $V_{n+1}$ itself must be shown measurable — an a priori supremum of measurable functions over an uncountable index set (all policies) need not be measurable — before the integral $\int V_{n+1}\, dQ_n$ even makes sense. (SAN)'s three clauses are exactly what supplies both a well-behaved measurability class $\mathrm{IM}_n$ closed under $T_n$ and a measurable maximizing selection at every stage, letting a backward induction on $n$ establish both facts together.

Formalization scope

State and action spaces are arbitrary measurable spaces (MeasurableSpace E, MeasurableSpace A type classes), not restricted to Borel subsets of Polish spaces, since none of this mission's statements use topology. Time is indexed by ℕ rather than Fin N, with n < N as an explicit side condition throughout (documented in MODERATION_NOTES.md); this changes no content but avoids Fin-cast noise in the several backward recursions the chapter's operators require. Extended-real values (EReal) are used throughout for value functions, restricted by hypothesis to never equal $+\infty$ , matching $\mathrm{IM}(E) := \{v : E \to [-\infty,\infty)\}$ exactly; a formalization using plain ℝ-valued value functions would be a strictly stronger — and unfaithful — claim, since it silently assumes no policy can drive the expected reward to $-\infty$ .

The mission does not construct the canonical path measure on the full trajectory space via the Ionescu–Tulcea theorem; the value of a policy is instead built as an explicit backward accumulator recursion over the model's one-step kernels, which computes the same quantity by the tower property of conditional expectation. Definitions 2.1.1, 2.1.5, 2.2.2, 2.3.1, and 2.3.6 — the Markov Decision Model, (Markov and history-dependent) policies, and the operators — are restated from scratch in this mission's own namespace, since drafts in this series cannot import one another; later missions in the same series restate the same vocabulary independently. A trivializing formalization of the goal would state $V_n$ as an unspecified object merely postulated to satisfy the Bellman equation (Theorem 2.3.7's weaker claim) rather than as the supremum-over-policies value function fixed before the theorem — this mission states the latter.

Selected references

N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete Time Case, Academic Press, 1978.
K. Hinderer, Foundations of Non-stationary Dynamical Programming with Discrete Time Parameter, Lecture Notes in Operations Research and Mathematical Systems 33, Springer, 1970.
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994.

13 thms3 active usersReviewed

Completed

Algorithmic Game Theory·Captain: mikedeng1

Monotonic Solutions of Cooperative Games 1: For Five or More Players No Core Allocation Rule Is Coalitionally MonotonicResearch Paper

Motivation

Cooperative games model the division of a jointly produced surplus, or a jointly incurred cost, among the participants of an enterprise: towns sharing a water supply system, divisions of a firm sharing overhead, members of a consortium sharing the savings of joint investment. In such applications allocations are rarely fixed once and for all. Costs and revenues are re-estimated, projects are re-scoped, and the allocation is recomputed. A natural requirement on any allocation method is then monotonicity: when the underlying data change in a player's favour, that player's share should not fall.

H. P. Young, Monotonic Solutions of Cooperative Games (Int. J. Game Theory 14, 1985), studies several forms of this principle. The weakest, aggregate monotonicity, asks that no player lose when only the value of the grand coalition increases; Megiddo (1974) had already shown that the nucleolus violates it. The paper's first theorem concerns a stronger and more natural form, coalitional monotonicity, which was first proposed by Shubik (1962) in the context of cost allocation within a firm, and shows that it cannot be reconciled with the core, the most widely used stability requirement. This mission formalizes that impossibility theorem.

Setting

Fix $n$ players, $N = \{1, 2, \dots, n\}$ . A cooperative game on $N$ is a function $v$ assigning a real number $v(S)$ to every coalition $S \subseteq N$ , with $v(\emptyset) = 0$ . No superadditivity or other structural assumption is imposed.

An allocation procedure is a map $\varphi$ that assigns to every game $v$ on $N$ an allocation $\varphi(v) = (\varphi_1(v), \dots, \varphi_n(v)) \in \mathbb{R}^N$ satisfying efficiency:

\sum_{i \in N} \varphi_i(v) = v(N).

The core of $v$ is the set of allocations that no coalition can improve upon on its own:

C(v) = \Big\{x \in \mathbb{R}^N : \sum_{i \in S} x_i \ge v(S) \text{ for all } S \subseteq N,\ \sum_{i \in N} x_i = v(N)\Big\}.

It may be empty. An allocation procedure is a core allocation rule if $\varphi(v) \in C(v)$ for every game $v$ whose core is nonempty. The nucleolus is the standard example.

An allocation procedure is coalitionally monotonic (Eq. (4) of the paper) if raising the value of a single coalition, with all other values unchanged, never decreases the allocation of any member of that coalition: for all games $v, w$ and every coalition $T \subseteq N$ ,

v(T) \ge w(T),\ \ v(S) = w(S)\ \ \forall S \ne T \ \Longrightarrow\ \varphi_i(v) \ge \varphi_i(w)\ \ \forall i \in T.

The paper notes that this is equivalent to its one-player form (5): if every coalition containing player $i$ weakly gains in value and every coalition not containing $i$ is unchanged, then $\varphi_i$ does not decrease.

In the Lean development these objects are Game n, IsAllocationProcedure, IsCoreRule and IsCoalitionallyMonotonic in the namespace MonotonicSolutions.CoreRules, and the core is the published definition Supermodularity.Cooperative.Core.

Formalization targets

Goal: Theorem 1

For every $n \ge 5$ ,

\neg\,\exists\,\varphi \ :\ \varphi \text{ is an allocation procedure on } N=\{1,\dots,n\},\ \varphi \text{ is a core allocation rule, and } \varphi \text{ is coalitionally monotonic}.

Milestones

Eqs. (4)–(5). Coalitional monotonicity is equivalent to the one-player condition (5).
The core of the game $w$ . For the explicit five-player game $w$ of the proof, built from the coalitions $S_1 = \{3,5\}$ , $S_2=\{1,2,3\}$ , $S_3=\{1,3,4\}$ , $S_4=\{2,4,5\}$ , $S_5=\{1,2,4,5\}$ with values $3,3,9,9,9$ and $w(N) = 11$ , the core is the single point $(0,1,2,7,1)$ .
The core of the game $v$ . For the game $v$ equal to $w$ except $v(S_5) = v(N) = 12$ , the core is the single point $(3,0,0,6,3)$ .
The case $|N| = 5$ . The goal with $n = 5$ .

An additional statement records the paper's remark that the egalitarian rule $\varphi_i(v) = v(N)/|N|$ satisfies (5), so that the monotonicity axiom on its own is satisfiable.

Significance

The theorem shows that no refinement of the core, however cleverly designed, can be coalitionally monotonic once there are five or more players. For the nucleolus this strengthens Megiddo's earlier observation, and the paper uses it to motivate the search for monotonic solution concepts outside the core, which leads to its second theorem: the Shapley value is the unique symmetric allocation procedure satisfying an even stronger monotonicity property (the subject of the companion mission). In cost-allocation practice the result says that an allocation method that is always stable against coalitional secession must sometimes penalise a division for making its own operations cheaper.

The result has been proved since 1985, and its proof is a short explicit counterexample. What the formalization adds is a machine-checked version of the counterexample (two explicit games whose cores are single points), a verified equivalence between the coalition-wise and player-wise forms of monotonicity, and the extension from five to arbitrarily many players, which the paper dismisses as an "obvious extension". To the best of the curators' knowledge none of these statements is formalized in any proof assistant.

Difficulty

The individual steps are elementary, but each requires care. Determining the core of each counterexample game exactly means showing both that the given point satisfies all $2^5$ coalition constraints and that no other point does. The equivalence of (4) and (5) is stated in the paper as following from "successive application" of (4), and every game involved must vanish on the empty coalition. The two counterexample games differ on two coalitions, $S_5$ and $N$ , so a single application of (4) does not suffice. Finally, the paper passes from five players to $n \ge 5$ players with the words "by obvious extension"; a formal proof has to make that step explicit, for arbitrary $n$ and for rules defined on all games with $n$ players, not only on those derived from five-player games.

Formalization scope

Players are Fin n; the paper's player $k$ is the Lean index $k-1$ . Thus the core points $(0,1,2,7,1)$ and $(3,0,0,6,3)$ appear as ![0,1,2,7,1] and ![3,0,0,6,3], and the players "2 and 4" whose allocations decrease are indices 1 and 3.
A game is the subtype Game n := {v : Finset (Fin n) → ℝ // v ∅ = 0}. Monotonicity axioms therefore quantify only over normalised games, as in the paper.
Allocations are real vectors Fin n → ℝ. Efficiency is part of the goal's hypotheses, matching the paper's definition of an allocation procedure.
The core is Supermodularity.Cooperative.Core Finset.univ v.1, the published core definition from Supermodularity and Complementarity, which coincides with the set on p. 68 of the paper.
IsCoreRule requires $\varphi(v) \in C(v)$ only when $C(v)$ is nonempty. The unconditional requirement would be unsatisfiable, because some games have an empty core, and would make the goal trivially true; that reading is ruled out.
IsCoalitionallyMonotonic is Eq. (4) with $T$ ranging over all coalitions, including $N$ . Restricting to $T \ne N$ , or restricting the games to superadditive ones, would change the theorem.
The counterexample games are defined in YoungGames: for $S \ne N$ , the value is the largest listed $w(S_k)$ over the $S_k \subseteq S$ , and $0$ if there is none.

Contributions welcome: proofs of the four milestones and the goal; a general lemma that padding a game with null players preserves the core up to zeros, which is reusable for other small-counterexample results in cooperative game theory; and decision procedures for linear feasibility over the coalitions of small games.

Selected references

H. P. Young, Monotonic Solutions of Cooperative Games, International Journal of Game Theory 14 (1985), 65–72. https://doi.org/10.1007/BF01769885
N. Megiddo, On the Nonmonotonicity of the Bargaining Set, the Kernel and the Nucleolus of a Game, SIAM Journal on Applied Mathematics 27 (1974), 355–358. https://doi.org/10.1137/0127026
M. Shubik, Incentives, Decentralized Control, the Assignment of Joint Costs and Internal Pricing, Management Science 8 (1962), 325–343. https://doi.org/10.1287/mnsc.8.3.325
D. B. Gillies, Solutions to General Non-Zero-Sum Games, in Contributions to the Theory of Games IV, Annals of Mathematics Studies 40 (1959), 47–85 (Princeton University Press). Cited as in Young (1985); no DOI checked.

10 thms3 active usersReviewed

Completed

Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks XIII: Back-Pressure Control for Packet NetworksTextbook

Motivation

Mission XII (12-packet-networks-model) built the discrete-time, slotted packet-network model from scratch and proved the chapter's own version of the fluid-to-stochastic stability bridge (Theorem 12.10). That result is only useful once paired with an actual control policy whose fluid model can be shown stable. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) supplies exactly such a policy in Sections 12.4-12.5: back-pressure control (called max-weight when the network is single-hop), a rule that has become the default choice in the switching and wireless-scheduling literature because it requires no advance knowledge of arrival rates and achieves the largest possible stability region. This mission formalizes back-pressure control for the discrete-time packet network model and proves it maximally stable — the chapter's own counterpart to mission VIII's continuous-time Theorem 9.12.

Setting

At the start of each timeslot, having observed the current buffer contents $z$ , the max-weight/ back-pressure (MW/BP) policy solves $\max_{s\in S(z)} z\cdot Rs$ (Eq. 12.41), where $S(z) := \{s\in S : Bs\le z\}$ restricts the schedule set $S$ (mission XII) to what is actually available given $z$ . Equivalently (Eq. 12.42-12.43), writing $w_j(z) := z_{u(j)} - z_{d(j)}$ (with $z_0 := 0$ ) for the "weight" of activity $j$ , the policy maximizes $\sum_j w_j(z) s_j$ — the schedule that clears the most "backlog pressure" per timeslot. The policy is deterministic (no randomization variable is needed, since (12.41) is a genuine optimization problem, not one that inherently requires randomized tie-breaking).

Formalization targets

Goal: Theorem 12.16 — aperiodicity, irreducibility, and conditional positive recurrence

Consider a packet network satisfying (12.1) and Assumption 12.1, operating under back-pressure control. The DTMC $Z$ is aperiodic and irreducible unconditionally. If the stability condition (12.26) — the existence of $\hat s\in\langle S\rangle$ with $\lambda < R\hat s$ — is additionally satisfied, $Z$ is positive recurrent. This is the mission's headline result, and it packages both a structural fact (irreducibility/aperiodicity, needed regardless of load) and a conditional stability fact (positive recurrence, needed only under (12.26)) in one theorem.

Supporting milestones

Lemma 12.17 shows the optimization problem (12.41) always has a nonzero solution whenever the network is nonempty — the fact that back-pressure never "idles unnecessarily," which Lemma 12.18 uses to show every state can reach the empty state (hence irreducibility) and that state $0$ has period $1$ (hence aperiodicity, via (12.1)'s own assumption that no external arrivals is possible with positive probability). Lemma 12.20 is the back-pressure fluid equation (12.44), the discrete-time analog of mission VIII's Theorem 9.8: at each regular point, the fluid-scaled buffer content dotted with the fluid departure rate equals the maximum of that same dot product over the convex hull of the schedule set. Lemma 12.21 shows this fluid model is stable whenever (12.26) holds, via an explicit quadratic Lyapunov function.

Significance

The result itself. Theorem 12.16 shows that back-pressure control — a rule requiring no knowledge of arrival rates, computed fresh from the current buffer contents every timeslot — is maximally stable: combined with Theorem 12.8 and Proposition 12.9 (mission XII), it stabilizes every packet network arrival-rate vector that any policy could possibly stabilize. This is the discrete-time, slotted analog of mission VIII's Theorem 9.12, and the two proofs share their essential Lyapunov argument (the book's own text calls Lemma 12.21's proof "almost identical to that of Theorem 9.12"), even though the two chapters' back-pressure equations are built from different underlying objects — mission VIII's continuous-time allocation polytope versus this chapter's convex hull of a discrete schedule set.

Formalizing it. A live prior-art check (GET /theorems?q=back-pressure, q=max-weight) finds no relevant hits, matching mission VIII's own finding for the continuous-time version. This mission formalizes the back-pressure optimization problem and policy, the back-pressure fluid equation, and its stability from scratch, restating (per this series' convention for concurrently-drafted chunks sharing a sub-namespace) the minimal apparatus needed from mission XII: the packet network model, Assumption 12.1, the raw processes, fluid limit paths, the fluid equations (12.31)-(12.36), and the ambient-chain machinery, plus a new Aperiodic predicate this chunk needs that mission XII's own results do not.

Difficulty

The obvious approach to Lemma 12.20's back-pressure fluid equation — directly differentiate the discrete system equation — obscures the actual argument, which reduces a maximum over the (potentially non-polytope) discrete schedule set $S$ to a maximum over its convex hull $\langle S\rangle$ (justified because a linear functional on a compact polytope is maximized at an extreme point) and then shows that every schedule with a strictly smaller objective value than the maximizer contributes zero derivative to the usage-counting process $\hat T_s$ — the discrete-time analog of mission VIII's Lemmas 9.10-9.11. A second difficulty is connecting the maximum-over-a- finite-set at the fluid-scaled level to Definition 12.3's discrete, arrival-indexed back-pressure policy: this mission's own Lemma 12.20 item states the fluid-relevant consequence of the discrete policy as a documented hypothesis (mirroring mission XI's own scope decision for its structurally identical WWTA fluid equation) rather than re-deriving it from the raw stochastic recursion, which would require reconstructing infrastructure outside this chapter's own numbered results.

Formalization scope

The packet network model, Assumption 12.1, the raw processes, and the fluid-limit apparatus are restated verbatim from mission XII (12-packet-networks-model), since concurrently-drafted chunks sharing a sub-namespace do not import one another's Lean files. IsBPOptimal is phrased via domination over the feasible-at- $z$ schedule set, not sSup/argmax, per this series' junk-value-avoidance convention; the same convention is applied to the maximum over $\langle S\rangle$ in the back-pressure fluid equation. The formalization does not admit a trivializing reading: irreducibility and aperiodicity are the same non-vacuous renewal-theoretic notions used throughout this series (Aperiodic requires a genuine positive self-transition probability, not a vacuously-true condition), and the goal's positive-recurrence conjunct is genuinely conditional on (12.26), stated with the correct strict inequality rather than weakened to $\le$ . Contributions completing the five by sorry proofs are welcome, particularly Lemma 12.17's hop-count induction and Lemma 12.20's extreme-point/zero-derivative argument (mirroring mission VIII's own Lemmas 9.10-9.11, adapted to discrete time).

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org

8 thms3 active usersReviewed

Completed

Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks XII: Packet Networks, Subcriticality and Fluid LimitsTextbook

Motivation

Internet routers, wireless base stations, and data-switch fabrics all face the same recurring decision: in each discrete time slot, which of many possible transfer operations should be executed, given the packets currently queued and the physical constraints (link capacities, interference between simultaneous transmissions) on what can be done at once? J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 12 to exactly this question, under the name packet networks. Unlike every prior chapter of the book, which works in continuous time with Poisson-driven Markov chains, this chapter builds its stability theory from scratch for a discrete-time, slotted model — the natural setting for a system that makes one scheduling decision per clock tick. This mission formalizes the chapter's foundational layer: the model itself, its notion of a feasible schedule and control policy, subcriticality, and the discrete-time fluid-limit machinery that Chapters 13 and 14 (back-pressure control and random proportional scheduling, respectively) build their own stability proofs on top of.

Setting

A packet network (Section 12.1) has I packet classes and J activities (service types); activity $j$ transfers a packet from its input class $u(j)$ to its output class $d(j)$ (or removes it from the network if $d(j)=0$ ), giving an $I\times J$ input-output matrix $R$ . A processing plan for class $i$ (Definition 12.2) is a chain of activities from $i$ to exit; Assumption 12.1 requires every class to have one and forbids cycles. In each timeslot the system manager chooses a schedule $s\in\mathbb Z^J_+$ from a feasible set $S$ satisfying the packet-availability constraint $Bs\le z$ (the current buffer contents); $S$ is typically built (Section 12.2) from a link usage matrix $A$ and a set $C$ of feasible link configurations via $S_c := \{s : As\le c\}$ , $S := \bigcup_{c\in C} S_c$ . A Markovian control policy (Definition 12.3, Eq. 12.8) chooses $s(\tau) = f(Z(\tau-1), U(\tau))$ from the current buffer contents and an independent randomization variable; it is admissible if it never overdraws a buffer, and stable if the resulting discrete-time Markov chain $Z$ is irreducible and positive recurrent.

Formalization targets

Goal: Theorem 12.10 — fluid limit stability implies positive recurrence

If the DTMC $Z$ under a Markovian policy $f$ is irreducible and its fluid limit is stable (Definitions 12.14-12.15), then $Z$ is positive recurrent. This is the chapter's own version of Theorem 6.2 (mission III) — the technical fulcrum that lets a deterministic fluid-model stability argument certify the stability of the original discrete, stochastic system — restated for a genuinely different probabilistic model, since Theorem 6.2 was built under continuous-time, Poisson-arrival hypotheses this chapter does not share.

Supporting milestones

Propositions 12.6-12.7 characterize the convex hulls $\langle S_c\rangle$ and $\langle S\rangle$ as explicit polytopes cut out by the link usage matrix — the combinatorial core that Theorem 12.8 (stability implies subcriticality, this chapter's analog of Theorem 5.2) and Proposition 12.9 (a necessary condition for subcriticality) both build on. Lemma 12.11 records that the schedule-usage counting process is Lipschitz; Lemma 12.12 is the functional strong law of large numbers the external arrival process satisfies; and Theorem 12.13 combines them to establish existence of discrete-time fluid limits satisfying the chapter's own fluid equations (12.31)-(12.36) — the chapter's analog of Theorem 6.5.

Significance

The result itself. Theorem 12.10 is what makes the rest of Chapter 12 (and Chapters 13-14) tractable: rather than analyzing an infinite-state discrete-time Markov chain's positive recurrence directly — a notoriously hard problem in general — it suffices to exhibit a deterministic fluid model and show every solution of that fluid model empties in finite time. This is the same strategy Chapter 6 established for the book's continuous-time model, but Chapter 12 cannot simply invoke that earlier theorem: the packet network model uses discrete time slots rather than a continuous clock, and its probabilistic structure (arbitrary i.i.d. arrival increments rather than Poisson arrivals) is different enough that the fluid-limit compactness argument has to be redone, even though — as the book's own text notes — "the proof mimics that of Theorem 6.2."

Formalizing it. A live prior-art check (GET /theorems?q=packet+network, q=discrete-time+Markov+chain, q=slotted+time) finds no relevant hits. A dedicated further check for MarkovMixing, a different mission's own corpus offering a PositiveRecurrent predicate for Markov chains, found a representationally distinct formalization (a row-function transition kernel rather than this series' own PMF-based jump-chain convention); this mission restates positive recurrence and irreducibility locally instead, consistent with every mission in this series since mission I. Everything else — the packet network model, schedules and configurations, the subcritical region, Markovian policies, and the discrete-time fluid-limit apparatus — is formalized from scratch.

Difficulty

The most consequential decision in this mission is representational, not mathematical: Theorem 12.10's fluid-limit-stability hypothesis quantifies over all fluid limit paths, which are themselves scaling limits of a genuinely stochastic discrete-time process — reconstructing that process from Chapter 2/4's own primitive stochastic elements (arrival processes, phase-type service mechanics) would require rebuilding infrastructure this chapter's own numbered results do not supply. Following mission III's own precedent for its structurally identical Theorem 6.5, this mission instead takes the raw, per-initial-state schedule-usage and arrival processes as given data satisfying only the recap properties the chapter's own proofs actually cite (Eq. 12.9-12.10's system equation, monotonicity), and fixes a single sample point together with an explicit SLLN hypothesis rather than a bare "for almost all $\omega$ " quantifier — matching the book's own statement of Theorem 12.13, which itself begins "Fix an $\omega\in\Omega_1$ " rather than quantifying almost everywhere within the theorem itself. A second difficulty is genuinely combinatorial: Proposition 12.6's proof constructs an explicit product-form probability distribution over schedules (one independent randomization per link) whose mean recovers an arbitrary point of the polytope $\{Ax\le c\}$ — a real combinatorial argument, not a formal consequence of the convex-hull operator's definition.

Formalization scope

Classes, activities, links, schedules and configurations are represented via Fin-indexed types throughout; S and C are taken as Finsets (every worked example in the book has finitely many configurations, and the link usage matrix's single-1-per-column structure bounds each schedule component, so this is a genuine, if implicit, standing feature of the model rather than an added restriction). IsScheduleSetAt/IsScheduleSet characterize $S_c$ / $S$ via an ↔ against the underlying capacity constraint, rather than constructing them, matching how set-valued model data is handled elsewhere in this series. The formalization does not admit a trivializing reading: the ambient chain's positive recurrence (PositiveRecurrent) is the same non-vacuous renewal-theoretic notion used throughout this series, PacketFluidLimitStable quantifies over every genuine fluid limit path (not a hand-picked one), and subcriticalRegion is stated with a strict inequality ( $A\hat s < \hat c$ ) exactly as Eq. 12.24 requires, not weakened to $\le$ . Contributions completing the eight by sorry proofs are welcome, particularly Proposition 12.6's explicit randomized- schedule construction and Theorem 12.13's compactness argument (mirroring mission III's own Theorem 6.5 proof, adapted to discrete time).

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org

14 thms3 active usersReviewed

Completed

Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks XI: Maximal Stability of Workload-Weighted Task AllocationTextbook

Motivation

Large-scale data-intensive computing splits a job into many small "map tasks," each of which must be assigned to one of thousands of general-purpose servers in a data center — the MapReduce paradigm introduced by Dean and Ghemawat (2008). Because a task's input data is stored on only a few of those servers, routing it to a server that already holds its data ("data locality") avoids costly network transfer, so a task-allocation policy that ignores locality can leave a server farm badly underutilized even when raw compute capacity is ample. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 11 to a rigorous stability analysis of Xie, Yekkehkhany, and Lu's (2016) workload-weighted task allocation (WWTA) policy, which routes each arriving task to whichever eligible server currently carries the least (locality-weighted) backlog. This mission formalizes the chapter's central result: WWTA is not merely a reasonable heuristic but is maximally stable — it keeps the system stable whenever any routing policy could.

Setting

A task allocation model (Sections 11.2-11.3) has L task categories and K servers; a class is a pair $(\ell,k)$ , a category routed to a specific server, with mean service time $m_{\ell k} > 0$ (Eq. 11.3) reflecting both data locality (local, rack-local, or remote access) and the server's relative processing speed. Tasks in category $\ell$ arrive according to a Markovian arrival process (MArP) with long-run average rate $\nu_\ell$ — a substantially more general model than the independent Poisson streams used elsewhere in the book, needed to capture batches of map tasks generated from a single job. Routing is by immediate commitment: each task is assigned to a server the instant it arrives, based only on its category and the current backlog, with no possibility of later reassignment. The workload of server $k$ at time $t$ (Eq. 11.7) is $W_k(t) := \sum_\ell m_{\ell k} Z_{\ell k}(t)$ , the locality-weighted total backlog assigned to it. Workload-weighted task allocation (WWTA), Definition 11.3, routes an arriving category- $\ell$ task to any server achieving $\operatorname{argmin}_{k} m_{\ell k} W_k(t-)$ (Eq. 11.8, ties broken arbitrarily), where $W(t-)$ is the workload vector's left limit at the arrival instant.

Formalization targets

Goal: Theorem 11.6 — WWTA fluid model stability under the load condition

If there exists $\lambda = (\lambda_{\ell k}) \ge 0$ with $\sum_k \lambda_{\ell k} = \nu_\ell$ for each category (Eq. 11.4) and $\sum_\ell m_{\ell k}\lambda_{\ell k} < 1$ for each server (Eq. 11.5), then the WWTA fluid model — the deterministic fluid equations (11.11)-(11.16) that arise as scaling limits of the stochastic model under WWTA control — is stable: every solution reaches the zero state in finite time proportional to its initial size.

Supporting milestones

Lemma 11.2 shows this load condition is equivalent to subcriticality of the task allocation model, in the sense of Section 5.2's general definition, reducing an existence statement over the model's full $G,R,A,b$ apparatus to a simple linear-feasibility check. Theorem 11.4 establishes that fluid limits of the stochastic model exist and satisfy the general fluid equations (11.11)-(11.15) under any immediate-commitment routing policy, and the WWTA-specific equation (11.16) under WWTA — the chapter's version of the fluid-limit machinery Chapter 6 builds for the book's standard model, adapted to Markovian (not Poisson) arrivals and immediate-commitment routing. Theorem 11.5 is the corresponding replacement for Theorem 6.2 (mission III): fluid limit stability implies stability of the original stochastic model. Corollary 11.7 is the mission's other headline consequence: WWTA is maximally stable, stabilizing the model whenever any simply structured routing policy could.

Significance

The result itself. A task-allocation heuristic motivated purely by an intuitive "balance-the-weighted-backlog" idea turns out to have the strongest stability guarantee a policy can have: it never needs re-tuning as arrival rates change, and no alternative policy can stabilize a regime WWTA cannot. Xie, Yekkehkhany, and Lu (2016) proved this fact (calling it "throughput optimality") by direct analysis of the discrete stochastic model using a quadratic Lyapunov function; Dai and Harrison's contribution is to prove the same conclusion via the fluid-model route, and — because the task allocation model violates two of the standing assumptions under which Chapter 6's general theory was built (MArP rather than Poisson arrivals, immediate-commitment routing rather than the book's default relaxed control) — to show that the general fluid-stability machinery survives those changes with only minor modification.

Formalizing it. A live prior-art check (GET /theorems?q=task+allocation, q=server%20farm, q=data%20locality) finds no relevant hits on the platform (workload returns one unrelated text-corpus-statistics result). This mission formalizes the task allocation model, WWTA, the fluid equations, and the stochastic-to-fluid bridge from scratch, reusing Mathlib's general real-analysis, measure-theory, and PMF-based Markov-chain substrate, and restating (per this series' convention for concurrently-drafted chunks) the minimal apparatus needed from missions I and III.

Difficulty

The obvious approach to Definition 11.3 — pick a canonical minimizer of $m_{\ell\cdot}W_\cdot(t-)$ , e.g. via Finset.min' — silently narrows WWTA to a single tie-breaking rule, when (11.8) explicitly allows any minimizer; this mission instead states WWTA as domination over every server, accepting every admissible tie-break. A second difficulty is genuinely structural: Theorem 11.4's "for almost all $\omega$ " existence claim is a measure-theoretic statement about a probability space that mission III's own analogous Theorem 6.5 sidesteps by fixing a sample point $\omega$ together with the specific SLLN limit that argument needs — this mission follows the same precedent rather than introducing a bare "almost everywhere" quantifier, which does not by itself supply the type information Lean's typeclass resolution needs to identify an ambient measure. A third is connecting Definition 11.3's discrete, arrival-indexed routing rule to the raw (pre-limit) process family that Theorem 11.4's existence argument operates on: the book's own proof derives the needed consequence (Eq. 11.22, "server $k$ receives no more category- $\ell$ tasks in a neighbourhood of $t$ ") via an explicit $\varepsilon$ - $\delta$ argument from the discrete policy, which this mission takes as a documented hypothesis rather than re-deriving, since building the arrival-sequence-to-counting-process reconstruction is genuinely Chapter 2/4 machinery outside this chapter's own numbered results.

Formalization scope

Classes are represented as pairs (ℓ,k) : Fin L × Fin K rather than flattened to a single index, avoiding an arbitrary choice of encoding. TaskAllocationProcessFamily, FluidLimitPath, and TaskAllocationFluidLimitStable restate mission III's SPNProcessFamily/FluidLimitPath/ FluidLimitStable apparatus, adapted to this model's (E,D,Z) triple and doubly-indexed classes; PositiveRecurrent restates mission I's renewal-theoretic positive-recurrence notion. The formalization does not admit a trivializing reading: IsWWTA accepts every admissible tie-break rather than a single canonical one, SatisfiesWWTAFluidEquation requires Nonempty (Fin K) so its min_{k} is a genuine minimum rather than a junk value at zero servers, and the goal's conclusion WWTAFluidStable is the same non-vacuous fluid-model-stability predicate (Definition 6.3, specialized) used throughout this series. Contributions completing the five by sorry proofs are welcome, particularly Theorem 11.4's fluid-limit compactness argument (mirroring mission III's own Theorem 6.5 proof) and Theorem 11.6's explicit quadratic-Lyapunov-function argument.

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
J. Dean and S. Ghemawat, "MapReduce: simplified data processing on large clusters," Communications of the ACM 51 (2008), 107–113.
Q. Xie, A. Yekkehkhany, and Y. Lu, "Scheduling with multi-level data locality: throughput and heavy-traffic optimality," IEEE INFOCOM 2016.

10 thms3 active usersReviewed

Completed

Dynamic Programming Probability·Captain: mikedeng1

Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem: The Base Stock Ordering Policy Is OptimalResearch Paper

Motivation

An inventory manager who stocks many products, faces random demand and pays ordering, holding and shortage costs must decide each period how much of each product to order. In general the optimal decision depends on the whole state and is found by solving a dynamic programme, which becomes impractical as the number of products grows. Myopic (or base stock) policies avoid this: in each period they aim at a target level computed from that period's data alone. Knowing when such a policy is optimal over an infinite horizon tells a practitioner when the multi-period problem decouples into a sequence of one-period problems.

Arthur F. Veinott, Jr. gave such conditions in Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem (Management Science 12(3):206–222, 1965). Earlier results of this type were for a single product (the paper cites Karlin, Management Science 6(3), 1960, Bellman–Glicksberg–Gross, Management Science 2(1), 1955, Iglehart–Karlin 1962, and the Arrow–Karlin–Scarf volume of 1958); Veinott's model allows several products, several demand classes, costs and demand distributions that change over time, general ordering constraints and general stock dynamics (backlogging, lost sales, and mixtures), and it does not use the functional equation of dynamic programming. Instead, the proofs analyse the inventory process directly.

Setting

There are $n$ products and $m$ demand classes. Vectors are compared componentwise: $u \le v$ means $u_j \le v_j$ for all $j$ . In period $i = 1, 2, \dots$ the manager observes the inventory vector $x_i \in X_i \subseteq \mathbb{R}^n$ (negative coordinates are backlogs) and orders up to a vector $y_i \in Y_i \subseteq \mathbb{R}^n$ , subject to $y_i \ge q_i(x_i)$ , where $q_i$ is a vector of extended-real functions (for instance $q_i(x) = x$ forbids disposal). A random demand vector $D_i$ with law $\Phi_i$ and values in a Borel set $\mathfrak{D}_i \subseteq \mathbb{R}^m$ then occurs, and the next inventory vector is $x_{i+1} = s_i(y_i, D_i) \in X_{i+1}$ . The demands $D_1, D_2, \dots$ are independent. Ordering $y_i - x_i$ costs $c_i \cdot (y_i - x_i)$ , the holding and shortage cost is $g_i(y_i, D_i)$ , and $\alpha_i \ge 0$ is the discount factor of period $i$ .

Regrouping the ordering costs gives the one-period cost

W_i(y,t) = c_i\, y + g_i(y,t) - \alpha_i\, c_{i+1}\, s_i(y,t), \qquad G_i(y) = \int_{\mathfrak{D}_i} W_i(y,t)\, d\Phi_i(t),

with discount weights $\beta_1 = 1$ and $\beta_i = \alpha_1 \cdots \alpha_{i-1}$ . The integrals are assumed finite, and $G_i \ge \gamma_i$ with $\sum_i |\beta_i \gamma_i| < \infty$ . An ordering policy $\bar Y$ chooses $y_i$ as a Borel function of the past; it is feasible if $y_i \in Y_i$ and $y_i \ge q_i(x_i)$ for every possible history. Its cost is

f(x_1 \mid \bar Y) = \sum_{i=1}^\infty \beta_i\, E\, G_i(y_i) \in (-\infty, +\infty],

and a feasible policy of least cost is optimal.

Let $\bar y_i$ minimize $G_i$ over $Y_i$ . When $\bar y_i$ is not attainable from $x$ , the minimal feasible level $w_i(x)$ is the least element of $Y_i \cap \{y : y \ge q_i(x),\ y \ge \bar y_i\}$ . The base stock ordering policy orders up to $\bar y_i$ if $q_i(x_i) \le \bar y_i$ and up to $w_i(x_i)$ otherwise.

Formalization targets

The hypotheses are: (3a) $\bar y_i \in Y_i$ minimizes $G_i$ over $Y_i$ ; (3b) $q_{i+1}(s_i(\bar y_i, t)) \le \bar y_{i+1}$ for $t \in \mathfrak{D}_i$ ; (3c) $Y_i$ is closed and linearly ordered by $\le$ ; (3d) $G_i$ and $s_i(\cdot, t)$ are nondecreasing on $\{y \in Y_i : y \ge \bar y_i\}$ , and $q_i$ is nondecreasing where $q_i(x) \not\le \bar y_i$ .

Goal: Theorem 3.2

Under (3a)–(3d), the base stock ordering policy

\bar Y_i^*(H_i^*) = \begin{cases} \bar y_i, & q_i(x_i^*) \le \bar y_i, \\ w_i(x_i^*), & q_i(x_i^*) \not\le \bar y_i \end{cases}

is feasible and optimal: $f(x_1 \mid \bar Y^*) \le f(x_1 \mid \bar Y)$ for every feasible $\bar Y$ .

Milestones

A nonempty, closed, linearly ordered, bounded-below subset of $\mathbb{R}^n$ has a least element (p. 212); hence $w_i(x)$ exists and equals $\bar y_i$ when $q_i(x) \le \bar y_i$ .
$w_i$ is nondecreasing where $q_i(x) \not\le \bar y_i$ (p. 214).
Once $q_k(x_k^*) \le \bar y_k$ , the base stock policy orders up to $\bar y_i$ for all $i \ge k$ .
Theorem 3.1: under (3a) and (3b), if $q_1(x_1) \le \bar y_1$ , ordering up to $\bar y_i$ in every period is optimal, with cost $\sum_i \beta_i G_i(\bar y_i)$ .
The coupling (3.1): before the first period $T$ with $q_T(x_T^*) \le \bar y_T$ ,

\bar y_i < y_i^* = w_i(x_i^*) \le w_i(x_i) \le y_i.

Pathwise dominance: $G_i(y_i^*) \le G_i(y_i)$ for every $i$ and every possible demand path.
The reduction behind (2.3): $E\, W_i(y_i, D_i) = E\, G_i(y_i)$ , by independence of $y_i$ and $D_i$ .

Significance

The theorem shows that under (3a)–(3d) the infinite-horizon, nonstationary, multi-product problem is solved by one-period optimization: compute $\bar y_i$ from $G_i$ alone, and when it is unreachable order the least feasible amount. No value function is computed. It covers backlogging and lost sales, products stocked in fixed proportions, and time-varying cost and demand data, and Theorem 3.1 alone settles the frequent case in which the initial stock is small.

The result is proved in the paper. To our knowledge it has not been machine-checked: this mission produces a Lean model of a general stochastic, infinite-horizon, multi-product inventory problem (feasible policies, the expected discounted cost with $+\infty$ allowed), and a checked proof that a myopic policy is optimal in it. The model and its cost are reusable for other base stock and myopic optimality results.

Difficulty

The obvious argument would compare the base stock policy with an arbitrary policy period by period using (3a) alone. That fails once $\bar y_i$ is unreachable. The base stock policy then holds less stock than $\bar y_i$ would require, and it has to be shown that no other policy can reach a lower-cost level later. The proof couples the two trajectories along every demand path, using the monotonicity in (3d) and the linear order of $Y_i$ from (3c), until the base stock level becomes attainable, after which (3b) keeps it attainable. The formal difficulties are:

the existence and monotonicity of the least element $w_i(x)$ in a closed chain of $\mathbb{R}^n$ ;
the measurability of the base stock policy, which is part of its feasibility;
the passage from pathwise dominance to the expected discounted cost when the cost may be $+\infty$ .

Formalization scope

Periods are 0-based in Lean (Lean period $k$ is the paper's period $k+1$ ). Vectors are Fin n → ℝ with the product order; $q_i$ takes values in Fin n → EReal. Policies are functions of the past demands. The paper shows on p. 219 that this loses no generality once $x_1$ is fixed. The cost is excess, a $[0,\infty]$ -valued series of lower Lebesgue integrals of $\beta_i(G_i(y_i) - \gamma_i)$ , plus the finite real $\sum_i \beta_i\gamma_i$ , taken in EReal. A divergent series therefore gives $+\infty$ and never the junk value $0$ . "Minimal element" is IsLeast. The $G_i$ in the statements is the integral of $W_i$ built from the data, and the policy in the goal is constructed from $\bar y$ , $q$ , $w$ and $s$ . Neither is an arbitrary object satisfying the conclusion. The goal concludes optimality, which includes feasibility: a pathwise or conditional statement would not be the theorem.

Hypotheses added relative to the page, each used by the paper without being stated:

Order feasibility: from every $x \in X_i$ some $y \in Y_i$ with $y \ge q_i(x)$ exists (p. 212 asserts the set defining $w_i(x)$ has a minimal element, which needs it nonempty). The least-element lemma likewise assumes $A$ nonempty.
(3d)'s $q$ -clause in one-sided form: if $x \le x'$ in $X_i$ and $q_i(x) \not\le \bar y_i$ , then $q_i(x) \le q_i(x')$ . This is the form the proof on p. 214 uses; monotonicity on the region $\{q_i(x) \not\le \bar y_i\}$ alone admits a counterexample to Theorem 3.2.
Integrability of $W_i(y_i, D_i)$ in the milestone $E W_i = E G_i$ .
Borel measurability of $q_i$ on all of $\mathbb{R}^n$ rather than on $X_i$ (a harmless strengthening).

A complete development needs: least elements of closed chains in $\mathbb{R}^n$ ; measurability of the least-element selection $x \mapsto w_i(x)$ ; a Fubini/independence argument for $E\,W_i(y_i,D_i)=E\,G_i(y_i)$ ; and monotone summation of lower integrals. The least-element lemma and the cost encoding are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments.

Selected references

A. F. Veinott, Jr., Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
R. Bellman, I. Glicksberg, O. Gross, On the Optimal Inventory Equation, Management Science 2(1):83–104, 1955. https://doi.org/10.1287/mnsc.2.1.83
S. Karlin, Dynamic Inventory Policy with Varying Stochastic Demands, Management Science 6(3):231–258, 1960. https://doi.org/10.1287/mnsc.6.3.231

11 thms3 active usersReviewed

Completed

Probability Stochastic Systems·Captain: Shuze Chen

Processing Networks X: Maximal Stability of Proportionally Fair ControlTextbook

Motivation

Mission IX (09-proportional-fairness-core) formalized proportional fairness (PF) as a control policy and proved the technical core of its stability theory: under a load condition, the PF fluid model is stable (Theorem 10.5), via an entropy Lyapunov function that is genuinely not Lipschitz continuous — a departure from every other stability argument in J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org). A stability theorem for one fixed arrival-rate vector is, on its own, a narrower claim than practitioners actually want: real systems see load that changes over time, and a control policy worth adopting should not need re-tuning every time the mix of traffic shifts. This mission completes Theorem 10.5's proof and turns it into exactly that stronger guarantee — proportional fairness is maximally stable: stable throughout the entire region where any policy could be stable, without knowing the arrival rates in advance — and specializes the result to two concrete network families, bandwidth-sharing networks and queueing networks under head-of-line proportional processor sharing (HLPPS), that were already familiar from earlier in the book under different control policies.

Setting

Fix a unitary network operating under PF control with mean service times $m > 0$ , routing matrix $P$ , a partition of job classes into demand groups $\{\mathcal I(\ell), \ell \in \mathcal L\}$ , and a reduced allocation set $\tilde{\mathcal A} \subset \mathbb R^{\mathcal L}_+$ (all restated from mission IX, Definition 10.3). The entropy Lyapunov function $\varphi(t) := \sum_i Z_i(t)\log(\dot D_i(t)/\alpha_i)$ (Eq. 10.38, mission IX) admits an alternative decomposition $\varphi = \sum_\ell \varphi_\ell$ in terms of the within-group entropy term

f(t) := \sum_{\ell\in\mathcal L}\sum_{i\in\mathcal I(\ell)} Z_i(t)\log\!\left(\frac{Z_i(t)}{Y_\ell(t)}\right), \qquad Y(t) := GZ(t) \quad \text{(Eq. 10.50)},

with the convention that the term for class $i$ is $0$ when $Z_i(t)=0$ . Here $D^+$ / $D^-$ denote the upper-right/upper-left Dini derivatives (Appendix A.4, Eqs. A.9-A.10): at a point where the ordinary derivative may not exist, these one-sided $\limsup$ s still let a Lyapunov-drift argument go through. A control policy is maximally stable (Section 5.7) for a network if its implementation does not depend on the arrival-rate vector $\lambda$ and it is stable for every $\lambda$ in the network's stability region $\Lambda^*$ — the largest region any policy could possibly stabilize.

Formalization targets

Goal: Corollary 10.16 — maximal stability of PF control for a unitary network

\text{IsMaximallyStable}\Big(\lambda \mapsto \text{PFFluidStable}(\lambda, m, P, \mathrm{grp}, \tilde{\mathcal A})\Big)

for the single PF policy value (its implementation never depends on $\lambda$ ). This is the applied payoff of Theorem 10.5 (mission IX): combined with Theorem 6.2 (mission III, fluid stability implies SPN stability) and Corollary 5.6 (mission II, a $\lambda$ -independent policy stable throughout the subcritical region is automatically maximally stable), it upgrades a single- $\lambda$ stability statement to the strongest form the book's own framework can express.

Supporting milestones

Lemmas 10.11-10.15 supply the remaining technical content of Theorem 10.5's proof that mission IX's own milestones left open: Lemma 10.11 is the uniform negative-drift bound $\sum_i \dot Z_i(t)\log(\dot D_i(t)/\alpha_i) \le -\varepsilon$ at every regular point with $Z(t) \ne 0$ ; Lemmas 10.12-10.14 establish continuity and two successively sharper Dini-derivative bounds on the within-group entropy term $f$ ; Lemma 10.15 shows that positivity of the departure rate $\dot D_i(t)$ propagates from occupied classes to every class. Corollaries 10.17 and 10.18 specialize the goal to bandwidth-sharing networks and to HLPPS-controlled queueing networks, respectively.

Significance

The result itself. A stability theorem tied to one fixed $\lambda$ is of limited practical use: it would need to be re-verified every time the arrival-rate vector changes, which real traffic does constantly. Maximal stability removes that dependency entirely — a single policy, implemented without any knowledge of $\lambda$ , is guaranteed stable throughout the full region any control could stabilize. Corollaries 10.17 and 10.18 make this concrete for two network families with independent histories in the literature: bandwidth-sharing networks (the original motivation for proportional fairness, Kelly 1997) and queueing networks under HLPPS, connecting PF's static, utility-theoretic motivation to a scheduling rule that predates it.

Formalizing it. A live prior-art check (GET /theorems?q=proportional%20fairness, q=maximal%20stability, q=bandwidth%20sharing) finds no relevant hits on the platform. This mission formalizes the remaining entropy-Lyapunov lemmas, the within-group entropy term, the BWS and HLPPS network models (restated locally, since no other drafted chunk covers Sections 4.5-4.6), and the maximal-stability predicate, reusing only Mathlib's general real-analysis substrate (Dini derivatives via Filter.limsup) and definitions restated from missions II, III, V, and IX under this series' restate-not-import convention for concurrently-drafted chunks.

Difficulty

The obvious approach to Corollary 10.16 — restate "maximally stable" with an explicit $\lambda$ -dependent policy family and add "the policy doesn't actually depend on $\lambda$ " as a side hypothesis — obscures the point: a policy that is definitionally independent of $\lambda$ is a stronger and cleaner claim than one that happens to satisfy an extra equation. This formalization instead instantiates the abstract policy type at Unit, so $\lambda$ -independence holds by construction rather than as a hypothesis to verify, matching the book's own reading of Section 5.7's definition. A second difficulty is Lemma 10.13's Dini-derivative inequality (Eq. 10.56): the plain-text extraction of this display equation loses bracket and subscript structure that changes its meaning, so the exact grouping was confirmed against the PDF page directly and cross-checked against the book's own re-derivation of the same bracketed expression inside Lemma 10.14's proof. A third is Corollary 10.17's proof, which genuinely depends on three facts outside this chunk's own chapter portion (Proposition 4.4 and the Section 4.4 model translation, Proposition 5.1, Theorem 5.2); rather than silently assuming them or re-deriving their proofs from scratch, they are stated as explicit hypotheses of the milestone itself, so the item's actual content — deriving the two-sided conclusion — is exactly what remains to be proved.

Formalization scope

RestatedCore, RestatedFluidModel, and the maximal-stability predicate MaximalStability are restated verbatim (or, for MaximalStability, in shape) from missions IX, III/V, and II respectively, since concurrently-drafted chunks in this series do not import one another's Lean files even when they share a sub-namespace. New to this chunk: diniUpperLeft (Eq. A.10, needed alongside mission IX's diniUpperRight for Lemma 10.13's two-sided bound), the within-group entropy term withinGroupEntropy (Eq. 10.50, deliberately not named f, since the book's own f already denotes the unrelated PF optimization objective of Eq. 10.2 within the same chapter), and BWSNetworkData/QueueingNetworkDataHL/HLPPSFluidStable (Sections 4.5-4.6, restated locally since no drafted chunk's BRIEF.md covers them). The formalization does not admit a trivializing reading: IsMaximallyStable is instantiated with the genuine, non-vacuous predicate PFFluidStable/HLPPSFluidStable — the same predicate whose stability Theorem 10.5 (mission IX) already establishes on the load-condition region — never with a policy type or stability predicate engineered to make the maximal-stability claim vacuous. Contributions completing the eight by sorry proofs are welcome, particularly Lemma 10.13's Dini-derivative estimate (Section B.4's preliminary results) and Lemma 10.15's connectivity argument (Appendix B.9/B.17).

Selected references

J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
F. P. Kelly, "Charging and rate control for elastic traffic," European Transactions on Telecommunications 8 (1997), 33–37.
F. P. Kelly, A. K. Maulloo, and D. K. H. Tan, "Rate control for communication networks: shadow prices, proportional fairness and stability," Journal of the Operational Research Society 49 (1998), 237–252.

13 thms3 active usersReviewed

Operations Research

Missions

Discrete Convex Analysis VIII: Quasi L-Convex Functions and the Quasi-Proximity TheoremTextbook

Motivation

Setting

Formalization targets

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

Milestones: Theorems 7.49, 7.53

Significance

Difficulty

Formalization scope

Selected references

Discrete Convex Analysis XXIV: Quasi M-Convex FunctionsTextbook

Motivation

Setting

Formalization targets

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

Supporting structural targets

Significance

Difficulty

Formalization scope

Selected references

Dual Stochastic Dominance and Related Mean-Risk Models 2: Mean–Gini Optimal Portfolios Exist and Are SSD-EfficientResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.3

Milestones

Companion: Theorem 5.4

Significance

Difficulty

Formalization scope

Selected references

Discrete Convex Analysis XXI: The Exchange Axiom as Local OptimalityTextbook

Motivation

Setting

Formalization targets

Goal: the exchange axiom as sequential improvement

Supporting structural targets

Significance

Difficulty

Formalization scope

Selected references

Star-Shaped Risk Measures 2: law-invariant star-shaped risk measures as robustified Value-at-RiskResearch Paper

Motivation

Setting

Formalization targets

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

Milestones

Significance

Difficulty

Formalization scope

Selected references

Star-Shaped Risk Measures 1: star-shaped risk measures are the minima of convex risk measuresResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 2643)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Markov Decision Processes XIV: Positive Models and Linear Programming Duality for MDPsTextbook

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Generalized Gradients and Applications II: Flow-Invariant Sets of Lipschitz Differential InclusionsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem (4.4)

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope