Optimization

Motivation

This mission continues chapter 11's account of the M♮-concave/M♮-convex exchange-economy model begun in mission 14-economic-equilibrium, placing seven of that chunk's own results that were previously left out-of-cone: the two gross-substitutes-style characterizations of M♮-concavity (§11.3), the transfer theorem that lifts an equilibrium of the continuous relaxation to one for indivisible commodities (§11.4), and the explicit polyhedral description of the equilibrium price set together with its feasibility criterion (§11.5).

Setting

Mission 14-economic-equilibrium built the exchange-economy vocabulary this mission redeclares in full (UDom, ArgMaxBot/ArgMinTop, PriceShift/PriceShiftConvex, DemandSet/SupplySet, IsEquilibrium, MNaturalConcave, IsMNaturalConvexSet, the concave/convex closures ConcaveClosureR/ConvexClosureR and their continuous analogues ContDemandSet/ContSupplySet/ IsContEquilibrium) and placed the qualitative structural theorems (Theorems 11.1-11.3, 11.4, 11.16-11.18, 11.23-11.24). This mission adds the gross-substitutes axioms (−M♮-GS[Z], the price-monotonicity property NegGS, and −M♮-SWGS[Z], its one-price-at-a-time refinement NegSWGS), the M♮-convex-set transfer machinery connecting a continuous equilibrium to a discrete one, and the equilibrium price polyhedron built from the three bound families ℓ(j), u(j), u(i,j) (Eqs. (11.40)-(11.42)) that make Theorem 11.16's qualitative L♮-convex-polyhedron fact concrete and linear-programming-checkable.

Formalization targets

Goal: The equilibrium price set is the explicit L♮-convex polyhedron (11.43) (Theorem 11.21)

For a fixed allocation (x,y), the set P* of all equilibrium price vectors is an L♮-convex polyhedron and equals the polyhedron cut out by max{0,ℓ(j)} ≤ p(j) ≤ u(j) and p(j)-p(i) ≤ u(i,j). Chosen as goal: it is the sharpest structural result of chapter 11's computation section, upgrading Theorem 11.16's qualitative fact to a concrete description, and is what Theorem 11.22 (also placed) builds on directly.

Supporting structural targets

Theorem 11.5 and Theorem 11.6 characterize M♮-concavity via the gross-substitutes and stepwise gross-substitutes properties, completing chapter 11's suite of M♮-concavity characterizations begun with Theorem 11.4 (mission 14). Theorem 11.15 is the general transfer theorem (continuous equilibrium ⟹ discrete equilibrium) that mission 14's own Theorem 11.14 invokes as a special case. Theorem 11.22 gives the feasibility criterion for the existence of an equilibrium price vector, the mission's second theorem built on the equilibrium price polyhedron.

Significance

Together with mission 14-economic-equilibrium, this mission completes the book's account of how M♮-concavity/convexity — a purely combinatorial exchange condition — reproduces, and sharpens, the classical gross-substitutes theory of competitive equilibrium for economies with indivisible goods: existence transfers from the continuous relaxation, and the equilibrium price set itself has a description exact enough to reduce to a linear feasibility question. None of these results are open — they are Murota's own account (attributed in the book's own notes to Danilov-Koshevoy- Lang and Murota-Tamura for the gross-substitutes theorems, and to Murota-Tamura for the equilibrium price polyhedron); this mission contributes a faithful, machine-checked formal statement of each (see Formalization scope).

Difficulty

Two of this chunk's seven BRIEF.md results are not drafted this pass, for a disclosed time- budget reason rather than any faithfulness failure: Proposition 11.19 and Theorem 11.20 require the H,L-indexed bipartite MSFP2 flow-network vocabulary (separate vertex sets V+_e, V+_l, V-_h, an M-convex/M-concave-combining flow objective) that neither this mission nor mission 14 builds, and building it in proportion to placing exactly these two results was judged disproportionate to the remaining time in this pass; see HARD.md and STATUS.md. This is explicitly not a hard exclusion — both results are well-posed and provable from the book's own complete proofs — and is recorded as an honest scope limitation for a future pass. Theorem 11.22's own trailing algorithmic remark (that equilibrium prices can be found via a shortest-path computation, yielding a polynomial-time equilibrium-checking algorithm) is a computational/ complexity claim outside this series' propositional-formalization methodology and is omitted; the mathematical "iff feasibility" content is placed in full. See HARD.md.

Formalization scope

Ground set K is a Fintype with DecidableEq; consumer/producer index sets H, L are Fintypes (Nonempty where the price-bound formulas (11.40)-(11.42) need a nonempty sup'/inf' range). All base vocabulary is redeclared fresh from mission 14-economic-equilibrium's own definitions, since this draft cannot import that sibling mission. The gross-substitutes axioms are formalized directly from their defining inequalities (Eqs. preceding (11.19) and following, and p.331); the equilibrium price polyhedron's bound families ℓ(j)/u(j)/u(i,j) are formalized literally from Eqs. (11.40)-(11.42), extracting each WithBot ℝ/WithTop ℝ operand to ℝ before subtracting (since WithBot ℝ carries no subtraction instance). Two results (Proposition 11.19, Theorem 11.20) are not drafted this pass for the disclosed time-budget reason above; one result (Theorem 11.22's trailing algorithmic remark) is scoped out as computational content. Contributions completing any of the five sorrys, or building the MSFP2 vocabulary to place Proposition 11.19/Theorem 11.20 in a follow-up mission, are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• V. Danilov, G. Koshevoy, K. Murota, "Discrete convexity and equilibria in economies with indivisible goods and money," Mathematical Social Sciences, 41 (2001), pp. 251-273 [33] (origin of the gross-substitutes characterization, Theorem 11.6).
• K. Murota, A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [160] (origin of the equilibrium price polyhedron, Theorems 11.20-11.22).

Motivation

Two strategic levers shape the balance of power between a manufacturer and the retailer that resells its product. The first is strategic inventory: a buyer that orders more than it sells today, and carries the surplus into the next period, weakens the supplier's leverage over tomorrow's wholesale price. Anand, Anupindi and Bassok (Management Science 2008) showed that in a two-period channel the buyer withholds inventory exactly when its unit holding cost is below $\alpha/4$. The second is supplier encroachment: a supplier that can sell directly to consumers competes with its own buyer. Arya, Mittendorf and Sappington (Marketing Science 2007) showed that the threat of encroachment can lower wholesale prices and benefit both parties.

Guan, Gurnani, Geng and Luo, Strategic Inventory and Supplier Encroachment (MSOM 2019), combine the two levers in one game. Their headline qualitative finding is Proposition 4.2. When the supplier's direct channel is costly, but not quite too costly to use, the buyer keeps withholding inventory at every finite holding cost. This contrasts with the $\alpha/4$ cutoff of Anand et al. This mission formalizes that proposition, together with the equilibrium characterizations of Appendix A on which it rests.

Setting

There is one supplier and one buyer, two periods, deterministic demand and complete information. In each period the market price is $p = \alpha - q$, where $q$ is the total quantity sold in that period and $\alpha > 0$ is the demand intercept. The buyer pays a per-unit holding cost $h \ge 0$ on inventory carried into period 2. The supplier pays a per-unit direct selling cost $s \ge 0$. All other costs and the salvage value are zero. The moves are:

1. The supplier quotes a wholesale price $w_1 \ge 0$.
2. The buyer orders $Q_1$ and sells $q_1$, with $0 \le q_1 \le Q_1$. It carries the inventory $I = Q_1 - q_1$ into period 2.
3. The supplier quotes $w_2 \ge 0$.
4. The buyer orders $Q_2 \ge 0$ and sells $q_2$, with $0 \le q_2 \le I + Q_2$.
5. Having observed everything, the supplier sells $q_s \ge 0$ directly. The period-2 price is $\alpha - q_2 - q_s$.

The total profits are

$$\Pi_b = (\alpha - q_1)q_1 - w_1 Q_1 - hI + (\alpha - q_2 - q_s)q_2 - w_2 Q_2, \qquad \Pi_s = w_1 Q_1 + w_2 Q_2 + (\alpha - q_2 - q_s - s)q_s .$$

A strategy profile assigns an action to every history at which a player moves. It is a subgame perfect equilibrium (SPE) if, at every feasible history, the mover's prescribed action is feasible and no feasible alternative, followed by the profile afterwards, raises the mover's total profit. The equilibrium path is the outcome the profile generates; the equilibrium inventory is $I$ on that path. Following the paper (§4), the goal theorem sets $\alpha = 1$.

Formalization targets

Goal: Proposition 4.2

With $\alpha = 1$,

$$\forall h > 0\ \ \exists \epsilon > 0\ \ \forall s \in \big(\tfrac56 - \epsilon, \tfrac56\big):\quad \text{an SPE exists, and every SPE has } I > 0 \text{ and } hI < \tfrac{11}{72}.$$

Here $\epsilon$ may depend on $h$, and the bound $11/72$ applies at the same $(h, s)$.

Milestones, in attack order

1. Stage-3 best response (§3.1.1): in every SPE, the supplier sells $q_s = (\alpha - q_2 - s)^+/2$ at every history.
2. Eq. (1) (§3.1.1): with no inventory, the buyer's period-2 quantity is the four-branch function $q_b(w)$ of the period-2 wholesale price $w$.
3. Proposition 4.1, existence half: an SPE exists for every $h \ge 0$ and $s \ge 0$.
4. Region 8 (Tables A.1 and A.4): for $h < h_{11}$ with $s_3 \le s < 5\alpha/6$, or for $h < \alpha/4$ with $5\alpha/6 \le s < \alpha$, every SPE has $I = 5(\alpha - 4h)/34$ and the path of Table A.4.
5. Region 7, second part (Tables A.1 and A.3): for $h_{11} < h < h_{10}$ and $s_3 \le s < 5\alpha/6$, every SPE has $I = I^* = (2\alpha - 3s + x)/2$ and the path of Table A.3.
6. Region 10, second part (Tables A.1 and A.4): for $h > h_7$ and $2\alpha/3 < s < 5\alpha/6$, every SPE has $I = 0$.

The thresholds $x$, $s_3$, $h_7$, $h_{10}$, $h_{11}$ are explicit algebraic functions of $s$, given in Appendix A.

Significance

Proposition 4.2 separates the combined model from the two models it merges. Without a direct channel, inventory disappears once $h \ge \alpha/4$. With a direct channel, a threat of encroachment that is only barely credible keeps inventory alive at every holding cost. The total holding cost nevertheless stays below a constant, because the inventory shrinks as $h$ grows. Milestone 6 shows the flip side: for a fixed $s < 5\alpha/6$, a large enough $h$ removes the inventory. This is why the window $\epsilon$ must depend on $h$.

The paper's proofs are in an online appendix that is not reproduced in the article. The article itself gives the equilibrium only as tables. A formal development would supply a checked backward-induction proof of those tables in the regions near $s = 5\alpha/6$. It would also give a machine-checked SPE framework for multi-stage pricing-and-quantity games in supply chains, which none of the following exists for: Stackelberg pricing, sequential quantity competition, or dual-channel encroachment. No part of this paper has been formalized before.

Difficulty

The equilibrium is found by backward induction through five stages. Each stage's value function is only piecewise smooth, because the supplier's direct-channel response $(\cdot)^+$ switches on and off. As a result the buyer's period-2 profit has kinks, the supplier's period-2 profit as a function of $I$ has several local maxima, and the period-1 problems must compare branches whose boundaries are the irrational thresholds of Appendix A. The obvious approach, solving the first-order conditions stage by stage, fails at the kinks. At some region boundaries it also misses that the supplier is indifferent between two first-period prices, which makes the equilibrium path change discontinuously. Proposition 4.2 then needs uniform control of $h_7$, $h_{10}$ and $h_{11}$ as $s \uparrow 5/6$, where the denominator $3s - 2 - x$ of $h_7$ tends to $0$.

Formalization scope

• Representation. Strategies are functions of the full history, not Markov rules in $I$. IsSPE imposes optimality at every feasible history, including off-path ones. All actions are real numbers; wholesale prices and quantities are nonnegative, with $q_1 \le Q_1$ and $q_2 \le I + Q_2$.
• Normalization. The goal instantiates $\alpha = 1$ as the paper does from §4 on. The milestones keep a general $\alpha > 0$.
• Uniqueness is not stated. Proposition 4.1's uniqueness claim is false for strategy profiles: after the off-path price $w_2 = 0$, every order $Q_2 \ge q_2 - I$ is optimal. The goal and the region milestones therefore quantify over every SPE and carry existence as a separate conjunct.
• Corrected hypotheses.
  • The printed $s_3 = (\sqrt{(37 - 3\sqrt{65})/34} + 4/6)\alpha \approx 1.28\alpha$ is replaced by $(\sqrt{37 - 3\sqrt{65}}/34 + 4/6)\alpha \approx 0.772\alpha$, which matches the paper's "≈0.77".
  • Eq. (1) excludes the corner $w = 0$, $s < \alpha/3$, where its second branch is wrong.
  • Region 8 drops its boundary $h = h_{11}$ and Region 7 drops $h = h_{10}$, because the equilibrium path switches there and need not be unique.
• Ruled-out trivialization. The inventory in the goal is the inventory on the path of an SPE of the game above. It is not the closed form $5(1 - 4h)/34$ or $I^*$ from the tables, and the regional characterization is not a hypothesis. Otherwise the goal would reduce to algebra about the thresholds.
• Infrastructure and contributions. The definitions Game, IsSPE and Thresholds are shared by every statement. Welcome contributions include:
  • lemmas on maximizing concave piecewise-quadratic functions on half-lines;
  • a reusable backward-induction lemma for finite-stage games with real action sets;
  • interval-arithmetic facts about $x$, $h_7$, $h_{10}$ and $h_{11}$ near $s = 5/6$;
  • proofs of the paper's other regions.

Selected references

• T. Guan, H. Gurnani, X. Geng, Y. Luo, Strategic Inventory and Supplier Encroachment, Manufacturing & Service Operations Management 21(3):536–555, 2019. https://doi.org/10.1287/msom.2018.0705
• K. Anand, R. Anupindi, Y. Bassok, Strategic Inventories in Vertical Contracts, Management Science 54(10):1792–1804, 2008. https://doi.org/10.1287/mnsc.1080.0894
• A. Arya, B. Mittendorf, D. Sappington, The Bright Side of Supplier Encroachment, Marketing Science 26(5):651–659, 2007. https://doi.org/10.1287/mksc.1070.0280

Motivation

Chapter 9 is where discrete convex analysis meets classical network flow theory: the minimum cost flow problem's three hallmark properties — an optimality criterion by potentials, an optimality criterion by negative cycles, and integrality of optimal solutions — are shown to survive, in a precise and increasingly general form, first for arbitrary polyhedral convex costs (MCFP3), then for the M-convex submodular flow problem (MSFP2/MSFP3), the chapter's own combinatorial generalization of the classical problem. This mission places the potential criterion (Theorem 9.4) and its cascade of six corollaries and generalizations, the block of results this book's own text uses to carry every other result in the chapter.

Setting

A digraph G = (V,A) with tail/head maps ∂⁺,∂⁻ : A → V. A flow ξ : A → R has boundary ∂ξ(v) = Σ{ξ(a) : ∂⁺a=v} − Σ{ξ(a) : ∂⁻a=v}. A potential p : V → R has coboundary δp(a) = p(∂⁺a) − p(∂⁻a). The minimum cost flow problem MCFP3 minimizes Γ₃(ξ) = Σₐ fₐ(ξ(a)) + f(∂ξ) over flows, for polyhedral convex arc costs fₐ : R → R∪{+∞} and boundary cost f : Rⱽ → R∪{+∞}; MCFP0 is its linear-cost, fixed-supply special case. The M-convex submodular flow problem MSFP3 is MCFP3 with f additionally M-convex; MSFP2 is its linear-arc-cost special case.

Formalization targets

Goal: The potential criterion for MCFP3 (Theorem 9.4)

For a feasible flow ξ, ξ is optimal for MCFP3 iff there is a potential p with ξ(a) a minimizer of the reduced arc cost fₐ[δp(a)] for every arc and ∂ξ a minimizer of the reduced boundary cost f[−p]; and any such optimal potential characterizes optimality of every feasible flow. This is the hub result of the whole chunk: the book states Theorem 9.14 is "immediate" from it, and every other placed result either specializes it directly or builds on that specialization.

Supporting structural targets

Theorem 9.5 reformulates MCFP0's optimality as the absence of a negative cycle in an auxiliary network; Theorem 9.6 gives MCFP0's primal and dual integrality, the latter identifying the optimal-potential set as an L-convex polyhedron. Theorem 9.14 specializes the goal to MSFP3; Theorem 9.15 upgrades this to a full polyhedral and integrality structure theorem for MSFP3's optimal-flow-boundary and optimal-potential sets (M2-convex and L-convex polyhedra respectively); Theorem 9.16 is the integer-flow analogue, with the boundary set now literally M2-convex and the integer-optimal-potential set literally L-convex. Theorems 9.18 and 9.20 give the negative-cycle reformulation for MSFP2, real and integer flows respectively, generalizing Theorem 9.5 by admitting a third class of auxiliary arcs governed by the M-convex boundary cost's directional derivative (or its discrete difference, in the integer case).

Significance

This is the chapter's demonstration that M-convexity is not merely an abstract combinatorial axiom but the exact structural hypothesis under which classical network-flow duality survives intact: every one of the four "nice properties" the book opens the chapter with (potentials, negative cycles, integrality, efficient algorithms) is preserved verbatim in the M-convex generalization, and this mission's eight results are the proof of that claim for the first three. The chunk's own internal dependency structure — one foundational theorem (9.4) from which every other placed result descends by specialization or direct generalization — is itself characteristic of how this book organizes its combinatorial machinery around a single convex- analytic core.

None of these results are open — they are Murota's own account of network flow duality under M-convexity (sections 9.1, 9.4, and 9.5). What this mission contributes is a faithful, machine-checked formal statement of each, extending the platform's coverage of chapter 9 begun in mission 12-network-flows (which covered §9.1.1-9.1.2 and §9.3, the feasibility and max-flow min-cut results, deliberately leaving this block for later apparatus); no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The eight results span real- and integer-flow versions of two nested problem hierarchies (MCFP0 ⊂ MCFP3, MSFP2 ⊂ MSFP3) and two distinct optimality certificates (potentials, negative cycles), which this mission handles by building one shared apparatus — FeasibleFlowMCFP3, Gamma3, OptimalFlowMCFP3, IsOptimalPotential — that MCFP0 and MSFP3 both instantiate (MCFP0 literally as the linear-cost/singleton-boundary special case of Eq. (9.11)), and one shared generic cycle/negative-cycle apparatus (IsCycle, CycleLength, HasNegativeCycle) instantiated three times with different auxiliary-arc types (A⊕A for MCFP0, A⊕A⊕(V×V) for MSFP2's extra Cξ arcs governed by the boundary cost's directional derivative). "Primal integral" and "dual integral" polyhedral convex functions (the book's own C[Z|R→R]/C[R→R|Z] notation, used in Theorem 9.15) needed a modeling decision, since the book's own definition of these classes lies outside this chunk's page range; see Formalization scope.

Formalization scope

Ground-set vertices V and arcs A are Fintype with DecidableEq. All base M-/L-convexity vocabulary is redeclared from prior missions in this series. "Primal integral" (C[Z|R→R], M[Z|R→R]) is formalized as integer effective domain (IsDomainIntegerArc/IsDomainIntegerR); "dual integral" (C[R→R|Z], M[R→R|Z]) is formalized as the existence of an integer subgradient at every domain point (IsDualIntegralArc/IsDualIntegralR) — a standard equivalent characterization for polyhedral convex functions, and a deliberate modeling choice recorded in MODERATION_NOTES.md rather than a literal transcription of the book's own (out-of-range) definition of these two notation classes. All eight numbered results found in this chunk's page range are placed in full, with no partial-coverage scope reduction. Contributions completing any of the eight sorrys are welcome; the goal and Theorem 9.15 carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• R. T. Rockafellar, Network Flows and Monotropic Optimization, Wiley, 1984 [178] (the classical potential/Fenchel-duality framework this mission's Theorem 9.4 adapts).
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (the Lagrange duality and negative-cycle theory of section 9.5 this mission's Theorems 9.18 and 9.20 draw from).

Motivation

Mission 29-ch08b-conjugacyduality opened chapter 8's account of M2-convex functions — sums of M-convex functions — proving their domains and minimizers are M2-convex and that they are integrally convex. This mission completes that program and builds its exact mirror for L2-convex functions (integer infimal convolutions of L-convex functions), the class that appears on the opposite side of Edmonds's intersection theorem's min-max relation from M2-convexity. It proves optimality and proximity theorems for both classes, shows their subdifferentials add (a discrete analogue of the classical subdifferential sum rule), derives how the Legendre-Fenchel transform interacts with the sum/infimal-convolution operation, and — the technically hardest result in the whole cluster — establishes that L♮₂-convex functions are integrally convex, by a genuinely different and more intricate argument than the M2-side analogue required.

Setting

Fix a finite ground set $V$. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is L2-convex if $g = g_1 \square g_2$, the integer infimal convolution $g_1\square g_2(p) = \inf\{g_1(p_1)+g_2(p_2) : p_1+p_2=p\}$, of two L-convex functions $g_1, g_2$; L$^\natural_2$-convex if the summands are L$^\natural$-convex. An M2-convex function is a sum $f_1+f_2$ of two M-convex functions (mission 29-ch08b-conjugacyduality). The integer subdifferential $\partial_{\mathbb Z} f(x)$ and real subdifferential $\partial_{\mathbb R} f(x)$ generalize the subgradient set to integer- and real-valued perturbation directions respectively.

Formalization targets

Goal: L$^\natural_2$-convex functions are integrally convex (Theorem 8.42)

Every L$^\natural_2$-convex function is integrally convex, and in particular every L$^\natural_2$-convex set is integrally convex. The book's own proof is the most intricate argument in this cluster: given $p$ in the Minkowski sum $D_1+D_2$ of two L-convex sets, it constructs an explicit representation of $p$ as a convex combination of finitely many integer points of $D_1+D_2$, all lying in $p$'s own integral neighborhood, via the sorted fractional-part values of a chosen decomposition $p=p_1+p_2$ — a genuinely different technique from the M2-side analogue (Theorem 8.31), whose proof is a two-line consequence of convex extensibility.

Supporting structural targets

Eleven further results build the M2-/L2-convex theory in parallel. Theorems 8.33-8.34 give the M2-optimality criterion (a nonnegative-sum condition over cyclic exchange families) and its scaling-based proximity theorem; Theorem 8.35 shows subdifferentials of a sum of M$^\natural$- convex functions add, and that subdifferentials of M2-/M$^\natural_2$-convex functions are L2-/L$^\natural_2$-convex; Theorem 8.36 computes the conjugate of a sum as the infimal convolution of conjugates, with biconjugacy recovering the original sum. Propositions 8.39-8.41 transfer L-(natural-)convexity from summands to the domain and minimizer set of an L2-convex function, and give the precise attainment condition under which a linearly-perturbed infimal convolution's minimizer set splits additively. Theorems 8.43-8.44 give the L2-optimality and L2-proximity theorems, the exact L-side mirrors of Theorems 8.33-8.34; Theorem 8.45 mirrors Theorem 8.35 for subdifferentials of an infimal convolution; and Theorem 8.46 (found by direct reading, immediately following 8.45 and explicitly named by the book as 8.36's counterpart) shows biconjugacy for L$^\natural$-convex infimal convolutions.

Significance

The M2-/L2-convex function classes are where discrete convex analysis's abstract machinery meets concrete combinatorial optimization: Edmonds's matroid intersection theorem and its generalizations are literally statements about M2-convex minimization, with the L2-convex side supplying the dual bound. Theorem 8.35's subdifferential additivity is the discrete analogue of the classical Moreau-Rockafellar sum rule, and its proof (via the M-convex intersection theorem, already a milestone of mission 10-conjugacy-i) shows the sum rule holding without the constraint-qualification technicalities the continuous theory needs — a case where the discrete theory is cleaner than its continuous ancestor. Theorem 8.42's harder, dedicated proof technique is itself informative: it demonstrates that L2-convexity's combinatorial structure is not a routine transcription of the M2-convex case, foreshadowing the book's broader theme that M- and L-convexity, while conjugate, are not interchangeable in how their proofs actually work.

None of these results are open — they are Murota's account of the sum/infimal-convolution closure properties of M-convex and L-convex functions, continuing chapter 8's duality program into its most combinatorially concrete corner. What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Theorem 8.46) the platform's own automated extractor missed, extending the shared Lean vocabulary (InfConv, L2Convex, M2ConvexSet) mission 29-ch08b-conjugacyduality began; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to adapt the M2-side integral-convexity proof (a direct appeal to convex extensibility) verbatim; the book's own proof shows this does not work, requiring instead a from-scratch construction: decompose $p=p_1+p_2$, take fractional parts $a_1 = p_1-\lfloor p_1\rfloor$ and $a_2=\lceil p_2\rceil-p_2$, sort their combined distinct values, build threshold sets exactly as in the Lovász-extension construction, and verify each resulting integer point $q_i = \lfloor p_1\rfloor+\chi_{U_{1i}}+\lceil p_2\rceil-\chi_{U_{2i}}$ both lies in $D_1+D_2$ (via L-convex-set closure properties, Theorem 5.10) and in $p$'s integral neighborhood (a case split on whether $p(v)$ is itself an integer) — a genuinely multi-stage combinatorial argument with no single-inequality shortcut, unlike almost every other result in this mission.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; M2-/L2-convex functions are (V→ℤ)→WithTop ℝ. All twelve numbered results found in this chunk's page range are placed, with no partial-coverage scope reduction needed — every clause of every result, including all three parts of Theorems 8.35 and 8.45 and the full cyclic-exchange condition of Theorems 8.33-8.34, is stated in full. One numbered result nominally in this chunk's page range, Theorem 8.32, is not re-placed here: it was already found and placed as a milestone in mission 29-ch08b-conjugacyduality, whose own page range overlaps this chunk's by one page (PDF245) — see HARD.md. "g1□g2 > −∞" hypotheses are omitted rather than translated, since WithTop ℝ has no −∞ element to violate. This mission's base vocabulary is redeclared verbatim from mission 29-ch08b-conjugacyduality rather than imported, since sibling drafts in this series cannot yet reference one another; ConvexConjugate is redeclared from mission 10-conjugacy-i. Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 8.35 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 [153] (the L2-convex integral-convexity proof this mission's goal is drawn from).
• K. Murota and A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [162] (the M2-proximity theorem, Theorem 8.34).

Motivation

Chapter 8 is where discrete convex analysis explains why it needed two separate notions — M-convexity (exchangeability) and L-convexity (submodularity) — rather than one. The answer is conjugacy: under the classical Legendre-Fenchel transform, the two classes turn out to be exactly dual to each other, the discrete analogue of the fact that convex analysis's transform is self-dual within a single class of convex functions. Mission 10-conjugacy-i proved the integer-lattice version of this fact (Theorem 8.12) but explicitly deferred the polyhedral version — Theorem 8.4, the chapter's own headline "Conjugacy theorem" — noting it needed a real-variable M-/L-convex-function layer the series had not yet built. That layer now exists, built across missions 23-24-ch06*-mconvexfunctions and 26-27-ch07*-lconvexfunctions. This mission proves Theorem 8.4 and its companions: the polar-cone correspondence it induces, its nonpolyhedral generalization, the separation and Fenchel-duality theorems for M♮-/L♮-convex functions, and the basic theory of M2-convex functions (sums of M-convex functions), which the Edmonds intersection theorem's own combinatorics is built from.

Setting

Fix a finite ground set $V$. For $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$, the Legendre-Fenchel transform is $f^\bullet(p) = \sup_x [\langle p,x\rangle - f(x)]$. A polyhedral convex function $f$ is M-convex ($f \in M[\mathbb R \to \mathbb R]$) if it satisfies (M-EXC[R]); $g$ is L-convex ($g \in L[\mathbb R \to \mathbb R]$) if it satisfies (SBF[R]) and (TRF[R]). A concave function $h$ is always represented via $h_2 = -h$, an ordinary convex function, so every "$f \ge h$" hypothesis is restated as "$f + h_2 \ge 0$" — an equivalent formulation avoiding any need to represent $-\infty$ in the codomain. A polyhedral cone's polar is $C^\circ = \{y : \langle y,x\rangle \le 0\ \forall x \in C\}$. A function is M2-convex if it is the sum of two M-convex functions.

Formalization targets

Goal: the conjugacy theorem (Theorem 8.4)

The classes of polyhedral M-convex functions and polyhedral L-convex functions are in one-to-one correspondence under the Legendre-Fenchel transform: $f \in M \Rightarrow f^\bullet \in L$, $g \in L \Rightarrow g^\bullet \in M$, and the transform is an involution ($f^{\bullet\bullet}=f$, $g^{\bullet\bullet}=g$) on each class, with the identical statement for the M$^\natural$/L$^\natural$ variants. This is the theorem mission 10-conjugacy-i deferred, citing exactly the missing infrastructure this series has since built.

Supporting structural targets

Twelve further results build the surrounding theory. Proposition 8.2 gives the easy two-variable case of the general submodularity-preservation fact (Theorem 8.1, already a milestone of mission 10-conjugacy-i); Proposition 8.3 is the technical minimizer-difference lemma the goal's harder direction is built from. Theorem 8.5 derives the M-convex/L-convex cone polarity from the goal, and Theorem 8.6 extends the correspondence beyond the polyhedral case to general closed proper convex functions. Proposition 8.14 and Theorems 8.15-8.16 build the separation theory for M♮-/L♮-convex and concave function pairs, with integral witnesses when the functions are integer valued; Theorem 8.21 (parts 1-2) derives the Fenchel-type strong-duality equality these separation theorems make possible. Propositions 8.29-8.30 and Theorem 8.31 (plus Theorem 8.32, found by direct reading immediately after 8.31) build the basic theory of M2-convex functions: their domains and minimizer sets are M2-convex, they are integrally convex, and their global optimality reduces to a finite local check.

Significance

The goal is the theorem that retroactively explains this entire series' two-track structure: missions 20-25 (M-convex sets and functions) and 08/21/26-28 (L-convex sets and functions) are not two independent theories that happen to share techniques — they are conjugate images of each other, so every theorem proved on one side has a dual counterpart automatically available on the other via Theorem 8.4. This is made concrete immediately: Theorem 8.5's cone polarity and the diagram the book draws connecting $M_0[\mathbb R]$, $0L[\mathbb R\to\mathbb R]$, and submodular set functions $S[\mathbb R]$ (already correspondences this series proved independently, in missions 24-ch06d-mconvexfunctions and 28-ch07d-lconvexfunctions) are shown to be facets of one single conjugacy fact rather than three separate coincidences. The separation and Fenchel duality theorems (8.15, 8.16, 8.21) are the discrete analogues of the two theorems every convex optimization course opens with, and the book is explicit that they are not corollaries of the classical versions plus convex extensibility — they carry genuinely combinatorial content, specializing to Frank's discrete separation theorem and Edmonds's intersection theorem as examples the book itself gives.

None of these results are open — they are Murota's account of the duality at the heart of discrete convex analysis, the reason the theory needed two dual notions rather than one. What this mission contributes is a faithful, machine-checked formal statement of each, completing a theorem mission 10-conjugacy-i explicitly left for a future session once the necessary polyhedral apparatus existed, and including one result (Theorem 8.32) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal's harder direction (L⇒M) would try to verify the exchange inequality for $g^\bullet$ directly from the definition of the transform; the book's actual proof instead identifies the exchange inequality with a statement about weighted minimizers of $g$ itself via Proposition 8.3 (the minimizer-difference bound), converting a claim about the conjugate function into a claim about $g$'s own combinatorial structure — a genuine change of perspective, not a direct calculation. Proposition 8.3's own proof is the hardest single argument in this block: it derives the minimizer-difference bound by a contradiction argument that constructs an explicit pair of "worse" minimizers via a join/meet perturbation and derives a strict inequality from Theorem 7.29's translation inequality — a multi-step combinatorial argument with no direct shortcut.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; convex functions are WithTop ℝ valued throughout (never EReal, except for the Legendre-Fenchel transform itself, whose defining supremum/infimum can genuinely be infinite). All thirteen numbered results found in this chunk's page range — the twelve in BRIEF.md's own table plus Theorem 8.32 — are placed, with one documented scope reduction: Theorem 8.21 states only its real-attainment parts (1)-(2), not the integer-attainment refinement of parts (3)-(4), which needs a separate argument no other result in this chunk requires — see HARD.md. Concave functions $h$ are always represented via $h_2 = -h$ and every inequality $f \ge h$ restated as $f + h_2 \ge 0$, avoiding WithTop ℝ negation entirely. This chunk's own BRIEF.md inherited the chapters-4-7 page-offset boilerplate (printed = PDF $-$ 19); chapter 8 uses offset 18, confirmed against the PDF's own footers — every citation here uses the corrected offset. This mission's base vocabulary is redeclared from missions 10-conjugacy-i, 20-ch04b-mconvexsets, 21-ch05b-lconvexsets, 23-24-ch06*-mconvexfunctions, and 26-27-ch07*-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 8.3 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 [152] (the polyhedral M-/L-convex conjugacy theory this mission's real-variable results are drawn from).

Motivation

The Legendre-Fenchel transform is the single most structurally important operation in convex analysis: for a proper closed convex function $f$, its conjugate $f^\bullet(p) = \sup_x \{\langle p,x\rangle - f(x)\}$ is again proper closed convex, and the transform is an involution — $f^{\bullet\bullet} = f$. This one fact underlies duality theory across optimization: every strong-duality theorem is, at bottom, a statement about conjugate pairs. Chapters 6 and 7 of this book developed M-convex and L-convex functions as if they were two separate theories, each with its own exchange axiom, optimality criterion, and proximity theorem. Chapter 8 reveals they were never separate: the Legendre-Fenchel transform, suitably discretized, is a bijection between the two classes. This mission formalizes that discrete conjugacy theorem together with its classical real-valued precursor and a genuine function-level generalization of Edmonds's intersection theorem, completing the picture that chunks 06 through 09 built the two halves of.

Setting

Let $V$ be a finite ground set. For $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$, the Legendre-Fenchel transform is $f^\bullet(p) = \sup\{\langle p,x\rangle - f(x) : x \in \mathbb R^V\}$; $f$ is submodular if $f(x)+f(y) \ge f(x\vee y)+f(x\wedge y)$ and supermodular under the reverse inequality. For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$, the discrete Legendre-Fenchel transform restricts the same supremum formula to $p \in \mathbb Z^V$: $f^\bullet(p) = \sup\{\langle p,x\rangle - f(x) : x \in \mathbb Z^V\}$ for $p \in \mathbb Z^V$ — a genuinely different object from the real-valued transform, since the supremum is now over integer $x$ only, and the codomain is checked back against the discrete M-/L-convexity axioms of chunks 06–09. The integer biconjugate $f^{\bullet\bullet}$ is the transform applied twice. $f$ is integer valued if every finite value it takes is an integer (the classes $M[\mathbb Z\to\mathbb Z]$, $L[\mathbb Z\to\mathbb Z]$ of the goal theorem are exactly the M-/L-convex functions with this property).

Formalization targets

Goal: Theorem 8.12 (the discrete conjugacy theorem)

(1) The classes $M[\mathbb Z\to\mathbb Z]$ and $L[\mathbb Z\to\mathbb Z]$ are in one-to-one correspondence under the discrete Legendre-Fenchel transform: for $f \in M[\mathbb Z\to\mathbb Z]$ and $g \in L[\mathbb Z\to\mathbb Z]$, $f^\bullet \in L[\mathbb Z\to\mathbb Z]$, $g^\bullet \in M[\mathbb Z\to\mathbb Z]$, $f^{\bullet\bullet}=f$, and $g^{\bullet\bullet}=g$. (2) The same correspondence holds between $M^\natural[\mathbb Z\to\mathbb Z]$ and $L^\natural[\mathbb Z\to\mathbb Z]$.

Milestones: Theorem 8.1, Proposition 8.11, Theorem 8.17

Theorem 8.1: the conjugate of a real-valued submodular function is always supermodular — the classical warm-up, and evidence that submodularity/supermodularity is not symmetric under conjugation on its own (the converse fails). Proposition 8.11: the integer biconjugate recovers $f$ at any point with a nonempty integer subdifferential — the fact that makes discrete biconjugation meaningful at all. Theorem 8.17 (the M-convex intersection theorem): a point jointly minimizes a sum of two M$^\natural$-convex functions if and only if a single linear functional separately certifies it as a minimizer of each perturbed function — the function-level generalization of chunk 04's Edmonds's intersection theorem for M-convex sets.

Significance

The result itself. The discrete conjugacy theorem is, in the book's own words, "the unifying result of the entire book": every theorem proved separately for M-convex functions (chunks 06–07) has an exact mirror for L-convex functions (chunks 08–09) precisely because the Legendre-Fenchel transform carries one class to the other. Theorem 8.17's function-level Edmonds generalization shows the payoff directly — the classical matroid-intersection-style min-max duality of chunk 04 was never really about sets; it is a special case (indicator functions) of a duality that holds for the whole class of M-convex functions.

Formalizing it. No matching item exists on the platform for conjugate functions, discrete conjugacy, or this generality of intersection theorem. This mission gives the first formal statement of the discrete conjugacy theorem, distinguishing it carefully from its real-valued (polyhedral) precursor, Theorem 8.4 — a genuinely different, harder theorem this mission does not draft (see Formalization scope), since the integer bijection needs the M-/L-proximity theorems of chunks 06–09 to control integrality under convex extension, while the real-valued case does not.

Difficulty

The obvious approach — try to prove the discrete conjugacy theorem directly by mimicking the real-valued proof (Theorem 8.4) with ℤ in place of ℝ everywhere — fails, because the real-valued proof's key step (Proposition 8.3, an infimal-convolution argument comparing arg min sets of perturbed polyhedral functions) has no immediate discrete analogue: a discrete arg min need not vary continuously with the perturbation the way a polyhedral one does. The book's actual strategy instead routes through the convex extension of the discrete function (chunk 06/08's bridge to chapter 3's integral convexity), applies the already-proved real-valued conjugacy theorem to the extension, and then must separately argue that the resulting conjugate, restricted back to integer points, is again integer-valued and satisfies the discrete exchange axiom — an argument that needs different treatment depending on whether the original function's domain is bounded or unbounded (an exhaustion argument via restriction to a growing integer interval, invoking chunk 06's proximity theorem to control convergence). Skipping this discreteness argument and treating the real-valued theorem as if it settled the integer case would silently discard exactly the chapter's own point.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq. ConvexConjugate (the discrete transform) has domain and codomain both (V → ℤ) → WithTop ℝ, obtained by taking the defining supremum in EReal (a complete lattice, so it is always total) and projecting back via a new FromEReal map — this is what lets the biconjugate f•• typecheck as an equality of functions of the same type as f. ConvexConjugateR (the real-valued transform, used only by the milestone Theorem 8.1) is a separate object with no shared code, per the explicit warning against conflating the two transforms; the two never appear in the same item.

A trivializing formalization of the goal would draft only the real-valued case (Theorem 8.4) as if it were the discrete theorem, or would silently allow WithTop ℝ's subtraction-avoidance convention to change which values are compared; neither is done. Theorem 8.4 itself (the polyhedral conjugacy theorem) is not drafted in this mission at all — it would require a fresh, otherwise-unused polyhedral M-/L-convex-function layer on Rⱽ that no other item here needs (see MODERATION_NOTES.md). The M-/L-separation theorems (8.15, 8.16) and the Fenchel-type duality theorem (8.21) are likewise left for a follow-on mission; contributions building the polyhedral bridge or the separation theorems, which depend on machinery this mission establishes, are welcome.

Selected references

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

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.

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

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