The OR Formalization Drive

Motivation

A decision maker who chooses a portfolio $x\in\mathbb R^n$ of risky assets with random return vector $R$ receives the scalar return $x'R$ and evaluates it by an expected utility $E[u(x'R)]$. In practice the law of $R$ is not known; what can be estimated with some confidence are its mean $\mu$ and covariance $\Sigma$. The robust mean-covariance objective replaces the unknown law by the worst law consistent with these two moments:

$$U(x)=\inf\{E[u(x'R)] : R \text{ has mean } \mu \text{ and covariance } \Sigma\}.$$

Ioana Popescu (Operations Research 55(1), 2007) showed that $U(x)$ depends on $x$ only through $\mu_x=x'\mu$ and $\sigma_x^2=x'\Sigma x$, and that for large classes of utilities it has a closed form or reduces to a one-dimensional search. This turns a robust stochastic program into a parametric mean-variance program, which is the practical point of the paper. This mission formalizes the closed form for concave utilities with a monotone second derivative (Proposition 7), a class that contains the exponential utility $1-e^{-ay}$ and all concave quadratics. The reduction to $(\mu_x,\sigma_x)$ is the subject of the companion mission Robust Mean-Covariance Solutions for Stochastic Optimization I; the two-point case is mission II.

The underlying univariate question is a moment problem in the tradition of Chebyshev-type bounds: the extremal value of $E[u(r)]$ over all laws with prescribed mean and variance. Scarf (1958) solved an instance for a piecewise-linear inventory cost, and Birge and Dulá (1991) treated two-point extremal laws on bounded domains.

Setting

Fix $m\in\mathbb R$ and $s\ge 0$. The mean-variance class $\mathbb M_{(m,s^2)}$ is the set of Borel probability measures $\nu$ on $\mathbb R$ with $\int r^2\,d\nu<\infty$, $\int r\,d\nu=m$ and $\int (r-m)^2\,d\nu=s^2$ (Lean: MeanVarClass m (s ^ 2)). For a utility $u:\mathbb R\to\mathbb R$ the robust objective is

$$U(m,s)=\inf\Big\{\int u\,d\nu : \nu\in\mathbb M_{(m,s^2)}\Big\},$$

with $\min$ read, as in the paper, "in the wide sense of $\inf$", so the value $-\infty$ is allowed. The paper's $U(x)$ is $U(\mu_x,\sigma_x)$.

For $p\in(0,1)$ the two-point law $r_p$ puts mass $p$ on $b=m+\sqrt{(1-p)/p}\,s$ and mass $1-p$ on $a=m-\sqrt{p/(1-p)}\,s$; these are exactly the two-point laws of $\mathbb M_{(m,s^2)}$. Its expected utility is the two-point objective (8),

$$U(p)=p\,u(b)+(1-p)\,u(a)\qquad(\texttt{twoPointValue u m s p}).$$

A supporting quadratic of $u$ is $q(y)=Ay^2+By+C$ with $q\le u$ on $\mathbb R$; the set of their coefficients is $\mathcal Q$. Since every $r\sim(m,s^2)$ has $E[q(r)]=A(m^2+s^2)+Bm+C$, each element of $\mathcal Q$ gives a lower bound on $U(m,s)$ (Proposition 3). The function $u$ has the one-point support property with respect to $(m,s^2)$ (Definition 3, OnePointSupportWrt u m s) if some supporting quadratic touches $u$ at $m$ and $E[u(r_p)]\to E[q(r_p)]$ as $p\to0^+$ or as $p\to1^-$; it has one-point support (OnePointSupport u) if this holds for every $m$ and every $s\ge0$.

Formalization targets

Goal: Proposition 7

Let $u$ be concave and twice differentiable with monotone $u''$.

(a) If $u'$ is convex, then

$$U(m,s)=u(m)+\lim_{y\to-\infty}u''(y)\,\frac{s^2}{2}\qquad\text{for all } m,\ s.$$

(b) If $u'$ is concave, the same holds with $\lim_{y\to+\infty}u''(y)$.

In each part the limit $L$ of $u''$ exists in $[-\infty,0]$. When $L$ is finite the goal asserts that $u$ is integrable under every law of every class, that $u(m)+Ls^2/2$ is the greatest lower bound of the expected utilities, and that $u$ has one-point support. When $L=-\infty$ and $s>0$ it asserts $U(m,s)=-\infty$.

Milestones

1. Display (9): $\partial U/\partial p=u(b)-u(a)-(b-a)\,\frac{u'(b)+u'(a)}{2}$.
2. For convex $u'$ and $s>0$, $U(p)$ is nonincreasing on $(0,1)$.
3. Appendix (4): $\lim_{p\to1^-}U(p)=u(m)+\frac{s^2}{2}\lim_{y\to-\infty}u''(y)$, including the value $-\infty$.
4. Proposition 3: every $E[u(r)]$ dominates every $A(m^2+s^2)+Bm+C$ with $(A,B,C)\in\mathcal Q$.
5. The function $d(y)=\frac{u(y)-u(m)}{(y-m)^2}-\frac{u'(m)}{y-m}$ is nondecreasing on $\{y \neq m\}$ when $u'$ is convex.
6. Appendix (5): $q(y)=\tfrac12u''(-\infty)(y-m)^2+u'(m)(y-m)+u(m)$ supports $u$, and $\inf_{y\ne m}d(y)=\lim_{y\to-\infty}d(y)=\tfrac12u''(-\infty)$.

An additional item states Proposition 8: a monotone convex $u$ has one-point support and $U(m,s)=u(m)$.

Significance

Proposition 7 turns the worst-case expected utility into a mean-variance criterion with an explicit risk weight: a prudent investor ($u'$ convex) is penalized by $\tfrac12\lim_{y\to-\infty}u''(y)$ per unit of variance, an imprudent one by the limit at $+\infty$. With Proposition 1, the robust portfolio problem becomes $\max_x\ u(\mu_x)+\tfrac12 L\,\sigma_x^2$, a concave mean-variance program. For exponential utility the weight is $-\infty$ (Example 3 of the paper), so the robust investor must eliminate variance entirely; this is a qualitative statement about robustness that follows only from the $-\infty$ case of the theorem.

The result is published with a proof in the appendix of the paper. It has, to the best of our search, no machine-checked version, and the platform currently holds no statement of Propositions 3, 7 or 8 or Definition 3. A formal proof would also check two points where the printed argument is incomplete: the proof's step "$\lim_{y\to-\infty}u'(y)=\infty$" fails for affine $u$, where the theorem nevertheless holds, and the claim that $u$ "has one-point support" fails when $\lim u''=-\infty$ (see the scope section). Related platform work on worst-case expectations over ambiguity sets is the mission Wasserstein Distributionally Robust Optimization II, which uses a different ambiguity set.

Difficulty

The infimum ranges over all laws with two prescribed moments, an infinite-dimensional set with no compactness, and in the relevant cases it is not attained. The natural first idea, restricting to two-point laws and minimizing over $p$, gives only an upper bound (display (7)), and here the minimizing $p$ runs off to the boundary: the extremal law puts vanishing mass on a point escaping to $-\infty$. Identifying the limiting value requires controlling $u(m-sq)/(1+q^2)$ as $q\to\infty$, a second-order asymptotic statement about $u$ at $-\infty$. The matching lower bound requires a supporting quadratic whose curvature is exactly $\tfrac12\lim u''$; showing that it lies below $u$ everywhere, not only near $m$, is a global statement that uses the convexity of $u'$ on the whole line. The finite-limit and infinite-limit cases also behave differently: in the second, no supporting quadratic exists at all.

Formalization scope

Laws are Measure ℝ with IsProbabilityMeasure, finite second moment is MemLp id 2, and the class is parameterized by mean $m$ and variance $s^2$ with $s\ge0$. The statements are univariate: $U(x)$ of the paper is the univariate objective at $(\mu_x,\sigma_x)$ by Proposition 1 of the paper (mission I). Derivatives are deriv u and deriv (deriv u); "twice differentiable" is differentiability of $u$ and of $u'$. Limits of $u''$ are explicit hypotheses (Tendsto … atBot (𝓝 L) or Tendsto … atBot atBot), never limUnder. Limits in $p$ are one-sided inside $(0,1)$. Expectations under two-point laws are written by the explicit formula (8).

"Min" is never a real ⨅, which Lean evaluates to $0$ on sets unbounded below. The finite case uses IsGLB together with integrability of $u$ under every law of the class; the infinite case asserts that integrable laws with arbitrarily small expected utility exist; Proposition 3 is stated as "every value $\ge$ every value". Proposition 3 assumes $u$ integrable under the law; Proposition 8 takes the infimum over laws under which $u$ is integrable, which for convex $u$ loses nothing.

One correction to the printed statement: Proposition 7 opens with "then $u$ has one-point support", which is false when $\lim u''=-\infty$, since no quadratic lies below $1-e^{-ay}$ on $\mathbb R$. The formalization asserts one-point support only in the finite-limit case and the value $-\infty$ in the other. A formalization that took $\min$ as a real infimum, dropped the integrability conjunct, or asserted one-point support unconditionally would be either trivially satisfiable or false; none of these is used.

A complete development needs: moments of two-point laws, a second-order l'Hôpital or Taylor argument at $-\infty$, the trapezoid inequality for convex functions, and Jensen-type integration of quadratic lower bounds. The mean-variance class, the two-point objective and the supporting-quadratic lemmas are reusable for mission II and for other moment-problem bounds. Proofs of any milestone, and of part (b), are welcome.

Selected references

• I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• H. Scarf, A min-max solution of an inventory problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• J. R. Birge, J. H. Dulá, Bounding separable recourse functions with limited distribution information, Annals of Operations Research 30, 1991.
• S. Karlin, W. J. Studden, Tchebycheff Systems: With Applications in Analysis and Statistics, Interscience, 1966.

Motivation

Supervisory control theory, introduced by Ramadge and Wonham (SIAM J. Control Optim. 25(1), 1987), models a manufacturing cell, a communication protocol or a resource-sharing system as an automaton whose transitions are events, some of which an external controller may disable. A controller, the supervisor, is itself an automaton that watches the event sequence and, in each of its states, decides which controllable events are currently allowed. The framework is the standard model for logical (untimed) control of discrete event systems and is the subject of textbooks such as Cassandras and Lafortune (Springer, 2008) and Wonham and Cai (Springer, 2019).

A practical concern is supervisor size. The synthesis procedure of the paper (§9) produces a supervisor whose automaton records exactly as much of the past as the desired closed-loop language requires, but there are many other supervisors realising the same behaviour. The paper's second main result, the quotient structure theorem (Theorem 10.1, p. 223), explains how they are related: any supervisor with two natural economy properties is obtained from a canonical one, built on a recognizer of the closed-loop language, by lumping states. This is the structural starting point of the later literature on supervisor reduction.

Setting

A generator is $\mathcal G = (Q, \Sigma, \delta, q_0, Q_m)$: a state set $Q$, a finite alphabet $\Sigma$ of events, a partial transition function $\delta : \Sigma \times Q \to Q$, an initial state $q_0$ and marker states $Q_m \subseteq Q$. Extending $\delta$ to strings gives the generated language $L(\mathcal G)$ (strings along which $\delta$ is defined from $q_0$) and the marked language $L_m(\mathcal G)$ (those that end in $Q_m$). The closure $\bar K$ of a language $K$ is its set of prefixes. Throughout, $\mathcal G$ is trim: $L(\mathcal G) = \bar L_m(\mathcal G)$. A recognizer for a language $K$ is an accessible generator whose marked language is $K$.

A subset $\Sigma_c \subseteq \Sigma$ of events is controllable. A supervisor is $\mathcal S = (S, \phi)$ where $S = (X, \Sigma, \xi, x_0, X_m)$ is an accessible deterministic automaton with possibly infinite state set and $\phi : X \to \{0,1\}^{\Sigma_c}$ is a state feedback map; events outside $\Sigma_c$ are always enabled. The closed loop $\mathcal S/\mathcal G$ runs $S$ and $\mathcal G$ in lockstep and allows $\sigma$ from $(x, q)$ iff $\xi(\sigma, x)$ and $\delta(\sigma, q)$ are defined and $\phi(x)(\sigma) = 1$. Its languages are $L(\mathcal S/\mathcal G)$, $L_m(\mathcal S/\mathcal G)$ (marker set $X_m \times Q_m$) and $L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G) \cap L_m(\mathcal G)$.

$\mathcal S$ is complete if $S$ never refuses an event that the plant can execute and $\phi$ enables: $s \in L(\mathcal S/\mathcal G)$, $s\sigma \in L(\mathcal G)$ and $\phi(\xi(s, x_0))(\sigma) = 1$ imply $s\sigma \in L(\mathcal S/\mathcal G)$. It is proper if it is complete and $\bar L_m(\mathcal S/\mathcal G) = \bar L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G)$.

A projection $\pi : \mathcal S \to \hat{\mathcal S}$ is a surjection $X \to \hat X$ with $\pi(x_0) = \hat x_0$, $X_m = \pi^{-1}(\hat X_m)$, $\hat\xi(\sigma, \pi(x)) = \pi(\xi(\sigma, x))$ wherever $\xi(\sigma, x)$ is defined, and $\hat\phi \circ \pi = \phi$.

For a language $K$, strings $s, s'$ are $\bar K$-equivalent if $st \in \bar K \iff s't \in \bar K$ for all $t$. The automaton $S$ is $\bar K$-reduced if $\bar K$-equivalent strings of $\bar K$ lead to the same state, and $\bar K$-trim if every state is reached by a string of $\bar K$.

Formalization targets

Goal: Theorem 10.1 (quotient structure theorem)

Let $\mathcal S = (S, \phi)$ be complete, $K_1 := L_m(\mathcal S/\mathcal G)$, $K_3 := L(\mathcal S/\mathcal G)$, with $S$ $K_3$-reduced and $K_3$-trim, and let $\hat S^0 = (X^0, \Sigma, \xi^0, x^0_0, X^0)$ be a trim recognizer for $K_3$. Then there are $X^0_m \subseteq X^0$ and $\phi^0$ such that $\mathcal S^0 = ((X^0, \Sigma, \xi^0, x^0_0, X^0_m), \phi^0)$ satisfies

$$\mathcal S^0 \text{ complete},\quad L_m(\mathcal S^0/\mathcal G) = K_1,\quad L(\mathcal S^0/\mathcal G) = K_3,\quad \exists\, \pi : \mathcal S^0 \to \mathcal S,\quad \mathcal S \text{ proper} \Rightarrow \mathcal S^0 \text{ proper}.$$

Milestones

Proposition 8.1 (p. 219): for complete $\mathcal S$ and a projection $\pi : \mathcal S \to \hat{\mathcal S}$, (i) $\pi$ is unique; (ii) $(L_m, L_c, L)(\mathcal S/\mathcal G) = (L_m, L_c, L)(\hat{\mathcal S}/\mathcal G)$; (iii) $\hat{\mathcal S}$ is complete; (iv) nonblocking, nonrejecting and proper transfer in both directions.

The displayed steps of the proof of Theorem 10.1 (pp. 223–224): $\pi(\xi^0(s, x^0_0)) := \xi(s, x_0)$ is well defined on $X^0$; it is a projection once $X^0_m := \pi^{-1}(X_m)$ and $\phi^0 := \phi \circ \pi$; $L(\mathcal S^0/\mathcal G) = K_3$ follows from two enablement conditions; $\mathcal S^0$ is complete; and $L_m(\mathcal S^0/\mathcal G) = K_1$.

Significance

Theorem 10.1 says that the reduction properties the synthesis procedure of §9 guarantees are exactly what makes a supervisor a quotient of the canonical supervisor on a recognizer of $K_3$. Combined with Proposition 8.1, which shows that a projection preserves every closed-loop language, completeness and properness, it identifies supervisors with the same behaviour up to state lumping. This is the basis on which supervisor reduction and the comparison of supervisor realisations rest.

The result is proved in the paper. What this mission produces is a machine-checked version of the model (generators with partial transitions, supervisors with infinite state sets, the closed loop, completeness and properness) and of the two results above. No formalization of Ramadge–Wonham supervisory control was found on Prove2Me at the time of drafting; the definitions of this mission are reusable by any later mission on the theory, including the synthesis results of the first mission of the series.

Difficulty

The mathematics is elementary; the difficulty is bookkeeping with partial functions. Every step compares runs of three automata (the plant, $S$ and the recognizer) that may be undefined at different strings, and a proof must track at each string which of them is defined. The tempting shortcut of treating the projection condition as full commutation, $\hat\xi(\sigma, \pi(x)) = \pi(\xi(\sigma, x))$ for all $\sigma, x$, is not available: the page asks for it only where $\xi(\sigma, x)$ is defined, and Proposition 8.1 (ii) holds only because completeness of $\mathcal S$ compensates for transitions that $\hat\xi$ has and $\xi$ lacks. Likewise, the map $\pi$ of Theorem 10.1 is defined through arbitrary representatives, and its well-definedness uses both that $\hat S^0$ recognizes $K_3$ with all states marked and that $S$ is $K_3$-reduced.

Formalization scope

The alphabet is a Lean type α with [Fintype α] (the page's $\Sigma$, which is Lean syntax); strings are List α, $s\sigma$ is s ++ [σ]. A generator is a structure with its own state type in Type and a partial transition δ : α → Q → Option Q; its extended transition is the left fold. The feedback map has type X → Ec → Bool, and "$\sigma$ enabled at $x$" means $\sigma \notin \Sigma_c$ or $\phi(x)(\sigma) = 1$; the page's $\phi : X \to \{0,1\}^\Sigma$ is the same object under this extension. The closed loop is run from $(x_0, q_0)$ without forming its accessible part, which changes none of its languages. Existential statements over supervisors quantify over state types in Type.

Standing assumptions that are hypotheses of every theorem: $\Sigma$ finite; $\mathcal G$ trim, stated as 𝒢.L = pre 𝒢.Lm; every supervisor automaton accessible. Theorem 10.1 and its proof steps also assume $\mathcal S$ complete, $S$ $K_3$-reduced and $K_3$-trim, and a trim recognizer $R$ for $K_3$ with all states marked, and $\mathcal S^0$ is built on that given $R$ rather than on a recognizer chosen by the prover. The conclusion names $K_1$ and $K_3$ as the languages of $\mathcal S$, not as free variables. A projection predicate that drops $\pi(x_0) = \hat x_0$, surjectivity or the marker equation would make the goal's clause (ii) trivially satisfiable by a constant map; the sanity check shipped with the mission rules this out on the primitive plant of §2.3.

Contributions welcome: proofs of the milestones, lemmas relating the fold-based extended transition to concatenation, and a reusable library for closed-loop runs.

Selected references

• P. J. Ramadge and W. M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. Control Optim. 25(1):206–230, 1987. https://doi.org/10.1137/0325013
• C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems, 2nd ed., Springer, 2008. https://doi.org/10.1007/978-0-387-68612-7
• W. M. Wonham and K. Cai, Supervisory Control of Discrete-Event Systems, Springer, 2019. https://doi.org/10.1007/978-3-319-77452-7

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

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

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

The augmented Lagrangian method (method of multipliers) of Hestenes, Powell and Rockafellar solves a constrained nonlinear program by repeatedly minimizing an unconstrained merit function in the primal variables and then updating the multipliers. For inequality constraints, the augmented Lagrangian in the form the paper takes from Rockafellar (Rockafellar 1981) is continuously differentiable but not twice differentiable, even when all problem data are smooth: its Hessian jumps across the surfaces where a constraint switches between the "active" and "inactive" formula. Newton's method for the inner minimization therefore has no classical Hessian to work with on those surfaces.

Qi and Sun (Math. Programming 58, 1993) extended Newton's method to equations $F(x) = 0$ with $F$ locally Lipschitz, replacing the Jacobian by an element of Clarke's generalized Jacobian, and proved local superlinear convergence when $F$ is semismooth. Section 4 of the paper, an example suggested by Rockafellar, shows that the gradient of the augmented Lagrangian of a $C^2$ program is semismooth, so the nonsmooth Newton method applies to the stationarity equation $\nabla L_r = 0$. This mission formalizes that result, Theorem 4.1.

Setting

Let $f_0, f_1, \dots, f_m : \mathbb{R}^n \to \mathbb{R}$ be of class $C^2$ and consider

$$\text{(NLP)}\quad \min f_0(x)\ \text{ s.t. }\ f_i(x) = 0,\ i = 1,\dots,p,\qquad f_i(x) \le 0,\ i = p+1,\dots,m. \tag{4.1}$$

Fix $r > 0$. For a constraint value $a$ and a multiplier $y$ put

$$\phi(r, a, y) = \begin{cases} y a + \tfrac12 r a^2, & y + r a \ge 0,\\ -\tfrac{1}{2r} y^2, & y + r a \le 0,\end{cases}$$

(the two cases agree when $y + ra = 0$). The augmented Lagrangian is the function of $(x, y) \in \mathbb{R}^n \times \mathbb{R}^m$

$$L_r(x, y) = f_0(x) + \sum_{i=1}^{p}\Big(y_i f_i(x) + \tfrac12 r f_i(x)^2\Big) + \sum_{i=p+1}^{m} \phi\big(r, f_i(x), y_i\big).$$

For a locally Lipschitz map $F$ between finite-dimensional spaces, let $D_F$ be the set where $F$ is differentiable. Clarke's generalized Jacobian is $\partial F(x) = \mathrm{co}\{\lim JF(x_i) : x_i \to x,\ x_i \in D_F\}$. $F$ is semismooth at $x$ if it is locally Lipschitz near $x$ and, for every direction $h$, the limit of $V h'$ over $V \in \partial F(x + t h')$, $h' \to h$, $t \downarrow 0$, exists.

For a single constraint function $g$ the proof works with $\eta(x, s) = \phi(r, g(x), s)$ on $\mathbb{R}^n \times \mathbb{R}$, and with the surface $s + r g(x) = 0$ on which the two formulas for $\phi$ meet.

Formalization targets

Goal: Theorem 4.1

For $r > 0$ and $f_0, \dots, f_m \in C^2$:

$$L_r \in C^1, \qquad \nabla L_r \text{ semismooth at } (x,y) \text{ whenever } \exists\, i > p:\ y_i + r f_i(x) = 0,$$ $$\nabla L_r \in C^1 \text{ near } (x, y) \text{ whenever } y_i + r f_i(x) \neq 0 \text{ for all } i > p.$$

All three clauses are the theorem; the last two together cover every point.

Milestones

1. $\eta \in C^1$, with $\nabla\eta(x,s) = \big((s + r g(x))\nabla g(x),\ g(x)\big)$ if $s + r g(x) \ge 0$ and $(0, -s/r)$ if $s + r g(x) \le 0$, and $\nabla \eta$ is locally Lipschitz.
2. Eq. (4.2): the Hessian of $\eta$ on each side of the surface, and $\nabla\eta \in C^1$ near every point off it.
3. Eq. (4.7): if $\bar s + r g(\bar x) = 0$ and $\bar s + t_j\alpha_j + r g(\bar x + t_j h_j) = 0$ with $h_j \to h$, $\alpha_j \to \alpha$, $t_j \downarrow 0$, then $\alpha + r\nabla g(\bar x)^{\mathsf T} h = 0$.
4. $\nabla\eta$ is semismooth, jointly in $(x, s)$, at every point of the surface.

Significance

The result places the inner problem of the augmented Lagrangian method inside the scope of the paper's convergence theory: with $F = \nabla L_r$, the generalized-Jacobian Newton iteration converges locally superlinearly at a root where every element of $\partial F$ is nonsingular. Its practical content is that second-order methods can be run on $L_r$ even though $L_r$ is only $C^{1}$, with the elements of $\partial \nabla L_r$ playing the role of Hessians. The same pattern (a $C^1$ merit function with semismooth gradient) recurs in extended linear-quadratic programming and in semismooth Newton methods for complementarity problems.

The theorem is proved in the paper by direct computation. As far as a search of the platform showed, none of the objects involved (Clarke's generalized Jacobian, semismoothness, Rockafellar's augmented Lagrangian) has a published formalization there, and Mathlib has none of them. The mission produces a machine-checked version of the computation and, as a by-product, reusable statements about $C^1$ functions obtained by gluing two $C^2$ pieces along a hypersurface.

Difficulty

Clauses 1 and 3 are calculus with a case split: one has to check that the two formulas for $\phi$ and for its gradient match on the surface. Clause 2 is where the argument is not routine. On the surface, $\nabla\eta$ is not differentiable, and the generalized Jacobian $\partial\nabla\eta$ there contains convex combinations of the two one-sided Hessians of (4.2). Semismoothness asks that $V(h', \alpha')$ have a single limit over all such $V$, for all approaches $(h', \alpha') \to (h, \alpha)$, $t \downarrow 0$, including approaches that cross the surface infinitely often. The two one-sided Hessians are different matrices, so no single derivative describes $\nabla\eta$ near the surface, and the existence of the limit must be shown for approaches that alternate between the two sides and for the convex combinations that $\partial\nabla\eta$ contains on the surface itself. General theorems that piecewise-smooth maps are semismooth appear in later literature but are not available in Mathlib, so they cannot be invoked as a shortcut. A second obstacle is infrastructure: Mathlib has no generalized Jacobian, so every fact about $\partial\nabla\eta$ (which limits of derivatives occur near the surface) must be derived from the definition.

Formalization scope

• $\mathbb{R}^n$ and $\mathbb{R}^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); $L_r$ is a function on their product, and $\eta$ on EuclideanSpace ℝ (Fin n) × ℝ.
• The constraint index $i \in \{1,\dots,m\}$ is i : Fin m with paper index i.val + 1; equality constraints are i.val < p, inequality constraints p ≤ i.val. The paper's implicit $p \le m$ is not assumed (for $p > m$ there are no inequality constraints).
• The paper's first sum prints $h(r_i, f_i(x), y_i)$; the single $r$ is used, as in the paper's definition of $h$.
• $\phi$ uses the first branch when $y + ra \ge 0$; the branches agree on the boundary. Every statement assumes $r > 0$.
• $C^2$ is ContDiff ℝ 2 on all of $\mathbb{R}^n$; "smooth" is the paper's continuously differentiable, ContDiffAt ℝ 1 of the gradient at the point.
• $\nabla L_r$ and $\nabla\eta$ are Fréchet derivatives, valued in continuous linear functionals; semismoothness is invariant under the Riesz isometry to gradient vectors and under equivalent norms on the domain (Mathlib's product has the sup norm).
• The Jacobian in Clarke's definition is fderiv, limits are along sequences, and no closure is taken in the convex hull. Semismoothness is the explicit $\varepsilon$–$\delta$ form of the paper's limit, uniform over $V \in \partial F(x + th')$.
• Hessians in (4.2) are stated as the Fréchet derivative of the gradient map applied to a direction.

A formalization that states only $L_r \in C^1$, or only the semismoothness of one term $\eta$, is not Theorem 4.1; the goal contains all three clauses for the full $L_r$. The combination step from the terms $\eta$ to $L_r$ uses that sums of semismooth maps and $C^1$ maps with locally Lipschitz derivative are semismooth; the paper cites this without proof, and a solver will need to prove it.

Contributions welcome: the lemmas above; general facts about clarkeJac (it contains fderiv at points of strict differentiability; it is a singleton for $C^1$ maps; behaviour under sums and linear maps); and the semismoothness of sums.

Selected references

• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
• R. T. Rockafellar, Proximal subgradients, marginal values, and augmented Lagrangians in nonconvex optimization, Mathematics of Operations Research 6 (1981) 427–437. https://doi.org/10.1287/moor.6.3.427
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983 (reprinted SIAM Classics in Applied Mathematics 5, 1990). https://doi.org/10.1137/1.9781611971309
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15 (1977) 959–972. https://doi.org/10.1137/0315061