Optimization

Motivation

A risk measure turns the random loss of a financial position into a single number: the amount of capital a regulator or a risk manager requires to hold the position. Two families of risk measures dominate practice and theory. Value-at-Risk (VaR), a quantile of the loss distribution, is used in banking and insurance regulation; it is positively homogeneous but not convex, so it can penalize diversification. Convex risk measures (Föllmer and Schied 2002; Frittelli and Rosazza Gianini 2002), and their positively homogeneous subclass of coherent risk measures (Artzner, Delbaen, Eber and Heath 1999), reward diversification and come with a duality theory, but they exclude VaR and many of its robust variants.

Castagnoli, Cattelan, Maccheroni, Tebaldi and Wang (Operations Research 70(5), 2022) study the class that contains both: star-shaped risk measures, those for which increasing the exposure to a position never decreases the risk per unit of exposure. The class is closed under the aggregation operations used in practice (averages across models, worst cases across scenarios, medians, risk sharing), which convexity is not. It contains VaR, Expected Shortfall, their scenario-based robustifications such as $\mathrm{MaxVaR}$, the benchmark-loss VaR of Bignozzi et al. (2020), and utility-based shortfall risk for utilities with the Landsberger–Meilijson property.

Timeline. Artzner et al. (1999) axiomatize coherent risk measures. Föllmer and Schied (2002) and Frittelli and Rosazza Gianini (2002) introduce convex ones. Föllmer and Schied (2016, Proposition 4.47) show that VaR is the minimum of the convex risk measures dominating it. Castagnoli et al. (2015) state the representation below without proof. The 2022 paper proves it for every star-shaped risk measure, and shows that the property characterizes the class.

Setting

Fix a set $\Omega$ of states. The space of positions $\mathcal X$ is a linear space of bounded functions $X:\Omega\to\mathbb R$ containing every constant function; the constant $m$ is identified with the position that pays $m$ in every state. A value $X(\omega)>0$ is a loss. No probability measure is fixed. $\mathcal X$ is ordered pointwise: $X\geqq Y$ means $X(\omega)\ge Y(\omega)$ for every $\omega$.

A risk measure is a function $\rho:\mathcal X\to\mathbb R$ that is monotone ($X\geqq Y\Rightarrow\rho(X)\ge\rho(Y)$), translation invariant ($\rho(X-m)=\rho(X)-m$ for all real $m$) and normalized ($\rho(0)=0$). It is

• star-shaped if $\rho(\lambda X)\ge\lambda\rho(X)$ for all $X$ and all $\lambda>1$;
• convex if $\rho(\lambda X+(1-\lambda)Y)\le\lambda\rho(X)+(1-\lambda)\rho(Y)$ for all $X,Y$ and all $\lambda\in(0,1)$;
• positively homogeneous if $\rho(\lambda X)=\lambda\rho(X)$ for all $\lambda>0$;
• coherent if it is positively homogeneous and subadditive, $\rho(X+Y)\le\rho(X)+\rho(Y)$.

The acceptance set of $\rho$ is $\mathcal A_\rho=\{X\in\mathcal X\mid\rho(X)\le0\}$. More generally, an acceptance set is a subset $\mathcal A\subseteq\mathcal X$ with $\sup\{m\in\mathbb R\mid m\in\mathcal A\}=0$ that is closed downwards ($X\in\mathcal A$, $Y\leqq X$ imply $Y\in\mathcal A$). It is convex if convex and coherent if a convex cone, and it generates $\rho_{\mathcal A}(X)=\inf\{m\mid X-m\in\mathcal A\}$. A set $S$ is star-shaped if $\lambda s\in S$ for all $s\in S$ and $\lambda\in[0,1]$.

In the Lean development the space of positions is PositionSpace Ω, positions are elements of 𝒳.carrier, and the predicates are IsRiskMeasure, IsStarShaped, IsConvexRiskMeasure, IsCoherentRiskMeasure, acceptanceSet, IsAcceptanceSet, IsConvexAcceptanceSet.

Formalization targets

Goal: Theorem 2 (p. 2643)

For a risk measure $\rho$, the following are equivalent:

1. $\rho$ is star-shaped;
2. there is a set $\Gamma$ of convex risk measures with

$$\rho(X)=\min_{\gamma\in\Gamma}\gamma(X)\qquad\text{for all }X\in\mathcal X;$$

3. there is a family $\{\mathcal A_\beta\}_{\beta\in B}$ of convex acceptance sets with

$$\rho(X)=\min\{m\in\mathbb R\mid X-m\in\mathcal A_\beta\text{ for some }\beta\in B\}\qquad\text{for all }X\in\mathcal X.$$

Moreover, for star-shaped $\rho$, $\Gamma$ may be taken to be the set of all convex risk measures $\gamma\geqq\rho$, and the family to be their acceptance sets. The minima are attained. The goal fixes no particular $\Omega$, $\mathcal X$ or $\Gamma$.

Milestones

• Proposition 1 (p. 2642): star-shapedness is equivalent to $\rho(\alpha X)\le\alpha\rho(X)$ for $\alpha\in(0,1)$, and to the risk-to-exposure ratio $\beta\mapsto\rho(\beta X)/\beta$ being increasing on $(0,\infty)$.
• Eq. (7) (p. 2642): $\rho(X)=\min\{m\mid X-m\in\mathcal A_\rho\}$.
• Proposition 2 (p. 2642): $\rho$ is star-shaped iff $\mathcal A_\rho$ is star-shaped iff $\rho=\rho_{\mathcal A}$ for a star-shaped acceptance set $\mathcal A$.
• Theorem 1 (p. 2643), in four parts: the infimum, supremum, $\mu$-average and inf-convolution of star-shaped risk measures are star-shaped risk measures.
• Proposition 3 (p. 2642): for subadditive risk measures, star-shaped, positively homogeneous and convex coincide.
• Theorem 2, positively homogeneous case: the same equivalence with "positively homogeneous", "coherent risk measures" and "coherent acceptance sets".
• Corollary 1 (p. 2645): $\inf_{X\in\mathcal Y}\rho(X)=\inf_{\gamma\in\Gamma}\inf_{X\in\mathcal Y}\gamma(X)$ for any $\mathcal Y\subseteq\mathcal X$.

Significance

Theorem 2 identifies star-shaped risk measures as exactly the lower envelopes of convex risk measures. Consequences drawn in the paper: minimizing a star-shaped risk measure over a set of positions reduces to a family of convex risk-minimization problems (Corollary 1, Proposition 6), each convex risk measure in the envelope carries its dual representation (Proposition 5), and VaR-type measures inherit a tractable structure without being convex. The positively homogeneous case gives the analogous statement for VaR-like measures in terms of coherent ones, generalizing Föllmer–Schied Proposition 4.47.

The paper proves these results; the mission adds a machine-checked proof on a general space of bounded positions, with the attainment of every minimum made explicit. No formalization of star-shaped risk measures is known to exist. The platform mission Coherent Measures of Risk formalizes the Artzner et al. axioms on finitely many states with a gain convention; its definitions are not reused here. The definitions of this mission (risk measures on a space of bounded functions, acceptance sets, the aggregation operations) are reusable by any later development of monetary risk measures without a reference probability.

Difficulty

The equivalence (2)⇔(3) and the direction (2)⇒(1) reduce to closure properties of the class; the content is (1)⇒(2) together with the "Moreover" clause. The obvious first idea, taking the convex hull or convex envelope of $\rho$ or of $\mathcal A_\rho$, fails: the convex hull of $\mathcal A_\rho$ generates a convex risk measure below $\rho$, not above it, and a single convex risk measure cannot equal a non-convex $\rho$. What is needed is, for each position, a convex risk measure that dominates $\rho$ everywhere and touches it at that position, and it must be monotone, translation invariant and normalized, not merely a convex functional. Attainment of the minimum, rather than an infimum, is part of the claim.

Formalization scope

• $\mathcal X$ is any Submodule ℝ (Ω → ℝ) containing the constants whose elements are bounded, bundled as PositionSpace Ω. It is not specialised to all bounded functions, and no measurability or probability is imposed; positive values are losses.
• "min" is always IsLeast (attained). The acceptance-set axiom $\sup\{m\mid m\in\mathcal A\}=0$ is IsLUB, not sSup … = 0. $\rho_{\mathcal A}$ uses the real sInf, which is genuine for acceptance sets on bounded positions.
• Every $\gamma\in\Gamma$ is a full risk measure: monotone, translation invariant, normalized and convex. A representation of $\rho$ as a minimum of arbitrary, non-normalized convex functionals holds for every monotone translation-invariant map and is not this theorem; such a formalization is ruled out.
• The family in (3) is a set of subsets of $\mathcal X$, with no finiteness or nonemptiness assumption.
• A coherent acceptance set is convex and closed under multiplication by every $t>0$.
• Theorem 1 adds the hypotheses the page leaves implicit: a nonempty index set for supremum and infimum; the power-set σ-algebra and a countably additive probability measure for the average (the paper's proof also covers capacities with Choquet integrals, which are not stated here); $n\ge1$ and the normality condition (10) for the inf-convolution.
• Corollary 1 computes infima in the extended reals, so the set $\mathcal Y$ may be empty and the infima may be $-\infty$.

Contributions welcome: proofs of any milestone, and in particular general lemmas on risk measures on a space of bounded functions (the bounds $\inf X\le\rho(X)\le\sup X$, properties of $\rho_{\mathcal A}$, convexity of $\rho_{\mathcal A}$ for convex $\mathcal A$), which are reusable across risk-measure missions.

Selected references

• E. Castagnoli, G. Cattelan, F. Maccheroni, C. Tebaldi, R. Wang, Star-Shaped Risk Measures, Operations Research 70(5):2637–2654, 2022. https://doi.org/10.1287/opre.2022.2303
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072
• M. Frittelli, E. Rosazza Gianin, Putting order in risk measures, Journal of Banking & Finance 26(7):1473–1486, 2002. https://doi.org/10.1016/S0378-4266(02)00270-4
• H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, 4th ed., De Gruyter, 2016. https://doi.org/10.1515/9783110463453

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

Chunk 07a built the general theory of infinite-horizon Markov Decision Processes and its sharpest special case, contracting models, where Banach's fixed point theorem delivers existence, uniqueness, and an explicit convergence rate all at once. That theory answers "does an optimal policy exist, and can I compute it by iterating a fixed point equation?" This mission answers the two questions a practitioner asks next: what happens when the reward's negative part, rather than its positive part, is the one that needs controlling (positive models, §7.4), and — more strikingly — can finding an optimal policy be reduced to solving a genuine linear program, the single most heavily-optimized computational primitive in all of operations research (§7.5)?

Setting

A positive Markov Decision Model is the mirror image of chunk 07a's general setup: instead of bounding the reward's positive part with an upper bounding function, the negative part is bounded by an integrability quantity $\varepsilon$, and the roles of "largest subharmonic" and "smallest superharmonic" swap accordingly. The computational sections build on chunk 07a's contracting theory directly: Howard's policy improvement algorithm iteratively replaces a decision rule with a strict pointwise improvement; the linear-programming approach recasts the entire optimization problem — the value function and the optimal policy — as a primal/dual pair of linear programs, not over finite vectors but over an infinite-dimensional space of measurable functions ($v \in IM$) and finitely-additive-in-spirit measures ($\mu \in M_b$); and state-space discretization approximates an infinite (Borel) state space by a finite grid, with an explicit, computable bound on the resulting numerical error.

Formalization targets

The goal, Theorem 7.5.8 (Strong Duality), is the section's deepest result: under chunk 07a's contracting Structure Theorem's own hypotheses, the primal linear program $(P)$ is solved exactly by the true optimal value function $J_\infty$, the dual program $(D)$ is solved by the occupation measure of any optimal stationary policy, and the two optimal values coincide. The milestones build up to it in three groups: the positive-model mirror theory (Lemmas 7.4.1-7.4.2, Theorems 7.4.3 and 7.4.5); Howard's policy improvement and its termination guarantee (Theorem 7.5.1, Corollary 7.5.3); and the linear-programming machinery itself (weak duality, complementary slackness, and the finite-state specialization that recovers an ordinary finite linear program, Theorems 7.5.6, 7.5.7, 7.5.9) together with the discretization error bounds that make the whole theory numerically usable (Proposition 7.5.11, Theorem 7.5.12).

Significance

The strong duality theorem is genuinely new content relative to what is already on the platform: the existing finite-dimensional LP duality missions (SmaleNinth.lp_strong_duality, LinearOptimization.lp_general_weak_duality, and others in the linear-optimization field) all operate over $\mathbb R^n$-valued vectors, while this theorem's primal and dual variables are a measurable function on a general Borel space and a measure on a general Borel space respectively — an infinite-dimensional linear program in the fullest sense. Theorem 7.5.9, the finite-state specialization, is the one point of genuine hypothesis-for-hypothesis contact with that prior art (checked directly; see STATUS.md for why it was drafted fresh rather than cited as a reference item), and it is exactly there that the reduction to an ordinary finite LP — with the platform's familiar vertex/extreme-point vocabulary — becomes visible.

Difficulty

Constructing the occupation measure $\mu^{f^\infty}_p$ without a canonical infinite-horizon path measure is the central technical challenge: it must be a genuine Measure (E × A), not merely a real-valued functional, since the dual program optimizes over a space of such measures. This mission builds it from iterated Measure.bind (pushing the initial law $p$ forward through the model's kernel under a fixed stationary decision rule) combined with a countable Measure.sum of $\beta^k$-scaled terms — a construction that stays entirely within Mathlib's existing measure-theoretic vocabulary without needing an Ionescu–Tulcea-style infinite product. A second, different difficulty is the state-space discretization section's grid interpolation, which presupposes a convex-combination structure ($x = \sum_k\lambda_kx_k$ for grid points $x_k$) on the state space that a general Borel space does not carry; this mission represents the grid operator and grid bounding function as data satisfying exactly the structural properties their two target theorems' own proofs use, rather than reconstructing the literal interpolation scheme — a deliberate, documented scope decision (see MODERATION_NOTES.md), not an approximation of either theorem's mathematical content.

Formalization scope

Every operator and value-function construction restates chunk 07a's own vocabulary (per this series' file-ownership convention, an independent copy in this chunk's own namespace), extended by the positive-model integrability bound $\varepsilon$, the occupation-measure/linear-program apparatus of §7.5.2, and the grid-approximation data of §7.5.3. The primal/dual optimal values $\mathrm{val}(P)$/$\mathrm{val}(D)$ are kept EReal-valued rather than real-valued specifically so that Theorem 7.5.6's own finiteness claims ($-\infty < \mathrm{val}(D)$, $\mathrm{val}(P) < \infty$) remain genuine, checkable content rather than being trivialized by a real-valued sInf/sSup's always-finite convention. Theorem 7.5.9's "optimal vertex" is stated via an explicit convex-combination (extreme-point) characterization using ENNReal weights, since Measure does not carry the module structure Mathlib's own Set.extremePoints requires.

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.
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960 (the policy improvement algorithm this section names after him).
• E. V. Denardo, "On linear programming in a Markov decision problem," Management Science, 1970 (the classical finite-state linear-programming formulation this section generalizes).
• W. J. Heilmann, "A note on the dual of a linear program with infinitely many constraints," cited by the book's own Remark 7.5.5 for the finitely-additive treatment the restricted dual $(D)$ over $M_b$ sidesteps.

Motivation

Shortest-path distances and network potentials are among the oldest objects in combinatorial optimization: a directed graph with arc lengths, its shortest-path distances, and the "feasible potentials" (vertex labels consistent with those lengths) underlie duality in min-cost flow, scheduling, and difference-constraint systems. Murota's Discrete Convex Analysis (SIAM, 2003) isolates the abstract structure behind these objects — distance functions satisfying the triangle inequality, and their associated sets of admissible potentials — and shows it is governed by exactly the same discrete-convexity machinery as submodular set functions: a one-to-one correspondence with a second family of well-behaved integer point sets, the L-convex sets. Where an M-convex set (chapter 4) is defined by an exchange axiom generalizing matroid base exchange, an L-convex set is defined by closure under coordinatewise lattice operations (∨, ∧) and translation by the all-ones vector — a genuinely different axiom system that nonetheless produces a parallel structural theory: hole-freeness, a polyhedral description via an induced distance function, and integral convexity.

Companion mission 05-lconvex-sets (Discrete Convex Analysis IV) covers this chapter's other half: the hole-free property (Theorem 5.2), the one-to-one correspondence between L-convex sets and integer-valued triangle-inequality distance functions (Theorem 5.5), the intersection properties (Theorem 5.7), and the chapter's discrete separation theorem (Theorem 5.9, its goal). This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the results the chapter leaves for its second half: the fundamental facts connecting a distance function to its admissible potentials (Proposition 5.1), the two-way polyhedral correspondence's supporting propositions (5.3-5.4), Minkowski-sum convexity (Theorem 5.8), and — this mission's goal — the explicit description of an L-convex set's convex hull that establishes its integral convexity (Theorem 5.10).

Setting

Fix a finite ground set $V$. A distance function is a map $\gamma : V \times V \to \mathbb R \cup \{+\infty\}$ with $\gamma(v,v) = 0$; it may take negative finite values and need not be symmetric. It defines a directed graph $G_\gamma = (V, A_\gamma)$ with $A_\gamma = \{(u,v) : \gamma(u,v) < +\infty\}$, arc $(u,v)$ having length $\gamma(u,v)$. Write $\bar\gamma(u,v)$ for the shortest-path length from $u$ to $v$ in $G_\gamma$ ($+\infty$ if none exists); $\gamma$ is well defined ($\bar\gamma$ finite-valued wherever a path exists) exactly when $G_\gamma$ has no negative cycle. The triangle inequality $\gamma(v_1,v_2) + \gamma(v_2,v_3) \ge \gamma(v_1,v_3)$ defines the class $T[\mathbb R]$ (or $T[\mathbb Z]$ when integer-valued). A vector $p \in \mathbb R^V$ is an admissible potential of $\gamma$ if $p(v) - p(u) \le \gamma(u,v)$ for all $u \ne v$; write $D(\gamma)$ for the set of all such potentials.

A nonempty set $D \subseteq \mathbb Z^V$ is L-convex if it satisfies (SBS[Z]): $p, q \in D \implies p \vee q,\ p \wedge q \in D$ (coordinatewise max/min), and (TRS[Z]): $p \in D \implies p \pm \mathbf 1 \in D$. A set $S \subseteq \mathbb Z^V$ is integrally convex if every point of its convex hull $\overline S$ lies in the convex hull of $S$ restricted to that point's integral neighborhood $N(p) = \{y \in \mathbb Z^V : \lfloor p \rfloor \le y \le \lceil p \rceil\text{ coordinatewise}\}$ — a strong, local form of "no holes" saying every real point of the hull is explained by nearby integer points alone.

Formalization targets

Goal: integral convexity of L-convex sets

For an L-convex set $D \subseteq \mathbb Z^V$, writing $a = p - \lfloor p \rfloor$ for the fractional part of $p \in \mathbb R^V$, $\alpha_1 > \cdots > \alpha_m$ for the distinct nonzero values of $a$, and $U_i(p) = \{v : a(v) \ge \alpha_i\}$ (with $U_0 = \emptyset$):

$$\overline D = \{p \in \mathbb R^V : \lfloor p \rfloor + \chi_{U_i(p)} \in D\ \ (i = 0, 1, \ldots, m)\}, \qquad \text{hence } D \text{ is integrally convex}.$$

This is the weakest stable form available: it exhibits an explicit, finite set of at most $|V|+1$ integer witnesses for every point of the hull, which is what "integrally convex" asserts abstractly, rather than a numerical bound that a sharper construction could later shrink.

Supporting structural targets

Four further results build the correspondence this goal uses: the basic duality between a distance function's admissible potentials, its shortest-path closure, and negative-cycle freedom (Prop. 5.1); the induced-distance-function construction recovering a triangle-inequality distance function from any integer point set, and the convex hull of an L-convex set as its associated polyhedron (Prop. 5.3); the converse construction recovering an L-convex set from an integer-valued distance function (Prop. 5.4); and convexity in Minkowski sum (Thm. 5.8).

Significance

Theorem 5.10 is what makes "L-convex" a genuinely convex-analytic notion rather than a combinatorial curiosity: it shows the convex hull of an L-convex set is not merely a polyhedron (already known from the chapter's polyhedral-description results) but one with the strongest local integrality property discrete convex analysis considers, integral convexity — every real point's hull membership is certified by a small, explicitly constructed set of nearby lattice points, uniformly across the whole set. This is the L-convex counterpart of the corresponding M-convex fact (chapter 4's Theorem 4.24) and is used later in the book wherever L-convex functions (chapter 7) need their epigraphs' local structure. Proposition 5.1 is the combinatorial engine underneath: it is exactly the LP-duality statement between shortest paths and feasible potentials that appears, in various guises, throughout network flow theory, made precise here as the base case the L-convex correspondence rests on.

None of these results are open — Murota presents them as, in his own words, "fundamental facts well known in network flow theory" (Proposition 5.1) systematized into the discrete convex analysis framework. What this mission contributes is a faithful, machine-checked formal statement of each, in the shared Lean vocabulary (LConvexSet, AdmissiblePotentials, ShortestDist) the rest of the Discrete Convex Analysis series can build on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The shortest-path closure $\bar\gamma$ is not a bookkeeping convenience but genuinely graph-theoretic content: proving Proposition 5.1 requires constructing an admissible potential from a shortest-path labeling and, conversely, deriving the negative-cycle-freeness of $G_\gamma$ from the mere existence of one admissible potential — a min-cost-flow-style LP duality argument, not a direct combinatorial check. Theorem 5.10's difficulty sits in a different place: the naive approach to "$D$ is integrally convex" would attempt an inductive argument peeling off one coordinate at a time, but the actual proof constructs a single, uniform family of $m+1$ witness points from the sorted fractional values of $p$ — a Carathéodory-style representation (Eq. (5.11)) that must simultaneously stay inside the integral neighborhood $N(p)$ and land in $D$ itself via the triangle inequality of $D$'s induced distance function, a construction with no one-coordinate-at-a-time shortcut.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; L-convex sets are Set (V → ℤ); distance functions are V → V → WithTop ℝ; admissible-potential sets are Set (V → ℝ). The shortest-path closure is formalized directly from finite walks (Fin (k+1) → V) rather than via a graph-library shortest-path predicate, matching the book's own construction. The Eq. (5.11) witnesses are built exactly as the book describes them — sorted distinct nonzero fractional values and their level sets — mirroring the Lovász-extension construction of the companion mission 20-ch04b-mconvexsets. No numeric constants are hard-coded anywhere in this mission (rule 7 is vacuous). The goal's explicit witness set (at most $|V|+1$ points) is not a trivializing special case: it holds for every L-convex set and every point of its hull, with no extra hypothesis narrowing the class. This mission's definitions (LConvexSet, AdmissiblePotentials, DistanceFunction, IsIntegrallyConvex) are redeclared from chunk 05-lconvex-sets (and, for IsIntegrallyConvex/IntegralNeighborhood, from chapter 3's own definitions) rather than imported, since sibling drafts in this series cannot yet reference one another; a later, published version of this book's namespace should consolidate them. Contributions completing any of the five sorrys are welcome; Proposition 5.1's LP-duality argument and the goal's Carathéodory-style construction are the two with the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• A. J. Hoffman, "On abstract dual linear programs," Naval Research Logistics Quarterly, 10 (1963), pp. 369-373 (feasible-potential duality in network flow theory).

Motivation

Submodular set functions are the combinatorial stand-in for convexity: a function $\rho : 2^V \to \mathbb R$ on the subsets of a finite ground set $V$ is submodular if $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$, and this single diminishing-returns inequality drives an enormous range of combinatorial optimization — matroid rank functions, graph cut capacities, entropy, coverage functions, and the max-flow min-cut theorem all arise as special or dual cases (Edmonds 1970; Lovász 1983; Fujishige 2005). M-convex sets are the "vector" incarnation of the same idea: subsets $B$ of $\mathbb Z^V$ satisfying an exchange axiom that generalizes the basis-exchange property of matroids to sets of integer points lying on a common hyperplane. Murota's Discrete Convex Analysis (SIAM, 2003) develops both sides of this correspondence and proves they coincide exactly: M-convex sets are precisely the integer points of the base polyhedra of integer-valued submodular functions. This mission covers the second half of that development — the structural theory (integrality, holes, Minkowski sums) that turns the correspondence into a working calculus, and its capstone, a discrete separation theorem for two disjoint M-convex sets whose separating hyperplane is forced to have $\{0,1\}$- or $\{0,-1\}$-valued coefficients.

Companion mission 04-mconvex-sets (Discrete Convex Analysis III) covers the same chapter's foundational results: the equivalence of the exchange-axiom variants, the one-to-one correspondence between M-convex sets and integer submodular functions (Theorem 4.15), Edmonds's intersection theorem (Theorem 4.18), and Frank's discrete separation theorem for submodular/ supermodular pairs (Theorem 4.17). This mission builds on that vocabulary (redeclared here, since draft missions in the same series cannot yet import one another) and proves the results the chapter leaves for its second half.

Setting

Fix a finite ground set $V$. A vector $x \in \mathbb Z^V$ assigns an integer $x(v)$ to each $v \in V$; write $x(X) = \sum_{v \in X} x(v)$ for $X \subseteq V$. For $x, y \in \mathbb Z^V$, the positive support $\operatorname{supp}^+(x-y) = \{v : x(v) > y(v)\}$ and negative support $\operatorname{supp}^-(x-y) = \{v : x(v) < y(v)\}$ record where $x$ exceeds, and falls short of, $y$. A nonempty set $B \subseteq \mathbb Z^V$ is M-convex if it satisfies the exchange axiom (B-EXC[Z]): for all $x, y \in B$ and $u \in \operatorname{supp}^+(x-y)$, some $v \in \operatorname{supp}^-(x-y)$ has both $x - \chi_u + \chi_v \in B$ and $y + \chi_u - \chi_v \in B$, where $\chi_u$ is the characteristic vector of $u$.

A set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ with $\rho(\emptyset) = 0$ and $\rho(V) < +\infty$ is submodular (the class $S[\mathbb R]$, or $S[\mathbb Z]$ when integer-valued) if $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$ for all $X, Y$. Its base polyhedron is $B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ (\forall X),\ x(V) = \rho(V)\}$. The Lovász extension $\hat\rho : \mathbb R^V \to \mathbb R \cup \{\pm\infty\}$ linearly interpolates $\rho$ off $\{0,1\}^V$: sorting the distinct values of $p \in \mathbb R^V$ as $\hat p_1 > \cdots > \hat p_m$ and setting $U_i = \{v : p(v) \ge \hat p_i\}$, it is $\hat\rho(p) = \sum_{i=1}^{m-1}(\hat p_i - \hat p_{i+1})\rho(U_i) + \hat p_m \rho(U_m)$.

Formalization targets

Goal: discrete separation for M-convex sets

$$B_1 \cap B_2 = \emptyset \implies \exists\, p^* \in \{0,1\}^V \cup \{0,-1\}^V,\quad \inf_{x \in B_1}\langle p^*, x\rangle - \sup_{x \in B_2}\langle p^*, x\rangle \ge 1,$$

for M-convex sets $B_1, B_2 \subseteq \mathbb Z^V$ (Theorem 4.21). This is the weakest stable form of the result — it asserts only the existence of a combinatorially special separator, not any bound tied to $|V|$ or a particular construction, so it is not invalidated by a sharper algorithm for finding $p^*$.

Supporting structural targets

Eleven further results build the calculus this goal rests on: the hyperplane property of M-convex sets (Prop. 4.1), an equivalent one-sided exchange axiom (Prop. 4.2), nonemptiness and the support-function identity for $B(\rho)$ (Props. 4.4-4.5), integrality of $B(\rho)$ for integer-valued $\rho$ (Prop. 4.6), the hole-free property identifying an M-convex set with the integer points of its own convex hull (Thm. 4.12), the two-way polyhedral description of M-convex sets via induced submodular functions (Props. 4.13-4.14), the equivalence of submodularity with convexity of the Lovász extension (Thm. 4.16, due to Lovász), integrality of the intersection of M-convex sets (Thm. 4.22), and Minkowski-sum identities for base polyhedra and M-convex sets (Thm. 4.23).

Significance

The discrete separation theorem is what makes M-convexity discrete rather than merely a polyhedral fact: ordinary separation of two disjoint convex sets by a hyperplane is classical, but here the separator is forced into $\{0,1\}^V \cup \{0,-1\}^V$ — a purely combinatorial object — with no loss of strength. This is the mechanism behind integrality results across combinatorial optimization (e.g., that the intersection of two integral base polyhedra is integral, Theorem 4.22, used pervasively in matroid intersection and submodular flow algorithms). The structural results (holes, Minkowski sums, the Lovász-extension convexity equivalence) are the working toolkit every later use of M-convexity in the book — proximity theorems for M-convex functions (chunks 06+), the discrete conjugacy theorem, submodular flows — draws on without restating.

None of these results are open: Murota attributes the exchange-axiom theory to the matroid and submodular-function literature it systematizes, citing Edmonds, Frank, and Lovász by name for the specific theorems. What this mission produces is a machine-checked formal statement of each result exactly as the book states it, in a shared Lean vocabulary (ExchangeAxiomB, BasePolyhedron, LovaszExtension) that the rest of the Discrete Convex Analysis series builds on; no result here has a prior formalization on the platform (see Formalization scope).

Difficulty

The separation theorem is not proved by convex separation directly — the whole point is that the naive proof (apply the ordinary hyperplane separation theorem to the convex hulls of $B_1, B_2$, then argue the separator can be taken $\{0,1\}$-valued) does not go through, because convex separation alone gives no control over the separator's coefficients. The book instead derives it from Edmonds's intersection theorem (Theorem 4.18, chunk 04-mconvex-sets) applied to a submodular/supermodular pair built from $B_1, B_2$'s associated set functions (Theorem 4.15), routed through Frank's discrete separation theorem (Theorem 4.17) — a genuine two-step reduction, not a direct argument. A second, independent difficulty sits in the supporting results: the hole-free property (Theorem 4.12) requires an explicit induction reducing an arbitrary convex combination representing an integer point to a single element of $B$, a combinatorial exchange argument with no shortcut through general polyhedral theory.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; M-convex sets are Set (V → ℤ); submodular/supermodular functions are Finset V → WithTop ℝ / WithBot ℝ; base polyhedra are Set (V → ℝ). The Lovász extension is formalized directly from the book's own sorted-values construction (SortedValues, LevelSet, Eq. (4.4)-(4.6)), not via an equivalent closed form. Since WithTop ℝ carries no Module ℝ structure, convexity for Theorem 4.16 is stated via a bespoke nonnegative-scalar action (ScalarWithTop) rather than Mathlib's ConvexOn — this changes no mathematical content, only its packaging (see MODERATION_NOTES.md). No numeric constants are hard-coded anywhere in this mission (rule 7 is vacuous). The goal's hypothesis (ExchangeAxiomB plus Nonempty on each $B_i$) is exactly the book's own definition of M-convexity — no weaker substitute (e.g. requiring a specific $\rho$ witness in the hypothesis rather than deriving one, or dropping the $\{0,1\}/\{0,-1\}$ constraint on $p^*$ in favor of a generic separator) would be faithful, and both trivializations are ruled out by construction. This mission's definitions (ExchangeAxiomB, BasePolyhedron, SubmodularSetFunction, LovaszExtension) are redeclared from chunk 04-mconvex-sets rather than imported, since sibling drafts in this series cannot yet reference one another; a later, published version of this book's namespace should consolidate them. Contributions completing any of the twelve sorrys are welcome; the hole-free property (Theorem 4.12) and the goal are the two with the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• J. Edmonds, "Submodular functions, matroids, and certain polyhedra," in Combinatorial Structures and Their Applications, 1970, pp. 69-87.
• A. Frank, "An algorithm for submodular functions on graphs," Annals of Discrete Mathematics, 16 (1982), pp. 97-120.
• L. Lovász, "Submodular functions and convexity," in Mathematical Programming: The State of the Art, Springer, 1983, pp. 235-257.

Motivation

A classical convex function's global minimality is equivalent to its local minimality — the single fact that makes convex optimization tractable, since checking a small neighborhood suffices to certify a global guarantee. The discrete analogue is not automatic: a function on the integer lattice can fail to have any well-behaved "local" notion at all, and even when a discrete convexity-like property is imposed, the naive candidate (a function's values agreeing with its own convex-hull interpolation) does not by itself guarantee that local optimality implies global optimality. Murota's Discrete Convex Analysis (SIAM, 2003) isolates exactly the extra condition — integral convexity — that restores this guarantee, and shows it is general enough to contain every other discrete convexity notion the book studies (M-convex, L-convex, and their variants), making it the common ancestor of the book's entire hierarchy of classes. This mission completes the chapter's account of integral convexity: how it behaves under sums, restrictions, and linear perturbations, how it transfers between a function and its domain or minimizer sets, and a companion fact about hole-freeness under intersection and Minkowski sums that motivates why integral convexity, not mere hole-freeness, is the right notion to use.

Setting

For $f : \mathbb Z^n \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain $\operatorname{dom}_{\mathbb Z} f$, the convex closure is $\bar f(x) = \sup_{p,\alpha} \{\langle p,x\rangle + \alpha : \langle p,y\rangle+\alpha \le f(y)\ \forall y \in \mathbb Z^n\}$. The integral neighborhood of $x \in \mathbb R^n$ is $N(x) = \{y \in \mathbb Z^n : \lfloor x_i \rfloor \le y_i \le \lceil x_i \rceil\}$, and the local convex extension $\tilde f$ replaces "for all $y \in \mathbb Z^n$" in $\bar f$'s definition with "for all $y \in N(x)$". A function is integrally convex if $\tilde f = \bar f$ everywhere on $\mathbb R^n$. A set $S \subseteq \mathbb Z^n$ is integrally convex if its indicator function is; it is hole free if $S = \bar S \cap \mathbb Z^n$, where $\bar S$ is the real convex hull of $S$. The discrete Minkowski sum is $S_1+S_2 = \{x_1+x_2 : x_1 \in S_1, x_2 \in S_2\}$. A function is separable convex if $f(x) = \sum_i f_i(x(i))$ for univariate functions $f_i$ satisfying the discrete convexity inequality $f_i(t-1)+f_i(t+1) \ge 2f_i(t)$. For $p \in \mathbb R^n$, $f[-p] (x) = f(x) - \langle p,x \rangle$ and $\arg\min f[-p]$ is its minimizer set.

Formalization targets

Goal (Theorem 3.29). For $f$ with nonempty bounded effective domain,

$$f \text{ is integrally convex} \iff \arg\min f[-p] \text{ is an integrally convex set for every } p \in \mathbb R^n.$$

This leaves the characterization at the level of the two named properties (integral convexity of the function versus of every minimizer set), the strongest statement of this kind that holds without extra hypotheses beyond boundedness of the domain.

Supporting milestones. Proposition 3.17 (four basic containment/equality relations between hole-free sets' intersections, Minkowski sums, and their real closures); Proposition 3.22 (for a periodic integrally convex function, global optimality reduces to a one-sided local check); Proposition 3.24 (an integrally convex function plus a separable convex function is integrally convex); Proposition 3.25 (separable convex functions are integrally convex, and integral convexity survives linear perturbation); Proposition 3.26 (an integrally convex set is hole free); Proposition 3.28 (the effective domain and every minimizer set of an integrally convex function are integrally convex sets — the forward direction of the goal); and Proposition 3.30 (for integer-valued integrally convex functions, a finite infimum is always attained).

Significance

Theorem 3.29 turns a statement about a function on all of $\mathbb R^n$ (integral convexity, a condition on $\tilde f$ and $\bar f$ that is a priori about uncountably many points) into a statement about a countable family of discrete sets (the minimizer sets $\arg\min f[-p]$), giving a genuinely different and often more tractable way to certify or refute integral convexity. Propositions 3.24–3.25 are the closure properties that make integral convexity useful in practice: without them, verifying integral convexity of a function built from simpler pieces (a sum with a separable cost, a linearly reweighted objective) would require re-deriving the property from scratch each time. Proposition 3.17, by contrast, is a cautionary result: Note 3.27 and Example 3.15 (the two hole-free sets whose Minkowski sum has a hole) show that hole-freeness alone does not inherit good behavior under set operations, which is exactly the gap integral convexity's stronger, locally-checkable condition is built to close — this mission's Proposition 3.17 documents the "obvious"/general-purpose relations that hold regardless, so that the reader can see precisely which inclusion is automatic and which requires more.

Difficulty

The naive approach to Theorem 3.29's converse direction (integral convexity of every minimizer set implies integral convexity of $f$) tries to check $\tilde f(x) = \bar f(x)$ directly at an arbitrary $x \in \operatorname{dom} f$; this is circular, since $\tilde f$ and $\bar f$ are themselves defined via suprema over affine minorants, not via minimizer sets. The book's actual proof instead sets up a primal-dual pair of linear programs whose optimal solutions witness $\bar f(x)$ and $\tilde f(x)$ respectively, uses LP duality's complementary slackness to show the dual optimal solution can be chosen supported inside $N(x)$, and only then concludes $\tilde f(x) = \bar f(x)$ — routing the entire argument through the integral convexity of the specific minimizer set $S = \arg\min f[-p^*]$ at the optimal dual price $p^*$. This is why Theorem 3.29's proof needs LP duality (Theorem 3.10, formalized in the previous mission in this series) as an ingredient, not just the closure-property machinery of Propositions 3.24–3.28.

Formalization scope

All apparatus (ConvexClosure, IntegralNeighborhood, LocalConvexExtension, IntegrallyConvex, ArgMinPerturbed, HoleFree, IntegrallyConvexSet, SeparableConvex, MinkowskiSumZ) is redeclared fresh in DiscreteConvex.IntegralConvexityC, mirroring chunk 03-integral-convexity's already-established constructions (Fin n-indexed, WithTop ℝ-valued functions, EReal-valued convex closures via sSup), since a draft mission cannot import another draft's definitions. IntegrallyConvexSet is defined via the book's own primary definition (indicator function integrally convex) rather than either of its two stated equivalent reformulations, since no result in this mission needs those forms as a named predicate. An integer-valued function (Proposition 3.30) is represented as Zⁿ → WithTop ℤ and cast to WithTop ℝ via a small casting map wherever the real-valued apparatus is needed — a faithful embedding. Boundedness of a discrete set is containment in a finite integer interval. The formalization does not trivialize: Theorem 3.29's hypothesis is exactly "nonempty bounded effective domain", not further restricted to, say, a fixed small dimension or a finite ground set with a fixed cardinality bound, and every milestone is stated at the same generality as Propositions 3.24–3.28 and 3.30 give it (arbitrary $n$, arbitrary integrally convex function). Infrastructure needed beyond Mathlib: all definitions are fresh; a contribution completing any milestone, or the LP-duality-based proof of Theorem 3.29's converse direction, would be a natural entry point, alongside chunk 03's Theorem 3.21 as background.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 3.
• K. Murota, A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research 24 (1999), 95–105 (Lemma 6.13, cited for Proposition 3.30).

Motivation

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

Setting

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

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

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

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

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

Formalization targets

Goal — Theorem 4.6.6 (the mean-variance problem)

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

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

Supporting milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

In economics, a pair of goods are substitutes if raising the price of one increases demand for the other, and complements if it decreases it; formally, a utility or value function is submodular in the substitutes case and supermodular in the complements case. A natural question is which of these two regimes a given optimization problem's value function falls into, and whether the answer depends on the underlying combinatorial structure of the problem rather than being a coincidence of the particular numbers involved. Murota's Discrete Convex Analysis (SIAM, 2003) answers this question for the maximum-weight circulation problem in a directed network: the value function is submodular in some coordinates and supermodular in others, purely as a consequence of a graph-theoretic distinction — whether the arcs involved are parallel or series — and this chapter shows the distinction is explained precisely by the dual pair of discrete convexity notions (L-natural-convexity and M-natural-convexity) developed elsewhere in the book. This mission also completes the quadratic-forms thread the previous mission in this series (Discrete Convex Analysis XV) began, by formalizing its natural generalization to functions that may take the value $+\infty$.

Setting

Let $G=(V,A)$ be a directed graph with vertex set $V$ and arc set $A$; write $\partial^+a$, $\partial^-a$ for the initial and terminal vertex of arc $a$. For a flow $\xi:A\to\mathbb R$, its boundary is $\partial\xi(v)=\sum_{a:\partial^+a=v}\xi(a)-\sum_{a:\partial^-a=v}\xi(a)$, the net flow leaving $v$. Given a capacity $c:A\to\mathbb R_{\ge0}$, $\xi$ is a feasible circulation for $c$ if $0\le\xi(a)\le c(a)$ for every arc and $\partial\xi(v)=0$ for every vertex. For a weight $w:A\to\mathbb R$, $F(w,c)=\max\{\langle w,\xi\rangle : \xi\text{ feasible for }c\}$ is the maximum-weight circulation value, and $\xi$ is optimal for $w$ (with capacity $c$) if it is feasible and attains this maximum. A simple cycle is an alternating sequence of pairwise distinct vertices $v_0,\dots,v_{k-1}$ and arcs $a_1,\dots,a_k$ with $\{\partial^+a_i,\partial^-a_i\}=\{v_{i-1},v_i\}$ (indices mod $k$) and $v_0=v_k$. Two arcs are parallel if every simple cycle containing both of them orients them oppositely, and series if every such cycle orients them the same way; a set of arcs is parallel (series) if its arcs are pairwise parallel (series). A circuit is a $\{0,\pm1\}$-valued $\pi:A\to\mathbb R$ with $\partial\pi=0$ whose support forms a simple cycle. For $x\in\mathbb R^n$, $\operatorname{supp}^+(x)=\{i:x_i>0\}$, $\operatorname{supp}^-(x)=\{i:x_i<0\}$. A function $g:\mathbb R^n\to\mathbb R$ is submodular if $g(p)+g(q)\ge g(p\vee q)+g(p\wedge q)$, supermodular with the reverse inequality, and has translation submodularity (is L-natural-convex) if the stronger inequality $g(p)+g(q)\ge g((p-\alpha\mathbf1)\vee q)+g(p\wedge(q+\alpha\mathbf1))$ holds for every $\alpha\ge0$. A function $f$ has the M-natural exchange property (is M-natural-convex) if for $i\in\operatorname{supp}^+(x-y)$ there exist $j\in \operatorname{supp}^-(x-y)\cup\{0\}$ and $\alpha_0>0$ with $f(x)+f(y)\ge f(x-\alpha(\chi_i-\chi_j))+f(y+\alpha(\chi_i-\chi_j))$ for $\alpha\in[0,\alpha_0]$; a function is M-natural-concave or L-natural-concave if its negation is M-natural- or L-natural-convex.

Formalization targets

Goal (Theorem 2.23). For $P$ a parallel arc set and $S$ a series arc set,

$$F\text{ is L-natural-convex in }w_P\text{ and M-natural-concave in }c_P,$$ $$F\text{ is M-natural-convex in }w_S\text{ and L-natural-concave in }c_S,$$

where $w_P$, $c_P$ denote $F$'s dependence on the coordinates of $w$, $c$ indexed by $P$ (resp. $S$) with the remaining coordinates held fixed. This is the mission's capstone: it upgrades the plain submodularity/supermodularity split of Theorem 2.22 to the sharper pair of combinatorial convexity classes that explains it.

Supporting milestones. Proposition 2.21 (the classical fact that $F$ is convex in $w$ and concave in $c$, with no combinatorial content — the baseline against which Theorem 2.23's sharper claim is measured); Theorem 2.16 (the general, possibly-$+\infty$-valued extension of the quadratic-form conjugacy from Discrete Convex Analysis XV's Theorem 2.11, to functions restricted to a linear subspace); Theorem 2.22 (plain submodularity/supermodularity of $F$ in $w_P,c_P$ and $w_S,c_S$, the result Theorem 2.23 strengthens); and Propositions 2.24–2.28 (the graph-theoretic lemmas — sparse intersection of a circuit's support with a parallel or series arc set, merging two circuits along a series set, and three existence statements for optimality-preserving perturbations — that the book's own proof of Theorem 2.23 is built from).

Significance

Theorem 2.23 gives a structural explanation, rather than a case-by-case verification, for a phenomenon well known in network flow theory: that convexity/concavity and submodularity/supermodularity are independent properties, appearing in all four combinations depending on which side of the problem (weights or capacities) and which graph-theoretic role (parallel or series) is varied. Without it, (2.55)'s four combinations would be four separate facts with no common cause; with it, they are corollaries of two applications of a single pair of dual discrete-convexity notions, the same notions the book uses throughout to unify matroid theory, submodular optimization, and convex analysis. Formalizing this mission produces, so far as a platform search shows, the first Lean statement of a combinatorial-convexity classification result for a network optimization value function, together with the graph-theoretic vocabulary (simple cycles, parallel/series arcs, circuits) needed to state it — infrastructure with no prior formalized counterpart on the platform that a later mission on network flows or matroid union could reuse.

Difficulty

The naive approach to Theorem 2.23 tries to verify translation submodularity or the exchange property directly from the linear-programming definition of $F$ as a maximum over a polytope, treating $w_P\mapsto F(w,c)$ as an abstract convex-piecewise-linear function; this loses the graph structure entirely and gives at best the plain submodularity of Theorem 2.22, not the sharper L-natural/M-natural classification, because submodularity alone does not distinguish a combinatorially meaningful discrete convexity from an arbitrary submodular function. The book's actual route instead works with explicit optimal circulations for the two perturbed weight vectors and reconstructs a feasible pair achieving the target inequality by rerouting flow along a circuit — and the existence of a usable circuit (one that touches the perturbed arcs in a way compatible with the parallel or series structure) is exactly what Propositions 2.24–2.28 supply via the conformal decomposition of a difference of two circulations into elementary circuits. This is why those five propositions, although individually narrow existence lemmas, are included as milestones: they are the load-bearing combinatorial content the naive convex-analytic argument cannot reach.

Formalization scope

The graph is {V A : Type*} with src dst : A → V rather than a bundled structure, matching the book's own $\partial^+,\partial^-$ notation directly. $F(w,c)$ is a real sSup over feasible circulations' weights (existence of a maximizer is not asserted, since no proof is attempted this pass); IsOptimalCirc is a separate, directly-stated primitive for "$\xi$ is optimal for $w$", matching the book's own working vocabulary in the propositions that need it. A simple cycle is formalized as an injective cyclically-indexed vertex sequence together with a matching arc sequence, exactly as the book's own footnote defines it; parallel and series arcs are defined by quantifying over every such representation of every simple cycle containing the two arcs, which is checked to be independent of which of a cycle's two traversal directions or starting vertex is chosen. Viewing $F$ as a function of $w_P$ alone extends a partial vector by a fixed background vector on the complement of $P$, the same partial-application device the book uses informally. M-natural- and L-natural-concavity are recorded as the corresponding convexity property of the negated function, the standard convention. The formalization does not trivialize: parallel and series arc sets are genuine graph-theoretic hypotheses (not, e.g., specialized to $|P|=1$ or a graph with no simple cycles, which would make the parallel/series distinction vacuous), and Theorem 2.23's four conclusions are stated with the same combinatorial-convexity predicates (TranslationSubmodular, MNatExchangeR) used for the book's sharpest discrete convexity classes, not weakened to plain submodularity/supermodularity. Theorem 2.16 additionally needs Set (V → ℝ)-valued subspaces K, H (following the book's own set-builder notation for ker M and X⊥ rather than bundling them as Mathlib Submodules) and a WithTop ℝ-valued Legendre- Fenchel conjugate. Infrastructure needed beyond Mathlib: all graph, circulation, and combinatorial-convexity vocabulary is defined fresh in DiscreteConvex.CombinatorialC; a contribution proving any of the five graph-theoretic lemmas (Propositions 2.24–2.28) or the convex/concave halves of Proposition 2.21 independently would be a natural entry point.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 2.
• K. Murota, A. Shioura, "Conjugacy relationship between M-convex and L-convex functions in continuous variables," Mathematical Programming 101 (2004), 415–433.
• R. T. Rockafellar, Network Flows and Monotropic Optimization, Wiley, 1984.

Motivation

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

Setting

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

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

Formalization targets

Goal — Theorem 2.4.22 (the convex structure theorem)

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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