The OR Formalization Drive

Completed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XVII: Random-Horizon Consumption-Investment and the De Finetti Dividend ProblemTextbook

Motivation

An insurance company collects premia and pays claims each period; the difference is a random, signed quantity that can push the company's risk reserve up or down. At the start of every period, before that period's premia and claims are realized, the company's owners may pay themselves a dividend out of the current reserve — but once the reserve goes negative the company is ruined and stops operating for good. How should the owners time and size these payments to maximize the total expected discounted dividend paid out before ruin? This is the classical De Finetti dividend problem, one of risk theory's oldest optimization questions, and Chapter 9 §9.2 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) solves its fully discrete-time version by identifying the exact combinatorial shape of the optimal policy — not just proving one exists. This mission also covers §9.1, a different application of Chapter 7's contracting theory to a consumption-investment problem whose planning horizon is itself random rather than fixed or infinite.

Setting

The dividend model is a stationary Markov Decision Model on the integers: the state $x \in \mathbb Z$ is the current risk reserve, the action $a \in \{0,1,\dots,x\}$ (for $x \ge 0$ ; only $a=0$ is available once ruined) is the dividend paid, the reward is $r(x,a):=a$ , and the reserve evolves by i.i.d. increments $Z_n$ (premia minus claims) after the dividend is deducted. Because the reward is bounded by an explicit function of the state (Lemma 9.2.2), Chapter 7's general existence theory applies directly, and the value function $J_\infty$ satisfies a genuine Bellman equation. The chapter's real content begins once existence is established: Theorem 9.2.3 pins down enough analytic structure of $J_\infty$ and its largest-maximizing policy $f^*$ (monotonicity, a Lipschitz-type inequality, and a self-consistency identity) to drive a purely combinatorial argument that $f^*$ 's shape is a finite alternation of "pay nothing" and "pay down to a fixed level" intervals — a band-policy (Definition 9.2.5). Section 9.1's random-horizon consumption-investment model reuses the same Chapter 7 machinery in a different setting: the usual $(c,a)$ (consumption, portfolio) decision each period, but where the horizon itself ends after each period with probability $1-p$ , making the effective one-period discount $\beta p$ rather than $\beta$ .

Formalization targets

The goal, Theorem 9.2.9, states the section's main claim in one sentence: the stationary policy $(f^*,f^*,\dots)$ is optimal and is a band-policy. Short as it is stated, its proof assembles every earlier result of the section. The milestones supply that assembly, in order: Lemma 9.2.2 gives the model's bounding function and the resulting integrability/convergence facts; Theorem 9.2.3 gives the value-function bounds and the self-consistency identity $f^*(x-f^*(x))=0$ ; Corollary 9.2.4 checks the two sign-definite degenerate cases directly from Theorem 9.2.3; Proposition 9.2.6 proves the top threshold $\xi := \sup\{x \mid f^*(x)=0\}$ is finite (not merely well-defined) and that $f^*$ is a simple barrier above it; Proposition 9.2.8 proves the increment property below $\xi$ that forces each band's shape; and Theorem 9.2.10 (a postscript refinement, stated after the goal) shows the wave lengths are bounded once the reserve's downward jumps are themselves bounded, collapsing to a single barrier-policy in the extreme case. Theorem 9.1.1, the random-horizon consumption-investment verification theorem, is included as a full item but is not a milestone of this goal, since its content and proof belong to a different, disjoint model — see Difficulty.

Significance

Band-policies and the discrete-time De Finetti dividend problem have no substrate anywhere in Mathlib or on the platform, and the result is a genuinely deep, classical one: a discrete-time analogue of the continuous-time De Finetti barrier-strategy theory, obtained here by pure dynamic-programming argument rather than the stochastic-calculus techniques the continuous-time theory usually relies on. The mission is explicit that the goal's conclusion is the general band-policy structure, not the strictly weaker barrier-policy special case that Theorem 9.2.10 b) proves only under an extra hypothesis (bounded downward jumps) — stating the goal with a barrier-policy conclusion instead would understate what Theorem 9.2.9 actually proves.

Difficulty

The central formalization challenge is Definition 9.2.5's own combinatorial intricacy: a band-policy is specified by an alternating chain of thresholds $0 \le c_0 < d_1 \le c_1 < d_2 \le \dots \le d_n \le c_n$ with a positive-width gap condition on every wave, and the policy's four piecewise branches case-split on which wave (if any) the current state falls into. This mission renders it existentially over the witnessing $(n,c,d)$ rather than as one closed-form function, a faithful but more verbose transcription that avoids conflating the different branch conditions. A second difficulty is Proposition 9.2.6's own finiteness claim: $\xi$ is a supremum over a subset of $\mathbb N_0$ that could, in principle, be unbounded, and Mathlib's convention for sSup over the naturals returns a finite junk value ( $0$ ) even for an unbounded set — using it directly would silently trivialize " $\xi<\infty$ " into a claim that is true regardless of the proposition's actual mathematical content. This mission instead states the proposition by exhibiting the finite value of $\xi$ directly, so that " $\xi$ is finite" survives as genuine content that the theorem's proof must establish. A third difficulty is scope: Theorem 9.1.1's random-horizon consumption-investment model shares no state space, action space, or definitions with the dividend model of the goal, despite both appearing in this chunk's assigned page range; it is formalized as a genuine application of a locally-restated copy of Chapter 7's contracting theory, but is excluded from the milestone list proper since it plays no role in the goal's own proof.

Formalization scope

The dividend model's transition law is built from Mathlib's PMF (probability mass function) type on $\mathbb Z$ , which supplies the "probabilities sum to one" fact automatically rather than as a separate hypothesis. J_\infty, \delta, and every finite-horizon value function throughout this mission use this whole book series' Filter.limsup-of-truncations convention for infinite-horizon reward, restated locally (own namespace copy, per this series' file-ownership boundary) from chunk 07a's identical apparatus rather than imported. The consumption-investment model of §9.1 is formalized with the number of risky assets $d$ as an explicit type parameter and its admissible-portfolio and domain restrictions as separate, citable fields rather than folded silently into the reward or transition definitions.

Selected references

N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
B. De Finetti, "Su un'impostazione alternativa della teoria collettiva del rischio", Transactions of the XVth International Congress of Actuaries, 1957 (the original continuous-time dividend problem this chapter's discrete-time analogue is modeled on).
H. Schmidli, Stochastic Control in Insurance, Springer, 2008 (cited by Remark 9.2.1 for the reduction from a continuous dividend-payout action space to the integer setting used throughout this section).
H. U. Gerber, "Games of economic survival with discrete- and continuous-income processes", Operations Research, 1972 (an early discrete-time treatment of the same class of problems, in the spirit this chapter's own model follows).

11 thms2 active usersReviewed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XVIII: Terminal Wealth in Jump Markets and Trade ExecutionTextbook

Motivation

Two problems in this mission, both about markets that do not behave the way the textbook Black–Scholes market does, and both solved by the same technique.

The first is portfolio choice in a pure jump market. Prices move by jumps at the epochs of a Poisson process, not by continuous Brownian fluctuation. This is not a technical variation: the market is incomplete, there is no replicating portfolio, and the machinery of stochastic analysis that makes the diffusion case tractable is unavailable. What is available instead is that the wealth process is piecewise deterministic — between jumps it follows an ODE, and all the randomness is in when the jumps happen and how big they are. Chapter 8's technique embeds such a process in its jump chain and turns the continuous-time control problem into a discrete-time Markov Decision Model with infinite horizon; Chapter 7's contracting theory then solves that.

The second is trade execution in an illiquid market. An agent must sell a large block of shares by a deadline. Placing the whole order at once moves the price against them, and in a traditional order book other participants can see the intention and trade against it — so the order goes to a dark pool, where there is no order book and matches arrive at random. The agent can only sell when a counterparty happens to appear, and whatever is unsold at the deadline must be dumped on the traditional market at once. The question is how much to offer at each opportunity.

The two problems have opposite curvature — the first is a concave maximisation of utility, the second a convex minimisation of cost — and the section is a good demonstration that the same embedding technique handles both, with each problem's structure entering only through which set of functions the value function is sought in.

Setting

The jump market (§9.3). The bond is S⁰_t = e^{ρt}; the risky assets follow dS^k_t = S^k_{t-}(μ_k dt + dC^k_t) where C_t = Σ_{n≤N_t} Y_n is a compound Poisson process of intensity λ whose jumps Y_n are supported in (-1,∞)^d, which keeps prices positive. Short-sellings are prohibited, so the admissible fractions of wealth form the compact set 𝒰 = {u ≥ 0, u·e ≤ 1}, and the wealth follows

dX_t = X_{t-}\big((\rho + \pi_t\cdot(\mu-\rho e))dt + \pi_t dC_t\big). \tag{9.10}

The investor maximises E^π_{tx}[U(X_T)] for a strictly increasing, strictly concave U.

The embedded model's state is (t,x) — a jump time and the wealth just after it — and its action is a whole control path α : [0,T] → 𝒰, followed until the next jump. Between jumps the wealth is φ^α_t(x) = x exp(∫₀^t (ρ + α_s·(μ-ρe))ds) (9.13), and the transition kernel is substochastic: with probability e^{-λ(T-t)} no further jump arrives before the horizon, and the reward r(t,x,α) = e^{-λ(T-t)}U(φ^α_{T-t}(x)) is collected instead.

The trade execution model (§9.4). A Poisson process of intensity λ delivers the trading epochs; selling a shares costs C(a) with C strictly increasing and strictly convex (the discrete form (9.19)), C(0) = 0; the inventory X_t = x₀ - ∫₀^t π_s dN_s is what remains, and C(X_T) is the terminal dump. Here the flow is uncontrolled — the inventory does not move between epochs — which makes the embedded model simpler.

What is being asked

The goal is Theorem 9.3.4, the main result for the terminal wealth problem, in all six of its parts: the value function is the limit of the value iteration and lies in IM_cv; it is the unique fixed point of the dynamic programming operator there; value iteration converges at the explicit geometric rate α_b^n/(1-α_b); there exists an optimal Markov portfolio strategy given by a single decision rule; policy iteration holds; and Howard's policy improvement algorithm holds. Parts a)–c) describe the value; parts d)–f) produce the strategy, and a formalization of the first three alone would omit the entire control half of the theorem.

The seven milestones are the rest of §9.3–9.4: the reduction from continuous to discrete time, the bounding function and its explicit contraction modulus, the invocation of Chapter 7's Structure Theorem, the iff-characterization of when holding only the bond is optimal, the stability of the value and of the optimal policies under perturbation of the utility, and then the trade execution problem's own bounding function and its monotone, unit-Lipschitz optimal execution rate.

Two formalization conventions run through everything here. The operator of §9.3 is a supremum over a space of control paths, and since Mathlib's sSup of a set unbounded above is 0 — with an unbounded reward that is a live risk, not a formality — it is carried as a relation defined by least upper bounds against explicit sets of achievable values, with its iterates a chain of such relations. And the continuous-time side is built, not assumed: Theorem 9.3.1 is the identification of the continuous-time value with the discrete-time one, so the law of the embedded jump chain is pinned by the one-step conditional law the book displays, and the terminal wealth is read off that chain.

10 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Approximation Algorithms for Combinatorial Problems III: The Worst-Case Ratio of the Weighted Algorithm B2Research Paper

Motivation

MAXIMUM SATISFIABILITY asks for a truth assignment satisfying as many clauses of a given set as possible. It was among the first NP-hard optimization problems for which an approximation algorithm came with a proven worst-case guarantee. In Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 1974, doi:10.1016/S0022-0000(74)80044-9), David S. Johnson set up a framework for measuring such guarantees and analyzed two heuristics for the problem. The second of these, algorithm B2, weights each clause by $2^{-|C|}$ and repeatedly sets a literal so that the heavier side is satisfied. On inputs whose clauses all have at least $k$ literals, it satisfies at least a $1 - 2^{-k}$ fraction of the optimum.

B2 is the ancestor of a line of work on MAX-SAT approximation:

1974. Johnson proves the $2^k/(2^k-1)$ bound for B2 on MS(k) and the $(k+1)/k$ bound for the unweighted greedy algorithm B1.
1994. Goemans and Williamson (SIAM J. Discrete Math. 7) present Johnson's algorithm as the derandomization, by conditional expectations, of the uniformly random assignment, and combine it with LP rounding to obtain a $3/4$ -approximation.
1999. Chen, Friesen and Zheng (JCSS 58) show that B2 is a $2/3$ -approximation on general inputs, sharper than the $1/2$ that Johnson's bound gives at $k = 1$ .

Setting

A literal is a variable $x_i$ or its negation $\bar x_i$ . A clause is a finite set of literals. A truth assignment is a set $T$ of literals containing no pair $\{x_i, \bar x_i\}$ ; it satisfies a clause $C$ when $C \cap T \ne \emptyset$ . An input is a finite set $S$ of clauses, and $S^*$ is the largest $|S'|$ over subsets $S' \subseteq S$ satisfied by one truth assignment. MS(k) is the restriction to inputs in which every clause contains at least $k$ distinct literals.

Algorithm B2 keeps a set SUB of satisfied clauses, a set LEFT of unsettled clauses, the literals LIT still available, and a weight $w(C)$ per clause, starting from $w(C) = 2^{-|C|}$ , $\mathrm{SUB} = \emptyset$ , $\mathrm{LEFT} = S$ . While some literal of LIT occurs in a clause of LEFT, it picks any such literal $y$ . Let YT be the clauses of LEFT containing $y$ and YF those containing $\bar y$ . If $\sum_{\mathrm{YT}} w \ge \sum_{\mathrm{YF}} w$ , it makes $y$ true, moves YT to SUB and doubles the weight of each clause of YF; otherwise it does the symmetric move with $\bar y$ . Finally it removes $y, \bar y$ from LIT. When no literal of LIT remains in LEFT it returns SUB.

The choice of $y$ is free, so several outputs may be choosable on one input. Johnson measures the algorithm by its worst choosable output, through the ratio $r(B2, S) = S^*/|\mathrm{SUB}|$ and its maximum $R[B2, \mathrm{MS}(k)](n)$ over inputs of size at most $n$ .

Formalization targets

Goal: Theorem 3, with the equality range corrected

For every $k \ge 1$ , every $S$ in MS(k) and every SUB choosable by B2 on $S$ ,

(2^k - 1)\,S^* \le 2^k\,|\mathrm{SUB}|,

and for every $k \ge 2$ there are $S$ in MS(k) and a choosable SUB with $|\mathrm{SUB}| > 0$ and

(2^k - 1)\,S^* = 2^k\,|\mathrm{SUB}|.

The paper states equality "for all sufficiently large $n$ " for every $k \ge 1$ . At $k = 1$ this is false: the ratio 2 would require every clause to be a unit clause and all clauses to be jointly satisfiable, and on such inputs B2 satisfies everything. The goal therefore asserts tightness for $k \ge 2$ . A separate item states that at $k = 1$ the ratio is never attained.

Milestones

Initially, the total weight of LEFT is at most $|S|/2^k$ .
No iteration increases the total weight of LEFT, so at halting it is still at most $|S|/2^k$ .
At halting, every clause left in LEFT has weight exactly $1$ .
At halting, $|\mathrm{LEFT}| \le |S|/2^k$ and $|\mathrm{SUB}| \ge |S|(1 - 2^{-k})$ .
The eight-clause instance for $k = 3$ has $S^* = 8$ and admits a choosable output of size $7$ .

Significance

The bound $1 - 2^{-k}$ is exactly the expected fraction of clauses a uniformly random assignment satisfies on MS(k). B2 attains it deterministically, and the proof bounds $|\mathrm{SUB}|$ against $|S|$ rather than against $S^*$ , a feature the paper points out. For $k = 3$ the constant $8/7$ was later shown by Håstad (2001) to be optimal among polynomial-time algorithms unless P = NP, so the guarantee of this 1974 algorithm is best possible for MAX-E3-SAT.

Formalizing the result produces a machine-checked potential-function argument for a nondeterministic algorithm: the invariant links each clause's weight to how many of its literals have been removed. The mission also records a correction to the printed statement at $k = 1$ . The paper's proof is complete; to our knowledge no machine-checked version exists.

Difficulty

The obvious argument follows the counting proof for algorithm B1 and compares clauses saved with clauses wounded in each step. It fails here: B2 can wound more clauses than it saves in a step, and the bound holds only in the weighted sense. The weight of a clause is not a static quantity. It is $2^{-|C|}$ times $2$ to the number of its literals already discarded, and this invariant must be carried through every step, including clauses that contain both $y$ and $\bar y$ . Tightness needs an explicit input and an explicit adversarial run that exploits the tie in Step 4, and then a proof that every assignment of the remaining variables kills exactly one clause.

Formalization scope

Literals and clauses. A literal is a pair (variable index in $\mathbb N$ , sign). Clauses are Finsets of literals, and an input is a Finset of clauses, so there are no duplicate clauses. Truth assignments are partial and consistent. $S^*$ is a maximum over the finite, nonempty family of satisfiable subsets.
B2 as a relation. B2 is a nondeterministic run relation, and "choosable" means reachable by finitely many steps from the initial state and halting. Step 3 allows a literal of either sign. The tie in Step 4 goes to $y$ , and the comparison and doublings use the weights before the update. Weights are rationals.
Size-free ratios. The size-dependent $R[B2, \mathrm{MS}(k)](n)$ is replaced by statements about every input (upper bound) and one attaining input (tightness). The two forms are equivalent because $R$ is a maximum over finitely many inputs and nondecreasing in $n$ .
No division. All ratios are multiplied out, so no division by zero can make a bound vacuous.
Trivializations ruled out. A deterministic tie-break in Step 3 or 4, or tightness at a single fixed $k$ , would be a weaker theorem and is not acceptable. So is stating only the upper bound.

The definitions (the MS layer, the run relation) can be reused by other MAX-SAT approximation results, and an identical MS layer appears in the companion mission on algorithm B1. Contributions welcome: proofs of the milestones, of the $k \ge 2$ tightness family, and of the $k = 1$ correction.

Selected references

D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9 (1974) 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
J. Chen, D. K. Friesen, H. Zheng, Tight bound on Johnson's algorithm for maximum satisfiability, J. Comput. System Sci. 58 (1999) 622–640. https://doi.org/10.1006/jcss.1998.1610
M. X. Goemans, D. P. Williamson, New 3/4-approximation algorithms for the maximum satisfiability problem, SIAM J. Discrete Math. 7 (1994) 656–666. https://doi.org/10.1137/S0895480192243516
J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001) 798–859. https://doi.org/10.1145/502090.502098

9 thms2 active usersReviewed

Completed

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

Discrete Convex Analysis XXII: Convex Extensibility of M-Convex FunctionsTextbook

Motivation

A discrete function defined only on the integer lattice cannot, by itself, be minimized by the tools of continuous optimization — gradients and convexity in the classical sense simply do not apply. Murota's theory of M-convex functions closes this gap by showing that the exchange axiom alone, a purely combinatorial condition, is enough to guarantee that a discrete function behaves exactly like a convex one: its minimizers form a well-structured (M-convex) set, it can be extended to a genuine convex function on real space without gaining any new local minima, and its behavior under a change of price vector (in the economic interpretation where the function is a cost and its argument a bundle of goods) satisfies the same gross substitutes law economists have studied since Kelso and Crawford's matching-market models. This mission develops the second half of that connection: from local optimality (established in the companion mission) to the full structural picture — minimizer sets, price-substitution laws, and the extension of M-convex functions to genuine convex functions in real variables.

Companion mission 06-mconvex-functions-i (Discrete Convex Analysis V) and sibling mission 22-ch06b-mconvexfunctions (Discrete Convex Analysis XXI) cover this chapter's optimality theory (the M-optimality criterion, the exchange axiom as sequential improvement) and its algebraic toolkit (domain operations, worked examples). This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the results on minimizer structure, gross substitutability, and convex extension that this chapter's remaining sections develop: the M-convexity of minimizer sets, the gross substitutes and stepwise gross substitutes properties and their characterizing role, a minimizer-cut theorem with scaling, integral convexity of M♮-convex functions, and — this mission's goal — the theorem characterizing M-convexity entirely through the polyhedral structure of a function's convex extension.

Setting

Fix a finite ground set $V$ . For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain, write $f[p](x) = f(x) - \langle p,x \rangle$ for the linear reweighting by $p \in \mathbb R^V$ , and $\arg\min g = \{x : g(x) \le g(y)\ \forall y\}$ for the minimizer set of any function $g$ . The convex closure $\bar f(x)$ of $f$ at a real point $x$ is the infimum, over finite convex combinations of points of $\operatorname{dom} f$ representing $x$ , of the corresponding combination of function values; $f$ is convex extensible if $\bar f$ agrees with $f$ on $\mathbb Z^V$ , and integrally convex if $\bar f(x)$ can always be computed using only points from $x$ 's own integral neighborhood $N(x)$ (the integer vectors within one unit of $x$ in every coordinate). A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (polyhedral) M-convex if it satisfies the real-variable exchange axiom (M-EXC[R]): for $x,y \in \operatorname{dom}_{\mathbb R} g$ and $u \in \operatorname{supp}^+(x-y)$ , some $v \in \operatorname{supp}^-(x-y)$ and $\alpha_0 > 0$ make the exchange inequality hold for every $\alpha \in [0,\alpha_0]$ .

Formalization targets

Goal: convex extensibility characterizes M-convexity

For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain,

f \text{ is M-convex} \iff \bigl(f \text{ is convex extensible}\bigr) \wedge \bigl(\forall p \in \mathbb R^V,\ \arg\min \bar f[-p] \text{ is an M-convex polyhedron, if nonempty}\bigr),

with the M♮-analogue using M♮-convex polyhedra (Theorem 6.43). This is the weakest stable form: it characterizes M-convexity purely by properties of the (unique) convex closure, without reference to any specific algorithm for computing it or any bound on the polyhedron's complexity.

Supporting structural targets

Ten further results build the toolkit this goal draws on and the picture it completes: the M-convexity of minimizer sets (Proposition 6.29), the gross substitutes and stepwise gross substitutes properties and the theorems showing they characterize M-convexity and M♮-convexity among convex-extensible functions (Propositions 6.32-6.33, 6.35, Theorems 6.34, 6.36), a minimizer-cut theorem with scaling used algorithmically in Chapter 10 (Theorem 6.39), integral convexity of M♮-convex functions (Theorem 6.42), a shared-coefficient convex-combination theorem for pairs of M♮-convex functions used in Chapter 8's separation theorem (Theorem 6.44), and the polyhedral-M-convexity of an M-convex function's convex extension together with the correspondence between polyhedral M♮-convexity and the real exchange axiom (Theorems 6.45, 6.47).

Significance

Theorem 6.43 is what makes the whole edifice of M-convex function theory a genuine extension of M-convex set theory (chapters 4-5) rather than a separate parallel development: it says that knowing a function's convex extension is polyhedral, with every price-weighted minimizer set an M-convex polyhedron, is not merely a consequence of M-convexity but an exact characterization of it. This is the theorem that lets later results (the discrete conjugacy theorem of Chapter 8, the separation theorems for M♮-convex functions) move freely between the discrete and continuous pictures. The gross substitutes property (Propositions 6.32-6.36) is independently significant outside this book: it is the exact condition, discovered independently in mathematical economics (Kelso-Crawford, Gul-Stacchetti), under which competitive equilibria with indivisible goods are guaranteed to exist — Murota's theorem that gross substitutability characterizes M-convexity (among convex-extensible functions) is what unifies the economic and combinatorial literatures on this question, taken up again in Chapter 11.

None of these results are open — they are Murota's systematic account of a theory with roots in matroid theory, submodular optimization, and mathematical economics. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (MExchangeAxiom, ConvexClosureVal, ArgMinOn) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The forward direction of Theorem 6.43 (M-convex $\implies$ convex extensible with polyhedral minimizers) is comparatively direct given Theorem 6.42 and Proposition 6.29. The converse is substantial: it must show that a function whose weighted minimizer sets are all M-convex polyhedra — a purely global, polyhedral condition — satisfies the local exchange axiom (M-EXCloc[Z]), and the book's proof does this by an edge-direction argument on the polyhedron $B = \arg\min f$ : every edge of an M-convex polyhedron must be parallel to some $\chi_u - \chi_v$ , a fact borrowed from the combinatorial structure of chapter 4's base polyhedra applied to a carefully perturbed weight vector. No shortcut through convex analysis alone succeeds, because ordinary polyhedral theory says nothing about which combinatorial directions a polyhedron's edges must follow — that content comes entirely from the M-convexity of the minimizer sets, not from convexity of the closure by itself.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; functions are (V→ℤ)→WithTop ℝ (integer domain) or (V→ℝ)→WithTop ℝ (real domain, for the polyhedral theorems). The convex closure is built directly from finite convex-combination representations rather than an abstract closure operator, and integral convexity compares it against the same construction restricted to each point's integral neighborhood (Fintype.piFinset of per-coordinate Finset.Icc). Real M-convex/M♮-convex polyhedra are defined as convex hulls of M-convex/M♮-convex integer sets, reusing chapters 4-5's own characterization. The real-variable exchange axioms (Theorems 6.45, 6.47) are formalized from the book's primal (interval-of- $\alpha$ ) definition, not the directional-derivative reformulation (M-EXC'[R]); Theorem 6.47's own three-way equivalence is correspondingly stated with only its first two legs (see Difficulty and MODERATION_NOTES.md/HARD.md — this is a documented scope choice, not a trivializing omission, since the six results using the primal axiom already exercise the chapter's real- variable machinery in full). No numeric constants are hard-coded anywhere in this mission beyond the book's own literal coefficients in Theorem 6.39's cut bound ((n-1)(α-1)). This mission's definitions are redeclared from chunks 06-mconvex-functions-i and 22-ch06b-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the twelve sorrys are welcome; the goal's converse direction and Theorem 6.44's shared-coefficient construction carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
A. S. Kelso Jr. and V. P. Crawford, "Job matching, coalition formation, and gross substitutes," Econometrica, 50 (1982), pp. 1483-1504.
F. Gul and E. Stacchetti, "Walrasian equilibrium with gross substitutes," Journal of Economic Theory, 87 (1999), pp. 95-124.

47 thms4 active usersReviewed

Analysis Operations Research Stochastic Systems·Captain: mikedeng1

Diffusion approximations for open queueing networks with service interruptions 1: explicit Lipschitz bounds for the oblique reflection mapResearch Paper

Motivation

Heavy-traffic and fluid approximations for open queueing networks are obtained by writing the queue-content process as a deterministic function of a simpler netput process (arrivals minus potential service, corrected for routing) and then transferring a functional limit theorem for the netput through that function. The function is the multidimensional reflection map of Harrison and Reiman (Harrison and Reiman 1981), extended from continuous paths to paths with jumps by Reiman (Reiman 1984). The transfer works only if the map is continuous, and quantitative bounds on the approximation error require it to be Lipschitz with a known modulus.

Chen and Whitt (Chen and Whitt 1993) use this map to derive diffusion approximations for networks whose servers are subject to interruptions. Before doing so, Section 2 of the paper supplies "explicit Lipschitz bounds" for the map in the uniform topology: a bound in the Harrison–Reiman scaling (Proposition 2.1) and a new bound that depends on the routing matrix only through its powers (Proposition 2.3).

Timeline. Harrison and Reiman (1981) proved existence, uniqueness and continuity of the map on continuous paths for a routing matrix of spectral radius less than one. Reiman (1984) extended it to paths with jumps. Chen and Mandelbaum (Leontief systems, RBV's and RBM's, 1991, cited in the paper as [4]) noted that a minor extension of the argument makes the map Lipschitz on $D([0,T],\mathbb R^n)$ with the uniform topology. Chen and Whitt (1993, Section 2) made the Lipschitz constants explicit.

Setting

Fix a dimension $n$ and an $n\times n$ matrix $Q$ whose transpose $Q^{\mathsf t}$ is substochastic: all entries of $Q$ are nonnegative and every column sum of $Q$ is at most $1$ . Assume also $Q^k \to 0$ as $k\to\infty$ . With Markovian routing, $Q^{\mathsf t}$ is the routing matrix of an open network of $n$ queues.

Vectors $c\in\mathbb R^n$ carry the norm $\|c\| = \sum_j |c_j|$ , and matrices carry the maximum absolute column sum $\|P\| = \max_j \sum_i |P_{ij}|$ (Eq. (2.5)). $D([0,T],\mathbb R^n)$ is the space of paths that are right-continuous with left limits on $[0,T]$ . For a path $x$ , $|x|\in\mathbb R^n$ is the vector of coordinatewise sup norms, $|x|_j = \sup_{0\le t\le T}|x_j(t)|$ , and $\|x\| = \big\||x|\big\| = \sum_j \sup_{t}|x_j(t)|$ .

The reflection of $x \in D$ is the pair $(y,z) = (\psi(x),\phi(x))$ with $y \in D$ and

z = x + (I-Q)\,y \ge 0, \qquad y_j \text{ nondecreasing},\ y_j(0) = 0, \qquad \int_0^T z_j(t)\,dy_j(t) = 0 \quad (1\le j\le n).

The last condition says that $y_j$ increases only when $z_j = 0$ . In queueing terms, $z$ is the vector of queue contents and $y$ the cumulative idleness. The operator $\pi_x(y) = (Qy - x)^{\uparrow}\vee 0$ , where $f^{\uparrow}(t) = \sup_{0\le s\le t} f(s)$ coordinatewise, has the reflection as its fixed point (Eq. (2.4)). Write $\gamma = \|Q^n\|$ .

Formalization targets

Goal: Proposition 2.3

For all $x_1,x_2\in D$ with reflections $(\psi(x_i),\phi(x_i))$ ,

|\psi(x_1)-\psi(x_2)| \le (I-Q)^{-1}|x_1-x_2| \quad\text{componentwise},\tag{2.9}

\|\psi(x_1)-\psi(x_2)\| \le \|(I-Q)^{-1}\|\,\|x_1-x_2\| \le \sum_{k=0}^\infty \|Q^k\|\,\|x_1-x_2\| \le \frac{n}{1-\gamma}\|x_1-x_2\|,\tag{2.10}

\|\phi(x_1)-\phi(x_2)\| \le \big(1+\|I-Q\|\,\|(I-Q)^{-1}\|\big)\|x_1-x_2\| \le \Big(1+\frac{2n}{1-\gamma}\Big)\|x_1-x_2\|.\tag{2.11}

The constants are those of the paper. The goal fixes nothing beyond the standing assumptions on $Q$ .

Milestones

Existence and uniqueness of the reflection for $x\in D$ with $x(0)\ge0$ (Section 2, p. 337).
Eq. (2.4): given (2.1)–(2.2), the complementarity condition (2.3) is equivalent to $y = \pi_x(y)$ .
$\gamma = \|Q^n\| < 1$ (p. 338).
Proposition 2.2: $\|\pi_x^k(y_1)-\pi_x^k(y_2)\| \le \|Q^k|y_1-y_2|\| \le \|y_1-y_2\|$ for $k\ge1$ , the factor $\gamma$ for $k\ge n$ , and $\pi_x^k(y_1)\to\psi(x)$ .
Proposition 2.1: for $Q^* = \Lambda^{-1}Q\Lambda$ with $\Lambda$ diagonal and $\|Q^*\| = \alpha<1$ , the moduli $\|\Lambda\|\|\Lambda^{-1}\|/(1-\alpha)$ for $\psi$ and $1 + \|I-Q\|\|\Lambda\|\|\Lambda^{-1}\|/(1-\alpha)$ for $\phi$ .
Remark (2.1): for $n=1$ , $Q=0$ the bounds are attained.
Remark (2.2): for two queues in series, (2.10) gives modulus $2$ , while (2.7) gives at best $4$ (every modulus $\ge 4$ is attained, $4$ at $z = 1/2$ ).

Significance

Proposition 2.3 makes the queue-content and idleness processes of an open network Lipschitz functions of the netput, in the uniform norm, with a modulus computed from the routing matrix alone. Combined with the fact that Lipschitz continuity in the uniform topology passes to the Skorohod $J_1$ and $M_1$ topologies (Section 2 of the paper), it is what turns a functional central limit theorem for arrival and service processes into a heavy-traffic limit for the network. The paper uses it in exactly this way in Sections 3–4. Explicit moduli also yield rates: an error of order $\varepsilon$ in the netput produces an error of at most $n\varepsilon/(1-\gamma)$ in the idleness process.

On the formal side, the results are proved in the paper, but neither the reflection map nor $D([0,T],\mathbb R^n)$ has a machine-checked development in Mathlib or on this platform. The mission would provide a reusable definition of the oblique reflection map with a Lebesgue–Stieltjes complementarity condition, its fixed-point characterization, and certified Lipschitz constants, as a foundation for any later formal heavy-traffic limit.

Difficulty

The componentwise bound (2.9) is short once the fixed-point form of the map is available. The difficulty lies in the infrastructure beneath it. The fixed-point characterization (2.4) is a one-dimensional Skorokhod-problem argument carried out coordinatewise for paths with jumps, where the complementarity condition must be handled through Lebesgue–Stieltjes measures. A jump of $y_j$ is allowed at a time where $z_j = 0$ even if $z_j$ was positive just before. Existence needs the iterates $\pi_x^k(0)$ to converge in $D$ and the limit to satisfy (2.1)–(2.3). The explicit constants involve $(I-Q)^{-1}$ , $\sum_k\|Q^k\|$ and $\gamma = \|Q^n\|<1$ . The last inequality is a combinatorial fact about transient substochastic matrices. It does not follow from $\|Q\|\le1$ .

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and $\|P\|$ is the maximum absolute column sum. Paths are functions ℝ → Fin n → ℝ, of which only the restriction to $[0,T]$ matters. Membership in $D([0,T],\mathbb R^n)$ is the predicate IsCadlagOn T x: right-continuous on $[0,T)$ , left limits on $(0,T]$ , and (redundantly) bounded on $[0,T]$ . The reflection is the predicate IsReflection Q T x y z. Every theorem is stated for all pairs satisfying it, so no choice function and no junk value are involved. Condition (2.3) is encoded as "the Lebesgue–Stieltjes measure $dy_j$ of $\{t\in[0,T]: z_j(t)>0\}$ is zero". For $z\ge0$ this is equivalent to $\int_0^T z_j\,dy_j=0$ . $\pi_x^k$ is Nat.iterate, $(I-Q)^{-1}$ is Mathlib's matrix inverse (invertible under the standing assumptions), and $\sum_k\|Q^k\|$ is a tsum stated together with its summability.

Corrections and conventions, each disclosed in the item concerned:

The norm (2.6). The page prints $\|x\| = \sup_t\sum_j|x_j(t)|$ . Under that norm Propositions 2.1 and 2.3 are false for $n\ge2$ . With $Q=0$ , $n=2$ , $T=1$ , $x_1\equiv0$ and $x_2 = (-\mathbf 1_{[0.1,0.2)}, -\mathbf 1_{[0.3,0.4)})$ , one gets $\|x_1-x_2\|=1$ but $\psi(x_2) = (\mathbf 1_{[0.1,1]},\mathbf 1_{[0.3,1]})$ has norm $2$ . The paper's proofs are valid for $\|x\| = \sum_j\sup_t|x_j(t)|$ , which is used throughout. In dimension one the two norms coincide.
(2.8) prints $\phi(x_1)-\phi(x_1)$ . The formalization states $\phi(x_1)-\phi(x_2)$ .
(2.2)–(2.3) print the index range $1\le j\le J$ . The dimension is $n$ .
$x(0)\ge0$ is added to the existence item. Conditions (2.1)–(2.2) force $z(0)=x(0)$ , so no reflection exists otherwise. The Lipschitz bounds are stated for all solution pairs and are vacuous exactly when some $x_i(0)$ has a negative coordinate.
Proposition 2.1 assumes only that $\Lambda$ is diagonal with nonzero entries. All quantities depend on $|\Lambda|$ , so this covers the positive scaling of Harrison and Reiman.
Eq. (2.4) keeps the standing assumptions on $Q$ as on the page, although the equivalence does not use them.

A trivializing formalization would read (2.3) through a Bochner integral, which is $0$ for non-integrable integrands, or take suprema over unbounded families. The measure-zero encoding and the boundedness built into IsCadlagOn rule both out. A sorry-free check shows that Remark (2.1)'s jump example satisfies IsReflection.

Welcome contributions: a general API for càdlàg paths on $[0,T]$ (boundedness, measurability, running suprema), the one-dimensional Skorokhod lemma for càdlàg paths, and the Neumann series for transient substochastic matrices. All of these are reusable beyond this mission.

Selected references

H. Chen and W. Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993) 335–359. https://doi.org/10.1007/BF01149260
J. M. Harrison and M. I. Reiman, Reflected Brownian motion on an orthant, Annals of Probability 9 (1981) 302–308. https://doi.org/10.1214/aop/1176994428
M. I. Reiman, Open queueing networks in heavy traffic, Mathematics of Operations Research 9 (1984) 441–458. https://doi.org/10.1287/moor.9.3.441
H. Chen and A. Mandelbaum, Discrete flow networks: diffusion approximations and bottlenecks, Annals of Probability 19 (1991) 1463–1519. https://doi.org/10.1214/aop/1176990220

10 thms2 active usersReviewed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XIX: Theory of Optimal Stopping ProblemsTextbook

Motivation

A gambler watching a sequence unfold has to decide, at each moment and knowing only the past, whether to take what is on the table or wait for something better. That is the whole of optimal stopping, and it is one of the few problems in stochastic control with a clean and completely general answer: the value of the problem is the smallest superharmonic function dominating the immediate payoff. Snell (1952) proved the martingale form; the dynamic-programming form is due to Chow, Robbins and Siegmund. It is the structure behind the pricing of American options, the secretary problem, sequential hypothesis testing, and the bandit problems of Chapter 5.

Bäuerle and Rieder's Chapter 10 (Markov Decision Processes with Applications to Finance, Springer, 2011) derives this from their own Markov-decision machinery rather than from martingale theory, which makes the whole development elementary and self-contained: a stopping problem is a Markov Decision Problem whose action space is {continue, stop}, so Chapter 2's finite-horizon theory and Chapter 7's unbounded-horizon theory apply to it verbatim. The chapter then runs the resulting theory on three classical problems and solves each one in closed form.

Setting

The problem. A Markov process (X_n) on a Borel space E is observed. A stopping time is a random time τ with {τ ≤ n} ∈ F_n — "upon observing the process until time n we can decide whether or not τ has already occurred". Stopping at τ collects

R_\tau := \sum_{k=0}^{\tau-1} c_k(X_k) + g_\tau(X_\tau),

a running reward c_k while continuing and a stopping reward g_τ at the end, and the problem is to find V_N^*(x) := sup_{τ ≤ N} E_x[R_τ] (10.1). Assumption (B_N) — finiteness of the supremum of the positive parts — is what makes this well posed.

The reduction (Theorem 10.1.2). Take A = {0,1}, let a = 0 mean continue and a = 1 mean stop, and make the transition law uncontrollable on continuation and absorbing on stopping. A policy π = (f_0,…,f_{N-1}) induces the stopping time τ_π = inf{n | f_n(X_n) = 1} ∧ N, and conversely every stopping time is a history-dependent policy. The theorem says the two suprema agree: the extra history buys nothing.

The recursion (Theorems 10.1.3, 10.1.5). The Bellman operator becomes a two-branch maximum,

\mathcal{T}v(x) = \max\Big\{g(x),\ c(x) + \beta\int v(x')Q^X(dx'|x)\Big\},

with no action variable left in it. In the stationary case J_0 = g, J_n = \mathcal{T}J_{n-1}; the J_n increase, the sets S_n^* = {J_n = g} shrink — "the tendency to stop is non-decreasing as time goes by" — and the optimal rule is "stop on first entry into S_{N-n}^*".

The unbounded horizon (§10.2). Now the reward is discounted, R_τ = Σ β^k c(X_k) + β^τ g(X_τ) for τ < ∞, the value is V_∞^*(x) = sup_{τ<∞} E_x[R_τ], and there is no terminal condition to induct from. Three candidate values present themselves: V_∞^*; G = sup_π liminf_n J_{nπ}, a supremum over policies of limits of finite-horizon values; and J = lim_n J_n, which exists by monotonicity. Theorem 10.2.2, the goal, says all three coincide, that the common value solves J = \mathcal{T}J and satisfies 0-free bounds, and — the characterization — that it is the smallest c-superharmonic function majorizing g.

Turning the value into a rule (Theorems 10.2.3, 10.2.7, Corollaries 10.2.6, 10.2.8). Knowing the value is not knowing when to stop. Theorem 10.2.3 produces the stopping region as S^* = {J = g} = {d ≥ 0} where d = lim_n d_n, under two conditions that Corollary 10.2.6 then gives three checkable sufficient conditions for. Theorem 10.2.7 is the practical one, the One-Step-Look-Ahead Rule: if the set where stopping now beats stopping one step later is closed under the transition law, then the myopic rule is globally optimal. Corollary 10.2.8 adds monotonicity and gets a threshold.

Three applications (§10.3). The house seller who receives i.i.d. offers and pays maintenance on each rejection should accept the first offer above an explicit threshold, obtained as the maximiser of a one-dimensional function (Theorem 10.3.1). The secretary problem's value function is computed exactly (Proposition 10.3.2), giving the classical rule — reject the first k^*, then take the first leader — with success probability (k^*/N)h(k^*) and k^*(N)/N → 1/e (Theorem 10.3.3). And when the offers' distribution has an unknown parameter, MTP_2 of the likelihood propagates into monotonicity of the value in the information state (Theorem 10.3.4), with a fully explicit solution for the exponential/Inverse-Gamma conjugate pair (Theorem 10.3.6).

What is being asked

Formalize Theorem 10.2.2 in full: the three-way equality of V_∞^*, G and J, the fixed point equation, and — the part that carries the theorem — minimality among all functions that are both c-superharmonic and above g. Asserting only that J is such a function, or only one of the two conditions, is a strictly weaker and different claim.

The twelve milestones are the rest of the chapter, in attack order: the reduction and the two recursions, then the unbounded-horizon apparatus, then the three worked problems.

The stopping-time apparatus is built rather than assumed — the chain's law pinned by its finite-dimensional distributions, stopping times valued in ℕ ∪ {∞}, rewards vanishing at ∞ — because every theorem here is the identification of a supremum over stopping times with something computable, and carrying the value as an abstract function would make them vacuous. Every supremum is taken as a least upper bound against an explicit set of achievable values rather than by sSup, so that a set unbounded above is not silently given the value 0.

16 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XX: Perpetual American Options and Credit GrantingTextbook

Motivation

An American option may be exercised at any moment up to maturity, so pricing one is not an integration problem but a stopping problem: the holder must decide, at each date and in each state of the market, whether the payoff available now beats the option value of waiting. A perpetual American put pushes this to its limit — there is no maturity at all, so the horizon is unbounded and the problem has no terminal condition to induct backwards from. What replaces the terminal condition is a fixed point characterization, and the classical answer, going back to McKean (1965) and Merton (1973) in continuous time and to Cox, Ross and Rubinstein (1979) in the binomial model, is that the price is the smallest superharmonic majorant of the payoff.

Bäuerle and Rieder's Chapter 11 (Markov Decision Processes with Applications to Finance, Springer, 2011) derives this from their own general unbounded-horizon stopping theory rather than from stochastic analysis, and in the same chapter applies the bounded-horizon version to a problem from banking rather than trading: when should a bank cancel a credit line? The two halves share one mathematical shape — a stopping problem whose optimal policy turns out to be of threshold type — and this mission formalizes both, with the perpetual put as the goal.

Setting

The binomial model (§11.1). A stock moves from price $x$ to $xu$ with risk-neutral probability $q$ and to $xd$ with $1-q$ , where $0 < d < u$ , and the discount factor is $\beta \in (0,1]$ . The defining relation of the risk-neutral measure,

\beta q u + \beta(1-q)d = 1,

is carried as a hypothesis of the model: it is what makes the discounted stock price a martingale, and the proofs use it directly.

The American put with strike $K$ pays $(K-x)^+$ when exercised. With $n$ periods to maturity its price satisfies the recursion $J_0(x) = (K-x)^+$ and

J_n(x) = \max\Big\{(K-x)^+,\ \beta\big(q J_{n-1}(xu) + (1-q)J_{n-1}(xd)\big)\Big\} =: \mathcal{T}J_{n-1}(x),

the maximum being "exercise now" against "hold". Proposition 11.1.2 describes the price $\pi_n(x) := J_{N-n}(x)$ at time $n$ of an option maturing at $N$ : it is continuous in $x$ , decreasing in $n$ , and — the part that carries the argument — $x \mapsto \pi_n(x) + x$ is increasing, even though $\pi_n$ itself decreases in $x$ . That single reformulation, obtained by adding $x$ to both sides of the recursion and using the risk-neutral relation, is what yields the threshold structure: there are exercise boundaries $K =: x_N^* \ge x_{N-1}^* \ge \dots \ge x_0^* \ge 0$ with $\tau^* = \inf\{n \le N \mid X_n \le x_n^*\}$ optimal. Exercise when the stock falls far enough, and the boundary rises as maturity approaches.

The perpetual put (Theorem 11.1.3, the goal). With no expiration date the price at time zero is a supremum over all stopping times, $\tau \le \infty$ included:

P(x) := \sup_{\tau \le \infty} \mathbb{E}^{\mathbb{Q}}_x\big[\beta^\tau (K - S_\tau)\big],

with the stopping reward set to zero on $\{\tau = \infty\}$ . The theorem says four things: $P$ is the limit of the finite-maturity prices $J_n$ ; $P$ solves $\mathcal{T}P = P$ and satisfies $0 \le P \le K$ ; $P$ is the smallest superharmonic function majorizing $(K-x)^+$ ; and, if the value $J_{f^*}$ of the exercise-region policy dominates $\mathcal{T}J_{f^*}$ , then $P$ equals that value and $\tau^* = \inf\{n \mid X_n \in E^*\}$ , the hitting time of $E^* = \{x \mid P(x) = (K-x)^+\}$ , is optimal.

The conditional in part d) is the book's own and is not decoration: without it the exercise region need not deliver an optimal stopping time, and the unconditional version is a different, false statement. The boundedness $0 \le P \le K$ in b) is likewise a genuine claim rather than a side remark — the fixed point equation alone admits other solutions, and it is boundedness together with minimality that pins $P$ down among them.

Credit granting (§11.2). A bank holds a credit contract of maximal duration $N$ . Each period it observes a rating class $x_n$ evolving as a Markov process $Q^X$ , and chooses to extend — earning $c(x)$ — or to cancel, ending the contract. The value iteration is $J_n(x) = \max\{0,\ c(x) + \beta\int J_{n-1}\,dQ^X(\cdot|x)\}$ . Under two structural assumptions — $c$ increasing, and $Q^X$ stochastically monotone, so that a better-rated borrower stays better-rated — Theorem 11.2.1 gives the same shape of answer as the option: cancel exactly when the rating falls below a threshold $x_n^*$ , and those thresholds rise as the remaining duration shortens, since a marginal borrower is no longer worth keeping when there is little time left to recover.

Theorem 11.2.2 repeats this when the borrower is not rated at all. The bank has only a prior $\mu_0$ on the repayment probability and one signal per period; the state $(s,n)$ records $s$ positive signals out of $n$ , and the expected repayment probability is the posterior mean $q(s,n)$ . Monotonicity here is for the order of p. 342 — more positive signals and fewer negative ones — and not the coordinatewise order, under which the claim would be false: an extra signal that is negative makes the state worse.

What is being asked

Formalize Theorem 11.1.3 in full, all four parts: the limit identification, the fixed point equation with its bounds, the minimality among superharmonic majorants, and the conditional optimality of the exercise-region stopping time. The three milestones are Proposition 11.1.2, the finite-horizon put whose threshold structure the perpetual case specializes, and the two credit granting theorems, which run the same bounded-horizon argument on a different model.

The stopping-time apparatus is built rather than assumed: the stock path, the law $\mathbb{Q}$ pinned by its finite-dimensional distributions, stopping times valued in $\mathbb{N}\cup\{\infty\}$ , and the reward vanishing at $\infty$ . Part a) of the goal is the identification of the supremum with $\lim_n J_n$ , so carrying $P$ as an abstract function would make the theorem vacuous.

6 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Diffusion approximations for open queueing networks with service interruptions 2: jump-diffusion heavy-traffic limit for long up and down timesResearch Paper

Motivation

Servers in manufacturing lines, communication links and service systems break down, are taken offline for maintenance, or go on vacation. When the interruptions are rare but long, they dominate congestion. A single down period can build a backlog that takes a long time to clear, and in a network that backlog propagates downstream. Standard heavy-traffic diffusion approximations, which describe queue lengths by reflected Brownian motion, do not capture this effect.

Chen and Whitt (Queueing Systems 13, 1993) identify a regime in which the effect survives in the limit. Up times are of order $n$ and down times of order $\sqrt n$ , while the load is within $1/\sqrt n$ of capacity. Under the diffusion scaling each down period then becomes a jump, and the limit of the queue-length process is a reflected jump-diffusion. The paper generalises the single-station result of Kella and Whitt (Adv. Appl. Probab. 22, 1990; reference [22] of the paper) to open networks.

Timeline:

1981: Harrison and Reiman define the multidimensional reflection map on continuous paths (Ann. Probab. 9). Reiman (Math. Oper. Res. 9, 1984) extends it to paths with jumps.
1990: Kella and Whitt prove the one-station jump-diffusion limit for long up and down times.
1991: Chen and Mandelbaum give fluid and diffusion limits of open networks without interruptions (Math. Oper. Res. 16 and Ann. Probab. 19; references [5], [6] of the paper).
1993: Chen and Whitt prove the network case with interruptions (this mission), in Skorohod's $M_1$ topology.

Setting

A network has $J$ single-server stations. Customers arrive from outside station $j$ according to a counting process $A_j$ . Station $j$ completes $S_j(t)$ services in its first $t$ units of busy time. The $l$ th departure from station $k$ is routed to station $j$ when the indicator $\chi_{kj}(l)=1$ , and $R_{kj}(m)=\sum_{l\le m}\chi_{kj}(l)$ counts such departures. Station $j$ alternates up periods $u^j_1,u^j_2,\dots$ and down periods $d^j_1,d^j_2,\dots$ , starting up, and $D_j(t)$ is its cumulative down time in $[0,t]$ . With a work-conserving discipline, the queue length $Z$ and the busy time $B$ satisfy

Z_j(t)=Z_j(0)+A_j(t)+\sum_{k}R_{kj}\big(S_k(B_k(t))\big)-S_j(B_j(t)),\qquad B_j(t)=\int_0^t 1[Z_j(s)>0,\ j\text{ up at }s]\,ds ,

and the idle time is $Y_j(t)=t-D_j(t)-B_j(t)$ .

The reflection map $(\psi,\phi)$ associated with a matrix $Q$ takes a path $x$ to the pair $(y,z)$ with $z=x+(I-Q)y\ge 0$ , $y$ nondecreasing, and $y_j$ increasing only when $z_j=0$ .

A sequence of networks is indexed by $n$ . The arrival, service and routing processes satisfy functional central limit theorems with rates $\lambda^n\to\lambda$ and $\mu^n\to\mu$ at speed $1/\sqrt n$ . Up and down times scale as $(u^{j,n}_k/n,\ d^{j,n}_k/\sqrt n)\Rightarrow(u^j_k,d^j_k)$ . The network is balanced, $\lambda=[I-P^{\mathsf t}]\mu$ , with $P$ the routing matrix. The limit down time $\hat D_j(t)$ is the sum of $d^j_k$ over the up periods completed by time $t$ , which is a pure-jump process.

The $M_1$ topology on paths with jumps compares completed graphs, in which each jump is filled in by the straight segment from $x(t-)$ to $x(t)$ , through their monotone parametrisations.

Formalization targets

Goal: Theorem 4.1, case $J=1$

For a single station with feedback probability $p\in[0,1)$ , with $\hat Z^n(t)=n^{-1/2}Z^n(nt)$ , $\hat B^n(t)=n^{-1/2}[B^n(nt)-nt]$ , $\hat Y^n(t)=n^{-1/2}Y^n(nt)$ and $\hat D^n(t)=n^{-1/2}D^n(nt)$ ,

(\hat Z^n,\hat B^n,\hat Y^n,\hat D^n)\Rightarrow(\hat Z,\hat B,\hat Y,\hat D)\quad\text{in }D((0,\infty),\mathbb R^{4},M_1).

Here $\hat Z=\phi(\hat X)$ , $\hat Y=\mu^{-1}\psi(\hat X)$ and $\hat B=-\hat D-\hat Y$ , with $Q=p$ and

\hat X(t)=\hat Z(0)+\hat\xi(t)+\big(c_\lambda-(1-p)c_\mu\big)t+(1-p)\mu\hat D(t).

The paper states Theorem 4.1 for $J$ stations, with the analogous formulas and $Q=P^{\mathsf t}$ . The mission's goal is its case $J=1$ (see Formalization scope).

Milestones

Lemma 4.1: $\hat D^n\Rightarrow\hat D$ in $D((0,\infty),\mathbb R^J,M_1)$ .
Lemma 4.2: $n^{-1}B^n_j(nt)\to t$ u.o.c.
Eq. (4.24): $n^{-1/2}\xi^n(nt)\to\hat\xi(t)$ u.o.c.
Eqs. (4.28)–(4.29): $\big(n^{-1/2}X^n(nt),\,n^{-1/2}D^n(nt)\big)\to(\hat X,\hat D)$ jointly in $M_1$ .
The almost-sure form of Theorem 4.1 on a Skorohod representation space, case $J=1$ .

Significance

The theorem yields a tractable approximation for networks with rare long interruptions: a reflected Lévy-type process driven by a Brownian part and a compound jump part. Its distribution can be studied through the reflection map. The jump directions $[I-P^{\mathsf t}]\operatorname{diag}(\mu)e_j$ make explicit how an outage at one station drains its downstream stations while its own queue builds up. Remark (4.3) of the paper derives a diffusion analogue of Little's law from the same limit.

The theorem is proved in the paper, and no part of it has been formalized. A formalization would produce the first machine-checked $M_1$ topology on paths with jumps, a heavy-traffic limit theorem for a queueing network, and the random-time-change argument for counting processes.

Difficulty

The obvious argument chains three facts: the primitive processes converge, hence so does the scaled free process $X$ , and the reflection map is continuous. Two steps break. First, subtraction is not continuous in $M_1$ when the two paths jump at the same time in opposite directions, so the joint convergence of $\hat D^n$ across stations needs (4.11) and one common parametrisation. Second, the reflection map is Lipschitz in the uniform topology, but the uniform topology cannot see jumps that occur at nearby times. Carrying the convergence through the reflection map in the $M_1$ topology requires controlling how the regulator and the regulated process move along each jump segment of $\hat X$ , jointly for all coordinates.

Formalization scope

Stations are Fin J; the network index is n : ℕ, and only $n\to\infty$ enters. Durations are indexed from $0$ in Lean. The queue length is integer valued, (3.2) is computed in $\mathbb Z$ , and a solution satisfies $Z\ge 0$ .

Solutions, not constructions. Every statement quantifies over all solutions $(Z^n,B^n)$ of (3.2)–(3.3) and all reflection pairs of $\hat X$ . Existence and uniqueness are asserted in the paper by citation and are not assumed or proved here.
$M_1$ . Parametric representations are monotone in the order of the completed graph, which is the standard definition. The page states only that the time component is nondecreasing. Convergence on $(0,\infty)$ means convergence on every $[a,b]$ with $0<a<b$ continuity points of the limit. Jump segments are segments in $\mathbb R^d$ (strong $M_1$ ). Convergence in $D((0,\infty),\cdot,M_1)$ includes the requirement that every path be càdlàg on $(0,\infty)$ , so a copy of the limit that is continuous nowhere cannot satisfy the continuity-point condition vacuously.
Weak convergence is in coupling form: one probability space carries copies with the right laws that converge almost surely. The limits in (4.1)–(4.4) are continuous, so there the mode is u.o.c.
Corrected printed errors. Lemma 4.2 is stated with $n^{-1}$ in place of the printed $n^{-1/2}$ , as in its proof. The map on p. 346 is read as $\phi(X)=Z$ , $\psi(X)=\operatorname{diag}(\mu)Y$ , following (4.13). The reflection map allows $y(0)\ge 0$ , because $\hat X(0)$ may leave the orthant when $\hat D(0)>0$ ; when $x(0)\ge 0$ this agrees with (2.2).
Added hypotheses. The processes $Z^n,B^n,\hat Z,\hat Y$ are assumed to be stochastic processes (measurable at each time). All networks share one probability space, so that the routing is literally common. No independence is assumed.
The goal is the case $J=1$ of Theorem 4.1. The printed theorem claims strong $M_1$ convergence, with one parametric representation for all $4J$ coordinates, for every $J$ . For $J\ge 2$ that claim fails: during an upstream outage, a downstream queue that empties part-way through the jump bends the prelimit graph of $(\hat D_j,\hat Y_k)$ , while the limit's completed graph is a straight segment. For $J=1$ every coordinate moves linearly through each jump. The milestones Lemma 4.1, Lemma 4.2, (4.24) and (4.28)–(4.29) are stated for general $J$ , and the almost-sure core of the proof for $J=1$ .

A trivializing formalization is excluded. The hypotheses are satisfiable (for example by deterministic arrival and service processes), $\hat N$ is used only when $\sum_ku^j_k=\infty$ , and laws are compared only for measurable path maps.

Needed infrastructure: the Skorohod space with the $M_1$ topology and its characterization on $(0,\infty)$ , continuity of addition and of composition with continuous time changes, the multidimensional reflection map on paths with jumps, and a Skorohod representation argument. Proofs of Lemma 4.1 and Lemma 4.2 are welcome independently.

Selected references

H. Chen, W. Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993) 335–359. https://doi.org/10.1007/BF01149260
O. Kella, W. Whitt, Diffusion approximations for queues with server vacations, Adv. Appl. Probab. 22 (1990) 706–729 (reference [22] of the paper).
J. M. Harrison, M. I. Reiman, Reflected Brownian motion on an orthant, Ann. Probab. 9 (1981) 302–308. https://doi.org/10.1214/aop/1176994472
H. Chen, A. Mandelbaum, Discrete flow networks: diffusion approximations and bottlenecks, Ann. Probab. 19 (1991) 1463–1519 (reference [6] of the paper).
M. I. Reiman, Open queueing networks in heavy traffic, Math. Oper. Res. 9 (1984) 441–458 (reference [25] of the paper).
W. Whitt, Some useful functions for functional limit theorems, Math. Oper. Res. 5 (1980) 67–85. https://doi.org/10.1287/moor.5.1.67
A. V. Skorohod, Limit theorems for stochastic processes, Theory Probab. Appl. 1 (1956) 261–290. https://doi.org/10.1137/1101022

10 thms1 active userReviewed

Completed

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

Discrete Convex Analysis XXIII: Directional Derivatives and Subdifferentials of M-Convex FunctionsTextbook

Motivation

An M-convex function is defined on the integer lattice, but chapter 6's earlier results (companion missions 06-mconvex-functions-i, 22-ch06b-mconvexfunctions, 23-ch06c-mconvexfunctions) show it always extends to a genuine convex function on real space. Once that extension exists, every tool of classical convex analysis — directional derivatives, subdifferentials, positive homogeneity — becomes available, and the natural question is whether these classical objects remain combinatorially special when applied to an M-convex function's extension. This mission answers that question at its sharpest: the directional derivative of an M-convex function at any point is again a positively homogeneous M-convex function, its subdifferential is exactly the admissible-potential set of a distance function satisfying the triangle inequality, and this correspondence between positively homogeneous M-convex functions and triangle-inequality distance functions is itself a clean one-to-one correspondence. This closes the loop between chapters 4-5 (M-convex and L-convex sets, distance functions) and the continuous convex-analytic machinery chapter 8 needs for its duality theory.

Companion missions 06-mconvex-functions-i, 22-ch06b-mconvexfunctions, and 23-ch06c-mconvexfunctions cover this chapter's optimality theory, algebraic toolkit, and convex-extensibility characterization. This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the chapter's real-variable capstones: the transfer of M-convexity's basic operations, optimality criterion, and supermodularity to the polyhedral (real-variable) setting, the identification of positively homogeneous M-convex functions with distance functions satisfying the triangle inequality, and — this mission's goal — the full directional-derivative/subdifferential correspondence.

Setting

Fix a finite ground set $V$ . A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (polyhedral) M-convex if it satisfies the real-variable exchange axiom (M-EXC[R]): for $x,y \in \operatorname{dom}_{\mathbb R} g$ and $u \in \operatorname{supp}^+(x-y)$ , some $v \in \operatorname{supp}^-(x-y)$ and $\alpha_0 > 0$ make the exchange inequality hold on $\alpha \in [0,\alpha_0]$ ; M♮-convex if its lift to one extra coordinate is M-convex. The directional derivative of $g$ at $x \in \operatorname{dom}_{\mathbb R} g$ in direction $d$ is $g'(x;d) = \inf_{t>0} (g(x+td) - g(x))/t$ . A function is positively homogeneous if $g(tx) = t \cdot g(x)$ for all $t > 0$ ; write $0M[\mathbb R \to \mathbb R]$ for the positively homogeneous polyhedral M-convex functions. A distance function $\gamma$ satisfying the triangle inequality and its set of admissible potentials $D(\gamma)$ were introduced in chapter 5; the subdifferential $\partial_{\mathbb R} f(x) = \{p : f(y) - f(x) \ge \langle p, y-x \rangle\ \forall y\}$ generalizes this to any function $f$ at a point $x$ in its domain.

Formalization targets

Goal: the directional-derivative/subdifferential correspondence

For $f \in M[\mathbb R \to \mathbb R]$ and $x \in \operatorname{dom}_{\mathbb R} f$ , setting $\gamma_{f,x}(u,v) = f'(x;-\chi_u+\chi_v)$ :

\gamma_{f,x} \text{ satisfies the triangle inequality}, \quad \partial_{\mathbb R} f(x) = D(\gamma_{f,x}) \ne \emptyset, \quad f'(x;\cdot) = \widehat{\gamma_{f,x}}(\cdot),

with the analogous statement for $f \in M[\mathbb Z \to \mathbb R]$ at an integer point $x$ , using $\gamma_{f,x}(u,v) = f(x-\chi_u+\chi_v)-f(x)$ (Theorem 6.61). This is the weakest stable form: it identifies the subdifferential exactly, as a set, rather than bounding its size or complexity, and holds at every point of the domain uniformly.

Supporting structural targets

Ten further results build the real-variable toolkit and the positive-homogeneity correspondence this goal completes: the transfer of M♮-convexity, the basic operations, the optimality criterion, supermodularity, and weighted-minimizer polyhedrality to the real-variable setting (Theorems 6.48-6.52, Proposition 6.53), the identification of the classes $0M[\mathbb Z|\mathbb R \to \mathbb R]$ and $0M[\mathbb R \to \mathbb R]$ and the compatibility of convex extension with positive homogeneity (Proposition 6.56), the two directions of the correspondence between positively homogeneous M-convex functions and triangle-inequality distance functions (Propositions 6.57-6.58, Theorem 6.59), and the fact that a directional derivative of an M-convex function is itself positively homogeneous and M-convex (Proposition 6.60).

Significance

Theorem 6.61 is the technical bridge that lets discrete convex analysis borrow the entire apparatus of classical convex duality: because the subdifferential of an M-convex function is always the admissible-potential set of a chapter-5 distance function, every fact already proved about $D(\gamma)$ (its polyhedral structure, its own L-convexity, its relationship to shortest paths) transfers immediately to subdifferentials of M-convex functions. This is exactly the mechanism the book calls out as essential for Chapter 8's separation theorem for M♮-convex functions. The $0M \leftrightarrow T$ correspondence (Theorem 6.59) is independently significant: it says the positively homogeneous special case of M-convex function theory — which is what directional derivatives of any M-convex function reduce to, by Proposition 6.60 — is exactly as rich as ordinary shortest-path distance function theory, no more and no less, so nothing new needs to be built to understand local behavior at a point.

None of these results are open — they are Murota's account of how the discrete exchange axiom interacts with directional differentiation and subgradients, a bridge chapter between the purely combinatorial theory of chapters 4-6 and the duality theory of chapter 8. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (MExchangeAxiomR, DirDeriv, GammaHat) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to Theorem 6.61 would try to compute $\partial_{\mathbb R} f(x)$ directly from the definition of subgradient and separately verify it happens to equal some $D(\gamma)$ ; the book's actual proof instead derives the equality of sets from the M-optimality criterion (Theorem 6.52) applied pointwise: $p \in \partial_{\mathbb R} f(x)$ is shown, via a chain of logical equivalences, to be exactly the condition defining $D(\gamma_{f,x})$ , so no separate verification of polyhedrality or nonemptiness is needed beyond what Theorem 6.52 and Proposition 6.60 already supply. The genuine difficulty is upstream, in Proposition 6.60 itself: showing a directional derivative is M-convex requires exploiting the local validity of the identity $f(x+d)-f(x) = f'(x;d)$ for small $\|d\|_1$ (Eq. (6.85)) and then extending the exchange property from that neighborhood to all of $\mathbb R^V$ using positive homogeneity — a two-step argument with no single-step shortcut, since the exchange axiom's defining inequality is not obviously homogeneous-invariant on its own.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; real-domain functions are (V→ℝ)→WithTop ℝ. The directional derivative is built directly as an infimum of difference quotients over $t>0$ , matching the book's own local characterization (Eq. (6.85)) without a separate limit construction. Positive homogeneity and the classes 0M[R→R]/0M[Z→R] are stated exactly as the book defines them (the latter via positive homogeneity of the convex extension, not of f itself, since f is undefined off Zⱽ). Theorems 6.49-6.50 restate 4 of their 8 operations (matching the identical scope decision for chunk 22-ch06b-mconvexfunctions's Theorem 6.13); Theorem 6.61 omits the dual-integral refinement clauses for the M[R→R|Z]/ M[Z→Z] sub-classes. Both reductions are documented, not trivializing omissions — see Difficulty above and HARD.md/MODERATION_NOTES.md. No numeric constants are hard-coded anywhere in this mission. This mission's definitions are redeclared from chunks 06-mconvex-functions-i, 21-ch05b-lconvexsets (for the distance-function/admissible-potential vocabulary), 22-ch06b-mconvexfunctions, and 23-ch06c-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the twelve sorrys are welcome; the goal and Proposition 6.60 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, "M-convex function on generalized polymatroid," Mathematics of Operations Research, 24 (1999), pp. 95-105 (the polyhedral M-convex function theory this mission's real-variable results are drawn from).

56 thms2 active usersReviewed

Completed

Control Theory Dynamic Programming Operations Research+1·Captain: mikedeng1

Robust Control of Markov Decision Processes with Uncertain Transition Matrices 2: The Robust Bellman Recursion for Discounted Infinite-Horizon MDPsResearch Paper

Motivation

A Markov decision process (MDP) is solved by dynamic programming only when its transition probabilities are known. In practice they are estimated from data, and the optimal policy of the estimated model can perform badly on the true one. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) showed that, when the uncertainty on the transition matrices has a product ("rectangular") structure, the robust problem, in which the controller minimises the worst expected cost over all admissible transition matrices, keeps the structure of dynamic programming. The robust Bellman operator replaces the expectation of the next-stage value by a support function of the uncertainty set. That operator is the basis of later work on robust MDPs and robust reinforcement learning.

Timeline:

Bagnell, Ng and Schneider (2001) considered the max–min value $\psi_\infty(\Pi, \mathcal T)$ and stated without proof that it is computed by the recursion below.
Iyengar (Math. Oper. Res. 30(2), 2005; technical report 2003) independently proved the robust Bellman recursion for the discounted infinite-horizon case.
Nilim and El Ghaoui (2005), Theorem 3, prove the recursion and perfect duality of the stationary discounted game. This mission formalizes that theorem.

Setting

The state space is $\mathcal X = \{1,\dots,n\}$ and the action set $\mathcal A$ is finite and nonempty. Each state–action pair has a cost $c(i,a) \ge 0$ , and costs are discounted by a factor $\nu \in [0,1)$ : the cost at stage $t$ is $\nu^t c(i,a)$ .

Write $\Delta_n = \{p \in \mathbb R^n_+ : p^T\mathbf 1 = 1\}$ for the probability simplex. For each action $a$ and state $i$ a nonempty set $\mathcal P_i^a \subseteq \Delta_n$ is given. It is the set of distributions of the next state that nature may use from state $i$ under action $a$ . No convexity or closedness is assumed. Uncertainty is rectangular: the admissible transition matrices for action $a$ form the product $\mathcal P^a = \mathcal P_1^a \times \cdots \times \mathcal P_n^a$ , so every row is chosen independently.

A stationary control policy $\pi = (\mathbf a, \mathbf a, \dots)$ applies one decision rule $\mathbf a : \mathcal X \to \mathcal A$ at every stage; $\Pi_s$ is the set of them. A stationary policy of nature $\tau \in \mathcal T_s$ fixes one matrix $P^a \in \mathcal P^a$ for each action and uses it forever. Nature chooses after the controller.

From an initial state $i_0$ , the state distribution evolves as $\mu_0 = e_{i_0}$ , $\mu_{t+1}(j) = \sum_i \mu_t(i) P^{\mathbf a(i)}(i,j)$ . The discounted cost is

C_\infty(\pi,\tau) = \sum_{t\ge 0} \nu^t \sum_i \mu_t(i)\, c(i,\mathbf a(i)).

The support function of a set $\mathcal P$ is $\sigma_{\mathcal P}(v) = \sup\{p^T v : p \in \mathcal P\}$ . The robust Bellman operator $g$ and, for a stationary policy $\pi$ , the robust evaluation operator $g_\pi$ act on $v \in \mathbb R^n$ by

g(v)_i = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \qquad g_\pi(v)_i = c(i,\mathbf a(i)) + \nu\,\sigma_{\mathcal P_i^{\mathbf a(i)}}(v).

The two values of the game are

\phi_\infty(\Pi_s,\mathcal T_s) = \min_{\pi\in\Pi_s}\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau), \qquad \psi_\infty(\Pi_s,\mathcal T_s) = \sup_{\tau\in\mathcal T_s}\min_{\pi\in\Pi_s} C_\infty(\pi,\tau).

Formalization targets

Goal: Theorem 3 (Robust Bellman Recursion)

There is a unique $v \in \mathbb R^n$ with $v = g(v)$ , i.e.

v(i) = \min_{a\in\mathcal A}\big(c(i,a) + \nu\,\sigma_{\mathcal P_i^a}(v)\big), \quad i \in \mathcal X, \tag{19}

value iteration $v_{k+1} = g(v_k)$ converges to $v$ from every starting vector (20), and

\phi_\infty(\Pi_s,\mathcal T_s) = v(i_0) = \psi_\infty(\Pi_s,\mathcal T_s).

In addition, every policy that picks a minimising action in (19) is optimal (21), every nature policy whose rows attain $\sigma_{\mathcal P_i^a}(v)$ is optimal for nature (22), and for each stationary $\pi$ the worst-case cost $\sup_\tau C_\infty(\pi,\tau)$ is $v^\pi(i_0)$ , where $v^\pi$ is the unique fixed point of $g_\pi$ (23).

Milestones

Lemma 2 (corrected): for a nondecreasing sup-norm contraction $g$ and $q \ge 0$ , the program $\max q^T v$ s.t. $v \le g(v)$ has value $q^T v_\infty$ at the fixed point $v_\infty$ , every feasible $v$ satisfies $v \le v_\infty$ , and $v_\infty$ is the unique optimizer when $q > 0$ .
The operators $g$ of (29) and $g_\pi$ of (30) are nondecreasing and $\nu$ -Lipschitz in $\|\cdot\|_\infty$ .
(26): $C_\infty(\pi,\tau) = \max\{v(i_0) : v(i) \le c(i,\mathbf a(i)) + \nu \sum_j P^{\mathbf a(i)}(i,j) v(j)\}$ .
(28) ⇒ (23): $\sup_{\tau\in\mathcal T_s} C_\infty(\pi,\tau) = v^\pi(i_0)$ .
(27) ⇒ (19): $\psi_\infty(\Pi_s,\mathcal T_s) = v(i_0)$ .

Significance

The theorem makes the robust discounted problem as tractable as the nominal one. The optimal robust policy is stationary, deterministic and computed by value iteration. Each iteration evaluates one support function per state–action pair, and the paper computes these efficiently for likelihood and entropy uncertainty sets (§§5–6). Perfect duality means that the order of play does not change the value: announcing the policy to an adversarial nature costs nothing. The sequel in this series (Theorem 4) uses Theorem 3 to show that restricting to stationary policies loses nothing.

The result is proved in the paper and, independently, by Iyengar (2005). No machine-checked proof of it is known to exist. Mathlib provides the Banach fixed-point theorem, but it has no MDP library, no discounted cost along a Markov chain and no robust Bellman operator. The mission produces that layer.

Difficulty

The fixed-point half is a direct application of the Banach fixed-point theorem once the $\nu$ -contraction is established. The substance is the link between the fixed point and the probabilistic cost, and the duality.

$C_\infty(\pi,\tau)$ is an infinite series along a Markov chain. Identifying it with the solution of a linear system requires summing a matrix geometric series.
Nature's sets are neither closed nor convex, so its maxima are suprema that need not be attained. The worst case over $\mathcal T_s$ must be approached by rows that nearly attain the support function, with an error controlled through the contraction.
The min–max and max–min values are taken over different information structures. Equality has to come from the fixed point, not from a minimax theorem: the policy set is finite and discrete and nature's set is not convex, so no convexity argument applies.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ, with the componentwise order and Mathlib's sup metric, which is $\|\cdot\|_\infty$ .
The model (RobustMDP.Discounted.Model) carries the costs, the discount $\nu \in [0,1)$ (the range printed in Theorem 3; §4 prints $(0,1)$ ) and the row sets. The row sets are assumed nonempty and contained in $\Delta_n$ and nothing else. Nonemptiness is implicit in the paper.
$\Pi_s$ is Fin n → A. $\mathcal T_s$ is the subtype of A → Fin n → Fin n → ℝ whose rows lie in the row sets, which encodes rectangularity.
$C_\infty$ is a tsum of the discounted stage costs along the forward state distribution. The terms are nonnegative and at most $\nu^t\max c$ , so the series is summable and the tsum is the limit of the $N$ -stage costs, the paper's definition.
$\sigma_{\mathcal P}$ is a real sSup. It is the genuine supremum because every set it is applied to is nonempty and inside $\Delta_n$ .
Every "max" over nature is a supremum: IsLUB, or ⨆ inside $\min_\pi\sup_\tau$ , whose inner sets are shown bounded by conclusion (23). Minima over the finite $\Pi_s$ and over $\mathcal A$ are ⨅ and Finset.inf'. The argmax rows of (22) appear only as a hypothesis on a given nature policy that attains them.
Corrected statements:
- Lemma 2 is false as printed for $q$ with zero entries, so uniqueness of the optimizer is stated only for $q > 0$ .
- In (30), $\sigma(v^\pi)$ is read as $\sigma(v)$ .
- The proof's references to "Lemma 1", "(15) and (16)" and "(14)" are read as Lemma 2, (27)–(28) and (26).
Defining $C_\infty(\pi,\tau)$ as the fixed point of $w = c_\pi + \nu P_\pi w$ would make milestone (26) a tautology and conclusion (23) nearly so. The cost here is the probabilistic series, and the fixed-point characterizations must be proved.
Welcome contributions include a reusable library of discounted Markov chain costs on finite state spaces (the geometric-series identity behind (26)) and support-function lemmas on the simplex (monotonicity, the bound $\sigma_{\mathcal P}(u) - \sigma_{\mathcal P}(v) \le \|u-v\|_\infty$ ). Both are needed by the other missions of this series.

Selected references

A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
J. A. Bagnell, A. Y. Ng, J. Schneider, Solving Uncertain Markov Decision Processes, Technical Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001. https://www.ri.cmu.edu/publications/solving-uncertain-markov-decision-processes/
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

10 thms4 active usersReviewed

Completed

Convex Optimization Functional Analysis Operations Research+2·Captain: mikedeng1

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

Motivation

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

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

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

Setting

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

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

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

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

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

The optimization problem is

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

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

Formalization targets

Goal: Theorem 5.3

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

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

Milestones

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

Companion: Theorem 5.4

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

10 thms4 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis XXIV: Quasi M-Convex FunctionsTextbook

Motivation

Every characterization of M-convexity so far in this series — the exchange axiom, the optimality criterion, convex extensibility, the directional-derivative/subdifferential correspondence — has been an equivalence with M-convexity itself: a function either is M-convex or it is not. Section 6.14 asks a different question: what happens when the exchange axiom's defining inequality is relaxed to only the sign patterns it actually forces? The answer is a hierarchy of "quasi M-convex" conditions — weaker than M-convexity, strong enough to keep the optimality criterion and the proximity/minimizer-cut theorems intact — and, at the top of that hierarchy, a genuinely new characterization of M-convexity itself: a function is M-convex if and only if every one of its linear perturbations is quasi M-convex in the weakest sense. This mission formalizes that entire hierarchy and its capstone, plus two further characterizations of polyhedral M-convexity (via directional derivatives, subdifferentials, and weighted-minimizer polyhedra) that complete the real-variable theory chunk 24-ch06d-mconvexfunctions began.

Setting

Fix a finite ground set $V$ and $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ . Write $\Delta f(z;v,u) = f(z + \chi_v - \chi_u) - f(z)$ . Relaxing the exchange axiom's inequality $\Delta f(x;v,u) + \Delta f(y;u,v) \le 0$ to the sign patterns it forces gives quasi M-convexity (QM) and semistrict quasi M-convexity (SSQM), and requiring only some pair $(u,v)$ rather than every $u$ gives their weaker variants (QMw), (SSQMw); the minimization-only variants (SSQM $\ne$ ), (SSQM $\ne_w$ ) replace " $x,y \in \operatorname{dom} f$ " with " $f(x) \ne f(y)$ ". The set-level analogue (Q-EXC)/(Q-EXCw) relaxes the M-convex-set exchange axiom the same way. For $\alpha \in \mathbb R$ , the level set $L(f,\alpha) = \{x \in \mathbb Z^V : f(x) \le \alpha\}$ . A polyhedral convex function $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (real-variable) M-convex, $f \in M[\mathbb R \to \mathbb R]$ , if it satisfies the real exchange axiom (M-EXC[R]) from chunk 24-ch06d-mconvexfunctions; $L_0[\mathbb R]$ denotes polyhedra realized as $D(\gamma)$ for a triangle-inequality distance function $\gamma$ , and $M_0[\mathbb R]$ denotes real M-convex polyhedral cones.

Formalization targets

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

For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ : (1) the implication diagram (M-EXC[Z]) $\Rightarrow$ (SSQM) $\Rightarrow$ (QM), (M-EXCw[Z]) $\Rightarrow$ (SSQMw) $\Rightarrow$ (QMw), (M-EXC[Z]) $\Leftrightarrow$ (M-EXCw[Z]), (SSQM) $\Rightarrow$ (SSQMw), (QM) $\Rightarrow$ (QMw); (2) $f$ satisfies (M-EXC[Z]) if and only if $f[p]$ satisfies (QMw) for every $p \in \mathbb R^V$ . This theorem is not named in the chunk's own extraction table — the automated extractor, which requires a result's label to start a text line, misses it because it opens mid-paragraph directly after an ASCII-rendered implication diagram — but it is the capstone of the section: its own proof is "combining Theorems 6.72 and 6.74," both formalized here as milestones, and part (2) answers exactly the question a reader of this stretch would ask: what does the entire apparatus of quasi M-convexity ultimately say about M-convexity itself?

Supporting structural targets

Fourteen further results build the hierarchy and complete the real-variable theory. Proposition 6.62 checks the two halves of chunk 24-ch06d-mconvexfunctions's Theorem 6.61 agree at integer points. Theorems 6.63–6.64 add two more characterizations of polyhedral M-convexity — via positively homogeneous directional derivatives and $L_0[\mathbb R]$ -valued subdifferentials, and via $M_0[\mathbb R]$ / $M_0[\mathbb Z|\mathbb R]$ -valued weighted-minimizer polyhedra — to the convex-extensibility characterization chunk 23-ch06c-mconvexfunctions proved. Theorem 6.67 gives two equivalent reformulations of (QMw) as pointwise inequalities; Propositions 6.69–6.70 and Theorems 6.72–6.74 build the level-set/perturbation machinery the goal needs. Theorem 6.75 is the (SSQM $\ne_w$ ) analogue of Theorem 6.67. Theorem 6.76 is the quasi M-optimality criterion (optimality still characterized by local non-improvement, under only the weak quasi-convexity hypotheses). Theorems 6.77–6.79 show the M-minimizer-cut and M-proximity theorems (from missions 06-mconvex-functions-i and 23-ch06c-mconvexfunctions) hold verbatim under the strictly weaker (SSQM $\ne$ ) hypothesis.

Significance

The hierarchy's practical payoff is immediate: Theorems 6.77–6.79 mean the algorithms of chapter 10 that rely on minimizer cuts and proximity bounds do not actually need the full exchange axiom to run correctly on nonlinearly rescaled M-convex functions (Example 6.66 shows any nondecreasing scaling $\phi \circ f$ of an M-convex $f$ is quasi M-convex, yet nonlinear scalings are common in practice and destroy M-convexity itself). The goal, Theorem 6.68, is significant independently: it says the exchange axiom — a condition that looks irreducibly combinatorial, quantifying over pairs of points and directions — is equivalent to a purely ordinal, perturbation-based condition (every linear tilt of $f$ has no strict local improvement that a level set can't witness), giving a genuinely different lens on why M-convexity is the right discrete analogue of convexity. Theorems 6.63–6.64 close out chunk 24-ch06d-mconvexfunctions's program of characterizing polyhedral M-convexity in every classical convex-analytic vocabulary at once (directional derivatives, subdifferentials, weighted minimizers), completing the bridge to Chapter 8's duality theory that chunk builds toward.

None of these results are open — they are Murota's account of how far the exchange axiom's defining inequality can be relaxed while keeping optimization theory intact. What this mission contributes is a faithful, machine-checked formal statement of each, including four theorems (6.68, 6.76, 6.77, 6.78) the platform's own automated extractor missed entirely, extending the shared Lean vocabulary (DeltaF, QMw, LevelSet) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to prove the implication diagram's six arrows and the perturbation equivalence as six independent facts; the book's own proof of part (2) instead derives it in one step from Theorems 6.72 and 6.74 — themselves nontrivial (Theorem 6.74's proof strengthens the local exchange axiom equivalence (Theorem 6.4) to hold whenever the domain merely satisfies (Q-EXCw), then runs a bipartite-matching argument on a 4-point neighborhood to verify the resulting local condition). The difficulty is genuinely upstream of the goal's own statement: everything the goal needs is already proved by the time Theorem 6.68 is reached, so the formalization work is in stating the sixteen distinct axioms and their level-set reformulations precisely enough that "combining 6.72 and 6.74" is literally how a Lean proof would proceed.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; integer-domain functions are (V→ℤ)→WithTop ℝ, real-domain ones (V→ℝ)→WithTop ℝ. All fifteen numbered results — including the four (6.68, 6.76, 6.77, 6.78) the automated extractor missed because their labels open mid-paragraph — are placed as milestone or goal, and every clause of every one is stated in full; no partial-coverage scope reduction was needed in this chunk (contrast chunks 22-ch06b-mconvexfunctions/24-ch06d-mconvexfunctions, which restated 4-of-8-part operations theorems). Two formalization choices are recorded in HARD.md/MODERATION_NOTES.md: " $\inf f[-p] > -\infty$ " is replaced by the equivalent (ArgMinOn ...).Nonempty hypothesis (WithTop ℝ has no $-\infty$ element), matching mission 23-ch06c-mconvexfunctions's identical substitution; and $M_0[\mathbb R]$ / $M_0[\mathbb Z|\mathbb R]$ are realized via the book's own indicator-function device rather than a freestanding cone axiom. This mission's definitions are redeclared from chunks 06-mconvex-functions-i, 22–24-ch06*-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the fifteen sorrys are welcome; the goal and Theorem 6.74 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
M. Avriel, W. E. Diewert, S. Schaible, and I. Zang, Generalized Concavity, Plenum Press, 1988 (the continuous quasi-convexity theory this chapter's discrete analogue generalizes).

56 thms3 active usersReviewed

Convex Optimization Functional Analysis Operations Research·Captain: mikedeng1

On the Maximal Monotonicity of Subdifferential Mappings II: Subdifferentials Are Exactly the Maximal Cyclically Monotone Operators, Unique up to an Additive ConstantResearch Paper

Motivation

A differentiable convex function on $\mathbb{R}^n$ is determined, up to an additive constant, by its gradient, and a vector field is a gradient of a convex function exactly when it satisfies a monotonicity condition along closed cycles. Convex analysis and optimization need the same statement for nonsmooth and extended-valued functions on infinite-dimensional spaces: the subdifferential replaces the gradient, and the question becomes which multivalued maps from a Banach space to its dual arise as subdifferentials, and how much of the function they determine. The answer underlies the treatment of optimality conditions, variational inequalities and evolution equations governed by subdifferentials, where one works with the operator $\partial f$ and needs to recover $f$ from it.

Timeline.

1966: R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific J. Math. 17 (DOI 10.2140/pjm.1966.17.497), studied cyclically monotone operators and stated the characterization of subdifferentials as the maximal cyclically monotone operators (its Theorem 3), together with the maximal monotonicity of subdifferentials (its Theorem 4).
1969: H. Brézis pointed out a gap in the 1966 proofs of maximality and uniqueness: a family of dual vectors $x_\varepsilon^*$ used in the argument might increase unboundedly in norm as $\varepsilon \to 0$ .
1970: Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (DOI 10.2140/pjm.1970.33.209), repaired the argument for arbitrary real Banach spaces, proving Theorem A (maximal monotonicity of $\partial f$ ) and Theorem B (the characterization treated here).

Setting

Let $E$ be a real Banach space with dual $E^*$ , and write $\langle x, x^* \rangle$ for the value of $x^* \in E^*$ at $x \in E$ . A proper convex function on $E$ is a function $f : E \to (-\infty, +\infty]$ , not identically $+\infty$ , with $f((1-\lambda)x + \lambda y) \le (1-\lambda)f(x) + \lambda f(y)$ for all $x, y \in E$ and $0 < \lambda < 1$ . It is lower semicontinuous (lsc) in the norm topology. Its subdifferential is the multivalued map

\partial f(x) = \{\, x^* \in E^* \mid f(y) \ge f(x) + \langle y - x, x^* \rangle \ \ \forall y \in E \,\}.

A multivalued map $T : E \to E^*$ is a cyclically monotone operator if

\langle x_0 - x_1, x_0^* \rangle + \cdots + \langle x_{n-1} - x_n, x_{n-1}^* \rangle + \langle x_n - x_0, x_n^* \rangle \ge 0 \qquad\text{whenever } x_i^* \in T(x_i),\ i = 0, \dots, n,

and maximal cyclically monotone if, in addition, its graph $\{(x, x^*) \mid x^* \in T(x)\}$ is not properly contained in the graph of any other cyclically monotone operator. The conjugate of $f$ is $f^*(x^*) = \sup_{x \in E} (\langle x, x^* \rangle - f(x))$ on $E^*$ , and $j(x) = \tfrac12\|x\|^2$ . In the Lean development these are ProperConvex, subdiff, IsCyclicallyMonotone, IsMaximalCyclicallyMonotone, conj and halfSqNorm, in the namespace RockafellarMaxMono.Cyclic.

Formalization targets

Goal: Theorem B (p. 210)

For every multivalued map $T : E \to E^*$ on a real Banach space $E$ ,

\bigl(\exists f \text{ lsc proper convex with } T = \partial f\bigr) \iff T \text{ is maximal cyclically monotone},

and if $f$ and $g$ are lsc proper convex with $\partial f = T = \partial g$ , then $g = f + c$ for a real constant $c$ . Both halves are one statement.

Milestones, in attack order

(3.7) For a finite continuous convex function $f$ on a real Banach space, $\partial f(x)$ is nonempty and weak* compact and $f'(x;u) = \max\{\langle u, x^* \rangle \mid x^* \in \partial f(x)\}$ .
Finite continuous case (pp. 214–215). For finite continuous convex $f, g$ on a real Banach space, $\partial g(x) \supset \partial f(x)$ for all $x$ implies $g = f + \mathrm{const}$ .
(3.1) $\partial(f + j)(x) = \partial f(x) + \partial j(x)$ for lsc proper convex $f$ .
Proposition 1 $x^{**} \in \partial f^*(x^*)$ if and only if $x^{**}$ is a weak** limit of a bounded net $x_i$ with $x_i^* \in \partial f(x_i)$ , $x_i^* \to x^*$ in norm.
(p. 213) $(f + j)^*$ is finite and continuous on $E^*$ .
(p. 211) $f^{**}$ restricted to $E$ is $f$ .
(3.6) For lsc proper convex $f, g$ : $\partial g(x) \supset \partial f(x)$ for all $x$ implies $g = f + \mathrm{const}$ .

Significance

The result. Theorem B gives an intrinsic description of subdifferential maps: an operator is the subdifferential of a closed proper convex function if and only if it satisfies the cycle inequality and cannot be enlarged without violating it. The uniqueness clause says that a closed convex function is recovered from its subdifferential up to a constant, the nonsmooth counterpart of recovering a function from its gradient. Milestone 7 is stronger than uniqueness: a one-sided inclusion $\partial f \subseteq \partial g$ already forces $g = f + c$ , and this is what gives maximality.

Formalizing it. The theorem is proved in the paper, and nothing of it is formalized on the platform. Mathlib has convex functions, continuous duals, biduals and weak-* topologies, but not extended-valued subdifferentials on Banach spaces, conjugate duality in the nonreflexive setting, or monotone operator theory. This mission produces formal statements of the paper's steps, the standard max formula for directional derivatives on a Banach space, and the Fenchel conjugate facts the argument uses, each as a separate target.

Difficulty

In a reflexive space the argument is short, because $\partial f^*$ is the inverse of $\partial f$ . In a nonreflexive space it is not: $\partial f^*$ maps $E^*$ into $E^{**}$ , and points of $E^{**} \setminus E$ appear. The naive route, transferring the inclusion $\partial f \subseteq \partial g$ to the conjugates by inverting the maps, breaks down there, and the 1966 argument failed at a related step, where the dual vectors in an approximation could be unbounded. Relating $\partial f^*$ to $\partial f$ without reflexivity is where the difficulty sits; the boundedness of the approximating nets in Proposition 1 is essential and cannot be dropped. The finite continuous case and the max formula (3.7) are needed on an arbitrary Banach space, including the dual $E^*$ , not only on $E$ .

Formalization scope

$E$ is a real Banach space (NormedAddCommGroup, NormedSpace ℝ, CompleteSpace); $E^*$ is StrongDual ℝ E with the operator norm, $E^{**}$ is StrongDual ℝ (StrongDual ℝ E), and $E \hookrightarrow E^{**}$ is NormedSpace.inclusionInDoubleDual. No reflexivity, inner product or finite dimension is assumed. Explicit readings:

Values in $(-\infty, +\infty]$ are EReal with the requirement $f(x) \ne -\infty$ ; convexity is the paper's inequality for $0 < \lambda < 1$ in EReal arithmetic. Lower semicontinuity is in the norm topology.
A multivalued map is E → Set (StrongDual ℝ E); $T = \partial f$ means $T(x) = \partial f(x)$ for every $x$ .
The cycle inequality quantifies over all $n \in \mathbb{N}$ and points indexed by Fin (n + 1) with wrap-around addition, so the last term is $\langle x_n - x_0, x_n^* \rangle$ . Maximality is graph inclusion among cyclically monotone operators, not among monotone operators.
The uniqueness constant is a real number, never $\pm\infty$ .
" $\supset$ " in (3.6) is non-strict inclusion, and the hypothesis is one-sided.
A net is a nonempty directed partially ordered index type with convergence along atTop; weak** convergence is pointwise convergence on $E^*$ ; "bounded" is a uniform norm bound.
"Finite and continuous" for $(f+j)^*$ means equal everywhere to a continuous real-valued function. The max in (3.7) is IsGreatest, so it is attained; the directional derivative is the limit along $\lambda \to 0^+$ .
The print's " $\partial(f + j) = \partial f(x) + \partial j(x)$ " in (3.1) is read as $\partial(f+j)(x)$ .

A formalization that drops lower semicontinuity, allows an extended-real constant, or replaces "maximal cyclically monotone" by "maximal monotone" states a different, and in the first two cases false or trivial, theorem; the statements here keep all three.

The proof reduces Theorem B to milestone 7 through Theorem 1 of Rockafellar (1966) and its Corollary 2, which are not stated in this paper and are not milestones; formal statements of them are welcome as supporting theorems. Contributions of reusable infrastructure are welcome: extended-valued subdifferentials and conjugates on normed spaces, the Fenchel–Moreau identity on $E$ , the sum rule with a continuous function, and the max formula for directional derivatives.

Selected references

R. T. Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (1970), 209–216. https://doi.org/10.2140/pjm.1970.33.209
R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific J. Math. 17 (1966), 497–510. https://doi.org/10.2140/pjm.1966.17.497
G. J. Minty, On the monotonicity of the gradient of a convex function, Pacific J. Math. 14 (1964), 243–247. https://doi.org/10.2140/pjm.1964.14.243
J.-J. Moreau, Fonctionnelles convexes, mimeographed lecture notes, Collège de France, 1967.
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

13 thms2 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis VII: The L-Optimality Criterion and the Proximity TheoremTextbook

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.

18 thms2 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

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

Motivation

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

Setting

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

Formalization targets

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

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

Milestones: Theorems 7.49, 7.53

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

8 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization+1·Captain: mikedeng1

Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders I: LP Rounding for Subadditive BiddersResearch Paper

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:

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$ ;
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}$ ;
picks the layer index $r$ maximizing $\sum_i v_i(S_i^r)$ and sets $T_i=S_i^r$ ;
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^*$ :

if $OPT^*>3\max_i v_i(M)$ , one rounding meets the two conditions of step 1 with probability $>1/6$ ;
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;

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

12 thms2 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis XXV: L-Convex Functions via Minimizer PolyhedraTextbook

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

34 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization+1·Captain: mikedeng1

Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders II: Clause-Based Randomized Rounding for XOS BiddersResearch Paper

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

$\sum_i v_i(O_i)\le\mathrm{OPT}^*$ for an optimal LP solution (step (i) of the proof of Theorem 3.1).
Pointwise, $\mathrm{ALG}\ge\sum_j Q_j$ with $Q_j=\max_i p^i_j$ .
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 .

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

9 thms2 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis XXVI: Polyhedral L-Convex FunctionsTextbook

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

50 thms3 active usersReviewed

Completed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

A Nonmonotone Line Search Technique and Its Application to Unconstrained Optimization II: R-Linear Convergence for Strongly Convex FunctionsResearch Paper

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:

Lemma 1.1: $f(x_k) \le C_k \le A_k$ when $g_k^{\mathsf T}d_k \le 0$ for each $k$ .
$C_{k+1} \le C_k$ , so all iterates lie in $\mathcal L$ .
(3.4): $f(x) - f(x^*) \le \gamma\|\nabla f(x)\|^2$ .
(2.15): $Q_{k+1} \le 1/(1 - \eta_{\max})$ .
(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\}.

(3.7): $\|g_{k+1}\| \le b\|g_k\|$ , $b = 1 + \mu c_2 L$ .
(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).

16 thms6 active usersReviewed

The OR Formalization Drive

Missions

Markov Decision Processes XVII: Random-Horizon Consumption-Investment and the De Finetti Dividend ProblemTextbook

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Markov Decision Processes XVIII: Terminal Wealth in Jump Markets and Trade ExecutionTextbook

Motivation

Setting

What is being asked

Approximation Algorithms for Combinatorial Problems III: The Worst-Case Ratio of the Weighted Algorithm B2Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3, with the equality range corrected

Milestones

Significance

Difficulty

Formalization scope

Selected references

Discrete Convex Analysis XXII: Convex Extensibility of M-Convex FunctionsTextbook

Motivation

Setting

Formalization targets

Goal: convex extensibility characterizes M-convexity

Supporting structural targets

Significance

Difficulty

Formalization scope

Selected references

Diffusion approximations for open queueing networks with service interruptions 1: explicit Lipschitz bounds for the oblique reflection mapResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Markov Decision Processes XIX: Theory of Optimal Stopping ProblemsTextbook

Motivation

Setting

What is being asked

Markov Decision Processes XX: Perpetual American Options and Credit GrantingTextbook

Motivation

Setting

What is being asked

Diffusion approximations for open queueing networks with service interruptions 2: jump-diffusion heavy-traffic limit for long up and down timesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1, case J=1J=1J=1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Discrete Convex Analysis XXIII: Directional Derivatives and Subdifferentials of M-Convex FunctionsTextbook

Motivation

Setting

Formalization targets

Goal: the directional-derivative/subdifferential correspondence

Supporting structural targets

Significance

Difficulty

Formalization scope

Selected references

Robust Control of Markov Decision Processes with Uncertain Transition Matrices 2: The Robust Bellman Recursion for Discounted Infinite-Horizon MDPsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (Robust Bellman Recursion)

Milestones

Significance

Difficulty

Goal: Theorem 4.1, case $J=1$