Operations Research

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

1. Existence and uniqueness of the reflection for $x\in D$ with $x(0)\ge0$ (Section 2, p. 337).
2. Eq. (2.4): given (2.1)–(2.2), the complementarity condition (2.3) is equivalent to $y = \pi_x(y)$.
3. $\gamma = \|Q^n\| < 1$ (p. 338).
4. 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)$.
5. 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$.
6. Remark (2.1): for $n=1$, $Q=0$ the bounds are attained.
7. 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

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.

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

Motivation

A correlated equilibrium (Aumann, 1974) is a joint distribution over the players' strategy profiles from which no player gains by deviating from a recommended strategy. A central question of learning in games is which equilibria repeated play of simple, myopic rules can reach. Foster and Vohra (1997) answered it for calibrated forecasting: if each player forecasts the opponent with a calibrated rule and best-responds to the forecast, the empirical distribution of play approaches the set of correlated equilibria (their Theorem 1). That result has become a basic reference point for no-regret and calibration-based learning in games (Hart and Mas-Colell, 2000).

This mission formalizes the paper's converse. Theorem 1 says calibrated learning ends up in the correlated equilibria; the converse says it can end up at any of them, for almost every game. Together the two results characterize exactly which long-run outcomes calibrated learning with best responses can produce.

Setting

Two players choose strategies from finite sets $S(1)$ with $m$ elements and $S(2)$ with $n$ elements; player $i$ receives payoff $u_i(x,y)\in\mathbb{R}$ and maximizes it. A game $G=(u_1,u_2)$ is a pair of real $m\times n$ matrices, that is, a point of $\mathbb{R}^{2mn}$; a set of games has measure zero if it is Lebesgue-null in $\mathbb{R}^{2mn}$.

A joint distribution $D$ on $S(1)\times S(2)$ is a correlated equilibrium if for every map $\Phi:S(1)\to S(1)$, $\sum_{x,y}D(x,y)u_1(\Phi(x),y)\le\sum_{x,y}D(x,y)u_1(x,y)$, and symmetrically for player 2. $\pi(G)$ is the set of correlated equilibria.

Play is repeated in rounds $t=0,1,2,\dots$. Before each round, player 1 issues a forecast $f_1(t)$, a probability vector over $S(2)$, produced by a deterministic forecasting rule from the history of play so far; player 2 likewise forecasts player 1. For a forecast sequence $f$ and the opponent's plays $z$, let $N(p,t)$ be the number of the first $t$ rounds with forecast $p$, and $\rho(p,j,t)$ the fraction of those rounds in which the opponent played $j$ (zero if $N(p,t)=0$). The forecasts are calibrated if for every $j$

$$\sum_p |\rho(p,j,t)-p_j|\,\frac{N(p,t)}{t}\ \longrightarrow\ 0 \qquad (t\to\infty).$$

Each player then plays $R_i$ of its forecast, where the best-reply function $R_i$ picks a best response to every forecast and does not depend on the round. $D_t(x,y)$ is the fraction of the first $t$ rounds in which $(x,y)$ was played.

$\lambda(G)$, the set of limit points of calibrated forecasts, consists of the $D$ for which some best-reply functions $R_1,R_2$ and some calibrated forecasting rules make $D_t(x,y)\to D(x,y)$ for all $(x,y)$.

Formalization targets

Goal: Theorem 2 (p. 47)

$$\text{for Lebesgue-almost every } G\in\mathbb{R}^{2mn}:\qquad \lambda(G)=\pi(G).$$

Milestones

1. $\lambda(G)\subseteq\pi(G)$ for every game (Theorem 1 restated, p. 46).
2. Every joint distribution $D$ is the limiting empirical distribution of a deterministic play sequence supported on $\{D>0\}$ (p. 47).
3. Along such a sequence the conditional forecasts $p_{1,t}=D(x_t,\cdot)/\sum_yD(x_t,y)$ and $p_{2,t}=D(\cdot,y_t)/\sum_xD(x,y_t)$ are calibrated (p. 47).
4. In a correlated equilibrium each recommended strategy is a best response to its conditional forecast (p. 47).
5. For almost every payoff matrix, each set $M_b(x)$ of forecasts to which $x$ is a best response is either empty or contains a forecast in the open simplex at which $x$ is the unique best response (p. 47).
6. The perturbed forecasts $p_i=(1-1/i)p^*+(1/i)q$ converge to $p^*$ and keep a unique best reply (p. 48).
7. For the $3\times3$ game of p. 48, a correlated equilibrium lies outside $\lambda(G)$, and $\lambda(G)$ is the single point mass on $(C,2)$.

Significance

Theorem 1 by itself leaves open whether calibration selects among correlated equilibria, for instance toward Nash equilibria or toward particular payoffs. Theorem 2 closes that question negatively for generic games: every correlated equilibrium is the genuine limit, not merely an accumulation point, of calibrated play with stationary best replies. As the paper notes, adding the assumption that the limit exists therefore does not refine the equilibrium reached, in contrast with Fudenberg and Kreps's result for asymptotically myopic Bayesian play. The $3\times3$ example shows that the genericity hypothesis cannot be dropped.

The results are proved in the 1997 paper; none is formalized. A complete development produces a reusable layer for repeated two-player games (calibration, empirical distributions, best-reply maps, correlated equilibria), a genericity lemma for best-response regions that is useful beyond this paper, and a machine-checked version of an argument that the paper gives only in outline.

Difficulty

The natural construction takes a correlated equilibrium $D$, a play sequence realizing $D$, and forecasts equal to the conditional distributions of $D$. The forecasts are then calibrated and each played strategy is a best response. What fails is the best-reply function: two strategies $x'\ne x''$ can have the same conditional forecast $p^*$, while a stationary $R_1$ maps $p^*$ to only one strategy. Separating them needs forecasts near $p^*$ at which each is the unique best response, and that exists only when the best-response regions have nonempty relative interior, a property that fails on a null set of games (the $3\times3$ example) and whose genericity must be proved. The perturbed forecasts are no longer exactly equal to the conditional frequencies, so calibration has to be re-established with errors that vanish along the sequence.

Formalization scope

• Strategies are Fin m and Fin n; payoffs are real matrices; players maximize. A game is a point of (Fin m → Fin n → ℝ) × (Fin m → Fin n → ℝ) with Mathlib's volume (Lebesgue measure on $\mathbb{R}^{2mn}$), and "almost every" is ∀ᵐ.
• A correlated equilibrium is the joint-distribution form of p. 44 (a joint distribution with the two deviation inequalities).
• Forecasting rules map finite histories to probability vectors; the play is generated recursively from the rules and the best-reply functions. Best-reply functions are arbitrary stationary selections of a best response at every probability vector; they may not depend on the round, since round-dependent tie-breaking enlarges $\lambda(G)$ (the matching pennies example of p. 46).
• Rounds are $0,\dots,t-1$; $D_0=0$. The calibration sum runs over the forecasts issued so far, which is the paper's sum over all $p$ since the other terms vanish.
• $\lambda(G)$ requires convergence of $D_t$, not a subsequence. Replacing the limit by a limit point, or stating only $\pi(G)\subseteq\lambda(G)$, does not formalize the theorem.
• The page's sentence "Almost every game has the property that all the sets $M_b(x)$ have non-empty interior" is false for dominated strategies ($M_b(x)=\emptyset$ on an open set of games). Milestone 5 states the dichotomy the page's argument proves: empty or with relative interior.
• The page prints the denominator of $p_{2,t}$ as $\sum_{x}D(x_t,y)$; the mission uses $\sum_xD(x,y_t)$.

The theorems are stated from the mission's own definitions of the game, calibration and $\lambda(G)$; no statement is vacuous: at $m=0$ or $n=0$ both sides of the goal are empty, and the $3\times3$ example exercises every definition. Contributions welcome: proofs of the milestones in any order, the genericity lemma (Lebesgue-null sets of linear degeneracies), and the calibration estimates for the perturbed forecasts.

Selected references

• D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77 (1982), 605–610. https://doi.org/10.1080/01621459.1982.10477856
• D. Fudenberg and D. M. Kreps, Learning mixed equilibria, Games and Economic Behavior 5 (1993), 320–367. https://doi.org/10.1006/game.1993.1021
• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153

Motivation

Convexity is normally defined additively — a function's value at a mixture is bounded by the mixture of its values — but many of the properties that make convexity useful in optimization (a local minimum is global, level sets are well-behaved) survive under a much weaker, purely ordinal notion: quasi-convexity, which compares function values rather than adding them. A nondecreasing rescaling of a convex function is generally not convex, but it is always quasi-convex — so a theory built only on ordinal comparisons automatically covers every such rescaling for free, at the cost of a more delicate proof architecture (since the algebraic cancellations available to additive convexity are no longer available).

Chapter 6's second half asks exactly how far this idea extends in the discrete setting: does the M-convexity exchange axiom have an ordinal, quasi-convex relaxation that still supports the same strong minimization theory — an optimality criterion, a minimizer-cut lemma, and, most significantly, a proximity theorem with the same explicit distance bound? This mission formalizes the chapter's answer: yes, and the relevant relaxed class, functions satisfying condition (SSQM$_{\ne}$), is large enough to include every strictly increasing rescaling of an M-convex function, a class the M-convex theory of chunk 06 alone says nothing about.

Setting

Let $V$ be a finite ground set and $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain. Building on chunk 06's M-convex exchange axiom (M-EXC[Z]), this chapter introduces several ordinal relaxations. $f$ is weakly quasi M-convex, satisfying (QMw), if for every pair of distinct points $x, y \in \operatorname{dom} f$ there exist $u$ in the positive support and $v$ in the negative support of $x - y$ with $f(x - \chi_u + \chi_v) \le f(x)$ or $f(y + \chi_u - \chi_v) \le f(y)$ — an "or" where (M-EXC[Z]) demands an additive inequality. Two further conditions restrict attention to points of different function value and sharpen the conclusion to a three-way trichotomy (strictly better on one side, or exactly tied on both): (SSQM$_{\ne}$) quantifies universally over $u$ (as in (M-EXC[Z])), while (SSQM$_{\ne,w}$) quantifies existentially over both $u$ and $v$ (as in (QMw)). The linear perturbation of $f$ by $p : V \to \mathbb R$ is $f[p](x) = f(x) - \langle p, x \rangle$.

Formalization targets

Goal: Theorem 6.78 (the quasi M-proximity theorem)

Let $f$ satisfy (SSQM$_{\ne}$), $n = |V|$, $\alpha$ a positive integer. If $x_\alpha \in \operatorname{dom} f$ satisfies $f(x_\alpha) \le f(x_\alpha + \alpha(\chi_v - \chi_u))$ for all $u, v \in V$, then $\arg\min f \ne \emptyset$ and there is $x^* \in \arg\min f$ with $\|x_\alpha - x^*\|_\infty \le (n-1)(\alpha - 1)$ — verbatim the same conclusion, and the same exact bound, as chunk 06's Theorem 6.37(1), now established for the strictly larger class satisfying (SSQM$_{\ne}$) rather than the M-convex exchange axiom itself.

Milestones: Theorems 6.68(2), 6.76, 6.77

Theorem 6.68(2): $f$ satisfies (M-EXC[Z]) if and only if every linear perturbation $f[p]$ satisfies (QMw) — quantifying exactly how much weaker (QMw) is pointwise, and how the gap closes once quantified over every perturbation. Theorem 6.76 (the quasi M-optimality criterion): the direct analogue of chunk 06's Theorem 6.26 for the quasi-convexity classes — a purely pairwise local check still characterizes global (or, in the (QMw) case, strict unique) optimality. Theorem 6.77 (the quasi M-minimizer cut): chunk 06's Theorem 6.28 continues to hold verbatim when its M-convexity hypothesis is replaced by (SSQM$_{\ne}$) — the structural fact the proximity theorem's proof is built from survives the relaxation intact.

Significance

The result itself. The proximity theorem is the result algorithms actually use: a scaling algorithm for minimizing quasi-convex functions of this kind inherits exactly the same correctness guarantee, with exactly the same distance bound, as the M-convex case — this is a genuine broadening of chapter 10's algorithmic reach, not a restatement dressed in weaker hypotheses. Every strictly increasing scalar transformation of an M-convex objective (a common modeling device — re-expressing a cost in utility units, or applying a monotone risk measure) now falls under a proximity theorem, whereas prior to this chapter's relaxation such a transformation would generally destroy M-convexity itself and leave optimization theory silent on the transformed problem.

Formalizing it. No matching item exists on the platform for quasi M-convexity in any of its forms. Formalizing Theorem 6.78 requires first pinning down (SSQM$_{\ne}$) exactly (there are six closely related axiom variants in this section of the book, only three of which — (QMw), (SSQM$_{\ne}$), (SSQM$_{\ne,w}$) — are needed for this mission's chosen results), and this mission also captures, via Theorem 6.68(2), the precise sense in which these relaxed conditions are strictly weaker than plain M-convexity while remaining tightly connected to it.

Difficulty

The natural first instinct, given how close the quasi-convexity axioms look to (M-EXC[Z]), is to try to prove Theorem 6.78 by directly imitating chunk 06's proof of Theorem 6.37 line by line. This mostly works — the proof structure (fix a target coordinate, build a chain of strictly decreasing values via repeated exchange steps, bound the chain's length using the scaled hypothesis) survives verbatim — but every step that chunk 06's proof took by adding two instances of the exchange inequality together must be replaced by an ordinal argument, since (SSQM$_{\ne}$) only ever asserts a disjunction of value comparisons, never an additive inequality relating four function values simultaneously the way (M-EXC[Z])'s $f(x)+f(y) \ge f(x-\chi_u+\chi_v)+f(y+\chi_u-\chi_v)$ does. The book's proof handles this by working with strict inequalities and the trichotomy structure of (SSQM$_{\ne}$) directly rather than algebraic cancellation — the same overall architecture, but every arithmetic step rebuilt as a case analysis on which disjunct of (SSQM$_{\ne}$) fires.

Formalization scope

This mission builds directly on chunk 06's published items (CharVec, SuppPos, SuppNeg, DomZ, MExchangeAxiom, ArgMin), per the platform's textbook convention that a later chapter of the same book imports an earlier one's definitions rather than redrafting them; its own namespace DiscreteConvex.MConvexFunctions.Quasi nests under chunk 06's DiscreteConvex.MConvexFunctions accordingly. Δf(z;v,u) (Eq. (6.2)) is never reified as a separate object; every occurrence is unfolded directly into an f-value comparison, avoiding WithTop ℝ subtraction throughout, consistent with chunk 06's own convention.

A trivializing formalization of the goal would silently strengthen (SSQM$_{\ne}$) back to plain M-convexity (making this mission redundant with chunk 06's Theorem 6.37) or loosen the exact bound $(n-1)(\alpha-1)$ to an unspecified function of $n, \alpha$; neither is done. Six axiom variants appear in this section of the book ((QM), (SSQM), (QMw), (SSQM$_w$), (SSQM$_{\ne}$), (SSQM$_{\ne,w}$)); only the three actually needed by this mission's four items are drafted, and Theorem 6.68's first part (an implication chain among the other three) is left out — see MODERATION_NOTES.md. Contributions building the polyhedral M-convex-function bridge (§6.11–6.12, Theorems 6.59–6.64), the level-set characterizations (Theorems 6.72, 6.74), or the scaled quasi M-minimizer cut (Theorem 6.79, the direct generalization of Theorem 6.77 drafted here) are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• M. Avriel, W. E. Diewert, S. Schaible, I. Zang, Generalized Concavity, Plenum Press, 1988.

Motivation

Chapter 7's abstract machinery — contracting Markov Decision Models, the Structure Theorem, value iteration with an explicit convergence rate — earns its keep by solving concrete problems. Section 7.6 works through four kinds of application: a return to the classical cash-balance inventory problem, now over an infinite horizon; the "red-and-black" gambling problem, where a player tries to reach a target fortune before going bankrupt; and, most substantially, the infinite-horizon two-armed bandit, where the general theory reveals something genuinely surprising — the qualitatively optimal policy can be computed one arm at a time.

Setting

Every application here specializes the general infinite-horizon, contracting-model machinery of chunks 07a/07b to a concrete transition structure. The cash-balance model orders inventory up to a level $a$ at linear cost, incurs a holding/shortage cost, then absorbs a random demand. The red-and-black model bets a fraction of a bounded fortune on a biased coin, absorbing at bankruptcy or at the target. The bandit model reconsiders the Beta-Bernoulli two-armed bandit of chunk 05b, now over an infinite horizon with a genuine discount $\beta<1$: the key new tool is the K-stopping problem, a fictitious single-arm decision problem where, at every stage, the decision maker may either pull the arm or retire with a fixed payment $K$. The Gittins index $I(m,n)$ is the smallest such payment at which retiring immediately is already as good as continuing.

Formalization targets

The goal, Theorem 7.6.10, is the Gittins index theorem for this book's two-armed bandit: always pulling the arm with the higher index is optimal for the full infinite-horizon problem. The milestones build the machinery it needs — the index's definition (Definition 7.6.5) and its equivalent representation as a supremum over stopping times (Theorem 7.6.6), the K-stopping value function's monotonicity/convexity/differentiability properties (Proposition 7.6.7), the index's optimal-stopping-set and indifference characterizations (Corollary 7.6.8), the two-arm joint stopping value's parallel structure (Proposition 7.6.9), and a fixed-point recasting useful for computation (Proposition 7.6.11) — plus, independently, the cash-balance and casino-game applications (Theorems 7.6.1-7.6.4), which use the general theory but not the bandit-specific machinery.

Significance

The Gittins index theorem's real content, emphasized by the book's own remark, is not merely that an optimal policy exists but how little computation it needs: instead of solving one optimization problem over the bandit's full four-dimensional joint state space $\mathbb N_0^2 \times \mathbb N_0^2$, the decision maker solves two independent two-dimensional single-arm problems and compares two numbers. This mission's formalization of the goal is built specifically to keep that separation visible — each arm's index is computed from a single, shared KStoppingValue structure applied to that arm's own state alone, never from a function that happens to take the whole joint state as an argument. The proof route here (via the K-stopping problem's explicit fixed-point characterization, Definition 7.6.5 and Proposition 7.6.11) is a genuinely different construction from the platform's existing Gittins-index theorems (BanditAlgorithm.gittins_index_theorem and related), which are built via Whittle's retirement/charge-accounting argument — checked directly and found to define the index differently enough that this mission drafts its own theorems rather than treat that construction as prior art.

Difficulty

The K-stopping value function $J(m,n;K)$ and the two-arm joint value $\tilde J(x;K)$ are both genuine fixed points of an infinite-horizon Bellman equation with no finite backward recursion to fall back on (the "stopping" option, rather than a terminal condition, is what makes the horizon infinite); this mission bundles them as data satisfying their own defining fixed-point equations, the same convention this series uses throughout for such objects. A second difficulty is Theorem 7.6.6's supremum over stopping times: without a canonical path measure for the underlying Markov chain (not built anywhere in this series), the two expectations the theorem compares are represented as data satisfying the positivity a genuine expectation must have, over an explicit, elementary notion of stopping time (a function of the whole observed path, adapted in the sense that whether it has fired by time $n$ depends only on the path up to $n$) — a faithful, if representational, rendering of the theorem's genuinely path-dependent content.

Formalization scope

The cash-balance model (Theorem 7.6.1) explicitly cites chunk 02d's finite-horizon critical-level sequences as a hypothesis rather than re-deriving them, since this mission's own content is the infinite-horizon extension, not a second proof of the finite-horizon theory those sequences come from. The casino-game theorems (7.6.2-7.6.4) state optimality for the specific, named timid and bold strategies, not for an unnamed "some optimal policy" — the theorems' entire content is that these particular policies, not merely some optimal one, are best in their regime. The bandit model's posterior mean and Bayes-update operator are kept identical in substance to chunk 05b's finite-horizon Beta-Bernoulli model (restated, since chunks cannot import each other's Lean), so a reader can see this section is solving the same underlying statistical model, now over an infinite horizon.

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.
• J. C. Gittins, "Bandit processes and dynamic allocation indices," Journal of the Royal Statistical Society, Series B, 1979 (the original index construction this section's K-stopping-problem approach reformulates).
• P. Whittle, "Multi-armed bandits and the Gittins index," Journal of the Royal Statistical Society, Series B, 1980 (the retirement-option construction the platform's existing Gittins theorems use, a different proof route from this chunk's own).
• L. E. Dubins and L. J. Savage, How to Gamble If You Must: Inequalities for Stochastic Processes, McGraw-Hill, 1965 (the classical red-and-black problem, Theorems 7.6.2-7.6.4).

Motivation

A competitive equilibrium is a list of production plans, consumption plans and prices at which every firm maximizes profit, every consumer maximizes utility within the budget, and no market has excess demand. Whether such prices exist at all is the consistency question behind general equilibrium theory, the welfare theorems, and applied equilibrium models used in policy analysis. Arrow and Debreu gave the first proof of existence for a model with production, private ownership and general convex preferences (Econometrica 22, 1954), using Debreu's existence theorem for abstract economies (PNAS 38, 1952).

Their Theorem I assumes that every consumer initially holds a positive amount of every commodity (Assumption IV.a). The authors call this "clearly unrealistic" (p. 280): a household does not hold every good, and most households own little beyond their labor. Theorem II, the subject of this mission, removes that assumption. It only asks that every consumer be able to supply some type of labor that is always productive of a commodity everyone desires. This is the version of the existence theorem that allows a wage-earner economy.

Timeline. Wald (1935–36) proved existence for special production models. Nash (1950) proved existence of equilibrium points for finite games, and Debreu (1952) extended it to abstract economies, in which each player's feasible set depends on the others' choices. Arrow and Debreu (1954) proved Theorems I and II. McKenzie's independent existence proof was published the same year (Econometrica 22, 1954).

Setting

There are $l$ commodities, $n$ producers and $m$ consumers; vectors live in $\mathbb R^l$ and $x\leqq y$ is componentwise. Producer $j$ has a production set $Y_j$. Consumer $i$ has a consumption set $X_i$, a utility $u_i$ on $X_i$, an endowment $\zeta_i$ and profit shares $\alpha_{ij}$. Write $Y=\sum_jY_j$, $X=\sum_iX_i$, $\zeta=\sum_i\zeta_i$, and let $P=\{p\geqq0,\ \sum_hp_h=1\}$ be the price simplex. A competitive equilibrium $(x_1^*,\dots,x_m^*,y_1^*,\dots,y_n^*,p^*)$ satisfies four conditions. Each $y_j^*$ maximizes $p^*\cdot y_j$ on $Y_j$. Each $x_i^*$ maximizes $u_i$ on $\{x_i\in X_i: p^*\cdot x_i\le p^*\cdot\zeta_i+\sum_j\alpha_{ij}p^*\cdot y_j^*\}$. The price vector satisfies $p^*\in P$. Finally $z^*=\sum x_i^*-\sum y_j^*-\zeta\leqq0$ and $p^*\cdot z^*=0$.

The assumptions of Theorem II are as follows. I: production sets are closed, convex and contain $0$; $Y\cap\Omega=\{0\}$ (no output without input); $Y\cap(-Y)=\{0\}$ (no reversible production). II: each $X_i$ is closed, convex and bounded below. III: $u_i$ is continuous, has no satiation point, and satisfies $u_i(tx+(1-t)x')>u_i(x')$ whenever $u_i(x)>u_i(x')$ and $0<t<1$. IV.b: shares are nonnegative and sum to one for each firm. Two sets of commodities are defined from the data. The set $\mathcal D$ contains the commodities always desired by every consumer: from any $x_i\in X_i$, adding some positive amount of the commodity stays in $X_i$ and raises $u_i$. The set $\mathcal P$ contains the types of productive labor: for every $y\in Y$, (a) $y_h\le0$, and (b) some $y'\in Y$ satisfies $y'_{h'}\ge y_{h'}$ for all $h'\ne h$ and $y'_{h''}>y_{h''}$ for some $h''\in\mathcal D$. The remaining assumptions are:

• IV′.a: each consumer has some $x_i\in X_i$ with $x_i\leqq\zeta_i$ and $x_{hi}<\zeta_{hi}$ for some $h\in\mathcal P$;
• V: some $x\in X$ and $y\in Y$ satisfy $x_h<y_h+\zeta_h$ for every $h$;
• VI: $\mathcal D\ne\emptyset$;
• VII: $\mathcal P\ne\emptyset$.

Formalization targets

Goal: Theorem II (§4.5, p. 281)

$$\text{Assumptions I–III, IV}',\ \text{V–VII}\ \Longrightarrow\ \exists\,(x^*,y^*,p^*)\ \text{satisfying Conditions 1–4.}$$

Milestones (§5, pp. 282–287)

They follow the paper's proof. Let $\pi=|\mathcal P|$ and $P^\varepsilon=\{p\in P: p_h\ge\varepsilon\ \forall h\in\mathcal P\}$ for $0<\varepsilon\le1/(2\pi)$. Let $E^\varepsilon$ be the abstract economy in which consumers maximize utility under budget constraints, producers maximize profit, and a market participant chooses $p\in P^\varepsilon$ to maximize $p\cdot z$. The milestones are:

1. §5.0 (1). On $P^\varepsilon$ every consumer can spend strictly less than $p\cdot\zeta_i$.
2. §5.1.1 (5). Equilibrium points of $E^\varepsilon$ satisfy $x^*-y^*\leqq\zeta'$ for a vector $\zeta'$ independent of $\varepsilon$.
3. §5.2.0. The attainable sets relative to $\zeta'$ are bounded.
4. §5.2.1. The truncated economy $\tilde E^\varepsilon$ has an equilibrium point.
5. §5.2.2 (3)–(5). An equilibrium point of $\tilde E^\varepsilon$ is one of $E^\varepsilon$.
6. §5.3.0 (2). If $p^*_h>\varepsilon$ for all $h\in\mathcal P$, the point is a competitive equilibrium.
7. §5.3.2 (1). Limits of equilibrium points as $\varepsilon\to0$ are quasi-equilibria for consumers.
8. §5.3.4 (3). If the floors bind, some desired commodity has limit price $0$.
9. §5.3.4 (6). If the floors bind, limit consumption minimizes expenditure over $X_i$.
10. §5.3.5. For some $\varepsilon$ the floor does not bind.

Significance

Theorem II is the existence theorem for a competitive economy in which consumers may own nothing but their labor. It shows that the survival assumption IV.a can be traded for conditions on labor, desirability and the possibility of an overall excess supply. Section 5.3.3 of the paper also isolates the quasi-equilibrium, in which utility maximization under the budget is replaced by cost minimization at a given utility level. That notion is used in later existence and welfare arguments.

The theorem has been proved since 1954; this mission does not reopen it. The work here is the machine-checked proof. The companion mission on Theorem I formalizes the shared model and Debreu's lemma. As of September 2026 neither theorem has a Lean formalization on the platform, and Mathlib contains no general equilibrium theory.

Difficulty

The obvious approach reuses the proof of Theorem I: build the abstract economy of consumers, producers and a price-choosing participant, and apply Debreu's lemma. That fails at the boundary of the price simplex. Without IV.a, a consumer's cheapest point in $X_i$ can cost as much as the endowment at some prices, so the budget correspondence is not continuous there and the lemma does not apply. The paper therefore keeps prices of productive labor at least $\varepsilon$ and must then show that the floor does not bind for some $\varepsilon$. That is a limit argument as $\varepsilon\to0$ which uses Assumptions V, VI and VII together, and each of the milestones 7–9 is a step of it. Debreu's lemma itself needs a Kakutani-type fixed point theorem for correspondences, which Mathlib does not provide.

Formalization scope

Commodity vectors are Fin l → ℝ. Consumers are indexed by Fin m and producers by Fin n. The inner product is ⬝ᵥ. The paper's $x<y$ is strict in every component and is written componentwise, never as Lean's < on functions. $\mathcal D$ and $\mathcal P$ are computed from the economy, not supplied as parameters. Utilities are total functions, but every assumption on $u_i$ quantifies over $X_i$ only. "Maximizes" is membership plus an inequality against every feasible alternative; no supremum is used. $E$, $E^\varepsilon$ and $\tilde E^\varepsilon$ are built by one constructor over the players Fin m ⊕ Fin n ⊕ Unit. The vector $\zeta'$ takes the lower bounds $\xi_i$ of Assumption II as an explicit argument. The milestones of §5.3 are stated for the limit of a sequence of equilibrium points, which is how the paper constructs them. Assumption V is dropped from every milestone except §5.3.5 and the goal. With V, the case assumption of §5.3.1 is contradictory and those milestones would hold vacuously.

A trivializing formalization is ruled out as follows. The assumptions are satisfiable with IV.a failing: a sorry-free check covers two goods, one consumer who owns nothing and can only supply labor, and one firm turning labor into the desired good. The goal therefore does not hold vacuously.

Needed infrastructure includes a Kakutani fixed point theorem or Debreu's lemma, compactness of truncated action sets, and sequential compactness arguments in $\mathbb R^l$. AGT.brouwer_fixed_point is on the platform and can serve as a starting point. The lemma is reusable well beyond this mission. Contributions to any milestone, to the lemma, or to the boundedness results shared with Theorem I are welcome.

Selected references

• K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3), 265–290, 1954. https://doi.org/10.2307/1907353
• G. Debreu, A Social Equilibrium Existence Theorem, Proceedings of the National Academy of Sciences 38(10), 886–893, 1952. https://doi.org/10.1073/pnas.38.10.886
• L. W. McKenzie, On Equilibrium in Graham's Model of World Trade and Other Competitive Systems, Econometrica 22(2), 147–161, 1954. https://doi.org/10.2307/1907352
• J. F. Nash, Equilibrium Points in n-Person Games, Proceedings of the National Academy of Sciences 36(1), 48–49, 1950. https://doi.org/10.1073/pnas.36.1.48

Motivation

Duality is the organizing principle of convex optimization: a minimization problem's optimal value equals a maximization problem's optimal value, and this coincidence, rather than being a lucky accident, follows from a separating-hyperplane argument that applies whenever the two problems' feasible regions are shaped compatibly enough. Werner Fenchel formalized this in the 1950s for pairs of convex and concave functions related by the Legendre-Fenchel transform, and the resulting Fenchel duality theorem specializes, for linear objectives over polyhedral feasible regions, to linear programming duality — the fact, central to the entire theory of combinatorial optimization, that a linear program's optimal value can always be certified from above and below by a pair of primal and dual feasible solutions. Murota's Discrete Convex Analysis (SIAM, 2003) collects this classical machinery, together with the integrality theory that lets it produce combinatorial (integer-valued) certificates rather than merely real ones, as the technical foundation the rest of the book builds its discrete theory on top of.

Setting

For $f : \mathbb R^n \to \mathbb R \cup \{+\infty\}$, the epigraph is $\operatorname{epi} f = \{(x,Y) : Y \ge f(x)\}$, and $f$ is convex iff $\operatorname{epi} f$ is a convex set; $f$ is proper if additionally its effective domain $\operatorname{dom} f = \{x : f(x) < +\infty\}$ is nonempty, and closed if $\operatorname{epi} f$ is topologically closed. A function $h : \mathbb R^n \to \mathbb R \cup \{-\infty\}$ is concave, proper, closed analogously via its hypograph. The convex conjugate is $f^\bullet(p) = \sup_x\{\langle p,x\rangle - f(x)\}$, and the concave conjugate $h^\circ(p) = \inf_x\{\langle p,x\rangle - h(x)\}$. The relative interior $\operatorname{ri} S$ of a set $S$ is the interior of $S$ relative to its affine hull. A function is polyhedral if its epigraph (or hypograph) is a finite intersection of half-spaces. Given an $m \times n$ matrix $A$, $b \in \mathbb R^m$, $c \in \mathbb R^n$, the primal and dual linear programs are $\min\{c^\top x : Ax=b,\ x\ge0\}$ and $\max\{b^\top y : A^\top y \le c\}$, with feasible regions $P$, $D$. A matrix is totally unimodular if every square submatrix has determinant $0$, $1$, or $-1$. A discrete set $S \subseteq \mathbb Z^n$ is hole free if $S = \bar S \cap \mathbb Z^n$, where $\bar S$ is the convex hull of $S$'s real embedding; the discrete Minkowski sum is $S_1+S_2 = \{x_1+x_2 : x_1\in S_1, x_2\in S_2\}$.

Formalization targets

Goal (Theorem 3.6, Fenchel duality). For proper convex $f$ and proper concave $h$ satisfying at least one of four alternative conditions — a relative-interior condition on $\operatorname{dom} f \cap \operatorname{dom} h$, a polyhedrality condition on the same, or the analogous pair of conditions on $\operatorname{dom} f^\bullet \cap \operatorname{dom} h^\circ$ together with closedness of $f$, $h$ —

$$\inf_x\{f(x)-h(x)\} = \sup_p\{h^\circ(p)-f^\bullet(p)\},$$

with the extremum on the appropriate side attained whenever the common value is finite. This is the mission's capstone: the four alternative hypotheses make it the most broadly applicable statement of the four convex-duality results in this mission, each of the other three being either a special case in substance (Theorem 3.5, separation, which 3.6 is proved from) or a literal specialization to linear data (Theorem 3.10, LP duality).

Supporting milestones. Theorem 3.2 (biconjugation: $f^\bullet$ is always closed proper convex, and $g^{\bullet\bullet}=g$ for closed proper convex $g$); Theorem 3.5 (the separation theorem for convex/concave functions, under two of Theorem 3.6's four hypotheses); Theorem 3.9 (the Farkas lemma, equality form); Theorem 3.10 (LP duality: weak duality, strong duality with attainment, and complementary slackness); Theorem 3.13 (total unimodularity of the constraint matrix guarantees an integral optimal solution whenever an optimal solution exists); Proposition 3.14 (an explicit potential function certifying a minimum-weight bipartite perfect matching, via the totally unimodular incidence-matrix LP); and Proposition 3.16 (for a translation-invariant family of hole-free discrete sets, the property that discrete disjointness implies closure disjointness is equivalent to the discrete Minkowski sum matching the integer points of the closures' Minkowski sum).

Significance

Fenchel duality is the single result from which the separation theorem, LP duality, and (via the totally-unimodular incidence matrix of a bipartite graph) the combinatorial duality underlying weighted bipartite matching all descend, in one unbroken chain of specialization; formalizing this chain in one mission exhibits that structure directly, rather than treating each result as an independent fact. Proposition 3.16 plays a different role: it is the chapter's warning that naive discrete analogues of convexity (hole-freeness) do not automatically inherit convexity's good closure properties under Minkowski sums, which is exactly the gap the book's later M-convexity and L-convexity machinery is built to close — this mission's Proposition 3.16 is therefore the motivating negative result for the rest of the book's positive theory, not a loose end. So far as a platform search shows, no existing formalization matches this chunk's specific combination of extended-valued (possibly $\pm\infty$) functions, the four-alternative Fenchel duality hypothesis, or the bipartite-matching-via-total-unimodularity argument; the one related platform result (VectorSpaceOpt.fenchel_duality, from Luenberger) is for real-valued functions on general normed spaces under a single relative-interior-and-solidness hypothesis, a different generality from the extended-valued, four-hypothesis statement here.

Difficulty

The naive approach to Theorem 3.6 tries to prove the duality gap is zero directly from the definitions of the two conjugates, which only gives the easy inequality $\inf \ge \sup$ (a one-line computation, shown in the book's own proof in three lines); the substantive content is the reverse inequality, and it genuinely fails without a constraint-qualification hypothesis like (a1)-(b2) — Example 3.8 in the book exhibits a convex/concave pair with $\inf = 0 \ne -1 = \sup$ when none of the four conditions hold. The book's actual route reduces Theorem 3.6 to the separation theorem (Theorem 3.5) applied to $f$ shifted down by the (assumed finite) infimum, which produces the separating affine function directly; this is why Theorem 3.5, although logically a special case in spirit, earns its own milestone rather than being subsumed silently.

Formalization scope

All convex and concave functions are represented uniformly as (V → ℝ) → EReal-valued (Fintype V), rather than mixing WithTop ℝ for convex and WithBot ℝ for concave functions, so that Theorem 3.2's biconjugate — whose properness is a conclusion, not an assumption — has a well-defined codomain without extra casts. Convexity is defined via the epigraph being a convex subset of the ordinary real vector space $(V\to\mathbb R)\times\mathbb R$ (Mathlib's Convex ℝ), following the book's own equivalent characterization, rather than unfolding the direct inequality definition, which would require a extended-arithmetic scalar-multiplication convention (0\cdot(+\infty)=0) that Mathlib does not provide for EReal. The relative interior is defined directly from the book's own metric-ball-intersected-with-affine-hull description, since Mathlib has no relative-interior primitive at the pinned revision. Polyhedra are finite intersections of explicit half-spaces. A bipartite perfect matching is represented as a bijection between the two vertex sides restricted to the edge set — a faithful, not narrower, representation since every perfect matching between equal-size parts arises this way. The formalization does not trivialize: Theorem 3.6's four hypotheses are carried in full (not reduced to the easiest single case), and no result is stated only for finite-valued (never $\pm\infty$) functions, which would discard the entire point of the extended-value convex-analysis framework this chapter sets up for the rest of the book. Infrastructure needed beyond Mathlib's Convex, Matrix, and EReal API: all epigraph/hypograph, conjugate, relative-interior, and polyhedral apparatus is defined fresh in DiscreteConvex.IntegralConvexityB; a contribution proving any of the seven milestones independently, or supplying Mathlib-quality relative-interior lemmas, would be a natural entry point.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 3.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

Motivation

Real investors do not merely accumulate wealth for a single terminal payoff; they consume along the way, and the market they invest in is rarely a single fixed statistical regime for years at a time — bull and bear markets, business cycles, and volatility regimes shift the distribution of returns. Bäuerle and Rieder's §4.3 extends the terminal-wealth theory of chunk 04a by adding a consumption choice at every stage (the Ramsey/Merton consumption-investment problem), and §4.4 extends it again by letting the return distribution itself depend on a hidden, Markov-modulated environment state. Both extensions are shown to be genuine instances of the same abstract finite-horizon Markov Decision Process machinery from Chapter 2 — the joint consumption-investment choice and the extra regime coordinate change the state and action spaces, but not the proof strategy, which is exactly the point.

Setting

The consumption-investment problem: state $E := \mathrm{dom}\,U_p$ (wealth), action $\mathbb{R}_{\ge0}\times\mathbb{R}^d$ (consumption $c$, amounts $a$ invested), transition $T_n(x,c,a,z) = (1+i_{n+1})(x-c+a\cdot z)$, reward $r_n(x,c,a) := U_c(c)$, terminal reward $g_N := U_p$. Value functions $V_n(x) := \sup_\pi \mathbb{E}^\pi_{n,x}[\sum_{k=n}^{N-1} U_c(c_k(X_k)) + U_p(X_N)]$. The one-period sub-problem: $D(x) := \{(c,a) : 0\le c\le x,\ (1+i)(x-c+a\cdot R)\in\mathrm{dom}\,U_p \text{ a.s.}\}$, $u(x,c,a) := U_c(c) + \mathbb{E}[U_p((1+i)(x-c+a\cdot R))]$, $v(x) := \sup_{(c,a)\in D(x)} u(x,c,a)$.

The regime-switching extension (§4.4): an environment process $(Y_n)$, a finite-state Markov chain with transition probabilities $p_{jk}$, modulates the risky-asset return law: given $Y_n=j$, the next relative risk $R_{n+1}$ has law $Q_j$, and $(R_{n+1},Y_{n+1})$ has joint law $Q_j(dz)p_{jk}$ given $Y_n=j$, $Y_{n+1}=k$. The augmented state is $(x,j) \in [0,\infty)\times E_Y$; value functions $J_n(x,j)$ are defined analogously, with the recursion incorporating a finite sum over the next regime.

Formalization targets

Goal — Theorem 4.3.3

$$V_N = U_p, \qquad V_n(x) = \sup_{(c,a)\in D_n(x)} \bigl[U_c(c) + \mathbb{E}\,V_{n+1}\bigl((1+ i_{n+1})(x-c+a\cdot R_{n+1})\bigr)\bigr],$$

with $V_n$ strictly increasing, strictly concave, continuous, and an optimal strategy realized by per-stage maximizers. This is chunk 04a's Theorem 4.2.2 with consumption added, and every closed-form corollary below specializes it.

Eight milestones: the one-period existence/regularity theorem (Theorem 4.3.1); the zero-mean special case (Theorem 4.3.5); power- and logarithmic-utility closed forms (Theorems 4.3.6, 4.3.7); the regime-switching generalization of the goal itself (Theorem 4.4.1), its power-utility closed form (Theorem 4.4.2), and two comparative-statics results on how the optimal policy moves across regimes under a stochastic order (Theorems 4.4.4, 4.4.5).

Significance

Theorem 4.3.3's consumption-investment structure theorem is the basis for every result about optimal spending and saving under uncertainty; its power/log closed forms (Theorems 4.3.6/4.3.7) recover the classical facts that a power-utility investor consumes and invests constant fractions of current wealth (myopic, wealth-independent policy fractions) while a log-utility investor's optimal consumption fraction, $1/(N-n+1)$, is the textbook "consume your remaining horizon's worth" rule. The regime-switching extension (§4.4) is the discrete-time analogue of Hamilton's regime-switching models, now standard in empirical finance; Theorems 4.4.4-4.4.5 give a rigorous comparative-statics answer to "does a riskier regime call for more or less stock exposure," using the increasing-concave stochastic order rather than a first- moment heuristic — the mathematically correct notion of "regime $k$'s returns dominate regime $j$'s for every risk-averse (concave, monotone) preference," not merely "regime $k$ has a higher mean."

No result of this chunk was found on the platform (searched "consumption investment", "regime switching", "stochastic order"). The proofs largely mirror chunk 04a's (the book itself says so explicitly for Theorems 4.3.1, 4.3.7, 4.4.2), so this mission's contribution is the precise joint-choice statement of each result and, for the comparative-statics theorems, the correct increasing-concave order (≤_icv, Definition B.3.9c) rather than the plain concave order (≤_cv) chunk 02c already needed for a different theorem — the two are genuinely different relations and must not be conflated.

Difficulty

The naive approach to the goal decouples the consumption and investment choices into two independent optimizations; the book's own proof shows they do separate at the level of the per-stage optimization (Theorem 4.3.6's proof: the transformed problem factors into a consumption fraction $\zeta$ and an investment fraction $\alpha$ optimized independently once the wealth scale is normalized out), but the admissible sets remain jointly constrained ($0\le c\le x$ interacts with the investable amount $x-c$), so treating them as literally independent unconstrained problems would silently solve an easier, different problem. For the regime-switching comparative statics (Theorem 4.4.5), the natural first attempt tries to prove monotonicity of $d_n(j)$ in $j$ directly from $Q_j\le_{\mathrm{icv}}Q_k$ alone; the book's own induction needs both hypotheses simultaneously (the environment chain's own stochastic monotonicity, governing how the regime itself evolves, and the return-distribution order, governing the one-period objective) — Theorem 4.4.4's monotonicity of $\alpha^*(j)$ handles the second factor of the induction's product (Eq. (4.22)) while the chain's stochastic monotonicity handles the first; dropping either hypothesis breaks the induction step.

Formalization scope

The consumption-investment vocabulary (ConsumptionInvestmentMarket, its value function, the one-period sub-problem) mirrors chunk 04a's pure-investment TerminalWealthMarket pattern exactly, extended to a joint $(c,a)$ action. The regime-switching model (RegimeSwitchingMarket) represents the finite regime set $E_Y$ abstractly (a Fintype with a row-stochastic transition matrix p : EY → EY → ℝ, not a PMF/product-measure construction on the joint disturbance): the book's own formula for $J_n^\pi$ is already a finite sum over the next regime of an integral against $Q_j$, so this is the direct, faithful representation and needs no additional measure-theoretic machinery — Jpi/J are built via an accumulator recursing through this finite-sum-of-integrals at each step (the natural generalization of chunk 04a's EFromToAcc pattern to a kernel that depends on an evolving state coordinate, rather than an exogenous process). Theorem 4.4.4/4.4.5 introduce LEIncreasingConcaveOrder (Definition B.3.9c) fresh, since chunk 02c's stochastic-order triple (≤_st/≤_cv/≤_cx) does not include the increasing-concave order this chunk's theorems actually use — reusing one of those three would silently substitute a different hypothesis, exactly the trap the chunk brief warns against. IsStochasticallyMonotoneChain (Definition B.3.13) is likewise restated fresh for a finite chain given by its transition matrix.

No trivializing formalization: D_n(x) is a genuine joint constraint on (c,a) (not two independent unconstrained choices); the six closed-form theorems (4.3.6, 4.3.7, 4.4.2, plus the comparative-statics pair) each state their own explicit recursion for $d_n$ — matching the brief's own note that the index-base convention is not uniform across them (Theorem 4.3.6 gives $d_N$ and recurses backward; Theorem 4.4.2 gives $d_0(j)$ and recurses forward) — encoded exactly as each theorem states it, not standardized to one direction.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. https://doi.org/10.1007/978-3-642-18324-9
• J. D. Hamilton, "A new approach to the economic analysis of nonstationary time series and the business cycle", Econometrica, 1989 (the regime-switching framework §4.4 specializes to a portfolio-choice setting).

Motivation

An investor with a fixed planning horizon, an initial fortune, and a personal attitude toward risk (a utility function) wants to allocate wealth between a riskless bond and several risky assets, rebalancing at each of $N$ periods, to maximize the expected utility of terminal wealth. This is the oldest and most basic problem of mathematical finance's dynamic-programming tradition, going back to Samuelson (1969) and Merton (1969, continuous time). Bäuerle and Rieder's Chapter 4 is where the abstract finite-horizon Markov Decision Process theory built up in Chapter 2 — the Bellman equation, existence of optimal policies under compactness and continuity, propagation of concavity through the value function — is first put to genuine financial work: the multiperiod terminal-wealth problem is shown to be exactly an instance of that general theory, and the reduction pays off immediately in six closed-form solutions for the standard families of utility functions used throughout the literature (power, HARA, logarithmic, exponential).

Setting

An investor with utility function $U : \mathrm{dom}\,U \to \mathbb{R}$ (Definition 3.4.1: strictly increasing, strictly concave, continuous) and wealth $x$ invests in a bond (interest rate $i_{n+1}$ on $[n,n+1)$) and $d$ risky assets with relative risk $R_{n+1}$ (Chapter 3). The one-period problem: admissible investments $D(x) := \{a \in \mathbb{R}^d : (1+i)(x+a\cdot R) \in \mathrm{dom}\,U \text{ a.s.}\}$, $u(x,a) := \mathbb{E}[U((1+i)(x+a\cdot R))]$, $v(x) := \sup_{a \in D(x)} u(x,a)$. The multiperiod problem is the $N$-stage Markov Decision Model with state space $E := \mathrm{dom}\,U$ (wealth), action space $\mathbb{R}^d$, transition $T_n(x,a,z) = (1+i_{n+1})(x+a\cdot z)$, zero one-stage reward, terminal reward $g_N := U$; its value functions are $V_n(x) := \sup_\pi \mathbb{E}^\pi_{n,x}[U(X_N)]$ over Markov portfolio strategies $\pi$.

Formalization targets

Goal — Theorem 4.2.2

$$V_N = U, \qquad V_n(x) = \sup_{a \in D_n(x)} \mathbb{E}\bigl[V_{n+1}\bigl((1+i_{n+1})(x+a\cdot R_{n+1})\bigr)\bigr],$$

with $V_n$ strictly increasing, strictly concave and continuous, and an optimal portfolio strategy $(f_0^*,\dots,f_{N-1}^*)$ realized by maximizers of the recursion. This is the structural result every closed-form solution below specializes.

Eight milestones: the one-period existence/regularity theorem the induction step reduces to (Theorem 4.1.1); the upper bounding function that makes Chapter 2's existence machinery apply (Proposition 4.2.1); the zero-mean special case (Theorem 4.2.4); and four utility-specific closed forms plus the binomial-model comparative-statics lemma (Theorems 4.2.6, 4.2.11, 4.2.13, 4.2.15; Lemma 4.2.9).

Significance

Theorem 4.2.2 is the template for every dynamic portfolio problem in the rest of this book (consumption-investment in Chapter 4 §4.3-4.4, mean-variance and index tracking later in Chapter 4, and the partially-observed and jump-market analogues in Chapters 6 and 9): check a handful of structural conditions on the market data, and the existence, regularity, and recursive computability of the optimal policy follow automatically from Chapter 2's general theory rather than needing a bespoke argument each time. The six closed-form corollaries are the results practitioners actually use: the power/HARA/log/exponential-utility feedback rules are the standard textbook portfolio formulas (the logarithmic case is Kelly betting; the exponential case's wealth-independent optimal amount is the CARA-utility hallmark used throughout insurance and reinsurance mathematics), and Lemma 4.2.9's monotonicity result is the discrete-time analogue of the Merton ratio's dependence on the market's risk premium.

No result of this chunk was found on the platform (searched "terminal wealth", "portfolio optimization", "power utility", "HARA utility"). The proofs are complete in the book and mostly short (each utility-specific theorem reduces to checking the Structure Assumption via a transformation to a fraction-of-wealth variable); this mission's contribution is the precise formal statement of each closed form, with its own explicit recursion for $d_n$, since the six theorems share a structure but genuinely differ in which one-period sub-problem and which scaling variable ($x$, $x+bS^0_n/S^0_N$, or a wealth-independent constant) each uses.

Difficulty

The obvious shortcut for the goal is to prove existence of an optimal policy and its concavity/monotonicity properties by separate, ad hoc arguments at each stage; the actual content of Theorem 4.2.2 is that both reduce, via Theorem 4.1.1, to a single one-period fact applied identically at every stage — the induction step is exactly "if $v \in \mathrm{I\!M}_{n+1}$ [strictly increasing/concave/continuous with linear growth], then $v$ is a utility function on $E$ up to the growth bound, so Theorem 4.1.1 applies directly to $T_n v$." Missing this reduction leads to reproving compactness/upper-semicontinuity arguments from Chapter 2 by hand at every stage instead of invoking Theorem 4.1.1 once per stage. For the six closed-form theorems, the shared trap is conflating the different one-period sub-problems: the power- and HARA-utility theorems solve the same sub-problem (4.7) after a wealth-shift transformation, while the exponential-utility theorem's sub-problem (4.13) has a fundamentally different scaling (the optimal amount, not fraction, is wealth-independent) — collapsing these into one "utility-agnostic" statement would hide exactly the distinction the book is making.

Formalization scope

The multiperiod value function V is defined as an explicit supremum over admissible Markov portfolio strategies (not the Bellman recursion itself, and not full history-dependent strategies), following the book's own citation of Theorem 2.2.3 to justify restricting to Markov strategies for this model; this keeps the goal's parts (b)/(c) genuine content rather than restatements of the value function's own definition. The one-period vocabulary (OnePeriodD/OnePeriodU/OnePeriodV, NoArbitrageOnePeriod) is a self-contained restatement matching §4.1's own notation (a single $i$, $R$, no time index), independent of chunk 03's full market/portfolio apparatus, since Theorem 4.1.1's own content is exactly this one-period reduction. Proposition 4.2.1's proof cites two facts as already established elsewhere in the book (a concave function is dominated by an affine function; no-arbitrage bounds admissible actions linearly in wealth) — both are taken as explicit hypotheses of the Lean statement rather than re-derived, since re-deriving them is not this proposition's own content. HARA and power utility share one sub-problem definition (Afrac/vPower, Eq. (4.7)); logarithmic and exponential utility each need their own (AfracLog/vLog, vExp, Eqs. (4.11), (4.13)) since their admissibility sets and objective functions genuinely differ (a strict vs. non-strict inequality; a fraction vs. an absolute amount).

No trivializing formalization: each of the six closed-form theorems states its own explicit recursion for $d_n$ (a finite product or sum over $k=n,\dots,N-1$ of genuinely different per-stage terms) rather than a shared abstract "some sequence $d_n$ exists with $V_n = d_n \cdot (\text{shape})$" — the latter would hide exactly which recursion each utility function produces, the actual content the brief for this chunk flags as the point of having six near-identical theorems rather than one parametrized statement. Optimal strategies are stated in their exact feedback form ($f_n^*(x) = \alpha_n^* x$, or the HARA-specific affine shift, or the wealth-independent exponential-utility amount), not merely asserted to exist.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. https://doi.org/10.1007/978-3-642-18324-9
• R. C. Merton, "Lifetime portfolio selection under uncertainty: the continuous-time case", Review of Economics and Statistics, 1969 (the continuous-time analogue this discrete-time theory approximates, per Chapter 3's binomial-to-Black-Scholes convergence result).

Motivation

A conic quadratic program minimizes a linear objective subject to constraints of the form $\|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell$. Interior-point methods solve such programs in polynomial time, but around 2000 the available solvers handled far smaller instances than linear programming codes did. Ben-Tal and Nemirovski (Math. Oper. Res. 26(2), 2001) asked whether a conic quadratic program can be replaced by a linear program of comparable size, and answered it by approximating each second-order cone by a projection of a polyhedral cone. Their Theorem 1.1 builds such an approximation with accuracy $\varepsilon$ using $O(k\ln(2/\varepsilon))$ variables and inequalities. The present mission is their Proposition 3.1: this size is optimal in order, because every polyhedral $\varepsilon$-approximation needs $\Omega(k\ln(1/\varepsilon))$ inequalities.

The question of how many linear inequalities are needed to represent or approximate a convex set as a projection (its extension complexity) has since become a subject of its own, and the lower bound of Proposition 3.1 is one of its early explicit instances for a non-polyhedral cone.

Setting

For $y\in\mathbb R^k$ write $\|y\|_2=\sqrt{y_1^2+\dots+y_k^2}$. The Lorentz cone is

$$L^k=\{(y,t)\in\mathbb R^k\times\mathbb R\mid t\ge\|y\|_2\}.$$

Let $\varepsilon>0$. A polyhedral $\varepsilon$-approximation of $L^k$ is a linear map $\Pi:\mathbb R^k\times\mathbb R\times\mathbb R^p\to\mathbb R^q$ such that

1. if $(y,t)\in L^k$, then $\Pi(y,t,u)\ge0$ for some $u\in\mathbb R^p$;
2. if $\Pi(y,t,u)\ge0$ for some $u$, then $\|y\|_2\le(1+\varepsilon)t$.

Here $\ge0$ is componentwise, $p$ is the number of auxiliary variables and $q$ the number of homogeneous linear inequalities. Equivalently, the polyhedral cone $K=\{(y,t,u)\mid\Pi(y,t,u)\ge0\}$ projects onto a cone $\widehat L^k$ of the $(y,t)$-space with $L^k\subseteq\widehat L^k\subseteq\{(y,t)\mid\|y\|_2\le(1+\varepsilon)t\}$. The slice of $\widehat L^k$ at height one is $G=\{y\mid(y,1)\in\widehat L^k\}$, and $B=\{y\mid\|y\|_2\le1\}$ denotes the closed unit ball.

Formalization targets

Goal: Proposition 3.1, Eq. (13)

$$\exists\,c>0\ \ \forall k\ge2,\ \forall\varepsilon\in(0,\tfrac12],\ \forall p,q,\ \forall\Pi\ \text{polyhedral }\varepsilon\text{-approximation of }L^k:\qquad q\ \ge\ c\,k\ln\tfrac1\varepsilon .$$

The constant is absolute, as in the paper, and no value is fixed; the goal asserts only the order of growth.

Milestones (claims of the proof, in order)

1. Reduction. For $\varepsilon>0$ one may replace $\Pi$ by an approximation with the same $q$, at most $p$ auxiliary variables and the same projection, whose cone $K$ contains no line.
2. Extreme rays. A line-free cone $\{z\mid Az\ge0\}$ defined by $q$ inequalities is the conic hull of at most $2^q$ extreme rays.
3. Sandwich. $B\subseteq G\subseteq(1+\varepsilon)B$.
4. Vertices. If $K$ has no line, $G$ is the convex hull of $N\le2^q$ points.
5. Covering. If $\operatorname{conv}\{y_1,\dots,y_N\}\supseteq B$ and all $\|y_i\|_2\le1+\varepsilon$, the closed balls of radius $\sqrt{2\varepsilon(1+\varepsilon)}$ about the $y_i$ cover the sphere $\{\|y\|_2=1+\varepsilon\}$.
6. Counting. For $k\ge2$ and $\varepsilon\le\tfrac12$ such a covering needs $N\ge\exp\{c\,k\ln(1/\varepsilon)\}$ balls.

Significance

The result. Proposition 3.1 shows that the construction of Theorem 1.1 is optimal up to an absolute factor in the number of inequalities: approximating a conic quadratic constraint in dimension $k$ to relative accuracy $\varepsilon$ by linear inequalities costs $\Theta(k\ln(1/\varepsilon))$ inequalities, no more and no less. It separates what lifting (auxiliary variables) buys, a logarithmic dependence on $1/\varepsilon$, from what it cannot buy, a sub-linear dependence on $k$ or on $\ln(1/\varepsilon)$. Without auxiliary variables a polytope approximating the ball needs $\varepsilon^{-\Omega(k)}$ facets; the proposition says the logarithm of that count is the true cost even when lifting is allowed.

Formalizing it. The result is proved in the paper, in about fifteen lines that appeal to "elementary geometry" and to an unstated covering estimate. No machine-checked proof is known to exist. The mission produces a checked proof of the lower bound together with reusable facts: the finiteness bound on extreme rays of a pointed polyhedral cone and a lower bound on the number of balls needed to cover a Euclidean sphere, which Mathlib does not contain in this form. A companion mission of this series formalizes the matching upper bound (Theorem 1.1).

Difficulty

The obvious argument counts vertices of $G$: at most $2^q$ of them, and a polytope between $B$ and $(1+\varepsilon)B$ needs many vertices. The difficulty is in making "many" quantitative with the right exponent. A direct volume comparison of $G$ with $B$ gives nothing, since $G$ may have the volume of $(1+\varepsilon)B$. The argument needs the transfer from "the convex hull of the points contains $B$" to "the points are $\sqrt{2\varepsilon(1+\varepsilon)}$-dense on the outer sphere", and then a lower bound on the size of a covering of a sphere by balls whose centres need not lie on the sphere, uniform down to $k=2$ and up to $\varepsilon=\tfrac12$, where $\ln(1/\varepsilon)$ is only $\ln2$ and the radius $\sqrt{2\varepsilon(1+\varepsilon)}$ is comparable to the sphere's radius. A second, easily overlooked step is the passage to a line-free cone: $K$ itself may contain lines in the $u$-directions, in which case it has no extreme rays at all.

Formalization scope

Vectors of $\mathbb R^k$ are Fin k → ℝ, and the Euclidean norm is written out as eucNorm y = √(∑ i, y i ^ 2); the norm Mathlib puts on Fin k → ℝ is the sup norm, under which $L^k$ is polyhedral and the goal is false. A polyhedral approximation is an $\mathbb R$-linear map (Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ), and $p$, $q$ are the dimensions of its types; with arbitrary (nonlinear) maps, $\Pi(y,t)=t-\|y\|_2$ would give $q=1$, so linearity is what makes the statement non-trivial. "Extreme ray" means a ray $\{sr\mid s\ge0\}$, $r\ne0$, that is an extreme subset (Mathlib IsExtreme) of the cone, counted once per ray.

Corrections of the printed statement. Proposition 3.1 is printed for every positive integer $k$. It is false for $k=1$: $L^1=\{|y|\le t\}$ is polyhedral, and $\Pi(y,t)=(t-y,t+y)$ is a polyhedral $\varepsilon$-approximation with $q=2$ for every $\varepsilon$, so $q\ge c\ln(1/\varepsilon)$ fails for small $\varepsilon$. The goal and the counting milestone are therefore stated for $k\ge2$, which is the case the proof covers. The phrase "polyhedral $\alpha$ approximation" in the proof is read as $\varepsilon$. The paper's $O(1)$ constants are existential and quantified before every variable they are uniform over; no numerical value is asserted.

A complete development needs the Minkowski–Weyl representation of pointed polyhedral cones by extreme rays, basic convex-hull and separation arguments in Euclidean space, and a lower bound for covering numbers of spheres (for instance by a cap-measure or volume argument). The extreme-ray and covering lemmas are independent of the Lorentz cone and are welcome as stand-alone contributions.

Selected references

• A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
• A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM, 2001. https://doi.org/10.1137/1.9780898718829