Optimization

Motivation

A firm that sells several products must decide, before demand is known, how much production capacity to build and of what kind. Dedicated capacity makes one product; flexible capacity makes any of them. The classic argument for flexibility is demand pooling: capacity that can follow demand to whichever product needs it wastes less than capacity locked to one product (Fine and Freund 1990; Van Mieghem 1998).

When capacity itself is unreliable, as with a supplier that may fail to deliver, a plant that may be disrupted, or a batch that may be rejected, flexibility has a second face. A single flexible resource concentrates the firm's supply in one place, so one failure removes all of it, whereas several dedicated resources rarely fail together. This resource-aggregation effect works against flexibility. Tomlin and Wang (2005) set up a newsvendor network in which both effects are present and ask when a firm should pay more for flexible capacity than for dedicated capacity. Their first answer (Proposition 1) is that a risk-neutral firm facing equal reliabilities and costs never loses by choosing flexibility, whatever the joint distribution of demand. This mission formalizes that answer.

Setting

There are $N$ products with a common unit contribution margin $p>0$. The demand vector $\tilde X=(\tilde X_1,\dots,\tilde X_N)$ is random, nonnegative and integrable; its total is $\tilde X_{N+1}=\tilde X_1+\dots+\tilde X_N$.

Two networks are compared. In the dedicated network SD, resource $n\in\{1,\dots,N\}$ makes only product $n$ and has marginal total cost $c>0$. In the flexible network SF, a single resource, labelled $N+1$, makes every product and has marginal total cost $c_{N+1}$.

Every resource $j$ is unreliable with a Bernoulli yield $\tilde Y_j\in\{0,1\}$, $\mathbb P(\tilde Y_j=1)=\theta$. The common reliability is $\theta\in[0,1]$, the yields are mutually independent, and they are independent of demand. Investing $K_j\ge 0$ in resource $j$ delivers capacity $\tilde Y_jK_j$ and costs $(\lambda+(1-\lambda)\tilde Y_j)c_jK_j$: the firm pays the committed cost $\lambda c_j$ per unit ordered and a further $(1-\lambda)c_j$ per unit delivered, with $\lambda\in[0,1]$.

The realized profits are

$$W^{SD}(K)=\sum_{n=1}^N\Big(-(\lambda+(1-\lambda)\tilde Y_n)cK_n+p\min\{\tilde X_n,\tilde Y_nK_n\}\Big),$$ $$W^{SF}(K_{N+1})=-(\lambda+(1-\lambda)\tilde Y_{N+1})c_{N+1}K_{N+1}+p\min\{\tilde X_{N+1},\tilde Y_{N+1}K_{N+1}\},$$

and a risk-neutral firm maximizes the expected profit $V^{SD}_{RN}(K)=\mathbb E[W^{SD}(K)]$ or $V^{SF}_{RN}(K_{N+1})=\mathbb E[W^{SF}(K_{N+1})]$ over nonnegative investments. Let $V^{SD,*}$ and $V^{SF,*}$ be the optimal values. SF is (weakly) preferred if $V^{SF,*}\ge V^{SD,*}$.

The indifference cost $c^I_{N+1}$ is a value of $c_{N+1}$ at which $V^{SF,*}=V^{SD,*}$, and the flexibility premium is $\Delta=(c^I_{N+1}-c)/c$. The firm prefers SF as long as $c_{N+1}\le(1+\Delta)c$.

The $\alpha$-expected shortfall of a random variable $Z$ is, for $\alpha\in(0,1)$ and the lower quantile $x_{(\alpha)}=\inf\{x:\mathbb P(Z\le x)\ge\alpha\}$,

$$ES_\alpha(Z)=-\frac1\alpha\Big(\mathbb E\big[Z\mathbf 1\{Z\le x_{(\alpha)}\}\big]+x_{(\alpha)}\big(\alpha-\mathbb P(Z\le x_{(\alpha)})\big)\Big).$$

Formalization targets

Goal: Proposition 1

For any demand random vector $\tilde X$:

1. $\Delta_{RN}\ge 0$ for all $0\le\theta\le 1$, that is, SF is preferred whenever $c_{N+1}\le c$;

$$0\le\theta\le\frac{\lambda c}{p-(1-\lambda)c}\ \Longrightarrow\ \Delta_{RN}=0;$$

3. $\Delta_{RN}=0$ if $\rho_X=\mathbf 1$, i.e. all pairwise demand correlations equal $1$.

No distributional form of demand is fixed and no constant is hard-coded beyond the paper's threshold.

Milestones

• (9): the closed form of $V^{SF}_{RN}$.
• (10)–(11), (12)–(13): the optimal investments are critical fractiles

$$F_{X_{N+1}}(K^*_{N+1})=1-\frac{(\lambda+(1-\lambda)\theta)c_{N+1}}{\theta p},\qquad F_{X_n}(K^*_n)=1-\frac{(\lambda+(1-\lambda)\theta)c}{\theta p},$$

and the optimal values are $\theta p$ times partial expectations of demand.

• (A-1) in expected-shortfall form: with $\alpha=1-(\lambda+(1-\lambda)\theta)c/(\theta p)\in(0,1)$,

$$V^{SF,*}\ge V^{SD,*}\ \text{at}\ c_{N+1}=c\iff \alpha\Big(\sum_n ES_\alpha(\tilde X_n)-ES_\alpha\Big(\sum_n\tilde X_n\Big)\Big)\ge 0 .$$

• Subadditivity of $ES_\alpha$ (Acerbi and Tasche 2002).
• The positivity threshold of part 2: investing is worthwhile iff $\theta>\lambda c/(p-(1-\lambda)c)$.
• Correlation $1$ implies $\tilde X_n=a\tilde X_1+b$ with $a>0$, and $ES_\alpha(aX+b)=aES_\alpha(X)-b$.

Significance

Proposition 1 separates the two effects of flexibility under unreliable supply. It shows that for a risk-neutral firm the demand-pooling benefit together with an upside effect of aggregation (one flexible resource succeeds more often than all dedicated ones together) always outweighs the downside aggregation risk. Even with no pooling benefit at all (perfectly correlated demand) the firm is indifferent, not averse. The later results of the paper (loss aversion, CVaR, dual sourcing) are measured against this baseline: a negative premium can appear only once the firm is risk-averse. The expected-shortfall form links newsvendor optimal values to a coherent risk measure, a connection that recurs in inventory risk analysis.

The result is proved in the paper, with a proof that cites Acerbi and Tasche (2002) for two properties of expected shortfall. No machine-checked version exists. A formalization adds three things: a proof for general demand distributions (the paper assumes a joint density and uses the continuous form of expected shortfall); a Lean development of Acerbi–Tasche expected shortfall for general integrable random variables, including subadditivity and affine equivariance; and a reusable model of newsvendor networks with Bernoulli yields and committed costs.

Difficulty

The newsvendor steps (9)–(13) are single-variable concave optimization, but they must be done without a density: the distribution function of total demand may have atoms and flat pieces, so the critical fractile need not be attained or may be attained on an interval, and optimal values must be expressed through lower quantiles. Subadditivity of expected shortfall is the heart of part 1 and is not elementary in the general (atomic) case, which is exactly why the correction term $x_{(\alpha)}(\alpha-\mathbb P(Z\le x_{(\alpha)}))$ appears. Part 3 requires identifying correlation $1$ with almost-sure positive affine dependence, which rests on the equality case of the Cauchy–Schwarz inequality in $L^2$, and then handling nonnegativity constraints on the investments that the affine change of variables may violate. The obvious shortcut of computing everything from densities is not available, because the goal is stated for every demand vector and part 3 is incompatible with a joint density when $N\ge 2$.

Formalization scope

Randomness lives on one probability space $(\Omega,\mu)$; demand is X : Ω → Fin N → ℝ and yields are Y : Ω → Fin (N + 1) → ℝ, where dedicated resource $n$ is Fin.castSucc n and the flexible resource $N+1$ is Fin.last N. Expectations are Bochner integrals and probabilities are μ.real. The standing assumptions are: $p>0$, $c>0$, $\lambda,\theta\in[0,1]$; demands measurable, almost surely nonnegative and integrable (integrability is needed for expected shortfall and makes every profit integrable); yields measurable, $\{0,1\}$-valued almost surely with $\mathbb P(\tilde Y_j=1)=\theta$, mutually independent, and independent of demand (the paper states the last in Appendix E). The paper's joint density of demand is deliberately not assumed.

The premium $\Delta$ and the indifference cost are not defined as real numbers, because Definition 1's indifference cost need not exist or be unique (for $\theta$ below the threshold both optimal values are $0$ for every $c_{N+1}$ near $c$). "$\Delta\ge 0$" is encoded as "SF is weakly preferred for every $c_{N+1}\le c$", and "$\Delta=0$" as "SF and SD are each weakly preferred to the other at $c_{N+1}=c$". Weak preference $V^{SF,*}\ge V^{SD,*}$ is stated as: every nonnegative SD investment is matched by some nonnegative SF investment; no real supremum is taken. Quantiles $F^{-1}$ in (10) and (12) appear only as parameters with the hypothesis $F(K^*)=$ fractile. Part 3 adds square integrability and positive variances, the conditions under which correlation coefficients exist; the threshold milestone adds almost surely positive demand and $N\ge 1$ for its "if" direction. When $p\le(1-\lambda)c$ the Lean value of the threshold is $\le 0$, so part 2 then covers only $\theta=0$, where it is true.

A formalization that assumed a joint density, took $\Delta$ as a free real satisfying Definition 1, or defined optimal values as real suprema over all of $\mathbb R^N$ would make parts of the goal vacuous or trivial; each is ruled out above.

Needed infrastructure: single-variable newsvendor optimality for general distributions; the Acerbi–Tasche expected shortfall with subadditivity and affine equivariance; the equality case of Cauchy–Schwarz for correlation. The expected-shortfall and correlation lemmas are reusable well beyond this mission, and contributions of them are especially welcome. Out of scope: the loss-averse and CVaR analyses (Propositions 2–3, §3.2–3.3), the perfect-reliability result (Proposition 4, a separate mission), the dual-sourcing networks (§4) and all numerical results.

Selected references

• B. Tomlin and Y. Wang, On the value of mix flexibility and dual sourcing in unreliable newsvendor networks, Manufacturing & Service Operations Management 7(1):37–57, 2005. https://doi.org/10.1287/msom.1040.0063
• C. Acerbi and D. Tasche, On the coherence of expected shortfall, Journal of Banking & Finance 26(7):1487–1503, 2002. https://doi.org/10.1016/S0378-4266(02)00283-2
• C. H. Fine and R. M. Freund, Optimal investment in product-flexible manufacturing capacity, Management Science 36(4):449–466, 1990. https://doi.org/10.1287/mnsc.36.4.449
• J. A. Van Mieghem, Investment strategies for flexible resources, Management Science 44(8):1071–1078, 1998. https://doi.org/10.1287/mnsc.44.8.1071

Motivation

For a convex function on $\mathbb R^n$, a point is a global minimizer as soon as it is a local minimizer — this is one of the earliest and most consequential facts of convex analysis, and it underlies why local-search and gradient methods can certify global optimality in convex programs. The discrete analogue is not automatic: a function on the integer lattice $\mathbb Z^n$ can be "locally optimal" with respect to any fixed finite neighborhood system and still fail to be a global minimizer, unless the function's discrete structure is compatible with that neighborhood in the right way. Identifying exactly which classes of lattice functions admit a local-to-global optimality principle, and with respect to which neighborhood, is one of the organizing questions of discrete convex analysis.

Integrally convex functions, introduced by Favati and Tardella (1990) and developed systematically by Murota, are the most general class of $\mathbb Z^n$-valued functions for which such a principle holds. They are defined purely in terms of the classical convex closure of a real relaxation, which lets one import theorems from ordinary convex analysis, but the resulting notion of local optimality — checking only the $3^n - 1$ neighbors obtained by independently nudging each coordinate by $-1$, $0$, or $+1$ (excluding the trivial no-change case) — is a genuinely discrete, dimension-independent statement about functions whose domain can be arbitrarily large. Almost every discrete convex function class studied later in the book, including M-convex and L-convex functions, is a special case of integral convexity, and this mission's goal theorem is the direct ancestor of the optimality criteria (Theorems 6.26 and 7.14) that drive the algorithms in the rest of the book.

Setting

Let $f : \mathbb Z^n \to \mathbb R \cup \{+\infty\}$ be a function with nonempty effective domain $\operatorname{dom}_{\mathbb Z} f = \{x \in \mathbb Z^n : f(x) \ne +\infty\}$. The convex closure of $f$ is

$$\bar f(x) = \sup_{p \in \mathbb R^n,\, \alpha \in \mathbb R} \{\langle p,x\rangle + \alpha : \langle p,y\rangle + \alpha \le f(y)\ \forall y \in \mathbb Z^n\} \qquad (x \in \mathbb R^n),$$

the pointwise supremum of every affine function minorizing $f$ on all of $\mathbb Z^n$. If $\bar f$ agrees with $f$ on integer points, $f$ is convex extensible. 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,\ 1 \le i \le n\},$$

and the local convex extension $\tilde f$ relaxes $\bar f$'s definition by requiring the affine minorant condition only on $N(x)$ rather than on all of $\mathbb Z^n$. Always $\tilde f \ge \bar f$ pointwise, and the two agree on $\mathbb Z^n$. A function $f$ is integrally convex if $\tilde f = \bar f$ everywhere on $\mathbb R^n$ — equivalently, if $\tilde f$ is a convex function on all of $\mathbb R^n$ (it is automatically convex on every unit cube $[z, z+1]^n$ with $z \in \mathbb Z^n$, but need not be convex globally without this extra condition).

A discrete set $S \subseteq \mathbb Z^n$ is hole free if $S$ equals the set of integer points in its own real convex hull, and $\arg\min f[-p]$ denotes the minimizer set, over $\mathbb Z^n$, of the linearly perturbed function $f[-p](x) = f(x) - \langle p,x\rangle$.

Formalization targets

Goal: Theorem 3.21 (local optimality characterizes global optimality)

For integrally convex $f$ and $x \in \operatorname{dom}_{\mathbb Z} f$:

$$f(x) \le f(y)\ (\forall y \in \mathbb Z^n) \iff f(x) \le f(x + \chi_Y - \chi_Z)\ (\forall\, Y, Z \subseteq \{1,\dots,n\}),$$

where $\chi_Y \in \{0,1\}^n$ is the indicator vector of $Y$. The right-hand side is a check over at most $3^n - 1$ points (each coordinate independently unchanged, incremented, or decremented), regardless of how large $\operatorname{dom}_{\mathbb Z} f$ is; this uniform, dimension-only bound is the entire content of the theorem, and is the weakest correct formulation — restricting to a single $(Y,Z)$ or letting the right-hand side range over all of $\mathbb Z^n$ would trivialize or falsify the equivalence.

Milestones: Propositions 3.18 and 3.19

Proposition 3.18: $f$ convex extensible $\implies$ $\arg\min f[-p]$ hole free for every $p$ (and conversely, when $\operatorname{dom}_{\mathbb Z} f$ is bounded). Proposition 3.19: $f$ is integrally convex if and only if every restriction $f_{[a,b]}$ to a finite integer interval is integrally convex — integral convexity is detectable by looking at bounded pieces of $f$ one at a time.

Significance

The result itself. Theorem 3.21 is what makes integrally convex functions tractable: without it, verifying global optimality on an infinite or exponentially large integer domain would require checking every point. The theorem reduces this to a check whose size depends only on the dimension $n$, not on the size of the domain, and it does so for the widest class of lattice functions for which such a reduction is possible — the class is defined precisely so that this property holds and no wider natural class enjoys it. Every specialized local-optimality theorem later in the book (for M-convex, M$^\natural$-convex, L-convex, and L$^\natural$-convex functions) restricts this same neighborhood-checking principle to a class where the local check can be made even smaller (a single-element exchange rather than a full sign pattern) precisely because those classes are integrally convex plus more.

Formalizing it. No matching item exists on the platform: a direct search for "integrally convex" returns no results, and the theorem's own proof leans on results (Theorem 1.1's local-to-global principle for ordinary convex functions on $\mathbb R^n$, and an LP-duality-based alternate formula for $\tilde f$) that are either classical convex analysis or belong to a different chapter of this same book. The remaining work is therefore to give a complete, correct account of the definitional chain — convex closure, local convex extension, integral convexity — in a form a solver can build a proof from directly, and to state the finite local-check equivalence itself exactly at the strength the book proves it, not a plausible-looking weakening of it.

Difficulty

The natural first attempt is to try to prove the "$\Leftarrow$" direction of Theorem 3.21 by a direct induction on the $\ell^1$-distance to a global minimizer, moving one coordinate at a time. This fails in general lattice functions (a function that is only "coordinatewise convex" can have strict local minima that are not global), and the theorem's actual proof instead routes through the real relaxation: it shows the neighborhood-check hypothesis forces $x$ to be a local minimizer of the local convex extension $\tilde f$ restricted to the unit ball around $x$, then invokes ordinary convex analysis (local minimality implies global minimality for a convex function on $\mathbb R^n$) to conclude $x$ globally minimizes $\bar f$, and finally uses integral convexity ($\tilde f = \bar f$) to transfer this back to $f$ on $\mathbb Z^n$. The identification of $f$'s local behavior with $\tilde f$'s convexity on a single unit cube — rather than any coordinatewise or separable argument — is the step that makes the class of integrally convex functions exactly the right one for this theorem, and is where a naive combinatorial argument breaks down.

Formalization scope

The ground set is $\mathbb Z^n$, represented as Fin n → ℤ; $f$'s codomain is WithTop ℝ (exactly $\mathbb R \cup \{+\infty\}$), while the convex closure $\bar f$ and local convex extension $\tilde f$ take values in EReal (exactly $\mathbb R \cup \{\pm\infty\}$, a complete lattice, so their defining suprema are total functions with no side conditions). A trivializing formalization of the goal would quantify the right-hand side over a single fixed $(Y,Z)$ pair, or over all of $\mathbb Z^n$ instead of the sign-pattern neighbors; both are excluded by keeping $Y, Z$ universally quantified Finset (Fin n) ranging over the full $3^n$ sign-pattern space (minus the trivial case, which the equivalence still holds through vacuously).

Checked against the platform (GET /theorems?q=integrally convex, 0 hits) and against Mathlib's Analysis/Convex/ for the classical facts this chapter's proof would eventually need (ordinary convex-function local-to-global optimality, LP duality): these are broadly available in Mathlib's convex-analysis library in some form, but none of them is imported here, since none appears in the statement of any item this mission drafts — they belong to a proof this pass does not attempt. Contributions to a shared DiscreteConvex.IntegralConvexity definitions layer are welcome from chunks 06–09, which specialize integral convexity to M-convex and L-convex functions and will need the same convex-closure/local-extension vocabulary.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• P. Favati, F. Tardella, "Convexity in nonlinear integer programming," Ricerca Operativa, 53, 1990, pp. 3–44.

Motivation

A multiple objective program asks to maximize $k$ objectives $f_1(x),\dots,f_k(x)$ simultaneously over a feasible set $S$. There is usually no point that is best in every objective, so the object of interest is the set of nondominated criterion vectors: those that cannot be improved in one objective without being worsened in another. Interactive procedures for multiple criteria decision making work by computing nondominated vectors one at a time, by solving a single-objective scalarization, and presenting them to a decision maker.

A scalarization is useful for this purpose only if it is complete (every nondominated vector is the solution of some instance of it) and sound (every solution is nondominated). The weighted-sum scalarization is sound for positive weights but not complete when the feasible region is nonconvex. R. E. Steuer and E.-U. Choo (Math. Programming 26 (1983) 326–344) built their interactive procedure on weighted Tchebycheff distances to an ideal point, following Bowman (1976) and Choo and Atkins (1983). In §3 they treat finite feasible regions with an augmented metric, which requires choosing a small parameter $\rho>0$. In §4 (pp. 334–336) they show that a lexicographic version of the weighted Tchebycheff program is complete and sound for any feasible region, including nonconvex continuous ones, with no parameter to estimate. This mission formalizes that result, Theorems 4.5 and 4.6.

Setting

Let $Z\subseteq\mathbb R^k$, $k\ge1$, be the set of feasible criterion vectors (the image of $S$ under $f=(f_1,\dots,f_k)$). A vector $z$ dominates $\bar z$ if $z_i\ge\bar z_i$ for all $i$ and $z_i>\bar z_i$ for at least one $i$. The nondominated set $N\subseteq Z$ consists of the $\bar z\in Z$ dominated by no $z\in Z$.

An ideal criterion vector is a $z^*\in\mathbb R^k$ with

$$z^*_i=\max\{z_i\mid z\in Z\}+\varepsilon_i,$$

where $\varepsilon_i\ge0$, and $\varepsilon_i>0$ is required whenever (i) more than one nondominated vector maximizes objective $i$, or (ii) the only nondominated vector maximizing objective $i$ also maximizes another objective. So $z^*$ may touch $Z$ in coordinate $i$ only in a controlled way.

The weight set is the simplex $\bar\Lambda=\{\lambda\in\mathbb R^k\mid\lambda_i\ge0,\ \sum_i\lambda_i=1\}$. For $\lambda\in\bar\Lambda$ the weighted Tchebycheff program minimizes $\alpha$ subject to $\alpha\ge\lambda_i(z^*_i-z_i)$ for all $i$ and $z\in Z$; its value at a fixed $z$ is

$$t_\lambda(z)=\max_{1\le i\le k}\lambda_i(z^*_i-z_i).$$

The lexicographic weighted Tchebycheff program first minimizes $t_\lambda$ over $Z$ and then, among the first-stage minimizers, minimizes $e^{\mathsf T}(z^*-z)=\sum_i(z^*_i-z_i)$. The paper writes it as $\min\{P_1\alpha+P_2e^{\mathsf T}(z^*-z)\}$ with pre-emptive priority factors. Finally, for $\bar z\in\mathbb R^k$ the weights $\bar\lambda$ of eq. (4.3) are $\bar\lambda_i\propto1/(z^*_i-\bar z_i)$, normalized to sum to one, when $\bar z_j\ne z^*_j$ for all $j$. When some $\bar z_j=z^*_j$, $\bar\lambda_i$ is $1$ on the coordinates with $\bar z_i=z^*_i$ and $0$ elsewhere.

Formalization targets

Goal: Theorem 4.6 (p. 336)

For compact $Z$, an ideal vector $z^*$ and $\bar z\in Z$,

$$\bar z\in N\iff\exists\,\lambda\in\bar\Lambda\ \text{such that}\ \bar z\ \text{minimizes the lexicographic weighted Tchebycheff program with weights }\lambda .$$

Milestones

1. Proof of Theorem 4.5 (pp. 335–336). For $\bar z\in N$, $\bar\lambda$ as in (4.3) and $\hat\alpha$ the minimal first-stage value,

$$\bar z\in\Phi(\hat\alpha),\qquad N\cap\Phi(\hat\alpha)=\{\bar z\},\qquad \Phi(\hat\alpha)=\{z\mid z_i\ge z^*_i-\hat\alpha/\bar\lambda_i\ \text{when}\ \bar\lambda_i>0\}.$$

2. Theorem 4.5 (p. 335). For $\bar z\in N$: $\bar\lambda\in\bar\Lambda$, and $\bar z$ is the unique minimizer of the lexicographic program with weights $\bar\lambda$.
3. Remark after Theorem 4.6 (p. 336). For every $\lambda\in\bar\Lambda$ the lexicographic program has a minimizer when $Z$ is compact and nonempty, and every minimizer is nondominated.

The goal is the characterization; Theorem 4.5 is the stronger half with uniqueness and an explicit weight.

Significance

Theorem 4.6 says that, as $\lambda$ ranges over the simplex, the lexicographic weighted Tchebycheff program returns exactly the nondominated set, for any feasible region: no convexity, no finiteness, no polyhedral structure. Theorem 4.5 adds that each nondominated vector is the unique output for a weight vector computable from the vector itself, which is what an interactive procedure needs to sample $N$ reliably. The price, as the paper notes, is two optimization stages instead of one; the gain is that no augmentation parameter $\rho$ must be estimated. The result is a standard entry in the textbook treatment of Tchebycheff scalarizations (Steuer, Multiple Criteria Optimization, 1986; Ehrgott, Multicriteria Optimization, 2005).

The result is proved on paper. To our knowledge no machine-checked version exists in Lean or Mathlib, which has no material on Tchebycheff scalarization of multiple objective programs. The formal statements below also pin down two points the printed text leaves loose: the direction of the priority factors, and a closedness assumption that the proof uses without stating it.

Difficulty

The ⇐ direction and the soundness remark are short: a dominating vector is at least as good in the first stage and strictly better in the second. The work is in Theorem 4.5. The obvious argument is that $\bar z$ is the unique minimizer of the first stage with weights $\bar\lambda$; the paper says so. That is true when $\bar z<z^*$ in every coordinate, but false when $\bar z_j=z^*_j$ for some $j$: then $\bar\lambda=e_j$, and every $z\in Z$ with $z_j=z^*_j$ ties with $\bar z$, dominated vectors included. For example, with $Z=\{(5,3),(5,1),(1,10)\}$ and $z^*=(5,10)$, the vectors $(5,3)$ and $(5,1)$ tie. Only the second stage separates them. Showing that it always selects $\bar z$ requires every tied vector to lie below a nondominated vector attaining $z^*_j$, which by the ideal-vector rule must be $\bar z$. That existence step fails for sets that are not closed.

Formalization scope

Criterion vectors are Fin k → ℝ with [NeZero k] ($k\ge1$); objectives are indexed from $0$. $S$, the objectives $f_i$ and the program's variable $\alpha$ are eliminated: $Z$ is a Set (Fin k → ℝ) and the first-stage value is $t_\lambda(z)$ above (the paper's metric uses $|z^*_i-z_i|$, which agrees with $z^*_i-z_i$ on $Z$). $\bar\Lambda$ is Mathlib's stdSimplex ℝ (Fin k). "Minimizes" is global minimization over $Z$; "uniquely minimizes" means every lexicographic minimizer equals $\bar z$ as a criterion vector.

Conventions and added hypotheses:

• The lexicographic program is encoded as the two-stage minimization IsLexMin. The printed "$P_1<<<P_2$" read literally gives the second stage priority; the paper's text on p. 336 and the goal-programming convention it cites give $\alpha$ priority. The two-stage reading is encoded, and the program is not replaced by a weighted sum $P_1\alpha+P_2e^{\mathsf T}(z^*-z)$ with fixed numbers, which would be the augmented program of §3.
• $Z$ compact is an added hypothesis in Theorem 4.5, in the goal, and in the existence half of milestone 3. The paper assumes only that $S$ is bounded, and its "max" in the ideal vector presupposes attainment. Without closedness the weight (4.3) can fail: for $Z=\{(5,3,0),(0,10,0),(0,0,6)\}\cup\{(5,0,4+t):0\le t<1\}$, $z^*=(5,10,6)$ and $\bar z=(5,3,0)\in N$, the program with $\bar\lambda=(1,0,0)$ has no lexicographic minimizer. Closedness is needed by the theorem itself, not only by this proof: adding the points $(5-s^2,\,3+s,\,0)$, $0<s\le1$, to that $Z$ (still bounded, $\varepsilon=0$ still admissible) leaves $\bar z=(5,3,0)\in N$ a lexicographic minimizer for no $\lambda\in\bar\Lambda$, so Theorems 4.5 and 4.6 are false for a bounded, non-closed $Z$. The ⇐ direction, soundness and milestone 1 hold without compactness and are stated without it.
• The ideal vector keeps the paper's $\varepsilon$-rule exactly. Replacing it with a strictly dominating $z^*$ ($\varepsilon>0$ in every coordinate) would remove the case $\bar z_j=z^*_j$ and weaken both theorems; such a formalization does not count.
• In (4.3) and in $\Phi$, division occurs only where the denominator is nonzero. That $\bar\lambda\in\bar\Lambda$ for $\bar z\in N$ is part of Theorem 4.5's conclusion, not an assumption.
• The paper's sentence "the associated weighted Tchebycheff program has a unique solution" (p. 336) is not formalized, since it fails in the tie described above.

Infrastructure needed: dominance and nondominated sets, the ideal vector, the weighted Tchebycheff value, the weights (4.3), and the lexicographic minimizer, all provided as definitions. Proofs will need existence of minimizers of continuous functions on compact sets and a maximal-element argument in the product order on a compact set. Both are reusable for other multiobjective results. Proofs of any item, and faithful statements of Corollaries 4.1 and 4.4 (polyhedral $S$), are welcome.

Selected references

• R. E. Steuer and E.-U. Choo, An interactive weighted Tchebycheff procedure for multiple objective programming, Mathematical Programming 26 (1983) 326–344. https://doi.org/10.1007/BF02591870
• V. J. Bowman, On the relationship of the Tchebycheff norm and the efficient frontier of multiple-criteria objectives, in: Multiple Criteria Decision Making (Jouy-en-Josas 1975), Lecture Notes in Economics and Mathematical Systems 130, Springer, 1976, 76–86. https://doi.org/10.1007/978-3-642-87563-2_5
• E.-U. Choo and D. R. Atkins, Proper efficiency in nonconvex multicriteria programming, Mathematics of Operations Research 8 (1983) 467–470. https://doi.org/10.1287/moor.8.3.467
• A. M. Geoffrion, Proper efficiency and the theory of vector maximization, Journal of Mathematical Analysis and Applications 22 (1968) 618–630. https://doi.org/10.1016/0022-247X(68)90201-1
• M. Ehrgott, Multicriteria Optimization, 2nd ed., Springer, 2005. https://doi.org/10.1007/3-540-27659-9

Motivation

Every financial application in the rest of this book — terminal wealth maximization, portfolio choice with consumption, index tracking, hedging — takes as given that the underlying market admits no risk-free profit: an arbitrage opportunity. Ruling this out is not a modeling nicety but a structural necessity, since a market with arbitrage has no sensible notion of a fair price at all. Bäuerle and Rieder's Chapter 3 fixes the discrete- and continuous-time market vocabulary the rest of the book builds on, and proves the one structural fact about no-arbitrage that the later chapters actually invoke: that the whole-horizon, global absence of arbitrage is equivalent to a much simpler one-period condition, checked separately at each stage. This reduction — not the deeper fundamental theorem of asset pricing (existence of an equivalent martingale measure), which the book does not prove in this section — is what turns a statement about strategies over the whole time horizon into something checkable stage by stage, exactly the form needed to embed a no-arbitrage assumption into a dynamic-programming argument.

Setting

An $N$-period financial market with $d$ risky assets consists of a probability space $(\Omega,\mathcal{F},\mathbb{P})$ with filtration $(\mathcal{F}_n)_{n=0}^N$, $\mathcal{F}_0$ trivial; a riskless bond with deterministic interest rate $i_n$ on $[n-1,n)$ (so $S^0_n = S^0_{n-1}(1+i_n)$); and $d$ risky assets with relative price changes $\tilde R_n = (\tilde R^1_n,\dots,\tilde R^d_n)$, $\mathcal{F}_n$-measurable and a.s. strictly positive ($S^k_n = S^k_{n-1}\tilde R^k_n$). A portfolio (trading strategy) is an $(\mathcal{F}_n)$-adapted process $\varphi = (\varphi^0_n,\varphi_n)$, $\varphi^0_n \in \mathbb{R}$, $\varphi_n \in \mathbb{R}^d$; $\varphi^k_n$ is the money invested in asset $k$ on $[n,n+1)$. Its value before/after trading at time $n$ is $X_n^- := \varphi^0_{n-1}(1+i_n) + \varphi_{n-1}\cdot\tilde R_n$, $X_n^+ := \varphi^0_n + \varphi_n\cdot e$; $\varphi$ is self-financing if $X_n^- = X_n^+$ a.s. for every interior $n$. An arbitrage opportunity is a self-financing $\varphi$ with $X_0^\varphi = 0$, $X_N^\varphi \geq 0$ a.s., $X_N^\varphi > 0$ with positive probability. The relative risk process $R_n^k := \tilde R_n^k/(1+i_n) - 1$ is the excess return of asset $k$ over the riskless rate.

Formalization targets

Goal — Theorem 3.1.5

$$\text{No arbitrage} \iff \forall\, n < N,\ \forall\, \mathcal{F}_n\text{-measurable } \varphi_n \in \mathbb{R}^d: \quad \varphi_n \cdot R_{n+1} \geq 0 \text{ a.s.} \implies \varphi_n \cdot R_{n+1} = 0 \text{ a.s.}$$

This is the weakest stable statement that captures the reduction: it asserts the equivalence of the global, whole-horizon absence of arbitrage strategies with a one-period static condition on the relative risk vector, without asserting the stronger (and here unproved) existence of a martingale measure.

No further milestone is formalized in this mission: this chapter's only other theorem, Theorem 3.3.1 (binomial-tree weak convergence to Black-Scholes), needs the Skorokhod topology on the space of càdlàg paths, absent from Mathlib and out of scope to construct here — see the Formalization scope section and HARD.md.

Significance

Theorem 3.1.5 is the tool that lets every later chapter's "assume the market has no arbitrage" hypothesis be checked and used one period at a time rather than as a global existential statement over an intractably large space of strategies. It is also the precise, minimal claim this section proves: contrasted with the full fundamental theorem of asset pricing (no arbitrage $\iff$ existence of an equivalent martingale measure, due to Harrison–Kreps 1979 and Dalang–Morton–Willinger 1990 in this discrete-time generality), Theorem 3.1.5 is a strictly weaker, purely measure-theoretic reduction that requires no separating-hyperplane or martingale-measure construction to state (only to prove). The definitions this chunk formalizes alongside it — portfolios, self-financing, arbitrage, and utility functions with the Arrow-Pratt risk-aversion coefficient — are the vocabulary every financial mission of this book (Chapters 4, 6, 9, 11) is built from.

Formalizing it contributes the exact discrete-time, filtration-indexed statement of the reduction — a result absent from the platform (searched "arbitrage", "self-financing", "martingale measure", "utility function"; the one related hit, LinearOptimization.no_arbitrage_iff_state_prices, is a static single-period linear-programming duality statement — no-arbitrage iff nonnegative state prices exist for a fixed return matrix — a different equivalence for a different, non-stochastic model, not reused here).

Difficulty

The direction "local no-free-lunch at every stage $\Rightarrow$ no arbitrage" is the easy one: an arbitrage strategy, unwound via the recursive wealth formula, forces a violation of the local condition at some stage by a stopping-time argument on the first period where the wealth increment is a.s. nonnegative and not a.s. zero. The converse, "an arbitrage opportunity forces the local condition to fail somewhere," is the direction that needs the reduction of the whole-horizon problem to a single period: the natural first attempt (induct forward from $n=0$) does not directly work, because whether a strategy is an arbitrage is a statement about the terminal wealth $X_N$, and a violation at an early stage does not obviously propagate; the book's proof instead identifies, from an arbitrage strategy, the last stage at which the one-period condition fails and constructs a genuinely one-period arbitrage there — an argument that needs care with the a.s.-qualifiers at every step (the difference between "$X \geq 0$ a.s." failing to imply "$X < 0$ with positive probability" only up to null sets is exactly where the measure-theoretic bookkeeping matters).

Formalization scope

The market is represented via DiscreteFinancialMarket, bundling the probability space, filtration, and the two primitives ($i$, $\tilde R$) actually used; price processes $S^0, S^k$ are not separately represented, since they would only be running products of these two primitives with no further role once the relative risk process $R$ is derived. Filtration is represented directly as a monotone family of sub-$\sigma$-algebras with a trivial Fam 0, not via Mathlib's Filtration structure, to avoid instance-juggling that would add no content here. Adaptedness/predictability and the a.s. conditions of every definition are exactly the book's own. Definitions 3.2.1-3.2.2 (the continuous-time portfolio and its self-financing condition, needed by chunk 09b's jump-market model) use an abstract StochasticIntegral operator taken as given data, since Mathlib has no general theory of integration against an arbitrary càdlàg semimartingale (only specific constructions such as Itô integration against Brownian motion); this is a deliberate infrastructure gap flagged for whoever eventually needs to instantiate it, not a hidden simplification of the definition's own content, which states the self-financing equation exactly as the book writes it.

Theorem 3.3.1 is not formalized in this mission and is recorded in HARD.md. The theorem asserts weak convergence of the whole path of the binomial-tree price process to the Black-Scholes-Merton stock price on the Skorokhod space $D[0,T]$ of càdlàg functions with the Skorokhod topology — a materially stronger and more setup-heavy claim than finite-dimensional convergence in distribution, and the book explicitly names this topology (it is not left implicit). Mathlib has no formalization of $D[0,T]$ or the Skorokhod topology, and building either from scratch (the space of càdlàg functions, the Skorokhod metric via time-warpings, the tightness criteria needed for Donsker-type invariance principles) is a substantial undertaking outside the scope of a single milestone; weakening the claim to convergence of finite-dimensional distributions, or silently substituting an unnamed alternative topology (e.g. uniform convergence, under which the claim would in fact be false, since the discretized paths have jumps the limit does not), would misstate the theorem rather than state a smaller piece of it faithfully. A general-purpose Skorokhod-space/Skorokhod-topology formalization in Mathlib — reusable well beyond this book — is the prerequisite contribution that would unlock this result.

No trivializing formalization: NoArbitrage quantifies over all self-financing portfolios (Portfolio M, an unrestricted adapted process, not a finite or parametrized family), and the one-period condition of part b) quantifies over all $\mathcal{F}_n$-measurable $\varphi_n \in \mathbb{R}^d$ — narrowing either quantifier (e.g. to strategies with bounded positions) would state a weaker, easier claim than the book's own theorem.

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
• J. M. Harrison and D. M. Kreps, "Martingales and arbitrage in multiperiod securities markets", Journal of Economic Theory, 1979 (the discrete-time fundamental theorem of asset pricing this chapter's Theorem 3.1.5 is a structural lemma toward, not itself proved in this section).

Motivation

Most concrete applications of Markov Decision Theory — inventory control, cash management, linear-quadratic regulation, sequential games — have data that does not change from one period to the next: the same state space, action space, transition mechanism and reward apply at every stage, only discounted by a fixed factor $\beta$ per period. Bäuerle and Rieder's Chapter 2, §2.5 specializes the general finite-horizon theory of the previous sections to this stationary case, and §2.6 shows the specialization at work on three classical models: a card game with a famously boring answer, a firm's cash-management problem, and stochastic linear-quadratic control. Together they demonstrate the payoff of the abstract theory: once the Structure Assumption is checked for a stationary model, the general machinery (the Forward Induction Algorithm) produces the concrete optimal policy — a critical-level $(s,S)$-type control for cash management, a linear feedback law for LQ control — with no further case-specific argument.

Setting

A stationary Markov Decision Model is a Markov Decision Model $(E,A,D,Q,r,g)$ (Definition 2.1.1) whose data does not depend on the stage: the reward at absolute time $n$ is $\beta^n r$ and the terminal reward at time $N$ is $\beta^N g$, for a fixed discount $\beta \in (0,1]$. For a policy sequence $\pi = (f_0,\dots,f_{n-1}) \in F^n$ (each $f_k$ a decision rule $E \to A$ with $f_k(x) \in D(x)$), the reward-to-go is $J_n^\pi(x) := \mathbb{E}^\pi_x\bigl[\sum_{k=0}^{n-1} \beta^k r(X_k,f_k(X_k)) + \beta^n g(X_n)\bigr]$ and the value function is $J_n(x) := \sup_{\pi \in F^n} J_n^\pi(x)$. The operators $(Lv)(x,a) := r(x,a) + \beta\int v(x')\,Q(dx'\mid x,a)$, $(Tv)(x) := \sup_{a \in D(x)} (Lv)(x,a)$, $(T^f v)(x) := (Lv)(x,f(x))$ are the stationary counterparts of §2.3's non-stationary operators. The (stationary) Structure Assumption (SAN) asks for sets $\mathrm{I\!M} \subseteq \mathrm{I\!M}(E)$, $\Delta \subseteq F$ with $g \in \mathrm{I\!M}$, $v \in \mathrm{I\!M} \Rightarrow Tv \in \mathrm{I\!M}$, and every $v \in \mathrm{I\!M}$ having a maximizer in $\Delta$.

Formalization targets

Goal — Theorem 2.6.2 (the cash balance problem)

A firm's cash level $x \in \mathbb{R}$ moves under i.i.d. shocks; each period the firm transfers to a new level $a$ at linear cost $c(a-x) = c_u(a-x)^+ + c_d(a-x)^-$, pays a convex, coercive holding cost $L(a)$ ($L(0)=0$), and the level becomes $a - Z_{n+1}$. Modeled as a stationary MDM with $E=A=\mathbb{R}$, $r(x,a) = -c(a-x) - L(a)$, $g \equiv 0$:

$$\exists\, S_n^- \le S_n^+ \ \text{(depending on $n$)}: \quad J_n(x) = \begin{cases} (S_n^- - x)c_u + L(S_n^-) + \beta\,\mathbb{E}[J_{n-1}(S_n^- - Z)] & x < S_n^- \\ L(x) + \beta\,\mathbb{E}[J_{n-1}(x-Z)] & S_n^- \le x \le S_n^+ \\ (x-S_n^+)c_d + L(S_n^+) + \beta\,\mathbb{E}[J_{n-1}(S_n^+ - Z)] & x > S_n^+, \end{cases}$$

with $J_0 \equiv 0$, and the optimal policy transfers up to $S_n^-$ below it, down to $S_n^+$ above it, and does nothing in between. This is the weakest stable statement: it asserts the existence of critical levels with the stated recursive characterization, not any closed form for $S_n^\pm$ itself (which depends on $L$'s exact shape and is not computable in general).

Three milestones build toward and alongside it: the Reward Iteration theorem and stationary Structure Theorem (Theorems 2.5.3-2.5.4, the general machinery instantiated), the trivial-but- sharp red-and-black card game (Theorem 2.6.1), and the stochastic linear-quadratic problem (Theorem 2.6.3, a Riccati-type recursion with random coefficients).

Significance

Theorem 2.6.2 is the textbook derivation of $(s,S)$-type control, the dominant policy structure in inventory theory and cash management: a firm should act only when its state leaves a band, and should act to bring it exactly to the band's edge, never further. Its proof pattern — verify (SAN) with $\mathrm{I\!M}$ the convex functions of at most linear growth, extract the critical levels from the derivative conditions of a one-stage minimization — is the template used across the inventory-control literature for essentially every variant of this problem. Theorem 2.6.1's answer ("no strategy beats stopping immediately") is a genuine, if minimal, comparative-statics fact: a positive-content instance of $\mathrm{I\!M}$ collapsing to functions constant on the game's absorbing set, forcing every action to be a maximizer. Theorem 2.6.3's Riccati-type recursion, with random transition coefficients, generalizes the classical deterministic-coefficient LQR (linear-quadratic regulator) of control theory; the recursion governs mean-variance and quadratic-hedging problems return to in later chapters of this book (Chapters 4 and 6).

None of the three examples' specific results were found on the platform (searched for "comparative statics", "convex Markov decision", the exact model names, and "bang-bang"/"LQR" adjacent terms). BertsekasDP.riccati_completion_of_square is the platform's one close relative to Theorem 2.6.3: it solves the deterministic-coefficient LQR by a completion-of-squares argument, not the random-coefficient recursion here, so it is cited as related work rather than reused. The proofs themselves are complete and self-contained in the book (a few pages each, using only single-variable convex analysis and elementary linear algebra); this mission contributes the formal statement of each, in its full generality (general convex $L$, general random $(A,B)$ coefficient pairs), as the task for a sorry-free proof.

Difficulty

The cash-balance proof's central step is showing the minimizer of the one-stage problem is of critical-level form for every $v$ in the candidate class $\mathrm{I\!M}$ — not just for the particular sequence $J_0, J_1, \dots$ that eventually arises. The obvious shortcut, guessing the form of $J_n$ directly and verifying it solves the Bellman equation by substitution, fails because $S_n^-, S_n^+$ are themselves defined only implicitly, via one-sided derivative conditions on $L(x) + \beta\mathbb{E}[v(x-Z)]$; there is no closed form to substitute except in degenerate special cases (e.g. $L$ quadratic). The genuine content is the general argument (convexity of the one-stage objective forces a unique critical-level minimizer structure, and this structure is preserved under $T$) that lets the induction go through for an arbitrary convex, coercive $L$. For Theorem 2.6.3, the natural first attempt — solve the deterministic LQR recursion and substitute expected coefficient matrices for the random ones — is not obviously valid, since $\mathbb{E}[B^\top Q B] \ne (\mathbb{E}[B])^\top Q\,\mathbb{E}[B]$ in general; the correct recursion genuinely involves the joint second moments of $(A,B)$, which is exactly what the standing positive-definiteness assumption on $\mathbb{E}[B^\top Q B]$ (not on $\mathbb{E}[B]$ itself) is there to make precise.

Formalization scope

The stationary vocabulary (StationaryMarkovDecisionModel, its operators, J, (SAN)) is restated independently of chunk 02a's non-stationary vocabulary — drafts in this series cannot import one another, and the book itself keeps the two notationally separate ($J_n$ vs. $V_n$, related by $V_n(x) = \beta^n J_{N-n}(x)$, a relation this mission does not separately formalize since no listed result needs it). Theorem 2.6.3's stochastic LQ problem is explicitly non-stationary in the book's own text, so a second, NS-prefixed restatement of the non- stationary model and value function (via the Bellman recursion established as Theorem 2.3.8, not the sup-over-policies primitive — the same simplification chunk 02c makes for its own V) is introduced solely for that one theorem. The card game (Theorem 2.6.1) is formalized on the concrete state space $\mathbb{N} \times \mathbb{N}$ and action space Bool, with the model's exact transition density, reward and terminal reward given as hypotheses on an abstract StationaryMarkovDecisionModel, matching the book's own discrete-density notation $q(x'\mid x,a) := Q(\{x'\}\mid x,a)$ (introduced in the text following Theorem 2.5.4) rather than built from an explicit PMF/Kernel construction — a lighter-weight but equally precise formalization, since the density equations pin the kernel exactly. The stochastic LQ problem uses Matrix (Fin m) (Fin m) ℝ and needs a MeasurableSpace (Matrix m n α) instance Mathlib does not provide (Matrix is a non-reducible def for m → n → α); this mission supplies it by transport across the definitional equality. Random matrix moments $\mathbb{E}[F(A,B)]$ are computed entrywise as ordinary Bochner integrals against the joint law of $(A,B)$.

A trivializing formalization is ruled out on two fronts: the cash-balance critical levels $S_n^-, S_n^+$ are existentially quantified as functions of $n$, not fixed constants (dropping the index would silently claim a single band works for every horizon length, which is false in general); and the card game's "every strategy is optimal" is stated as a universally-quantified claim over all policy sequences, not weakened to mere existence of an optimal one. Reusable infrastructure: the jointMatMean/xQx helpers and the MeasurableSpace (Matrix m n α) instance are generic and available to any later chunk needing random-matrix moments (none of the remaining chunks' briefs currently list one, but Chapter 4's mean-variance and LQ-flavored missions may). sorry-free proofs of all five items are welcome contributions; Theorem 2.5.3's short inductive proof (unwinding the accumulator definition against the operator-composition recursion) is likely the easiest entry point.

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. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005 (the classical deterministic-coefficient LQR, BertsekasDP.riccati_completion_of_square on the platform).

Motivation

Single-machine sequencing with deferral costs asks how to order jobs when the price of finishing a job depends on when it finishes. A job completed at time $s$ incurs the cost $P_i(s)$; lateness penalties, holding costs and service-level penalties are special cases. Two objectives are standard: the sum of the costs, studied by McNaughton (Management Science 6(1), 1959) and Lawler (Management Science 11(2), 1964), and the maximum cost, the bottleneck objective, which asks that no single job be charged too much.

At the end of his 1968 paper on minimizing the number of late jobs (Moore, Management Science 15(1)), J. M. Moore added a short section, suggested by E. L. Lawler, showing that the maximum-cost problem reduces to a family of feasibility problems with due-dates. Each such problem is settled by one sort, by Jackson's earliest-due-date rule (J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, UCLA Research Report 43, 1955). This reduction is the unconstrained case of what later became Lawler's algorithm for $1|\mathrm{prec}|f_{\max}$ (Lawler, Management Science 19(5), 1973).

Timeline:

• 1955: Jackson shows that ordering jobs by due-date minimizes the maximum tardiness, so a schedule with no late jobs exists iff the due-date order has none.
• 1959, 1964: McNaughton and Lawler study the sum of deferral costs.
• 1968: Moore (this paper) reduces the maximum deferral cost to Jackson's lemma through the generalized inverses $P_i^*$.
• 1973: Lawler's backward rule handles general non-decreasing costs with precedence constraints.

Setting

A finite nonempty set $J$ of jobs is processed on one machine that starts at time $0$ and runs without idle time or preemption. Job $j$ has processing time $t_j \ge 0$. A schedule $S$ is an ordering of $J$ with each job appearing exactly once, and $C_j^S$ is the completion time of $j$ in $S$: the sum of the processing times of $j$ and of every job before it.

Each job has a deferral cost $P_j : \mathbb R \to \mathbb R$, which is continuous, bounded and non-decreasing. The maximum deferral cost of $S$ is

$$\mathrm{maxCost}(S) = \max_{j \in J} P_j(C_j^S).$$

For a cost level $y$, the generalized inverse $P_j^*(y) \in \mathbb R \cup \{+\infty\}$ is the latest time at which job $j$ can be completed at cost at most $y$. Following the paper's definition (p. 108), with times $s \ge 0$:

• $P_j^*(y) = \max\{s \ge 0 : P_j(s) = y\}$ if that level set is nonempty (this includes the paper's case of an existing inverse);
• $P_j^*(y) = 0$ if $P_j(s) > y$ for all $s \ge 0$;
• $P_j^*(y) = +\infty$ if $P_j(s) < y$ for all $s \ge 0$.

For each $y > 0$, $S_D(y)$ is a schedule ordered by the "due-dates" $D_j = P_j^*(y)$, with ties broken arbitrarily. $S_D(y)$ has no late jobs if $C_j^{S_D(y)} \le P_j^*(y)$ for every $j$.

In Lean these are IsSchedule, completionTime, Pstar, NoLateAt and maxCost in the namespace MooreLateJobs.MaxDeferral.

Formalization targets

Goal: $S_D(y^*)$ is optimal

Let $y^* > 0$ satisfy: (1) $S_D(y^*)$ has no late jobs; (2) for every $0 < y < y^*$, $S_D(y)$ has at least one late job. Then for every schedule $S$ of $J$,

$$\mathrm{maxCost}\bigl(S_D(y^*)\bigr) \le \mathrm{maxCost}(S).$$

This is the last sentence of the section (p. 109). The goal takes $y^*$ with its two properties as given, so it needs no hypothesis beyond the model.

Milestones

1. Lemma (Jackson), p. 105: a schedule with no late jobs exists iff every due-date ordering has none. It is stated for extended-real due-dates, which is how the section uses it.
2. Monotonicity of $P_j^*$, p. 109: $y_1 \le y_2 \Rightarrow P_j^*(y_1) \le P_j^*(y_2)$.
3. A feasible level exists, pp. 108–109: for bounded costs there is $y > 0$ with $S_D(y)$ on time.
4. Existence of $y^*$, p. 109 with footnote 3. If some $S_D(y_1)$ is on time and some $S_D(y_0)$ is not, a level $y^*$ with properties (1) and (2) exists.

Significance

The result. The theorem turns a min–max problem over all $n!$ schedules into a monotone one-parameter feasibility question. Each value of $y$ is checked by a single sort, and the optimal level is the threshold where feasibility switches on. The same threshold structure underlies bottleneck scheduling and the backward rule for $1|\mathrm{prec}|f_{\max}$. Special cases include minimizing the maximum lateness, $P_j(s) = s - d_j$, clipped to be bounded, and minimizing the maximum weighted tardiness.

Formalizing it. The result is classical and proved on paper, but no machine-checked proof of it, or of Jackson's lemma, is known to exist. The mission would produce a checked Jackson lemma for extended-real due-dates, a verified generalized inverse of a monotone continuous function with the paper's case analysis, and the threshold argument connecting them. Jackson's lemma is shared with part I of this series (minimizing the number of late jobs).

Difficulty

The reduction is short on paper. The work is in the edge cases that the paper passes over:

• The generalized inverse. The comparison $C_j \le P_j^*(y)$ agrees with $P_j(C_j) \le y$ only away from the corner case $C_j = 0$ with $P_j(0) > y$. That job is never "late", yet its cost exceeds $y$. The goal must still hold when such jobs exist.
• Monotonicity. The monotonicity of $P_j^*$ needs continuity. It fails if times range over all of $\mathbb R$ instead of $s \ge 0$.
• Attainment. The feasible levels form an up-set of $(0,\infty)$. That its infimum is attained, so that $y^*$ exists, needs right-continuity in $y$ of the feasibility of each of the finitely many schedules.
• Jackson's lemma. The exchange argument must handle due-dates equal to $0$ or $+\infty$ and zero processing times.

Formalization scope

Conventions committed to in Lean:

• Jobs form a type ι with decidable equality, and the job set is J : Finset ι, assumed nonempty in the goal. Processing times are t : ι → ℝ with 0 ≤ t i: this is added, because the page never states it but processing times are durations.
• Costs are P : ι → ℝ → ℝ, each continuous, bounded (∃ M, ∀ s, |P i s| ≤ M) and monotone, as on p. 108. The Introduction's assumption $t_i \le D_i$ has no counterpart, since the problem has no given due-dates, and it is not assumed.
• A schedule is a duplicate-free list whose elements are exactly $J$. Completion times are prefix sums of processing times, starting at $0$.
• Pstar f y : EReal, with every time in the definition ranging over $s \ge 0$. If the level set $\{s \ge 0 : f(s) = y\}$ is unbounded, its "max" does not exist, and the value is fixed to $+\infty$. The final case is "otherwise", which for continuous monotone $f$ is the paper's case (c).
• The family $S_D$ is any SD : ℝ → List ι such that SD y is a due-date-ordered schedule for every $y > 0$. Theorems hold for every such family, so every tie-break is covered.
• "For all $y < y^*$" is read as $0 < y < y^*$, because $S_D(y)$ is defined only for $y > 0$.
• The existence milestone takes footnote 3's hypothesis (some feasible level) in place of boundedness. It also takes the added hypothesis that some level $y_0 > 0$ is infeasible: with all costs identically $0$, every $S_D(y)$ is on time and no $y^* > 0$ has property (2).

The goal is not the trivializing statement "every on-time $S_D(y)$ is optimal", which is false for large $y$. It concerns exactly the threshold level $y^*$. The minimum is over all schedules of $J$, not over the $S_D(y)$ only.

The needed infrastructure is list permutations, prefix sums and Finset.sup', plus basic facts about sSup of closed sets bounded above in ℝ, and the intermediate value theorem. The Jackson lemma and the generalized inverse are reusable beyond this mission. Contributions are welcome on any milestone, in any order. The goal depends only on the Jackson lemma and on properties of Pstar.

Not in scope: the remark that $y^*$ "can be found to whatever accuracy is desired by a binary search technique" (computational), and the sum-of-costs problem the section contrasts itself with.

Selected references

• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Sciences Research Project, UCLA, 1955.
• E. L. Lawler, On Scheduling Problems with Deferral Costs, Management Science 11(2):280–288, 1964. https://doi.org/10.1287/mnsc.11.2.280
• R. McNaughton, Scheduling with Deadlines and Loss Functions, Management Science 6(1):1–12, 1959. https://doi.org/10.1287/mnsc.6.1.1
• E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5):544–546, 1973. https://doi.org/10.1287/mnsc.19.5.544

Motivation

Quadratic minimization problems with a combinatorial sign pattern in their Hessian arise throughout applied mathematics: discretizations of elliptic boundary-value problems such as the Poisson equation, resistor-network energy functionals, and the Dirichlet forms of Markov-process potential theory all produce a symmetric matrix whose off-diagonal entries are nonpositive and whose rows are diagonally dominant (Fukushima, Oshima, and Takeda, Dirichlet Forms and Symmetric Markov Processes, De Gruyter, 1994). Such matrices are exactly the diagonally dominant symmetric M-matrices of classical numerical linear algebra (Berman and Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994). Murota's Discrete Convex Analysis (SIAM, 2003) identifies the combinatorial content of this sign pattern with a discrete convexity property — submodularity, and its strengthening translation submodularity — of the associated quadratic form, and shows that passing to the Legendre-Fenchel conjugate of such a quadratic form (i.e., inverting the matrix) transports this property to a dual combinatorial property, an exchange axiom, on the conjugate side. This mission formalizes that correspondence for the special, matrix-algebraic case of quadratic forms — the case in which Murota's book gives a self-contained proof using only the classical Farkas lemma, before generalizing the same conjugacy to a much broader class of functions in Chapter 8.

Setting

Let $V$ be a finite ground set (identified with $\{1,\dots,n\}$ in the book) and let $L = (\ell_{ij})_{i,j\in V}$ be a symmetric real matrix. $L$ has off-diagonal nonpositivity if $\ell_{ij}\le 0$ for all $i\ne j$, and diagonal dominance if $\sum_{j} \ell_{ij}\ge 0$ for every row $i$. The associated quadratic form is $g(p) = \tfrac12 p^\top L p$ for $p \in \mathbb R^V$. For $p,q\in\mathbb R^V$ write $p\vee q$, $p\wedge q$ for the componentwise maximum and minimum. A function $g:\mathbb R^V\to\mathbb R$ is submodular if $g(p)+g(q)\ge g(p\vee q)+g(p\wedge q)$ for all $p,q$, and has translation submodularity if the stronger inequality $g(p)+g(q)\ge g((p-\alpha\mathbf 1)\vee q)+g(p\wedge(q+\alpha\mathbf 1))$ holds for every $\alpha \ge 0$, where $\mathbf 1$ is the all-ones vector (ordinary submodularity is the case $\alpha=0$).

On the conjugate side, for $x\in\mathbb R^V$ write $\operatorname{supp}^+(x)=\{i : x_i>0\}$, $\operatorname{supp}^-(x)=\{i:x_i<0\}$, and let $\chi_i$ denote the $i$-th unit vector ($\chi_0$ denotes the zero vector). A function $f:\mathbb R^V\to\mathbb R$ has the exchange property if for all $x,y\in\mathbb R^V$ and $i\in\operatorname{supp}^+(x-y)$ there exist $j \in \operatorname{supp}^-(x-y)\cup\{0\}$ and $\alpha_0>0$ such that $f(x)+f(y)\ge f(x-\alpha(\chi_i-\chi_j))+f(y+\alpha(\chi_i-\chi_j))$ for every $\alpha\in[0,\alpha_0]$. The Legendre-Fenchel conjugate of $f$ is $f^\bullet(p) = \sup_x\{\langle p,x\rangle - f(x)\}$; two functions $g,f$ are conjugate to each other when $g=f^\bullet$ and $f=g^\bullet$. For positive-definite symmetric $M,L$, the quadratic forms $f(x)=\tfrac12x^\top Mx$ and $g(p)=\tfrac12p^\top Lp$ are conjugate to each other exactly when $M$ and $L$ are matrix inverses of one another.

Formalization targets

Goal (Theorem 2.11). For conjugate strictly convex quadratic forms $g$ and $f$ as above,

$$g \text{ has translation submodularity} \iff f \text{ has the exchange property.}$$

This is the mission's capstone: the statement leaves the correspondence at the level of the two named combinatorial properties, without hard-coding which of the two properties is verified in a given application, so it survives exactly as strongly as the underlying conjugacy fact does.

Supporting milestones, in the order the book develops them: Proposition 2.4 (off-diagonal nonpositivity plus diagonal dominance implies positive semidefiniteness); Proposition 2.6 (off-diagonal nonpositivity is equivalent to plain submodularity of $g$); Theorem 2.7 (the full sign pattern is equivalent to translation submodularity of $g$); Proposition 2.9 (conjugate quadratic forms correspond exactly to inverse matrix pairs); Theorem 2.12 (a nine-way equivalence, for a nonsingular symmetric $M$, among membership in the matrix class $\mathcal L^{-1}$, two sign-consistency inequalities on the columns of $M$ together with their strict forms, two directional-derivative reformulations of the exchange property together with their strict forms, and the exchange property itself together with its strict form); Proposition 2.13 (the Farkas lemma in equality form, together with the strict variant valid for a nonsingular coefficient matrix); and Proposition 2.14 (the class $\mathcal L^{-1}$ is closed under taking principal submatrices).

Significance

The M-natural exchange property is the function-level analogue of the base-exchange axiom for matroids, and translation submodularity is the analogue, on the "primal" side, of ordinary submodularity for set functions; Chapter 2's quadratic-form case is the historical and pedagogical entry point for the general conjugacy Chapter 8 proves for the full M-convex/ L-convex function classes. Establishing it here, in the self-contained matrix-algebraic setting, isolates exactly which properties of a quadratic form are combinatorial (tied to the coordinate axes) rather than purely convex-analytic (rotation-invariant): submodularity and the exchange property are not preserved by an orthogonal change of variables, in contrast to ordinary convexity, which Proposition 2.4 shows the same sign pattern also implies.

Formalizing this mission produces the first Lean statement, in this project's namespace, of a genuine conjugacy theorem between a primal-side and a dual-side combinatorial convexity property for a concrete function class; nothing of this kind is yet proved (or, so far as the platform's own search shows, formalized at all) elsewhere on the platform. The nine-way equivalence of Theorem 2.12 is a substantial independent contribution beyond the goal itself, since it is what makes the goal's proof possible via elementary linear algebra rather than the general convex-analytic machinery Chapter 8 needs.

Difficulty

The naive approach to Theorem 2.11 tries to derive the exchange property for $f$ directly from the defining supremum in the conjugate relation $f = g^\bullet$, differentiating under the sup; this fails because the exchange property compares $f$ along a specific combinatorial direction $\chi_i - \chi_j$ tied to two coordinates, not along an arbitrary direction, and no naive first-order argument isolates the right pair $(i,j)$ without already knowing the sign pattern of $M = L^{-1}$. The book's actual route is Theorem 2.12: it reduces the exchange property to a column-wise sign-consistency statement on $M$ itself (conditions (b)/(c)) via the identity $f'(x;d) = x^\top Md$, and closes the loop back to membership in $\mathcal L^{-1}$ using the Farkas lemma applied to the linear system $ML = I$ — a genuinely matrix-algebraic argument that does not generalize verbatim to non-quadratic M-/L-convex functions, which is exactly why Chapter 8 needs a different (convex-analytic) proof for the general case.

Formalization scope

Vectors and matrices are indexed by a general finite type V ([Fintype V] [DecidableEq V]) rather than a fixed Fin n, matching this project's convention elsewhere and letting Proposition 2.14's principal-submatrix statement reuse the class predicate at the restricted index type directly. Quadratic forms are real-valued ((V → ℝ) → ℝ, using Matrix.mulVec and dotProduct) since this chapter's functions are always finite everywhere; the Legendre-Fenchel conjugate is EReal-valued via sSup, since a supremum over an infinite domain need not be finite in general even though it is finite here. Every min(0, \dots)-based condition in Theorem 2.12 and the exchange axioms is unfolded as the logically equivalent disjunction over the finitely many terms achieving the minimum, rather than reified via Finset.inf/WithTop machinery — a faithful, checked-equivalent simplification, not a narrowing (see MODERATION_NOTES.md). "Nonsingular" is Matrix.det ≠ 0. No numeric constant needs instantiation anywhere in this mission. The formalization does not trivialize: the goal's exchange property is stated for the specific combinatorial direction $\chi_i - \chi_j$ with $i\in \operatorname{supp}^+(x-y)$, $j \in \operatorname{supp}^-(x-y)\cup\{0\}$ — not an arbitrary direction, which would reduce the exchange property to a restatement of ordinary convexity and discard the entire combinatorial content the mission is about.

Infrastructure needed: Matrix.PosDef/Matrix.PosSemidef/Matrix.IsSymm (present in Mathlib); everything else (submodularity, translation submodularity, the exchange axioms, the sign-consistency conditions) is defined fresh in DiscreteConvex.CombinatorialB. A solution to the goal will likely want Proposition 2.9, Theorem 2.12, and the Farkas lemma (Proposition 2.13) as lemmas; contributions completing any of the seven milestones independently, or supplying the Schur-complement induction behind Proposition 2.4, are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 2.
• A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994.
• M. Fukushima, Y. Oshima, M. Takeda, Dirichlet Forms and Symmetric Markov Processes, De Gruyter, 1994.
• J. Farkas, Theorie der einfachen Ungleichungen, J. Reine Angew. Math. 124 (1902), 1–27.