The OR Formalization Drive

Motivation

Submodularity — the diminishing-returns property $g(p) + g(q) \ge g(p \vee q) + g(p \wedge q)$ on a lattice — is one of the most useful structural hypotheses in combinatorial optimization, underlying efficient algorithms for network flows, matroid theory, and set-function minimization. Chapter 7 studies L-convex functions: functions on the integer lattice $\mathbb Z^V$ that are submodular and linear along the all-ones direction. This is the "dual" notion, under the conjugacy developed later in the book, to chunk 06's M-convex functions, and it inherits the same strong minimization theory — a purely local optimality criterion and a proximity theorem with an explicit distance bound — while additionally supporting a genuinely new characterization with no M-convex counterpart: discrete midpoint convexity, the direct lattice analogue of the classical real-valued midpoint convexity condition. This mission formalizes the chapter's definitional theorem, its midpoint-convexity characterization, the L-optimality criterion, and the L-proximity theorem itself.

Setting

Let $V$ be a finite ground set. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain is an L-convex function if it satisfies (SBF[Z]): $g(p) + g(q) \ge g(p \vee q) + g(p \wedge q)$ for all $p, q$ ($\vee, \wedge$ componentwise max/min), and (TRF[Z]): there is $r \in \mathbb R$ with $g(p + \mathbf 1) = g(p) + r$ for all $p$, where $\mathbf 1$ is the all-ones vector. An L$^\natural$-convex function is one whose lift to the extended ground set $\{0\} \cup V$ is L-convex; equivalently (Theorem 7.1), $g$ satisfies the translation-submodularity axiom (SBF$^\natural$[Z]): $g(p) + g(q) \ge g((p - \alpha\mathbf 1) \vee q) + g(p \wedge (q + \alpha\mathbf 1))$ for all $p, q$ and all nonnegative integers $\alpha$. Discrete midpoint convexity asks $g(p) + g(q) \ge g(\lceil (p+q)/2 \rceil) + g(\lfloor (p+q)/2 \rfloor)$ componentwise. For $\alpha$ a positive integer, a point satisfies scaled local optimality if $g(p_\alpha) \le g(p_\alpha \pm \alpha \chi_Y)$ for every $Y \subseteq V$.

Formalization targets

Goal: Theorem 7.18 (the L-proximity theorem)

Assume $\alpha$ is a positive integer and $n = |V|$. (1) If $g$ is L-convex with $g(p) = g(p+\mathbf 1)$ for all $p$, and $p_\alpha \in \operatorname{dom} g$ satisfies $g(p_\alpha) \le g(p_\alpha + \alpha\chi_Y)$ for all $Y \subseteq V$, then $\arg\min g \ne \emptyset$ and there is $p^* \in \arg\min g$ with the componentwise bound

$$p_\alpha \le p^* \le p_\alpha + (n-1)(\alpha-1)\mathbf 1.$$

(2) If $g$ is L$^\natural$-convex and $p_\alpha$ satisfies the two-sided version, then there is $p^*$ with $p_\alpha - n(\alpha-1)\mathbf 1 \le p^* \le p_\alpha + n(\alpha-1)\mathbf 1$. The bound is a genuine vector (lattice-order) inequality, not an $\ell^\infty$-norm bound — the form later chapters' applications need.

Milestones: Theorems 7.1, 7.7, 7.14

Theorem 7.1: L$^\natural$-convexity (defined via the lift) is equivalent to the direct translation-submodularity axiom. Theorem 7.7: this same class is also characterized by discrete midpoint convexity — a three-way equivalence with the approach property (L$^\natural$-APR[Z]) as a bridge — giving L-convexity a genuinely different, more geometric face than anything available on the M-convex side. Theorem 7.14 (the L-optimality criterion): global optimality reduces to a purely local check against the sign-pattern neighbors $p \pm \chi_Y$, mirroring chunk 06's Theorem 6.26 but with the plain L-convex case additionally requiring the periodicity condition $g(p) = g(p+\mathbf 1)$.

Significance

The result itself. Discrete midpoint convexity (Theorem 7.7) is philosophically important: it shows the lattice-submodularity definition of L-convexity is not an arbitrary discretization choice but coincides exactly with the most direct discrete analogue of ordinary midpoint convexity, the classical characterization of convex functions via $f((p+q)/2) \le (f(p)+f(q))/2$. The L-optimality criterion and L-proximity theorem give L-convex minimization the same algorithmic footing as M-convex minimization (chunk 06): scaling algorithms for L-convex objectives — which arise naturally from network flow and submodular-function duality — inherit a provable, dimension-and-scale-explicit distance guarantee between a coarse-scale local optimum and the true minimizer.

Formalizing it. No matching item exists on the platform for L-convex functions, discrete midpoint convexity, or the L-optimality/proximity theorems. This mission gives the first formal statement of these results, completing (alongside chunk 06's M-convex-function results) both halves of the exchange-axiom-based theory that chapter 8's conjugacy duality later unifies.

Difficulty

A natural shortcut, given the structural parallel to chunk 06, is to assume the L-proximity theorem's proof is a mechanical relabeling of the M-proximity theorem's proof. It is not: the M-convex proof (chunk 06) crucially uses the exchange axiom's additive four-term inequality to build a chain of strictly improving points, whereas the L-convex proof instead exploits (TRF[Z])'s periodicity directly — it reduces to the case $p_\alpha = 0$ using translation invariance, then constructs a minimal (with respect to the lattice order) point among all sufficiently good solutions and shows this minimality, combined with submodularity (SBF[Z]), forces the componentwise bound. The vector (rather than norm) form of the conclusion is not cosmetic: it is exactly what this lattice-order argument naturally produces, and is the form needed by later chapters' applications.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is (V → ℤ) → WithTop ℝ. Unlike chunk 06's M-convex axiom, (SBF[Z]), (TRF[Z]), and (SBF$^\natural$[Z]) are stated for all of $\mathbb Z^V$, not restricted to $\operatorname{dom} g$, so no explicit import of chunk 05's L-convex-set vocabulary was needed for dom g's structure (unlike the corresponding note in chunk 06's BRIEF.md, which flagged the same concern for dom f). L$^\natural$-convexity is represented via an explicit lift to Option V, matching the book's own primary definition, with the direct axiom (SBF$^\natural$[Z]) kept as a separate object related to it by Theorem 7.1.

A trivializing formalization of the goal would convert its componentwise vector bound into an $\ell^\infty$-norm bound (losing the direction-of-approach information the vector form carries) or drop Part (1)'s periodicity hypothesis $g(p) = g(p+\mathbf 1)$; neither is done here. Propositions establishing dom g as an L-convex set, the L/L$^\natural$ relationship (Theorem 7.3), the submodular-set-function embedding (Proposition 7.4), and several structural closure properties are cut from this mission's scope (see MODERATION_NOTES.md) but are natural targets for a follow-on mission or for chunk 09, which builds directly on this chunk's exchange-axiom vocabulary, mirroring chunks 06→07.

Selected references

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

Motivation

Milgrom and Shannon's theory of quasi-supermodularity, developed for monotone comparative statics in economics, showed that many of the consequences of lattice submodularity survive under a much weaker, purely ordinal relaxation of the defining inequality. Chapter 7's final section imports this idea into discrete convex analysis: does L-convexity's optimality and proximity theory survive when the additive submodularity inequality is relaxed to an ordinal condition on the sign pattern of the two relevant differences, rather than their sum? This mission formalizes the chapter's answer for the strongest of the relevant relaxations, (SSQSB) (semistrict quasi submodularity): yes, and the class is large enough to include every strictly increasing rescaling of an L-convex function — exactly mirroring chunk 07's result for the M-convex side, and completing the "quasi" theory on both halves of the exchange-axiom framework before chapter 8 unifies them under conjugacy.

Setting

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

Formalization targets

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

Let $g$ satisfy (SSQSB) and $g(p) = g(p + \mathbf 1)$ for all $p$, $n = |V|$, $\alpha$ a positive integer. If $p_\alpha \in \operatorname{dom} g$ satisfies $g(p_\alpha) \le g(p_\alpha + \alpha \chi_Y)$ for all $Y \subseteq V$, then $\arg\min g \ne \emptyset$ and there is $p^* \in \arg\min g$ with the componentwise bound $p_\alpha \le p^* \le p_\alpha + (n-1)(\alpha-1) \mathbf 1$ — verbatim the same conclusion, and the same exact bound, as chunk 08's Theorem 7.18(1), now established for the strictly larger class satisfying (SSQSB) rather than (SBF[Z]).

Milestones: Theorems 7.49, 7.53

Theorem 7.49: the full nesting chain (SBF[Z]) $\Rightarrow$ (SSQSB) $\Rightarrow$ (QSB), (SSQSB) $\Rightarrow$ (SSQSBw) $\Rightarrow$ (QSBw), together with the collapse theorem that (SBF[Z]) holds if and only if every linear perturbation of $g$ satisfies (QSBw) — precisely quantifying how weak (QSBw) is pointwise and how the classes reunite under universal perturbation. Theorem 7.53 (the quasi L-optimality criterion): the direct analogue of chunk 08's Theorem 7.14, showing that global (or, for the weaker (QSBw) case, unique-up-to-translation) optimality still reduces to a purely local check against the $2^n - 2$ nontrivial sign-pattern neighbors $p + \chi_X$.

Significance

The result itself. As with the M-convex case (chunk 07), the proximity theorem is what algorithms actually need: an L-convex-flavored objective transformed by any strictly increasing scalar rescaling (a common device — expressing a network-flow cost in a different currency, or applying a monotone risk adjustment) retains a scaling algorithm's correctness guarantee with exactly the same distance bound, even though the rescaled function is generally no longer L-convex itself.

Formalizing it. No matching item exists on the platform for quasi submodularity or quasi L-convexity in any form. Together with chunk 07 (the M-side quasi-convexity theory), this mission completes the "quasi" relaxation on both halves of the exchange-axiom framework the book develops, immediately before chapter 8 unifies M-convexity and L-convexity under a single conjugacy relationship.

Difficulty

As with chunk 07's quasi M-proximity theorem, the temptation is to imitate chunk 08's L-proximity proof line by line. The overall architecture does survive — translate so $p_\alpha = 0$, find a lattice-minimal sufficiently-good point, and bound the gap using submodularity — but chunk 08's proof uses (SBF[Z])'s additive inequality directly to compare four function values at once, while this proof must instead route every such comparison through (SSQSB)'s two one-directional implications (Proposition 7.50's quasi-version of the same two-sided inequality), which only ever license moving in one direction at a time depending on which side of a comparison is tight. The book's proof handles this by working with the specific implications (7.43)–(7.44) in place of the L♮-approach property used in chunk 08's proof — an ordinal substitute for the same additive step, at the cost of a case analysis chunk 08's proof did not need.

Formalization scope

This mission builds directly on chunk 08's published items (SBF, DomZ, ArgMin, IndicatorVec), per the platform's textbook convention that a later chapter section of the same book imports an earlier one's definitions; its own namespace DiscreteConvex.LConvexFunctions.Quasi nests under chunk 08's DiscreteConvex.LConvexFunctions accordingly. Note the sign convention of the linear perturbation here, $g[x](p) = g(p) + \langle p,x\rangle$, is the opposite of the M-side's $f[p](x) = f(x) - \langle p,x\rangle$ (chunks 06–07) — verified against the book's own formula rather than assumed by analogy.

A trivializing formalization of the goal would silently strengthen (SSQSB) back to plain (SBF[Z]) (making this mission redundant with chunk 08's Theorem 7.18) or loosen the exact bound $(n-1)(\alpha-1)$; neither is done. Only (QSB), (SSQSB), (QSBw), (SSQSBw) are drafted, matching exactly what the chosen three items need; the polyhedral L-convex-function bridge (§7.8–7.9, Theorems 7.40–7.46) and the level-set characterizations (Theorems 7.51–7.52) are left for a follow-on mission. Contributions building the 0L ↔ S correspondence (Theorem 7.40, a bridge back to chunk 04's submodular-set-function vocabulary) or the scaled quasi L-minimizer-cut analogue are welcome.

Selected references

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

Motivation

In a combinatorial auction a seller offers $m$ indivisible items to $n$ bidders, each of whom values bundles of items rather than single items. Allocating the items to maximize total value is the basic welfare problem of spectrum auctions, procurement and resource allocation, and it is the running example of algorithmic mechanism design. For general valuations no polynomial-time algorithm achieves a ratio polynomially better than $\sqrt m$ under standard assumptions, so positive results require restricting the valuations. The most natural restriction is complement freeness (subadditivity): a bundle is never worth more than the sum of its parts.

Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010; conference version STOC 2005) gave the first polynomial-time algorithms with sub-polynomial approximation ratios for complement-free bidders given demand oracles. This mission formalizes their Section 3.1 algorithm, which rounds the linear-programming relaxation of the auction and splits the resulting infeasible solution into feasible ones.

Timeline. Lehmann, Lehmann and Nisan (2001) introduced the complement-free hierarchy and treated submodular bidders. The original version of the algorithm formalized here claimed an $O(\log m)$ ratio; Feige observed that the same algorithm achieves $O(\log m/\log\log m)$ and that its ratio is at least $\Omega(\sqrt{\log m/\log\log m})$ (Feige, SIAM J. Comput. 39(1), 2009). Feige then obtained a constant ratio ($2$) for subadditive bidders by a different rounding.

Setting

Items are $M=\{1,\dots,m\}$ and bidders $N=\{1,\dots,n\}$. Bidder $i$ has a valuation $v_i$ assigning a real value $v_i(S)$ to each bundle $S\subseteq M$. Every valuation is normalized, $v_i(\emptyset)=0$, and monotone, $S\subseteq T\Rightarrow v_i(S)\le v_i(T)$. A valuation is complement free if $v(S\cup T)\le v(S)+v(T)$ for all $S,T$. An allocation is a tuple $(S_1,\dots,S_n)$ of pairwise disjoint bundles; its welfare is $\sum_i v_i(S_i)$, and $OPT$ denotes the largest welfare.

The LP relaxation has a variable $x_{i,S}\ge0$ for each bidder and bundle, with $\sum_{i,S\ni j}x_{i,S}\le1$ for each item $j$ and $\sum_S x_{i,S}\le1$ for each bidder $i$; its objective is $\sum_{i,S}x_{i,S}v_i(S)$, with optimum $OPT^*\ge OPT$. Randomized rounding lets each bidder independently draw bundle $S$ with probability $x_{i,S}$ and $\emptyset$ with the remaining probability. The result, a preallocation, has expected welfare $OPT^*$ but may give an item to several bidders.

The algorithm takes $k=\lfloor 3\log m/\log\log m\rfloor$ and:

1. rounds until the preallocation $(S_1,\dots,S_n)$ has every item in at most $k$ bundles and $\sum_i v_i(S_i)\ge OPT^*/3$;
2. splits each $S_i$ into layers $S_i^r$, $r=1,\dots,k$, where $S_i^r$ holds the items of $S_i$ that appear in exactly $r-1$ of $S_1,\dots,S_{i-1}$;
3. picks the layer index $r$ maximizing $\sum_i v_i(S_i^r)$ and sets $T_i=S_i^r$;
4. if some bidder has $v_i(M)\ge\sum_{i'}v_{i'}(T_{i'})$, gives that bidder everything instead.

Formalization targets

Goal: Theorem 3.1, with the explicit ratio

For all sufficiently large $m$, for normalized, monotone, complement-free valuations and an optimal LP solution $x$ with value $OPT^*$:

1. if $OPT^*>3\max_i v_i(M)$, one rounding meets the two conditions of step 1 with probability $>1/6$;
2. from any preallocation meeting them, every admissible run of steps 2–4 outputs an allocation with

$$\sum_i v_i(\text{output}_i)\ \ge\ \frac{OPT}{3k},\qquad k=\Big\lfloor\frac{3\log m}{\log\log m}\Big\rfloor;$$

3. if $OPT^*\le3\max_i v_i(M)$, the bidder maximizing $v_i(M)$ alone achieves $OPT/3$.

Milestones

• $OPT\le OPT^*$ (proof, step (i)).
• The layers of each index form an allocation and partition each $S_i$ (proof, step (ii)).
• Complement freeness gives $\sum_r v_i(S_i^r)\ge v_i(S_i)$, and the best layer has welfare $\ge OPT^*/(3k)$ (proof, step (iii)).
• Lemma 3.1: independent Bernoulli variables with $\sum_i p_i\le1$ exceed $3\log m/\log\log m$ with probability $\le1/m^2$.
• Lemma 3.2: for $X$ a sum of independent $[0,1]$ variables with mean $\mu$, $\Pr[|X-\mu|\ge\alpha]\le\mu/\alpha^2$.
• §3.1.1: some item appears more than $3\log m/\log\log m$ times with probability $\le1/m$; the preallocation's welfare falls below $OPT^*/3$ with probability $<3/4$.

Significance

Theorem 3.1 was among the first polynomial-time approximation guarantees for welfare maximization with general subadditive bidders, and its layering argument is the standard way to turn an LP solution that is feasible up to a factor $k$ into a feasible allocation losing only a factor $k$ for subadditive objectives. The same argument applies to the $k$-duplicates auction and reappears in later rounding schemes. Lemma 3.1 is the standard balls-in-bins tail bound behind every $\log m/\log\log m$ load estimate.

The results are proved in the paper; none of them is formalized, on this platform or in Mathlib, as far as searches show. The mission produces a machine-checked version of the algorithm's guarantee with an explicit constant $3k$ in place of $O(\cdot)$, a precise statement of the probabilistic step, and reusable statements of two concentration inequalities for sums of independent bounded variables.

Difficulty

The combinatorial part (steps (ii) and (iii)) is short. The difficulty is in step (i). The rounding is a product distribution over bundles, while the count of an item is a sum over bidders of indicators that depend on each bidder's whole bundle; connecting the finite product law to independent Bernoulli variables, and then to Lemma 3.1, requires building the independence structure explicitly. Lemma 3.1 itself does not follow from a Chernoff bound with a fixed relative deviation: the threshold $3\log m/\log\log m$ grows with $m$ while the mean stays at most $1$, and the bound must hold uniformly in the number of variables, which a fixed-deviation Chernoff statement does not give. Finally, the event-$B$ bound needs the preallocation's welfare as a sum of independent variables in $[0,1]$, which requires rescaling by $\max_i v_i(M)$ and monotonicity.

Formalization scope

Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity, the paper's standing assumptions (p. 1), are hypotheses of the goal. $\log$ is the natural logarithm; the paper does not fix a base. The rounding law is written as explicit finite sums over profiles $\sigma:\texttt{Fin } n\to\texttt{Finset (Fin } m)$ with product weights, so independence across bidders is literal; Lemmas 3.1 and 3.2 are stated measure-theoretically with Mathlib's iIndepFun.

Explicit constants and conventions that replace the paper's notation:

• The ratio $O(k)=O(\log m/\log\log m)$ is stated as $3k$ with $k=\lfloor3\log m/\log\log m\rfloor$, the constant the proof establishes (step (iii), p. 6). "Sufficiently large $m$" is an existential $m_0$.
• The w.l.o.g. scaling $\max_i v_i(M)=1$ and the split at $OPT^*=3$ become the scale-free split at $OPT^*=3\max_i v_i(M)$.
• The choice of $r$ in step (iii) and of the bidder in step (iv) are universally quantified over all admissible choices.

Printed slips resolved in the statements:

• Lemma 3.1 mixes $n$ and $m$. Here the number of variables is arbitrary, "sufficiently large" refers to $m$, and $\sum_ip_i=1$ is relaxed to $\sum_ip_i\le1$, which is what the application uses.
• The display after Lemma 3.1 writes the threshold $\log m/(3\log\log m)$; the lemma's $3\log m/\log\log m$ is used.
• "$\Pr[\vee_jE_j]<1/n$" and "$\le 1/n+3/4$" should read $1/m$.
• The event $B$ is defined without its sum; it means $\sum_iv_i(S_i)<OPT^*/3$.

Trivializing formalizations are ruled out: the guarantee assumes the item-count bound (without it the layers do not cover the bundles), the probability statements assume an LP-feasible $x$, neither the layer index nor the step-(iv) bidder is fixed, and the ratio is the explicit $3k$ rather than an unspecified constant. Running time, the ellipsoid method and oracle complexity are out of scope. Contributions of general concentration lemmas for sums of independent bounded variables are welcome and reusable beyond this mission.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• U. Feige, On Maximizing Welfare When Utility Functions Are Subadditive, SIAM Journal on Computing 39(1):122–142, 2009. https://doi.org/10.1137/070680977
• B. Lehmann, D. Lehmann, N. Nisan, Combinatorial Auctions with Decreasing Marginal Utilities, Games and Economic Behavior 55(2):270–296, 2006. https://doi.org/10.1016/j.geb.2005.02.006
• M. Mitzenmacher, E. Upfal, Probability and Computing, Cambridge University Press, 2005. https://doi.org/10.1017/CBO9780511813603

Motivation

Chapter 5 characterized L-convex sets — sublattice-closed, translation-periodic subsets of $\mathbb Z^V$ — and showed they interact cleanly with integral convexity. Chapter 7 asks the functional analogue: which functions on the integer lattice deserve to be called convex in the "L" sense, and how do they relate back to L-convex sets? This mission (continuing mission 08-lconvex-functions-i, which built the axioms (SBF[Z])/(TRF[Z])/(SBF$^\natural$[Z]) and proved the L-optimality and L-proximity theorems) answers the second question at its sharpest: an L-convex function is exactly a function whose every weighted-minimizer set is an L-convex polyhedron — the discrete analogue of the fact that a convex function is determined by the convex geometry of its sublevel sets. Along the way it settles the chapter's basic toolkit: operations that preserve L-convexity, the local nature of submodularity, the correspondence with ordinary submodular set functions, and the first two structural facts about the convex extension every L-convex function admits.

Setting

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

Formalization targets

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

For $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with bounded nonempty effective domain: $g$ is L-convex if and only if $\arg\min g[-x]$ is an L-convex set for every $x \in \mathbb R^V$; the L$^\natural$ analogue holds with L$^\natural$-convex sets. This is the direct mirror of mission 23-ch06c-mconvexfunctions's own goal (Theorem 6.43, characterizing M-convex functions via M-convex weighted-minimizer polyhedra) — the book's text calls it exactly "how the concept of L-convex functions can be defined from that of L-convex sets."

Supporting structural targets

Eleven further results build the chapter's basic vocabulary. Theorem 7.2 strengthens translation submodularity to allow negative shifts; Theorem 7.3 places L-convexity inside L$^\natural$- convexity; Proposition 7.4 identifies submodular set functions with a subclass of L$^\natural$-convex functions via the indicator embedding, and Theorem 7.15 derives the classical submodular-minimizer local-optimality criterion as its corollary; Proposition 7.5 shows submodularity is a local property, needing only unit-distance pairs; Proposition 7.8 transfers L-(natural-)convexity from functions to their effective domains; Proposition 7.9 and Theorem 7.10–7.11 give the chapter's basic examples (univariate and pairwise-difference functions) and its six-operation closure toolkit (scaling, affine reparametrization, linear perturbation, projection, infimal convolution with a separable function, and sums), both for L-convex and L$^\natural$- convex functions, the latter also admitting interval and coordinate restrictions; Proposition 7.16 shows minimizer sets of L-convex functions are themselves L-convex, the special case ($x=0$) the goal generalizes to every linear perturbation; Theorem 7.19 begins the convex-extension program this chapter's next chunk completes, establishing that the convex closure agrees with $g$ on $\mathbb Z^V$ and inherits its translation constant.

Significance

The goal is significant for the same structural reason as its M-side counterpart: it says L-convexity is not merely a combinatorial condition on lattice differences but is equivalent to a purely polyhedral-geometric one, closing the loop between chapters 5 and 7 the way Theorem 6.43 closes the loop between chapters 4 and 6. Theorem 7.15's corollary status is itself instructive: the well-known fact that a submodular set function's global minimizer needs only local verification against comparable sets — the theoretical basis of every submodular-minimization algorithm in chapter 10 — falls out of the L-optimality criterion (mission 08-lconvex-functions-i's Theorem 7.14) applied to the indicator embedding, rather than needing an independent proof. Theorem 7.10–7.11's six operations are the toolkit every later construction in this chapter and chapter 9's network transformations builds new L-convex functions from old.

None of these results are open — they are Murota's account of the basic function-level theory of L-convexity, mirroring chapter 6's M-convex function theory chunk-by-chunk. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (SBF, TRF, LNaturalConvex, LConvexSet) that missions 08-lconvex-functions-i and 21-ch05b-lconvexsets began; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to verify L-convexity's submodularity inequality directly against the definition of an L-convex set applied to each minimizer family; the book's actual proof instead routes through Theorem 7.10 (3)'s closure of L-convexity under linear perturbation and Proposition 7.16's minimizer-is-L-convex-set fact for the forward direction, and defers the converse entirely to a later note (Note 7.47, outside this chunk and mission 08's combined range) proved via the integral-convexity machinery of section 7.7 onward. The genuine combinatorial difficulty in this block is upstream, in Theorem 7.10 (5)'s infimal-convolution operation: proving L-convexity of the perturbed function requires a four-term submodularity inequality assembled from the separable function's own convexity and $g$'s submodularity applied at the optimal $q_1,q_2$ simultaneously — a genuine two-hypothesis combination with no single-inequality shortcut.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; L-(natural-)convex functions are (V→ℤ)→WithTop ℝ. All twelve numbered results found in this chunk's page range are placed, with one documented scope reduction: Theorem 7.19 states only parts (3)-(4) (that the convex closure agrees with $g$ on $\mathbb Z^V$ and inherits its translation constant), not the explicit Lovász-extension-formula construction of parts (1)-(2) and (5), which needs a sorted-distinct- component apparatus no other result in this chunk requires — see HARD.md. "$g_U > -\infty$" and its variants are replaced by the equivalent (DomZ ...).Nonempty hypothesis throughout, matching mission 24-ch06d-mconvexfunctions's identical substitution (WithTop ℝ has no $-\infty$ element). This mission's base vocabulary (SBF, TRF, LNaturalConvex, etc.) is redeclared verbatim from mission 08-lconvex-functions-i rather than imported, since sibling drafts in this series cannot yet reference one another; LConvexSet is likewise redeclared from mission 21-ch05b-lconvexsets. Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 7.10 carry the most independent proof content.

Selected references

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

Motivation

In a combinatorial auction a seller offers $m$ indivisible items to $n$ bidders, each of whom values bundles of items rather than single items. Allocating the items so as to maximize the total value (the social welfare) is the central optimization problem of the area: it models spectrum auctions, procurement and resource allocation, and it is NP-hard and hard to approximate for general valuations. A large literature therefore studies restricted classes of valuations without complementarities. Among them the class XOS (valuations that are a maximum of additive valuations, also called fractionally subadditive) sits strictly between submodular and subadditive valuations and has become a standard benchmark class in algorithmic game theory.

Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010) gave, among other results, a randomized algorithm that approximates the optimal welfare for XOS bidders within a factor $1/(1-(1-1/n)^n)$, which is at most $e/(e-1)\approx 1.582$. The algorithm rounds the standard LP relaxation and resolves conflicts between bidders using the XOS structure. This mission formalizes that guarantee (Theorem 3.2 of the paper).

A short timeline: Lehmann, Lehmann and Nisan (EC 2001) introduced the XOS terminology and a 2-approximation for submodular bidders; the conference version of the present paper (STOC 2005) gave the $e/(e-1)$ bound for XOS with demand and XOS oracles; Feige (STOC 2006) extended the $e/(e-1)$ ratio to XOS bidders with demand oracles only and gave a 2-approximation for subadditive bidders.

Setting

Items are $M=\{1,\dots,m\}$ and bidders are $N=\{1,\dots,n\}$ with $n\ge1$. Bidder $i$ has a valuation $v_i$ assigning a real number $v_i(S)$ to every bundle $S\subseteq M$. An allocation is a tuple $(O_1,\dots,O_n)$ of pairwise disjoint bundles; its welfare is $\sum_i v_i(O_i)$.

A clause is an additive valuation $w$ given by nonnegative item values $w_1,\dots,w_m$, with $w(S)=\sum_{j\in S}w_j$. A valuation $v$ is XOS if there is a nonempty finite set $W$ of clauses with

$$v(S)=\max_{w\in W}\ \sum_{j\in S}w_j\qquad(S\subseteq M).$$

A clause of $W$ attaining the maximum for $S$ is a maximizing clause for $S$ in $v$; an XOS oracle returns one (arbitrarily, if several attain it).

The LP relaxation has a variable $x_{i,S}$ for every bidder $i$ and bundle $S$ and asks to maximize $\mathrm{OPT}^*=\sum_{i,S}x_{i,S}v_i(S)$ subject to $\sum_{i}\sum_{S\ni j}x_{i,S}\le1$ for each item $j$, $\sum_S x_{i,S}\le1$ for each bidder $i$, and $x_{i,S}\ge0$.

Randomized rounding draws a preallocation $S_1,\dots,S_n$: independently for each bidder $i$, bundle $S$ is chosen with probability $x_{i,S}$ and the empty bundle with the remaining probability $1-\sum_S x_{i,S}$. The preallocation can give an item to several bidders.

The algorithm of §3.2: (i) draw a preallocation from an optimal LP solution $x$; (ii) let $p^i=(p^i_1,\dots,p^i_m)$ be the maximizing clause for $S_i$ in $v_i$; (iii) give each item $j$ to a bidder $i$ with $p^i_j\ge p^{i'}_j$ for all $i'$. Write $\mathrm{ALG}$ for the welfare of the resulting allocation.

Formalization targets

Goal: Theorem 3.2

For every XOS profile, every optimal LP solution $x$, every choice of maximizing clauses, every tie-breaking in step (iii) and every allocation $O$,

$$\Big(1-\Big(1-\frac1n\Big)^n\Big)\sum_i v_i(O_i)\ \le\ \mathbb E[\mathrm{ALG}].$$

Milestones

1. $\sum_i v_i(O_i)\le\mathrm{OPT}^*$ for an optimal LP solution (step (i) of the proof of Theorem 3.1).
2. Pointwise, $\mathrm{ALG}\ge\sum_j Q_j$ with $Q_j=\max_i p^i_j$.
3. Eq. (1): for $1\le k\le n$ and $X_1,\dots,X_k\in[0,1]$ with $\sum X_i\le1$,

$$1-\prod_{i\le k}(1-X_i)\ \ge\ 1-\Big(1-\tfrac{\sum X_i}{k}\Big)^k\ \ge\ \Big(1-\big(1-\tfrac1k\big)^k\Big)\sum X_i\ \ge\ \Big(1-\big(1-\tfrac1n\big)^n\Big)\sum X_i .$$

4. Lemma 3.3: $\mathbb E[Q_j]\ge(1-(1-1/n)^n)\sum_i\sum_{S\ni j}x_{i,S}\,p^{(i,S)}_j$ for every feasible $x$.
5. $\mathbb E[\mathrm{ALG}]\ge(1-(1-1/n)^n)\,\mathrm{OPT}^*(x)$ for every feasible $x$.

Milestone 5 is stronger than the goal (it compares with the fractional value); the goal is stated against the integral optimum because that is what Theorem 3.2 asserts.

Significance

The bound $1-(1-1/n)^n\ge1-1/e$ is a constant-factor guarantee for a class that includes every submodular valuation, obtained from nothing more than the LP relaxation and the clause structure of XOS. It shows that the integrality gap of the configuration LP for XOS bidders is at most $1/(1-(1-1/n)^n)$, a fact reused in later work on welfare maximization, online allocation and posted-price mechanisms. The per-item analysis (Lemma 3.3 and Eq. (1)) is the same "$1-1/e$" correlation-gap argument that recurs in submodular maximization and prophet-inequality proofs.

The result is proved in the paper. To our knowledge it has no machine-checked proof. This mission produces a Lean statement and proof of the guarantee with the randomness made explicit, a reusable model of the configuration LP and of randomized rounding over bundles, and a formal version of the inequality in Eq. (1), which is independently useful.

Difficulty

Each piece of the argument is short; the work is in the bookkeeping. The preallocation is infeasible, so welfare cannot be read off from the rounding directly; the proof reduces it to per-item quantities $Q_j$ and then lower-bounds $\mathbb E[Q_j]$ by comparing with a different assignment of item $j$ that is not the algorithm's. The expectation of that auxiliary assignment involves a product of probabilities over bidders ordered by a conditional expectation, and the final bound needs the calculus inequality of Eq. (1) together with a summation by parts. A naive attempt to bound $\mathbb E[\mathrm{ALG}]$ bidder by bidder fails, because a bidder's received bundle is not contained in its preallocated bundle, and the clause values of other bidders decide what it receives.

Formalization scope

• Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. XOS is stated through its expression: each $v_i$ comes with a nonempty finite clause set $W_i$ of nonnegative clauses, and $v_i(S)$ is attained by a clause of $W_i$ and bounded by all of them. Normalization and monotonicity, the paper's standing assumptions (p. 1), follow from this.
• The LP has a variable for every bundle, including $\emptyset$. "Optimal" is stated as feasible and not beaten by any feasible solution; existence of an optimum is not asserted.
• The rounding is a finite product distribution over profiles $\sigma:\mathrm{Fin}\,n\to$ bundles, with bidder $i$'s law $q_i(S)=x_{i,S}+\mathbf 1[S=\emptyset](1-\sum_T x_{i,T})$; expectations are finite sums.
• The XOS oracle is a function parameter with its specification, and step (iii) is any rule selecting a bidder with maximal clause value; every statement quantifies over all of them.
• "Approximation" in Theorem 3.2 is read in expectation, as its proof establishes. There are no $O(\cdot)$ constants in this mission.
• Printed slip: the display of Lemma 3.3 (and the identity for $\mathrm{OPT}^*$ before it) sums $x_{i,S}p^{(i,S)}_j$ over all $(i,S)$; the proof's final line restricts to $S\ni j$, and the printed version is false. The Lean states Lemma 3.3 with $S\ni j$.
• Running time, the ellipsoid method and oracle complexity are out of scope.
• Ruled out as trivializing: dropping the LP constraints on $x$ (the item constraint is what makes Eq. (1) apply), stating the bound for a fixed preallocation instead of the expectation, or allowing negative clause values.

A complete development needs finite product distributions over bundles, the AM–GM inequality, monotonicity of $(1-1/k)^k$, and a summation-by-parts argument. The LP and rounding model are reusable for the other randomized-rounding results of the paper; proofs of any milestone are welcome.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• S. Dobzinski, N. Nisan, M. Schapira, Approximation algorithms for combinatorial auctions with complement-free bidders, STOC 2005. https://doi.org/10.1145/1060590.1060681
• B. Lehmann, D. Lehmann, N. Nisan, Combinatorial auctions with decreasing marginal utilities, EC 2001. https://doi.org/10.1145/501158.501161
• U. Feige, On maximizing welfare when utility functions are subadditive, STOC 2006. https://doi.org/10.1145/1132516.1132540

Motivation

L-convex functions were defined purely combinatorially, on the integer lattice. Chapter 6's M-convex theory showed that combinatorial definition always extends to a genuine convex function on real space (missions 23-ch06c-mconvexfunctions/24-ch06d-mconvexfunctions); this mission carries out the identical program for the L side. It first shows L$^\natural$-convexity is exactly integral convexity plus ordinary submodularity — a clean synonym that also explains why submodular set functions are a natural special case — then builds the entire polyhedral (real-variable) theory of L-convex functions: the axioms (SBF[R])/(TRF[R]), two practical local criteria for verifying submodularity without checking every pair of points, the fact that the classical Lovász extension of a submodular set function is itself a polyhedral L-convex function, the six-operation closure toolkit, and — this mission's goal — the L-optimality criterion in its full polyhedral generality, characterizing global optimality by finitely many directional derivatives.

Setting

Fix a finite ground set $V$. A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain is polyhedral L-convex, $g \in L[\mathbb R \to \mathbb R]$, if it satisfies (SBF[R]): $g(p)+g(q) \ge g(p\vee q)+g(p\wedge q)$, and (TRF[R]): $\exists r \in \mathbb R$, $g(p+\alpha\mathbf 1) = g(p)+\alpha r$ for all $p \in \mathbb R^V$, $\alpha \in \mathbb R$; it is polyhedral L$^\natural$-convex if its lift to one extra real coordinate is polyhedral L-convex. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is integrally convex if its convex closure agrees, at every real point, with the closure taken using only that point's integral neighborhood. The Lovász extension $\hat\rho$ of a submodular set function $\rho$ is the piecewise-linear interpolation built from the sorted distinct components of $p \in \mathbb R^V$. The directional derivative $g'(p;d)$ is $\inf_{t>0}(g(p+td)-g(p))/t$.

Formalization targets

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

For a polyhedral L-convex function $g$ and $p \in \operatorname{dom}_{\mathbb R} g$: $g(p) \le g(q)$ for all $q$ if and only if $g'(p;\chi_Y) \ge 0$ for every $Y \subseteq V$ and $g'(p;\mathbf 1)=0$; for polyhedral L$^\natural$-convex $g$, the criterion simplifies to $g'(p;\pm\chi_Y) \ge 0$ for every $Y$. This is the direct L-side mirror of mission 24-ch06d-mconvexfunctions's M-optimality criterion (Theorem 6.52) and the polyhedral generalization of mission 08-lconvex-functions-i's integer-domain L-optimality criterion (Theorem 7.14): checking global optimality against exponentially many points reduces to $|V|+1$ (or $2|V|$) directional-derivative inequalities.

Supporting structural targets

Twelve further results build the polyhedral theory from the ground up. Theorems 7.20-7.21 identify L$^\natural$-convexity with the conjunction of ordinary submodularity and integral convexity — a genuinely different, function-analytic characterization from the exchange-axiom- style definitions used so far. Propositions 7.23-7.24 give two practical sufficient conditions for verifying (SBF[R]) locally, at a single scale, rather than globally. Proposition 7.25 shows the Lovász extension of any submodular set function is automatically polyhedral L-convex — not in this chunk's own extraction table (its label is preceded by an unlabeled restatement of the same fact, which evidently confused the extractor), found and placed by direct reading. Theorem 7.26 shows an L-convex function's convex extension, when polyhedral, inherits polyhedral L-convexity, continuing mission 26-ch07b-lconvexfunctions's Theorem 7.19. Theorems 7.28-7.32 restate the discrete theory's core equivalences (translation submodularity, the L/L$^\natural$ correspondence, the six basic operations, restrictions) in the polyhedral setting, and Proposition 7.34 shows minimizer sets of linearly-perturbed polyhedral L-convex functions are themselves L-convex polyhedra — flagged by the book itself as a partial result whose full converse characterization (Theorem 7.45) lies beyond this chunk's range.

Significance

Theorems 7.20-7.21's synonym is structurally important: it means every algorithm and theorem already known for submodular-function minimization over $\{0,1\}^V$-type domains applies, after a midpoint-convexity check, to the vastly larger class of integer-lattice L$^\natural$-convex functions, with no new proof technique required. Proposition 7.25 is the bridge that lets the combinatorial Lovász extension — the workhorse of submodular optimization for forty years — be recognized as a special case of the polyhedral L-convex function theory this mission builds, explaining why algorithms for one transfer so readily to the other. The goal, Theorem 7.33, is the precise tool chapter 10's continuous-relaxation algorithms for L-convex-function minimization actually verify against: a scaling algorithm's claimed optimum is confirmed correct exactly by checking the criterion's finitely many directional-derivative inequalities.

None of these results are open — they are Murota's account of how the integer-lattice theory of L-convexity survives, result by result, the passage to polyhedral convex functions on $\mathbb R^V$, mirroring chapter 6's identical program for M-convexity. What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Proposition 7.25) the platform's own automated extractor missed, extending the shared Lean vocabulary (SBFR, TRFR, LovaszExtension, DirDeriv) this series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to verify $g(p) \le g(q)$ directly against every $q \in \mathbb R^V$; the book's actual proof instead reduces this to the finite family of directional derivatives via Theorem 7.20's integral-convexity fact (an L$^\natural$-convex function's local behavior determines its global behavior) applied to the polyhedral setting through Theorem 3.21's general optimality criterion for integrally convex functions — a two-layer reduction (polyhedral $\to$ integral-convexity $\to$ finite local check) with no direct one-step argument. The genuine combinatorial content in this block is in Proposition 7.25's proof: showing the Lovász extension is submodular requires the finite-valued case (a direct calculation split on whether the two perturbed coordinates land in the same or different threshold sets) and then a limiting argument over a sequence of finite-valued truncations $\rho_k \to \rho$ for the general, possibly-infinite case — a genuine two-step argument, not a single inequality chase.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; polyhedral L-(natural-)convex functions are (V→ℝ)→WithTop ℝ. All thirteen numbered results found in this chunk's page range are placed, with one documented scope reduction: Proposition 7.24 states only part (1) (the unconditional-on-magnitude sufficient condition), not part (2)'s sharper, sorted-index-restricted version, which needs the same SortedValues apparatus a second time for no other result's benefit — see HARD.md. "$g_U > -\infty$" and its variants are replaced by the equivalent (DomR ...).Nonempty hypothesis throughout, matching mission 24-ch06d-mconvexfunctions's identical substitution. "Domain is closed"/"domain is an interval" (Propositions 7.23-7.24) are stated via Mathlib's IsClosed and Set.OrdConnected respectively, the latter being the precise order-theoretic notion of "interval" in a pointwise-ordered space. This mission's base vocabulary is redeclared from missions 08-lconvex-functions-i, 20-ch04b-mconvexsets (for the Lovász extension machinery), 21-ch05b-lconvexsets, 23-ch06c-mconvexfunctions/ 24-ch06d-mconvexfunctions, and 26-ch07b-lconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the thirteen sorrys are welcome; the goal and Proposition 7.25 carry the most independent proof content.

Selected references

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

Motivation

Line search methods for unconstrained minimization of a smooth function $f : \mathbb{R}^n \to \mathbb{R}$ choose a direction $d_k$ and a step $\alpha_k > 0$ and set $x_{k+1} = x_k + \alpha_k d_k$. Classical rules (Armijo, Wolfe) insist that every step decrease $f$. For quasi-Newton and conjugate gradient directions this monotonicity requirement often forces short steps, and nonmonotone line searches, which only ask for a decrease relative to some reference value built from past iterates, have been used since Grippo, Lampariello and Lucidi (1986) to let such methods take longer steps.

Zhang and Hager (SIAM J. Optim., 2004) replaced the maximum of recent function values used by Grippo et al. with a weighted average $C_k$ of all past function values. The paper proves two results: global convergence to stationary points (the companion mission) and, the subject of this mission, R-linear convergence of the function values when $f$ is strongly convex.

Timeline:

• 1986, Grippo, Lampariello, Lucidi: nonmonotone line search based on the maximum of the last $M$ function values; global convergence.
• 2002, Dai: R-linear convergence of the max-based scheme for strongly convex $f$.
• 2004, Zhang and Hager: the averaged reference value $C_k$; global convergence (Theorem 2.2) and R-linear convergence for strongly convex $f$ (Theorem 3.1).

Setting

Fix parameters $0 \le \eta_{\min} \le \eta_{\max} \le 1$, $0 < \delta < \sigma < 1 < \rho$ and $\mu > 0$. Write $g_k = \nabla f(x_k)$ and $\nabla f(x)d = \langle \nabla f(x), d\rangle$. The Nonmonotone Line Search Algorithm (NLSA) keeps weights $Q_k$ and reference values $C_k$:

$$Q_0 = 1,\ \ Q_{k+1} = \eta_k Q_k + 1,\qquad C_0 = f(x_0),\ \ C_{k+1} = \frac{\eta_k Q_k C_k + f(x_{k+1})}{Q_{k+1}},$$

with $\eta_k \in [\eta_{\min}, \eta_{\max}]$ chosen freely at each step. A step $\alpha_k$ is accepted either by the nonmonotone Wolfe conditions

$$f(x_k + \alpha_k d_k) \le C_k + \delta\alpha_k g_k^{\mathsf T} d_k,\qquad \nabla f(x_k + \alpha_k d_k) d_k \ge \sigma g_k^{\mathsf T} d_k,$$

or by the nonmonotone Armijo rule $\alpha_k = \bar\alpha_k \rho^{h_k}$, where $\bar\alpha_k > 0$ is a trial step and $h_k$ is the largest integer such that the first inequality holds and $\alpha_k \le \mu$. With $\eta_k = 0$ one recovers the monotone rules.

The direction assumption asks for constants $c_1, c_2 > 0$ with $g_k^{\mathsf T} d_k \le -c_1\|g_k\|^2$ and $\|d_k\| \le c_2\|g_k\|$. The function $f$ is strongly convex with constant $\gamma > 0$ if

$$f(x) \ge f(y) + \nabla f(y)(x - y) + \frac{1}{2\gamma}\|x - y\|^2\quad\text{for all } x, y.$$

Let $x^*$ be the minimizer, $\mathcal L = \{x : f(x) \le f(x_0)\}$, $d_{\max} = \sup_k\|d_k\|$, and $\bar{\mathcal L}$ the set of points within distance $\mu d_{\max}$ of $\mathcal L$.

Formalization targets

Goal: Theorem 3.1

Let $f$ be strongly convex with minimizer $x^*$, let $\nabla f$ be Lipschitz continuous on bounded sets, let $\eta_{\max} < 1$, let the directions satisfy the direction assumption at every iteration, and let $\alpha_k \le \mu$ for all $k$. Then there is $\theta \in (0,1)$ with

$$f(x_k) - f(x^*) \le \theta^k\big(f(x_0) - f(x^*)\big)\quad\text{for each } k.$$

The goal fixes no value of $\theta$: it asserts only the existence of a linear rate.

Milestones

In the paper's order of use:

1. Lemma 1.1: $f(x_k) \le C_k \le A_k$ when $g_k^{\mathsf T}d_k \le 0$ for each $k$.
2. $C_{k+1} \le C_k$, so all iterates lie in $\mathcal L$.
3. (3.4): $f(x) - f(x^*) \le \gamma\|\nabla f(x)\|^2$.
4. (2.15): $Q_{k+1} \le 1/(1 - \eta_{\max})$.
5. (3.6): $f(x_{k+1}) \le C_k - \beta\|g_k\|^2$, with

$$\beta = \min\left\{\frac{\delta\mu c_1}{\rho},\ \frac{2\delta(1-\delta)c_1^2}{L\rho c_2^2},\ \frac{\delta(1-\sigma)c_1^2}{Lc_2^2}\right\}.$$

6. (3.7): $\|g_{k+1}\| \le b\|g_k\|$, $b = 1 + \mu c_2 L$.
7. (3.8): the explicit contraction

$$C_{k+1} - f(x^*) \le \theta\,(C_k - f(x^*)),\qquad \theta = 1 - \beta b_2(1-\eta_{\max}),\quad b_2 = \frac{1}{\beta + \gamma b^2}.$$

Here $L$ is a Lipschitz constant of $\nabla f$ on $\bar{\mathcal L}$. A further result on the same definitions is Theorem 3.2: if $f(x_k)$ converges R-linearly with ratio $\theta < \eta_{\min}$ inside a compact convex set on which $f$ is strongly convex, then the sufficient decrease condition with reference value $C_k$ holds for all large $k$.

Significance

Theorem 3.1 shows that averaging past function values costs nothing in the rate: on strongly convex functions the nonmonotone method keeps the linear rate of monotone descent, for any direction sequence satisfying the direction assumption (steepest descent, L-BFGS with bounded condition numbers, and so on). Theorem 3.2 is the converse side: for weights close enough to 1, the averaged test eventually accepts the steps of any R-linearly convergent iteration of this kind. The paper contrasts this with the max-based test of Grippo et al.

These results are proved in the paper. As far as the platform catalogue shows, no line search with the Wolfe conditions or a nonmonotone reference value has been formalized. The only related item is a monotone backtracking gradient descent rate, which is a different theorem. Machine-checked proofs would give reusable Lean statements of the nonmonotone Wolfe and Armijo rules and of the averaged reference value. They would also give the explicit constants $\beta$, $b$ and $\theta$ in checked form, and a checked record of the repair of the printed statement described below.

Difficulty

The obvious argument would show that $f(x_k) - f(x^*)$ contracts at each step. It fails: the method is nonmonotone, and $f(x_{k+1})$ may exceed $f(x_k)$. The quantity that contracts is $C_k - f(x^*)$, and only $C_k$ is controlled by the line search. The contraction must be derived by relating $\|g_k\|^2$ to $C_k - f(x^*)$ in two regimes, and the second regime needs a bound on $f(x_{k+1}) - f(x^*)$ from the gradient at the previous iterate. That bound requires the Lipschitz constant on a region containing every point the line search examines, which is why the region $\bar{\mathcal L}$ and the step bound $\mu$ enter. In Lean, the sufficient decrease (3.6) also rests on the step-length lower bounds of Lemma 2.1 for both rules, including the integer-exponent Armijo rule with its maximality condition.

Formalization scope

Conventions:

• The space is EuclideanSpace ℝ (Fin n), $f$ is ContDiff ℝ 1, and $\nabla f(x)d$ is ⟪gradient f x, d⟫_ℝ.
• A run is infinite, uses one rule throughout (Wolfe or Armijo), and has arbitrary directions subject to the stated hypotheses.
• $Q_k$ and $C_k$ are defined by recursion from the run.
• The Armijo exponent ranges over $\mathbb{Z}$ and "largest" is IsGreatest.
• $d_{\max}$ and distances are taken in $[0,\infty]$, so unbounded directions make $\bar{\mathcal L}$ the whole space.
• Strong convexity keeps the paper's constant $\gamma$, the inverse modulus.
• "Lipschitz on bounded sets" means that every bounded set admits a Lipschitz constant for $\nabla f$.

Repair of the printed statement: the paper's direction assumption holds only for all sufficiently large $k$, but Theorem 3.1 concludes (3.5) for each $k$, and its proof uses the assumption at every $k$. As printed the theorem is false: $d_0 = 0$ with the Wolfe step $\alpha_0 = 1$ gives $x_1 = x_0$, which violates (3.5) at $k = 1$ whenever $x_0 \ne x^*$. The goal therefore requires the direction assumption for every $k \ge 0$.

The step bound "there exists $\mu > 0$ with $\alpha_k \le \mu$" is stated with $\mu$ the algorithm's parameter. For the Armijo rule this holds by construction. The Wolfe rule does not use $\mu$, so nothing is lost.

Trivializing formalizations are ruled out:

• the printed hypotheses with "for each $k$" (false, as shown above);
• a $\theta$ allowed to equal 1, or an unspecified constant factor in front of $\theta^k$ (weaker than (3.5));
• a globally Lipschitz gradient, or a step bound different from the $\mu$ used to build $\bar{\mathcal L}$.

A complete development needs:

• the NLSA model and Lemma 1.1;
• the step-length lower bounds of Lemma 2.1 for both rules (via the descent lemma for Lipschitz gradients);
• the geometric bound on $Q_k$;
• boundedness of level sets of strongly convex functions.

The NLSA definitions are reusable by any later mission on nonmonotone line searches. Proofs of the milestones in any order are welcome, as are a proof of the counterexample to the printed statement and a proof that the platform theorem ConvexOptimization.strong_convexity_quadratic_lower_bound implies (3.4).

Selected references

• H. Zhang, W. W. Hager, A Nonmonotone Line Search Technique and Its Application to Unconstrained Optimization, SIAM J. Optim. 14(4):1043–1056, 2004. https://doi.org/10.1137/S1052623403428208
• L. Grippo, F. Lampariello, S. Lucidi, A Nonmonotone Line Search Technique for Newton's Method, SIAM J. Numer. Anal. 23(4):707–716, 1986. https://doi.org/10.1137/0723046
• Y.-H. Dai, On the Nonmonotone Line Search, J. Optim. Theory Appl. 112:315–330, 2002 (reference [4] of the paper).

Motivation

In a combinatorial auction a set of $m$ items is sold to $n$ bidders who value bundles of items rather than single items. Spectrum auctions, procurement of transportation lanes and the allocation of cloud resources all have this form, and the central algorithmic question is how to allocate the items so as to maximize the social welfare, the sum of the bidders' values for what they receive. Even to describe a general valuation takes $2^m$ numbers, so algorithms access the bidders through queries, and the achievable approximation depends on the class of valuations allowed.

Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010) study bidders without complementarities. For the class of XOS valuations, maxima of additive valuations, which strictly contains the submodular valuations, they give LP-based algorithms and, in §3.3, a purely combinatorial algorithm: bidders arrive one at a time, take their demanded bundle at the current item prices, and raise the prices of what they took. Its analysis charges the welfare of any allocation to the item prices the algorithm sets, an argument that uses only the demand and XOS oracles.

Setting

The items are $M=\{1,\dots,m\}$ and the bidders $1,\dots,n$.

• An additive valuation (a clause) $w$ assigns nonnegative values $w(1),\dots,w(m)$ to the items and $w(S)=\sum_{j\in S}w(j)$ to a bundle $S\subseteq M$.
• An XOS valuation $v$ is given by a nonempty finite set of clauses $\{w_1,\dots,w_t\}$ (its XOS expression) through $v(S)=\max_k w_k(S)$. A clause $w_k$ with $w_k(S)=v(S)$ is a maximizing clause for $S$. Every XOS valuation is normalized, $v(\emptyset)=0$, and monotone.
• An allocation is a tuple of pairwise disjoint bundles $O_1,\dots,O_n$; items may stay unallocated. Its welfare is $\sum_i v_i(O_i)$.
• A demand oracle for bidder $i$ answers, given item prices $p\in\mathbb R^m$, a bundle maximizing $v_i(T)-\sum_{j\in T}p_j$. An XOS oracle answers, given a bundle $S$, a maximizing clause for $S$ in $v_i$.

The greedy price-update algorithm. Start with all bundles empty and all prices $p_j=0$. For $i=1,\dots,n$: let $S_i$ be bidder $i$'s demand at the current prices; remove the items of $S_i$ from the bundles of the earlier bidders; let $q^i$ be the maximizing clause for $S_i$ in $v_i$; set $p_j=q^i_j$ for $j\in S_i$. Write $p^k$ for the prices after stage $k$ ($p^0=0$), $p^k(T)=\sum_{j\in T}p^k_j$, and $A_1,\dots,A_n$ for the final bundles.

In the Lean development these objects are XOSExpr, XOSExpr.val, IsAllocation, welfare, IsDemandOracle, IsXOSOracle, greedyState, greedyPrices and greedyAlloc in the namespace ComplementFreeCA.XOSGreedy.

Formalization targets

Goal: Theorem 3.3

For XOS valuations $v_1,\dots,v_n$, every demand oracle and every XOS oracle, and every allocation $O_1,\dots,O_n$,

$$\sum_{i=1}^n v_i(O_i)\;\le\;2\sum_{i=1}^n v_i(A_i).$$

The comparison with every allocation is the paper's comparison with the optimal allocation.

Milestones

1. Lemma 3.4. The final prices are paid for by the algorithm's welfare:

$$p^n(M)\le\sum_i v_i(A_i).$$

2. Lemma 3.5. Prices never decrease: $p^k_j\le p^{k'}_j$ for all items $j$ and stages $k\le k'$.
3. Lemma 3.6. For every allocation $O$,

$$\sum_i v_i(O_i)\le 2\,p^n(M).$$

Three further statements are included without being milestones: the output $A_1,\dots,A_n$ is an allocation (used implicitly by the paper); the first sentence of the proof of Lemma 3.6, that with $\Delta^i=p^i(M)-p^{i-1}(M)$ one has $\Delta^i=\max_{T\subseteq M}\bigl(v_i(T)-p^{i-1}(T)\bigr)$; and the factor $2$ is attained on the paper's two-item, two-bidder example (p. 9).

Significance

Theorem 3.3 shows that a factor-2 approximation of the optimal welfare for XOS bidders needs no linear program: one pass over the bidders, one demand query and one XOS query each. The paper's LP-based algorithm of §3.2 attains the better ratio $e/(e-1)$, and Theorem 4.1 of the paper shows that for the larger class of complement-free bidders no $(2-\epsilon)$-approximation is possible with polynomial communication.

The result is proved in the paper; to the best of our knowledge it has no machine-checked proof. This mission produces a formal model of XOS valuations, demand and XOS oracles and the greedy run that is reusable for other price-based arguments, and a formal proof of the guarantee for every tie-breaking in both oracles.

Difficulty

The argument is elementary, but its bookkeeping is where a formal proof can go wrong. Items move between bidders: an item taken from an earlier bidder in step (b) is re-priced in step (d), and every priced item lies in exactly one final bundle. Lemma 3.4 needs this invariant across all $n$ stages, together with the fact that a maximizing clause for the demanded set bounds $v_i$ on every subset, which holds because it is a clause of $v_i$ itself, not merely an additive function agreeing with $v_i$ on $S_i$. Lemma 3.5 is a contradiction argument using optimality of the demand; Lemma 3.6 telescopes the price increases and needs prices to stay nonnegative. The argument must hold for arbitrary oracle answers, so no canonical demand can be assumed.

Formalization scope

• Bidders are Fin n, items Fin m, bundles Finset (Fin m), values in ℝ. An XOS valuation is represented by its expression: a nonempty Finset (Fin m → ℝ) of clauses with nonnegative entries, evaluated with Finset.sup'. The paper's standing assumptions, normalized and monotone valuations (p. 1), hold automatically in this representation.
• The oracles are function parameters dem : Fin n → (Fin m → ℝ) → Finset (Fin m) and cl : Fin n → Finset (Fin m) → (Fin m → ℝ) with hypotheses IsDemandOracle and IsXOSOracle; every theorem holds for every such pair, so no tie-breaking rule is fixed.
• The run is a recursion on the stage: stage $k+1$ processes the 0-based bidder $k$, i.e. the paper's bidder $k+1$; after stage $n$ the state is constant.
• The paper's goal compares with the optimal allocation; the Lean goal compares with every allocation, which is equivalent and avoids an argmax. Stating the bound against one particular allocation, or against the algorithm's own output, would be trivial and is excluded.
• There are no $O(\cdot)$ constants: the factor $2$ is the paper's.
• Printed slip: the model on p. 1 writes an allocation as $S_1,\dots,S_m$; it is one bundle per bidder, $S_1,\dots,S_n$.
• Out of scope: running time, the cost of simulating oracles (Proposition 2.1), and communication lower bounds.

Contributions welcome: proofs of the three milestones and of the goal, and reusable lemmas on the invariant that every priced item lies in exactly one final bundle.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• B. Lehmann, D. Lehmann, N. Nisan, Combinatorial auctions with decreasing marginal utilities, Games and Economic Behavior 55(2):270–296, 2006. https://doi.org/10.1016/j.geb.2005.02.006