Operations Research

Motivation

Two of the oldest simplifying assumptions in portfolio theory are that trading is frictionless and that risk means variance. Neither survives contact with practice: every real market charges a transaction cost proportional to the size of a trade, and variance penalizes upside deviations exactly as much as downside ones, which is not what an investor actually fears. Bäuerle and Rieder's §4.5 reopens the multiperiod terminal-wealth problem of chunk 04a with proportional transaction costs added to every trade, and finds that the qualitative shape of the solution survives — a buy/hold/sell rule with explicit thresholds, still obtained from the Structure Theorem of chunk 02a. Their §4.6 then leaves expected-utility maximization altogether and solves the classical Markowitz mean-variance problem in its genuinely dynamic, multiperiod form: choose a self-financing trading strategy that attains a target expected terminal wealth $\mu$ while minimizing the variance of that terminal wealth. This is Markowitz's one-period portfolio selection problem (H. Markowitz, Portfolio Selection, Journal of Finance, 1952) transplanted into a stage-by-stage trading horizon, and it earns its own solution technique: the objective is not linear in the underlying probability measure, so no direct Bellman equation applies, and the chapter instead builds a Lagrangian-embedding argument from scratch. Section §4.7 closes the chapter by replacing variance with the Average-Value-at-Risk, an axiomatically better-behaved risk measure (P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk, Mathematical Finance, 1999), and solves the resulting mean-risk problem in the binomial model by the same Lagrangian route.

Setting

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

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

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

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

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

Formalization targets

Goal — Theorem 4.6.6 (the mean-variance problem)

$$\mathrm{Var}_{x_0}^{\pi^*}[X_N] = \frac{d_0}{1-d_0}\big(\mathbb{E}_{x_0}^{\pi^*}[X_N] - x_0S^0_N\big)^2, \qquad \mathbb{E}_{x_0}^{\pi^*}[X_N] = \mu,$$ $$f_n^*(x) = \Big(\frac{\mu-d_0x_0S^0_N}{1-d_0}\cdot\frac{S^0_n}{S^0_N} - x\Big)\, C_{n+1}^{-1}\,\mathbb{E}[R_{n+1}],$$

where $(d_n)$ is a recursively-defined sequence in $(0,1)$ (Lemma 4.6.4) built from the one-period return moments $C_n,\mathbb{E}[R_n]$. This closes the loop the chapter opens: it is the exact value and optimal strategy of the dynamic mean-variance problem, obtained by specializing the auxiliary problem $QP(b)$'s closed-form solution (Theorem 4.6.5) at the Lagrange multiplier that Lemma 4.6.2's saddle-point argument selects.

Supporting milestones

The Lagrangian route itself: the equivalence of (MV) and its equality-constrained form (Lemma 4.6.1), the saddle-point value identity (Lemma 4.6.2), the reduction of the Lagrange problem $P(\lambda)$ to $QP(b)$ (Lemma 4.6.3), the boundedness of $(d_n)$ (Lemma 4.6.4), and $QP(b)$'s own explicit solution (Theorem 4.6.5) — the four-step argument the goal theorem is the payoff of. Upstream of §4.6: the transaction-cost model's upper bounding function (Proposition 4.5.1), its Structure Assumption via buy/hold/sell decision rules (Proposition 4.5.2), and the resulting explicit three-region optimal policy (Theorem 4.5.4). Downstream: the Two-Fund Theorem (Corollary 4.6.7), and the parallel mean-risk development — the auxiliary problem $P(\lambda,b)$'s solution (Theorem 4.7.1), the binomial value of $P(\lambda)$ (Proposition 4.7.2), and the mean-risk problem's own explicit solution in both orderings of $p$ and $q$ (Theorems 4.7.3 and 4.7.4).

Significance

Theorem 4.6.6 is the multiperiod extension of the single most-used result in portfolio theory: the mean-variance efficient frontier, here derived stage by stage rather than assumed static, and it recovers the classical Two-Fund Theorem (every investor holds the same risky portfolio, scaled by wealth) as an immediate corollary rather than a separate argument. The transaction-cost results answer a standing objection to frictionless portfolio theory by showing that its qualitative conclusions — a threshold trading rule derived from a value function via the same abstract Structure Theorem — survive costs, with the thresholds now depending on the current value function rather than being fixed. The mean-risk results extend the whole technique to a risk measure that, unlike variance, is coherent in the sense of Artzner et al., showing the Lagrangian-embedding method is not an accident of the quadratic case.

None of this chapter's results have machine-checked proofs on Prove2Me at the time of writing (the platform's saddle-point sufficiency results, VectorSpaceOpt.lagrangian_saddle_sufficient_pointed and ConvexOptimization.lagrangian_saddle_iff_strong_duality, are stated over a closed convex cone in a normed vector space, not over the finite-horizon admissible-policy space $F^N$ that Lemma 4.6.2 needs, and were checked and ruled out as reusable for this mission). Formalizing this chapter means building the Lagrangian-embedding argument for a dynamic (rather than static) optimization problem from scratch: no existing platform infrastructure covers a saddle point of a Lagrangian defined over a sequence of Markov policies.

Difficulty

The obvious first attempt at (MV) is to apply the Structure Theorem of chunk 02a directly to the variance objective, exactly as chunk 04a does for expected utility. This fails outright: $\mathrm{Var}_{x_0}^\pi[X_N] = \mathbb{E}_{x_0}^\pi[X_N^2] - (\mathbb{E}_{x_0}^\pi[X_N])^2$ is not additive over time and has no Bellman recursion of the usual form, because the square of an expectation over the whole horizon cannot be decomposed into a sum of one-period rewards. The chapter's actual route — Lagrangian relaxation to $P(\lambda)$, then a further reduction to the quadratic (and hence tractable) $QP(b)$ — is not a shortcut around this obstacle but the only way the mean-variance problem admits a Markov Decision Process reformulation at all. A correct formalization of the goal theorem must go through this exact chain (saddle_point_value, plambda_implies_qp, qp_solution), not around it.

Formalization scope

The financial market and the four named optimization problems (MV), (MV=), $P(\lambda)$, $QP(b)$ are formalized as explicit structures and Prop-valued predicates in MDPFinance.MeanVariance (none of them is a numbered definition in the book — each is introduced only in prose — so each gets its own precise Lean definition rather than being left implicit). Wealth is real-valued, policies are sequences of measurable Markov maps $\mathbb{N}\to\mathbb{R}\to(\mathrm{Fin}\ d\to \mathbb{R})$, and values that can be $\pm\infty$ in the book (the value of $P(\lambda,b)$, of $P(\lambda)$, and of (MR) itself) are typed EReal rather than ℝ, matching the book's own use of infinite values as legitimate outcomes rather than failure states. A formalization that solved the goal theorem by first proving a Bellman equation for $\mathrm{Var}_{x_0}^\pi[X_N]$ directly would not be proving Theorem 4.6.6 — no such recursion exists — and the goal statement is phrased purely in terms of IsOptimalMV, varXN, and meanXN, independent of any intermediate value function, precisely so that only the actual saddle-point argument can discharge it. The transaction-cost model's buy/hold/sell threshold functions $q^-(V_{n+1}),q^+(V_{n+1})$ are represented by their defining maximizing property rather than a closed form, since the book itself only pins them down as an argmax. Reusable beyond this mission: the MVMarket/ MeanRiskMarket structures and the Lagrangian-saddle-point machinery are natural substrate for any later mission that needs a dynamic risk-constrained portfolio problem. Contributions completing any milestone's sorry are welcome, particularly a sorry-free proof of Lemma 4.6.2 (the saddle-point value identity), since it is the one genuinely general technique this mission introduces.

Selected references

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

Motivation

Once a finite-horizon Markov Decision Model (MDM) is known to admit an optimal policy — the existence theory of continuity/compactness models — a natural next question is qualitative: does the optimal value function inherit structural properties (monotonicity, concavity, convexity) of the model's own data, and are the resulting optimal actions themselves monotone in the state? These questions matter beyond aesthetics. A value function known in advance to be concave in wealth, say, restricts the search for an optimizer to a much smaller, better-behaved class of candidates, simplifies numerical solution (dynamic programming over convex functions can exploit shape-preserving approximation schemes), and is often the only handle available for comparative-statics questions — e.g. "if the model's transition mechanism becomes riskier, does the decision-maker's value go down?" — the kind of question that drives applications in inventory theory, insurance, and portfolio choice. The general theory traces to Topkis's lattice-programming approach to comparative statics (Topkis, Supermodularity and Complementarity, Princeton University Press, 1998) and to the stochastic-orders literature (Müller and Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002); Bäuerle and Rieder's Chapter 2, §2.4.4-2.4.5 specializes both to the Borel-space finite-horizon Markov Decision Model of their own Definition 2.1.1.

Setting

Fix a (non-stationary) Markov Decision Model $(E, A, D_n, Q_n, r_n, g_N)_{n=0,\dots,N-1}$ as in Definition 2.1.1: $E$, $A$ measurable spaces, $D_n \subseteq E \times A$ the admissible state-action pairs, $Q_n(\cdot\mid x,a)$ the transition kernel, $r_n$ the one-stage reward, $g_N$ the terminal reward. Write $D_n(x) := \{a \in A : (x,a) \in D_n\}$. An upper bounding function $b : E \to \mathbb{R}_{\geq 0}$ (Definition 2.4.1) is a measurable function for which constants $c_r, c_g, \alpha_b \geq 0$ exist with $r_n^+(x,a) \leq c_r\, b(x)$, $g_N^+(x) \leq c_g\, b(x)$, and $\int b(x')\,Q_n(dx'\mid x,a) \leq \alpha_b\, b(x)$ for all admissible $(x,a)$ and all $n$; $\mathbb{I\!B}_b^+$ is the set of measurable $v : E \to [-\infty,\infty)$ with $v^+ \leq c\, b$ for some $c \geq 0$. The two central operators are $(L_n v)(x,a) := r_n(x,a) + \int v(x')\,Q_n(dx'\mid x,a)$ and $(T_n v)(x) := \sup_{a \in D_n(x)} (L_n v)(x,a)$; a decision rule $f_n$ is a maximizer of $v$ at time $n$ if $(L_n v)(x, f_n(x)) = (T_n v)(x)$ for every $x$. The Structure Assumption (SAN) on families $(\mathrm{I\!M}_n)_{n \leq N} \subseteq \mathrm{I\!M}(E)$ and $(\Delta_n)_{n<N}$ of decision rules says: $g_N \in \mathrm{I\!M}_N$; $v \in \mathrm{I\!M}_{n+1}$ implies $T_n v \in \mathrm{I\!M}_n$; and every $v \in \mathrm{I\!M}_{n+1}$ has a maximizer in $\Delta_n$. It is the single hypothesis from which the whole finite-horizon theory — a well-defined Bellman recursion, an optimal policy built rule-by-rule — follows (established elsewhere in this mission series).

For this section only, $E \subseteq \mathbb{R}^d$ and $A \subseteq \mathbb{R}^m$ carry the usual componentwise order, and the same spaces are given a real vector-space structure when convexity statements are in play; $\mathbb{I\!M}_n^{\diamond}$ denotes $\{v \in \mathbb{I\!B}_b^+ : v$ has property $\diamond\}$ for $\diamond \in \{\text{increasing}, \text{concave}, \text{convex}\}$. A set $D \subseteq E \times A$ is completely monotone (Definition 2.4.15) if $(x,a'), (x',a) \in D$ with $x \leq x'$, $a \leq a'$ forces $(x,a), (x',a') \in D$. A function $f$ on a lattice is supermodular (Definition A.3.1) if $f(x) + f(y) \leq f(x \wedge y) + f(x \vee y)$ for all $x,y$. The comparison theorem below additionally uses three orders between probability measures: the usual stochastic order $\mu \leq_{\mathrm{st}} \nu$ ($\int f\,d\mu \leq \int f\,d\nu$ for every bounded increasing $f$, Definition B.3.2/Theorem B.3.3(ii)), the convex order $\mu \leq_{\mathrm{cx}} \nu$ (same, for convex $f$, Definition B.3.9a), and its concave-function dual $\mu \leq_{\mathrm{cv}} \nu$ (matching $\mathrm{I\!M}_n^{\mathrm{cv}}$; see the Formalization scope section on how the book's own, non-monotone "cv" differs from the increasing-concave order $\leq_{\mathrm{icv}}$ it also uses elsewhere, e.g. in Definition B.3.9c).

Formalization targets

Goal — Theorem 2.4.22 (the convex structure theorem)

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

This is the weakest stable statement: it names exactly the compatibility conditions between the kernel, reward, and terminal payoff that propagate convexity through $T_n$, without committing to any particular model beyond them.

Six further results of the same section are formalized as milestones on the way to, or alongside, the goal: the monotone (increasing) analogue (Theorem 2.4.14), the accompanying result that a largest maximizer under a supermodular $L_n v$ on a completely monotone $D_n$ is itself weakly increasing (Proposition 2.4.16), the concavity-preservation step for $T_n$ and its structure theorem (Proposition 2.4.18, Theorem 2.4.19), the convexity-preservation step together with the existence of a bang-bang maximizer when $A$ is a polytope (Proposition 2.4.21), and the comparison theorem for two models whose kernels are ordered (Theorem 2.4.23).

Significance

Theorems 2.4.14/2.4.19/2.4.22 give three parallel, reusable templates: once a modeler checks three or four structural conditions on $D_n$, $Q_n$, $r_n$, $g_N$ individually — never on the recursively-defined value function itself, which is usually inaccessible in closed form — the corresponding shape of the value function is guaranteed for every horizon, with no further induction needed by the modeler. This is what makes results like the concavity of the optimal consumption-investment value function (used in later chapters of this book) checkable from the market model alone. Proposition 2.4.16's comparative-statics conclusion (optimal actions inherit monotonicity in the state) is the Markov-decision-process incarnation of Topkis's monotone comparative statics, and Theorem 2.4.23 formalizes the intuitive but non-trivial fact that making the transition mechanism "worse" in a precise stochastic-order sense can only lower the optimal value — a comparison that requires the compatibility between the order and the very shape (monotonicity/concavity/convexity) the Structure Assumption already pins down.

All of these results, including the goal, are unformalized on the platform prior to this mission: no result matching "supermodular", "completely monotone", "comparative statics", or a Borel-space convex Markov decision model was found in a platform search at drafting time. The proofs themselves are short (Bäuerle and Rieder give complete, self-contained arguments for every result in this section), so what this mission contributes is the formal statement — getting the exact quantifiers and hypothesis set right in a general Borel/vector-space setting — rather than a technically deep proof; the sorry-free companion proofs are left as the formalization task.

Difficulty

The obvious first idea for the goal is to prove convexity of $T_n v$ by convexity of a supremum of convex functions — true only when $D_n(x)$ does not itself depend on $x$ in a way that mixes domains under a convex combination. The book's own hypothesis (i), $D_n := E \times A$ (constant), is exactly what rules out the general case and makes the argument work: for a genuinely $x$-dependent $D_n(x)$, a convex combination $\alpha(x,a) + (1-\alpha)(x',a')$ need not even have its action component available at the combined state, so "supremum of convex functions is convex" does not apply termwise. A second trap is treating $\mathrm{I\!M}_n^{\mathrm{cv}}$ (closed under concave, not-necessarily-increasing $v$) as if it required the stronger increasing-concave order $\leq_{\mathrm{icv}}$ that the appendix's Definition B.3.9c actually names — the two are different relations, and only the plain "concave-test-function" order is compatible with $\mathrm{I\!M}_n^{\mathrm{cv}}$ as stated (see Formalization scope).

Formalization scope

Because Mathlib's ConvexOn/ConcaveOn require a Module ℝ structure on the codomain, and EReal (needed for value functions that may equal $-\infty$) carries no such structure, this mission introduces ConvexOnEReal/ConcaveOnEReal: the same defining inequality with the real convex-combination coefficients cast into EReal and multiplied there (EReal does carry a Mul). Real-valued convexity/concavity of $r_n$ and $g_N$ uses Mathlib's own ConvexOn/ ConcaveOn directly. "Vertex of a polytope" (Proposition 2.4.21) is formalized via Mathlib's Set.extremePoints, and "$A$ is a polytope" as compact, convex, with finitely many extreme points. The comparison theorem's order $\leq_{\mathrm{cv}}$ has no verbatim numbered definition in the book: Appendix B.3 defines the stochastic order $\leq_{\mathrm{st}}$ (Definition B.3.2, via CDFs, with the increasing-test-function characterization given as an equivalent condition, Theorem B.3.3(ii)) and the convex order $\leq_{\mathrm{cx}}$ (Definition B.3.9a, directly via $\mathbb{E}f(X) \leq \mathbb{E}f(Y)$ for convex $f$), but never a bare "$\leq_{\mathrm{cv}}$" — only the increasing-concave order $\leq_{\mathrm{icv}}$ (Definition B.3.9c). This mission defines $\leq_{\mathrm{cv}}$ as the direct concave-test-function analogue of $\leq_{\mathrm{cx}}$ ($\mathbb{E}f(X) \leq \mathbb{E}f(Y)$ for every concave $f$), matching the book's own $\mathrm{I\!M}_n^{\mathrm{cv}}$ (plain concavity, not required to be increasing) and consistent with the standard "st/cv/cx" triple of Müller and Stoyan (2002), the reference the book cites for this whole appendix section. Likewise $\leq_{\mathrm{st}}$ is formalized directly via Theorem B.3.3(ii)'s functional characterization (bounded increasing test functions) rather than the CDF definition, since Theorem 2.4.23 compares kernels on a general $E \subseteq \mathbb{R}^d$ rather than real-valued random variables. The value function $V_n$ used only in the comparison theorem is given by its recursive characterization ($V_N = g_N$, $V_n = T_n V_{n+1}$, established as this series' Theorem 2.3.8) rather than by re-deriving the sup-over-policies primitive definition and its supporting history/policy machinery, which is not otherwise needed in this mission.

A trivializing formalization is ruled out: taking $E := \mathbb{R}$ throughout would make hypothesis (i) ("$E$ is convex") vacuously true and hide the genuinely restrictive role $D_n = E \times A$ plays in the proof; this mission keeps $E$ (and $A$) as general real vector spaces (with a Preorder added only where monotonicity, rather than convexity, is at stake), so the convexity hypotheses carry their full content. Reusable infrastructure: ConvexOnEReal/ConcaveOnEReal (any later chunk needing shape-preservation results for EReal-valued value functions can reuse the same pattern, restated per this series' convention), and the LEStochasticOrder/LEConcaveOrder/LEConvexOrder triple (reused, restated, by mission 04b's Theorems 4.4.4-4.4.5 and mission 05b's Definition 5.4.9, which need the same or a closely related order). sorry-free proofs of the milestones (all short in the book) are welcome contributions.

Selected references

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

Motivation

Newton's method converges quadratically near a non-degenerate minimum, but on its own it has no global guarantee: far from a minimum the Newton step may not exist or may increase the objective. Nesterov and Polyak (Math. Program. 108 (2006) 177–205) replaced the Newton step by the minimizer of a cubic-regularized second-order model. The resulting method has global complexity bounds on non-convex problems, which the other missions of this series formalize. This mission formalizes the complementary local result, Theorem 3 of the paper. Close to a non-degenerate local minimum, a relaxed version of the method keeps the quadratic rate of the classical Newton method. It no longer needs the safeguards (a lower bound on the regularization parameter and a descent test) that the global analysis relies on.

The cubic-regularized step later became the basis of adaptive cubic regularization (Cartis, Gould and Toint, Math. Program. 127 (2011)). Local quadratic convergence is the property that makes such second-order methods worth their per-iteration cost.

Setting

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3, item 3

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

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

Milestones

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

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

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

Significance

Theorem 3 shows that the cubic-regularized scheme does not lose Newton's local behaviour. Once the iterates enter the region $\{f'' \succ 0,\ \delta \le 1/4\}$, any choice $M_k \in (0, 2L]$ gives a doubly exponential decrease of the gradient norm. The theorem thus supplies the final phase of the paper's complexity estimate (6.1) (Section 6), which counts the iterations until $\delta \le 1/4$ is reached and then adds a last phase of order $\log\log(1/\epsilon)$ steps.

On the formal side, the result is proved in the literature but, as far as a search of the platform shows, not formalized. A complete development yields a machine-checked local convergence theorem for a regularized Newton method under a Lipschitz Hessian. The ingredients include the Taylor bound (2.2), the stationarity system (2.5) of the cubic model, and eigenvalue perturbation bounds for Lipschitz Hessians, and they are reusable for other second-order methods. The published proof of (3.8) contains a gap in its constant (see Difficulty), so a formal proof would also certify the printed constant.

Difficulty

The obvious argument treats $x_{k+1}$ as a Newton step with a small perturbation and invokes the classical Kantorovich-type analysis. That analysis assumes the regularization vanishes. Here $M_k$ can be as large as $2L$, and the step solves a nonlinear system (2.5) in which the step length appears in the operator. The proof must control three coupled quantities at once: the gradient, the smallest Hessian eigenvalue, and the step length. The eigenvalue lower bound has to survive infinitely many steps, so the per-step losses of curvature must be summable, and positive definiteness at the next iterate has to be established before $\delta_{k+1}$ is even defined.

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

Formalization scope

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

The theorem assumes positivity of the Hessian and $\delta \le 1/4$ only at $x_0$. A formalization that assumes $f$ strongly convex, $f''(x) \succ 0$ everywhere, or $\delta_k \le 1/4$ for all $k$, or that imports the lower bound $L_0$ or the descent test of method (3.3), proves a different theorem and is excluded.

Needed infrastructure: the Taylor bound with Lipschitz Hessian, first-order optimality of the non-smooth-looking but $C^1$ cubic model, perturbation bounds for lamMin under operator-norm changes, and the inverse bound $\|(A + cI)^{-1}\| \le 1/(\lambda_n(A) + c)$. These are reusable well beyond this mission. Contributions welcome: proofs of the milestones, and a proof of (3.8) with the printed constant.

Selected references

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

Motivation

Maximizing a nonnegative submodular set function without constraints contains Max Cut, Max Directed Cut and facility-location problems as special cases. In the value-oracle model an algorithm knows nothing about the function except the values $f(S)$ of the sets $S$ it queries, and it is judged by the number of queries it makes. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave constant-factor algorithms in this model and matching limits on what any algorithm can do. For symmetric functions, such as cut functions of undirected graphs, a uniformly random set already achieves $\tfrac12$ of the optimum in expectation (Theorem 2.1 of the paper). The question this mission formalizes is whether any algorithm can do better, and the answer given by Theorem 4.5 is: not without exponentially many value queries. The same factor $\tfrac12$ was later shown to be achievable for general (non-symmetric) nonnegative submodular functions by Buchbinder, Feldman, Naor and Schwartz (FOCS 2012 / SIAM J. Comput. 2015), so the bound of Theorem 4.5 is the tight limit of the whole problem in the value-oracle model.

Timeline:

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 4.5 with the constants of its proof

For every such $n, m$:

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

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

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

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

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

Milestones

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

Significance

The theorem shows that the factor $\tfrac12$ for symmetric submodular maximization, and hence for unconstrained submodular maximization in general, cannot be improved by any algorithm that uses a subexponential number of value queries, whatever its running time. It is an information-theoretic bound and needs no complexity assumption. Along with the later matching $\tfrac12$-approximation, it settles the value-oracle approximability of the problem. The construction, a function equal to a symmetric function on "balanced" sets and larger elsewhere, is the prototype of the symmetry-gap technique used for many later oracle lower bounds.

The result is proved in the paper. No machine-checked version is known to exist: the platform has no value-oracle or query-lower-bound statement. Formalizing it requires a precise model of adaptive randomized query algorithms, a concentration bound for the hypergeometric distribution, and a finite verification of submodularity of an explicit two-regime function, and it fixes the constants that the printed statement leaves as $O(\cdot)$ terms.

Difficulty

Two steps of the printed argument do not go through as written. First, the proof bounds the probability that a fixed query is unbalanced by citing the Chernoff bound for independent variables, but for a uniformly random half-size set $C$ the count $|Q\cap C|$ is hypergeometric, and the summands are not independent. A bound for sampling without replacement is needed instead. Replacing the balanced partition by independent coin flips is not an option: then $|C| \ne n/2$ in general, and the function is no longer the paper's instance.

Second, the argument counts only the queries, but the value an algorithm receives is $f_C$ of its output, which equals $g$ of the output only if the output is balanced as well. That event has to be controlled too.

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

Formalization scope

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

Selected references

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

Motivation

Many polytopes that arise in combinatorial optimization, such as the matching, cut, stable set and travelling salesman polytopes, have exponentially many facets, yet some of them can be written as the linear projection of a polyhedron with far fewer facets. The smallest number of facets of such a lift decides whether the polytope admits a compact linear-programming formulation. Yannakakis (Expressing combinatorial optimization problems by linear programs, J. Comput. System Sci. 43 (1991)) showed that this number equals the nonnegative rank of the polytope's slack matrix, turning a question about formulations into a question about matrix factorizations. Gouveia, Parrilo and Thomas (arXiv:1111.3164v2) extended this correspondence from polytopes and nonnegative orthants to arbitrary convex bodies and closed convex cones.

Exact nonnegative rank is NP-hard to compute (Vavasis, SIAM J. Optim. 20 (2009)), so lower bounds matter. The oldest ones are combinatorial: they see only which entries of the slack matrix are zero. Goemans (Smallest compact formulation for the permutahedron, Math. Program. 153 (2015)) observed that a polytope with $n_C$ faces needs a lift with at least $\log_2 n_C$ facets. Section 4.2 of Gouveia–Parrilo–Thomas recasts these support-based bounds through the face lattice and derives, alongside Goemans' bound, a sharper antichain bound. This mission formalizes that chain of results.

Setting

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

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

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

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

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

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

Formalization targets

Goal: Corollary 4.13 (p. 16)

For a polytope $C$:

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

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

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

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

Milestones

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

Significance

Both bounds depend only on the combinatorial type of the polytope. For a square they give $\operatorname{rank}_+ \ge \log_2 10 \approx 3.32$ and $\operatorname{rank}_+ \ge 4$; for a three-dimensional cube $\log_2 28 \approx 4.81$ and $6$ (p. 16). For the regular $n$-gon, whose slack matrices all have rank $3$, the face-count bound gives $\operatorname{rank}_+ \ge \log_2 n$, which is of the optimal order (Example 4.14). Theorem 4.11 is the statement that the Boolean rank of a slack matrix, also known as its rectangle covering number, is an invariant of the face lattice; the rectangle-covering version is phrased as Theorem 2.9 of Fiorini, Kaibel, Pashkovich and Theis (Combinatorial bounds on nonnegative rank and extended formulations, arXiv:1111.0444), as cited by the paper.

The results are proved in the paper. The formalization provides machine-checked definitions of the polar, the slack operator of a polytope, its nonnegative and Boolean ranks and its face lattice, reusable for later work on extension complexity (for instance, rectangle-covering lower bounds for specific polytopes). No formal proof of these statements is known to exist in Lean or on this platform.

Difficulty

Milestone 1 and the passage from Corollary 4.12 to Corollary 4.13 are short: Sperner's theorem is available in Mathlib as IsAntichain.sperner, and an embedding of $L(C)$ into $2^{[k]}$ is injective. The weight lies in Theorem 4.11, which needs facts about polytopes that Mathlib does not state in this form: every vertex is an exposed point, each extreme point of the polar cuts out a face, every face of a polytope is the convex hull of the vertices it contains, and every proper face is the intersection of the facets containing it, with those facets indexed by $\operatorname{ext}(C^\circ)$. The last fact is where the origin-in-the-interior assumption and the polar enter, and it fails for faces described by an arbitrary list of inequalities that is not the facet description. A second, smaller difficulty is finiteness: the face-count bound needs the set of faces of a polytope to be finite.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with the Euclidean inner product. The polar is the one-sided polar above, not Mathlib's absolute polar. A polytope is the convex hull of a Finset with the origin in its interior; $n = 0$ is allowed ($C = \{0\}$), and all targets hold there. Faces are Mathlib's exposed faces (IsExposed ℝ C F), which include $\emptyset$ and $C$, as the paper's counts do; for a polytope these are all faces. The factorization maps are total functions on $\mathbb{R}^n$ constrained only on extreme points. The nonnegative rank is valued in ℕ∞, the infimum of the empty family being $+\infty$; part (2) of the goal is stated for every finite value of the rank. Part (1) is stated for every antichain of faces, equivalent to the paper's "largest antichain". "Smallest $k$" is sInf of a set of naturals that is nonempty in each case (the set of $k$ with $p \le \binom{k}{\lfloor k/2\rfloor}$, and the set of $k$ admitting an embedding of the finite lattice $L(C)$).

The paper says "lattice embedding". Its proof of Theorem 4.11 constructs, and uses, only a map that preserves and reflects inclusion, and $\varphi(F) = \bigcup_{v \in F} A(v)$ need not preserve joins or meets; the formalization reads "lattice embedding" as an order embedding (Face C ↪o Finset (Fin k)) throughout.

Trivializing formalizations are ruled out: the rank is not a natural-number infimum (which would be $0$ when no factorization exists); faces are not arbitrary subsets of $C$; and an embedding is order-reflecting, not merely monotone (every poset maps monotonically into $2^{[0]}$).

Welcome contributions: a proof of milestone 1; a library of polytope facts (vertices are exposed points, faces are convex hulls of their vertices, finiteness of the face lattice, facets from the polar), which is reusable well beyond this mission; then Theorem 4.11 and the corollaries.

Selected references

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

Motivation

Many optimization problems ask for a subset of a finite ground set that maximizes a submodular function, a set function with diminishing marginal returns. Max Cut and Max Directed Cut in graphs, facility location with fixed costs, and the maximization of mutual information or entropy of a subset of random variables are all of this form. Unlike the monotone case, where a greedy algorithm achieves $1 - 1/e$, a general nonnegative submodular function may decrease when elements are added, and the empty set and the full set can both be poor. The question is how large a constant fraction of the optimum a polynomial-time algorithm can guarantee when the function is given only through an oracle that returns $f(S)$ for a queried set $S$.

Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor algorithms for this problem. A uniformly random set achieves $1/4$ of the optimum, a deterministic local search achieves $1/3 - \epsilon/n$, and a randomized smooth local search achieves $2/5 - o(1)$. The last result is the paper's best approximation for general nonnegative submodular functions (Table 1, p. 1136), and it is the subject of this mission.

Timeline. Feige, Mirrokni and Vondrák: $1/4$, $1/3$ and $2/5$ (FOCS 2007; journal version 2011). Gharan and Vondrák (SODA 2011): about $0.41$ by simulated annealing. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015): a randomized double greedy algorithm achieving $1/2$, which matches the $1/2$ hardness in the value oracle model proved in the same paper by Feige, Mirrokni and Vondrák.

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3.6 in the explicit form of its proof

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

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

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

Milestones, in attack order

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

Significance

The $2/5$ bound showed that local search on a smoothed objective, the multilinear extension restricted to points with two coordinate values, beats both uniform sampling and plain local search for non-monotone submodular maximization. The multilinear extension later became the standard tool for submodular maximization under constraints, through continuous greedy methods, contention resolution schemes and the analysis of randomized rounding. Display (∗) and Lemma 2.2 are the basic sampling inequalities for submodular functions and are reused throughout that literature.

The result is proved in the paper; it has been superseded in ratio by later algorithms reaching $1/2$. To our knowledge none of it is machine-checked: Mathlib has no multilinear extension and no submodular maximization results. This mission produces a checked form of the analysis with every constant explicit: the $o(1)$ as $\frac{9}{5n}$, "polynomial time" as $n^2/\delta$ iterations, and the dependence on the accuracy of the sampled estimates as an explicit hypothesis.

Difficulty

The iteration bound and the increment identity are routine once the multilinear extension is set up. The substance lies in the lower bounds. The returned set $R$ is random, so the comparison with the optimal set $C$ cannot be made through a single local-optimality inequality as in deterministic local search; and approximate local optimality holds only for the smoothed marginals $\omega_{A,\delta}$, which are averages over the random set, not for $f$ at any fixed set. Sampling inequalities such as (∗) are stated for independent samples of arbitrary, possibly overlapping sets, and their expectations are sums over products of subsets; the bookkeeping of such sums is the main formalization burden. The constants must also balance exactly: with $\delta = 1/3$ the $27$ths add up so that the $\frac{9}{10}/\frac{1}{10}$ mixture yields $2/5$. A different split or a different $\delta$ gives a different constant.

Formalization scope

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

The algorithm is a relation, not a choice: any element meeting the step-3 condition may be added, and removal is allowed only when no addition applies. The goal quantifies over every run from $\emptyset$, every choice of accurate estimates, recomputed at every iteration, and every termination point. Accuracy is non-strict ("within $\pm$"); the thresholds are strict. The thresholds and accuracy use $OPT$ itself, as the proof does, although step 1 of the algorithm says an estimate of $OPT$ is used. The sampling that produces the estimates and its "with high probability" are not modelled, and the goal is conditional on accurate estimates. The value of the $\delta' = -1$ branch is written as $\mathbf{E}[f(\mathcal{R}(A,-1))]$, which equals $f(X \setminus A)$.

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

A complete development needs basic calculus of the multilinear extension: affinity in one coordinate, translation $f(\cdot \cup D)$ and restriction $f(\cdot \cap D)$, and splitting a sample into disjoint pieces. These lemmas are reusable for any work on submodular maximization, and contributions of them as separate theorems are welcome. The golden-ratio variant $\delta = \delta'$ (proof omitted in the paper), the tight example and the hardness results of §4 are out of scope.

Selected references

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