Probability

Motivation

Chapters 2 and 3 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (Cambridge University Press, 2014, doi:10.1017/CBO9781107298019), set up the framework in which the whole book asks what learning is. A learner sees a sample drawn independently from an unknown distribution over examples, chooses a hypothesis from a class fixed in advance, and is judged by its risk, the expected loss on a fresh example. The natural rule is Empirical Risk Minimization: pick a hypothesis that does best on the sample. Chapter 2 shows that ERM over an unrestricted class overfits, that restricting the class is what makes learning possible, and that a finite class never overfits once the sample is larger than $\log(|H|/\delta)/\epsilon$ (Corollary 2.3). Chapter 3 turns this into a definition, Probably Approximately Correct learnability with its sample-complexity function $m_H(\epsilon, \delta)$, restates the finite-class result as Corollary 3.2, and then generalizes in two directions that the rest of the book lives in: the agnostic model, in which no hypothesis need be perfect and the learner competes with the best hypothesis in the class, and general loss functions, which cover regression, multiclass prediction and unsupervised tasks. Chapter 4 adds the notion of an ε-representative sample and of uniform convergence, the tool by which the finite-class result extends to the agnostic case; its definitions are included here since they complete the framework.

Setting

A domain $Z$ of examples, a class $H$ of hypotheses and a loss $\ell : H \times Z \to \mathbb{R}$. The risk of $h$ under a distribution $D$ is $L_D(h) = \mathbb{E}_{z \sim D}\,\ell(h, z)$ and its empirical risk on $S = (z_1, \dots, z_m)$ is $L_S(h) = \frac1m\sum_i \ell(h, z_i)$; a sample is drawn i.i.d., $S \sim D^m$; an ERM hypothesis minimizes $L_S$ over $H$; a learning algorithm maps samples of each size to hypotheses. In binary classification the examples are $(x, f(x))$ with $x \sim D$ over $X$ and $f$ a labeling function, and the true error is $L_{(D,f)}(h) = D(\{x : h(x) \ne f(x)\})$; the realizability assumption says some $h^\star \in H$ has $L_{(D,f)}(h^\star) = 0$. $H$ is PAC learnable if some sample-complexity function $m_H$ and algorithm guarantee, for all $\epsilon, \delta \in (0,1)$, all $D$ and all realizable $f$, true error at most $\epsilon$ with probability at least $1 - \delta$ from $m \ge m_H(\epsilon, \delta)$ examples; agnostic PAC learnability with respect to a loss asks instead for $L_D(h) \le \min_{h' \in H} L_D(h') + \epsilon$ for every distribution over $Z$.

Formalization targets

Goal: Corollary 3.2

Every finite hypothesis class is PAC learnable with sample complexity

$$m_H(\epsilon, \delta) \le \Big\lceil \frac{\log(|H|/\delta)}{\epsilon} \Big\rceil,$$

by the ERM rule: for a nonempty finite class of measurable hypotheses there is an ERM learner satisfying the PAC guarantee with that sample-complexity function.

Milestone

Corollary 2.3: under realizability, with $m \ge \log(|H|/\delta)/\epsilon$ examples, every ERM hypothesis has true error at most $\epsilon$ with probability at least $1 - \delta$.

Significance

Corollaries 2.3 and 3.2 are the first learning theorem of the book and the template for all later sample-complexity bounds: a bad hypothesis is consistent with an i.i.d. sample with probability at most $(1 - \epsilon)^m \le e^{-\epsilon m}$, and a union bound over the class turns this into a guarantee that holds uniformly over all distributions and all realizable labelings. Everything that follows, uniform convergence for finite classes, the fundamental theorem for classes of finite VC dimension, structural risk minimization, replaces the count $|H|$ by a finer measure of the class's complexity but keeps the argument. None of this is machine-checked. The mission fixes on the platform the objects that the rest of the series uses without change: risks, empirical risks, the product law of a sample, the ERM relation, and the four learnability notions of Definitions 3.1, 3.4, 4.1 and 4.3.

Difficulty

The milestone needs that, for a fixed measurable hypothesis whose true error exceeds $\epsilon$, the product law gives the event "zero empirical risk" probability at most $(1-\epsilon)^m$; this is the product structure of Measure.pi on the event that each labeled example lies in the measurable set where the hypothesis agrees with $f$, followed by $1 - \epsilon \le e^{-\epsilon}$, the union bound over the finite class and the observation that under realizability every ERM hypothesis has zero empirical risk, so a bad ERM hypothesis is a consistent bad hypothesis. The goal packages this as a learner: existence of an ERM hypothesis for every sample (a finite nonempty class has a minimizer), and the arithmetic of the ceiling.

Formalization scope

The framework is the book's, with the risk as a Bochner integral, the sample law as a product measure, ERM as a relation and learners as deterministic functions of the sample; failure probabilities are stated as upper bounds on the outer measure of the failure set, the strong form of "with probability at least $1 - \delta$"; the comparison with $\min_{h' \in H} L_D(h')$ is written without an infimum. Sample-complexity functions are carried explicitly: the book's $m_H$ as the minimal such function is not defined, and "$m_H \le f$" is stated as "the learner satisfies the guarantee with the function $f$". Hypotheses and labeling functions are assumed measurable (Remark 3.1). The union bound (Lemma 2.2) is Mathlib's measure_union_le and is not an item. Hypotheses: $\epsilon > 0$, $\delta \in (0,1)$, $H$ finite (and nonempty for the learner to exist).

Trivializing readings are excluded: the milestone's failure event ranges over every ERM hypothesis, and the goal quantifies over all distributions, all realizable labelings and all $\epsilon, \delta$. Welcome contributions: the product-law bound for a fixed hypothesis and the union bound over a finset, which every later mission of the series reuses.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapters 2–4. doi:10.1017/CBO9781107298019
• L. G. Valiant, A theory of the learnable, Communications of the ACM 27(11), 1984. doi:10.1145/1968.1972
• V. N. Vapnik, The Nature of Statistical Learning Theory, Springer, 1995. doi:10.1007/978-1-4757-2440-0
• D. Haussler, Decision theoretic generalizations of the PAC model for neural net and other learning applications, Information and Computation 100(1), 1992. doi:10.1016/0890-5401(92)90010-D

Motivation

Chapter 2 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), gives a formal justification of Occam's Razor inside the PAC model. An Occam algorithm is judged not by the predictive power of its hypothesis but by how succinctly the hypothesis explains the sample before it: it must be consistent with the data and short, in the sense that its representation has fewer bits than the data it reproduces. The chapter's theorems say that, when the examples are drawn independently from a fixed distribution, such compression automatically yields prediction: a consistent hypothesis drawn from a small class is, with high probability, accurate on unseen examples. This turns the design of PAC learning algorithms into a combinatorial task, finding a short consistent hypothesis, and the chapter demonstrates the method three times: it shaves a logarithmic factor off the conjunction bound of Chapter 1, it learns conjunctions with few relevant variables through the greedy set-cover heuristic, and it learns Rivest's decision lists, a class strictly more expressive than $k$-CNF and $k$-DNF, by a greedy algorithm whose correctness is a one-line consequence of consistency.

Setting

The framework is that of Mission I: a measurable instance space, concepts as boolean functions, a target distribution $D$, the product law of a sample of $m$ labeled examples, the error $\mathrm{error}(h) = \Pr_{x \sim D}[h(x) \neq c(x)]$, and consistency of a hypothesis with a sample. Hypotheses may be represented by binary strings through a representation map, with size the bit length; an $(\alpha, \beta)$-Occam algorithm outputs a consistent hypothesis of size at most $(n \cdot \mathrm{size}(c))^\alpha m^\beta$ with $0 \le \beta < 1$. The set cover problem asks for a minimum subcollection of a collection $\mathcal{S}$ of subsets of a finite universe $U$ that covers $U$; the greedy heuristic repeatedly picks the set covering the most uncovered elements. A $k$-decision list is a sequence of conditions, each a conjunction of at most $k$ literals, with a bit attached to each and a default bit; it evaluates to the bit of the first satisfied condition. The greedy decision-list algorithm repeatedly finds a useful condition, one satisfied by some remaining examples all of which carry the same label, appends it with that label and removes those examples.

Formalization targets

Goal: Theorem 2.2 (Occam's Razor, cardinality version)

For a finite hypothesis class $H$, a target $c$, a distribution $D$ and $0 < \epsilon \le 1$, the probability that a sample of $m$ examples is consistent with some $h \in H$ of error greater than $\epsilon$ is at most $|H|(1 - \epsilon)^m$; hence

$$m \ge \frac{1}{\epsilon}\Big(\ln|H| + \ln\frac{1}{\delta}\Big)$$

makes this probability at most $\delta$, and any algorithm that outputs a consistent hypothesis from $H$ has error greater than $\epsilon$ with probability at most $|H|(1-\epsilon)^m$.

Milestones

Theorem 2.1 (an $(\alpha, \beta)$-Occam algorithm is a PAC algorithm, with explicit sample-size conditions in place of the constant $a$); the greedy set-cover bound of §2.3 ($|U_i| \le (1 - 1/\mathrm{opt})^i|U|$ and $\mathrm{opt}\ln|U|$ sets cover); the improved conjunction bound of §2.2; Theorem 2.3 ($k$-decision lists are PAC learnable by the greedy algorithm, which never fails and whose outputs are consistent).

Significance

Theorem 2.2 is the single most used tool of the subject: every finite-class sample bound, including the ones for conjunctions, decision lists, $k$-CNF and the discretized geometric classes, is an instance of it, and the Vapnik–Chervonenkis theory of Chapter 3 is its extension to infinite classes with the growth function in place of $|H|$. Theorem 2.1 is the philosophical statement, that succinct explanation implies prediction, and its converse (Exercise 2.3, and more strongly the boosting theorem of Chapter 4) makes Occam learning equivalent to PAC learning. The greedy set-cover bound is Chvátal's classical approximation guarantee, used in the book for learning with few relevant variables and again in later chapters. Theorem 2.3 is Rivest's result, and its proof exhibits the pattern "consistency by construction plus a counting bound" in its purest form. None of these is machine-checked. Their formalization gives the platform the union-bound-over-a-finite-class argument once and for all, in a form that the later missions of this series reuse verbatim.

Difficulty

Theorem 2.2 requires that, for a fixed measurable hypothesis with error greater than $\epsilon$, the product law gives the event "consistent with all $m$ examples" probability at most $(1 - \epsilon)^m$, which is the product structure of Measure.pi applied to the event that each coordinate lies in the set where $h$ agrees with $c$; the union bound over $H$ and the elementary inequality $(1 - \epsilon)^m \le e^{-\epsilon m}$ finish. Theorem 2.1 adds only the count of binary strings of length at most $K$ and arithmetic with real exponents. The set-cover bound is a discrete induction: an optimal cover of $U$ restricted to the uncovered elements has at most $\mathrm{opt}$ sets, so one of them, hence the greedy choice, covers a $1/\mathrm{opt}$ fraction; the covering clause needs the strict inequality $1 - 1/\mathrm{opt} < e^{-1/\mathrm{opt}}$. Theorem 2.3 needs that a run of the greedy algorithm never repeats a condition (its satisfied examples are removed), so outputs lie in an explicit finite class, that the first condition of the target list satisfied by a remaining example is useful, and that a complete run is consistent; the bound is then Theorem 2.2.

Formalization scope

Everything is in the sample-complexity sense on the Mission I framework; running time is not modelled and "efficient" is dropped from every statement, which is recorded in the natural-language statements. Theorem 2.2's constant $b$ is $1$ with natural logarithms; Theorem 2.1's constant $a$ is replaced by three explicit sufficient conditions. Hypotheses in the finite class are required to be measurable. The greedy heuristic and the greedy decision-list algorithm are relations (any tie-breaking), and the theorems quantify over every run; the decision-list theorem is stated for every $k$ with the $k$-conjunctions as conditions, so that its hypothesis is a $k$-decision list rather than the expansion the book sketches for $k > 1$. The conjunction count is $3^n + 1$, including the empty concept that the elimination algorithm outputs on a sample without positive examples. The few-relevant-variables algorithm of §2.3 is not stated (its bound has an unspecified constant and $m$ on both sides). Hypotheses: $0 < \epsilon \le 1$, $0 < \delta$ (and $\delta < 1$ where $\ln(1/\delta)$ must be nonnegative).

Trivializing readings are excluded: the bad-consistent event is over all of $H$, the decision-list failure event ranges over every possible output, and the set-cover bound holds for every greedy run. Welcome contributions: the product-law bound for a fixed hypothesis, the union bound over a finset, the string-counting lemma, and the no-repetition lemma for greedy runs.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 2. doi:10.7551/mitpress/3897.001.0001
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Occam's razor, Information Processing Letters 24(6), 1987. doi:10.1016/0020-0190(87)90114-1
• V. Chvátal, A greedy heuristic for the set-covering problem, Mathematics of Operations Research 4(3), 1979. doi:10.1287/moor.4.3.233
• R. L. Rivest, Learning decision lists, Machine Learning 2(3), 1987. doi:10.1007/BF00058680
• D. Haussler, Quantifying inductive bias: AI learning algorithms and Valiant's learning framework, Artificial Intelligence 36(2), 1988. doi:10.1016/0004-3702(88)90002-1

Motivation

Chapter 1 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), introduces Valiant's Probably Approximately Correct model, the framework for the whole book. A learner sees labeled examples of an unknown target concept drawn from an unknown but fixed distribution, and must output a hypothesis that, with probability at least $1 - \delta$ over the sample, misclassifies a fresh example with probability at most $\epsilon$; the model is distribution-free, and the hypothesis is judged on the same distribution it was trained on. The chapter's three positive results are the templates for everything that follows. The rectangle game (Theorem 1.1) shows that an infinite class can be learned from a finite sample by exploiting the geometry of the error region. Conjunctions (Theorem 1.2) are learned by the elimination algorithm, whose analysis, a union bound over "bad" literals, is the prototype of every sample-size bound in the book. And 3-CNF formulae (Theorem 1.4) are learned by a change of variables that reduces them to conjunctions, which, set against the intractability of learning 3-term DNF as 3-term DNF (Theorem 1.3), is the reason the final definition of the model lets the hypothesis class differ from the concept class.

Setting

The instance space is a measurable space $X$, a concept is a function $c : X \to \{0, 1\}$, and the target distribution $D$ is a probability measure on $X$. The error of a hypothesis $h$ is $\mathrm{error}(h) = \Pr_{x \sim D}[h(x) \ne c(x)]$. A sample of $m$ examples is $S = ((x_1, c(x_1)), \dots, (x_m, c(x_m)))$ with the $x_i$ independent draws from $D$; a learning algorithm is a function from samples to hypotheses; it has the $(\epsilon, \delta)$ guarantee on a class $C$ if for every $c \in C$ and every $D$ the probability that its hypothesis has error greater than $\epsilon$ is at most $\delta$; $C$ is PAC learnable using $H$ if for all $\epsilon, \delta \in (0, 1/2)$ some sample size and algorithm with hypotheses in $H$ achieve the guarantee. For $X = \{0,1\}^n$ a literal is a variable or its negation and a conjunction is a finite set of literals; the elimination algorithm starts from all $2n$ literals and deletes every literal contradicted by a positive example. For $X = \mathbb{R}^2$ the concepts are the closed axis-aligned rectangles and the tightest-fit algorithm returns the smallest rectangle containing the positive examples. A 3-CNF formula is a conjunction of clauses of at most three literals; the expansion $a \mapsto a'$ records for each triple $(u, v, w)$ of literals the value $u \vee v \vee w$.

Formalization targets

Goal: Theorem 1.2

Conjunctions of boolean literals are PAC learnable by the elimination algorithm: for every target conjunction, every distribution on $\{0,1\}^n$ and $\epsilon, \delta > 0$, the elimination hypothesis is consistent with every sample labeled by the target, and with

$$m \ge \frac{2n}{\epsilon}\Big(\ln 2n + \ln\frac{1}{\delta}\Big)$$

examples its error exceeds $\epsilon$ with probability at most $\delta$; hence conjunctions are PAC learnable using conjunctions.

Milestones

Theorem 1.1 (rectangles by the tightest fit, $m \ge (4/\epsilon)\ln(4/\delta)$) and Theorem 1.4 (3-CNF formulae by elimination over the $(2n)^3$ expanded variables, the hypothesis being itself a 3-CNF formula).

Significance

Theorem 1.2 is Valiant's original result and the first instance of the two ideas that organize the subject: a hypothesis that is more specific than the target never errs on negative examples, and the error of the hypothesis decomposes as a sum over a polynomial number of "bad" events, each of which is avoided with probability exponentially close to one. Theorem 1.1 is the first learning result for an infinite concept class and the seed of the Vapnik–Chervonenkis theory of Chapter 3. Theorem 1.4 is the first reduction between learning problems and, together with Theorem 1.3, the demonstration that the choice of hypothesis representation can separate tractable from intractable. None of these theorems is machine-checked. Formalizing them fixes, for the rest of the series, the framework in which the error of a hypothesis, the law of a sample and the learnability of a class are stated, so that the Occam, VC-dimension, boosting and noise results of later chapters can be stated on the same objects.

Difficulty

The elimination analysis needs that the hypothesis contains every literal of the target, that its error is at most the sum over its literals $z$ of $p(z) = \Pr[c(a) = 1 \wedge z = 0 \text{ in } a]$, and that a literal with $p(z) \ge \epsilon/2n$ survives $m$ independent examples with probability at most $(1 - \epsilon/2n)^m$; the probabilistic content is the independence of the coordinates of the sample law, which is a product measure, and the inequality $1 - x \le e^{-x}$. The rectangle analysis is the four-strip argument, which for an arbitrary distribution, possibly with atoms, requires choosing the strip $\{y \ge t^*\}$ with $t^*$ the supremum of the heights at which the strip has weight at least $\epsilon/4$ and using the left-continuity of the weight in the height. The 3-CNF result transports the conjunction bound along the injective expansion: the pushforward of the sample law is the sample law of the expanded distribution, and the error of the composed hypothesis equals the error over the expanded variables. The deduction of PACLearnable from the explicit bounds is a choice of sample size.

Formalization scope

The model is stated in the sample-complexity sense: algorithms are functions of the sample, and the guarantee bounds the outer measure of the failure set under the product law of the sample, which is the strong form of "with probability at least $1 - \delta$" and requires no measurability of the failure set. Running time, and hence "efficiently", is not modelled, and the hardness Theorem 1.3 is not stated; each theorem carries instead the explicit algorithm and the explicit sample bound of the book's analysis. Concepts on general instance spaces are required to be measurable in the guarantee. The cube is $\{0,1\}^n$ as functions Fin n → Bool; the expanded variables are indexed by the triples of literals, so $N = (2n)^3$ is a Fintype.card. Rectangles are closed, possibly empty; the tightest fit of a sample without positive examples is the empty concept. Hypotheses: $\epsilon > 0$, $0 < \delta < 1$; the sample bounds are as printed, with natural logarithms.

Trivializing readings are excluded: the failure bound is uniform over all distributions and all targets in the class, consistency is asserted for every sample labeled by the target, and the learnability clause quantifies over all $\epsilon, \delta$. Welcome contributions: the product-law bound $\Pr[\text{a fixed event of probability} \ge p \text{ is missed by all } m \text{ examples}] \le (1 - p)^m$, the union bound over literals, and the pushforward identity for the expanded sample.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 1. doi:10.7551/mitpress/3897.001.0001
• L. G. Valiant, A theory of the learnable, Communications of the ACM 27(11), 1984. doi:10.1145/1968.1972
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4), 1989. doi:10.1145/76359.76371
• L. Pitt, L. G. Valiant, Computational limitations on learning from examples, Journal of the ACM 35(4), 1988. doi:10.1145/48014.63140

Why the policy class is not up for debate

Every model in Chapters 5 and 6 of Axsäter's Inventory Control assumes at the outset that the ordering policy is of $(R,Q)$ or $(s,S)$ type. Section 6.2 asks whether better policies exist and answers, for the case in which there are no ordering costs but every order must be a multiple of a fixed batch quantity $Q$, that none do: Proposition 6.1, "an $(R,Q)$ policy is optimal", with a proof the book attributes to Chen (2000). For $Q = 1$ it is the optimality of an order-up-to-$S$ policy in the absence of ordering costs, and for continuous or Poisson demand it transfers to $(s,S)$ policies, which are then the same thing. The proposition is the one place in the book where a policy is compared against every feasible alternative rather than against other members of its own family, and its proof is short enough to be given in full, which makes it the natural capstone of Chapter 6.

Setting

Demand is compound Poisson: customers arrive according to a Poisson process with rate $\lambda$ and each demands an integral number of units, with sizes $D_0, D_1, \dots$ independent and identically distributed with law $f$ on the positive integers, independent of the arrival process. The book's standing assumption that not all demands are multiples of some integer larger than one is kept. Writing $T_n$ for the $n$-th arrival time, $N(t)$ for the number of arrivals by time $t$ and $S_n = D_0 + \dots + D_{n-1}$, the total demand by time $t$ is $S_{N(t)}$.

The replenishment lead-time $L$ is constant and $D(L)$, the demand over a lead-time, has law $D$. A holding cost $h > 0$ and a shortage cost $b_1 > 0$ per unit and time unit are charged. There are no ordering costs, but all orders must be multiples of a given batch quantity $Q \ge 1$ and can only be triggered by customer demands. A policy is therefore any rule $m$ that decides at each demand epoch how many batches to order; with initial position $y_0$ the inventory position evolves as $y_{n+1} = y_n - D_n + m_nQ$ (Eq. 6.22), and $y_t = y_{N(t)}$.

The standard argument of Sect. 5.3.2 gives the cost rate at time $t + L$ as

$$g(y_t), \qquad g(k) = -b_1(k - \mu') + (h+b_1)\sum_{j=1}^{k} j\,\Pr[D(L) = k - j],$$

the expected holding-plus-shortage cost rate of an inventory level $k - D(L)$ (Eq. 6.20), which is convex in $k$ with $g(k) \to \infty$ as $|k| \to \infty$. The band cost is $\bar g(y) = \sum_{j=1}^{Q} g(y+j)$ and $R$ denotes an integer minimizing $\bar g$. The $(R,Q)$ policy orders, as soon as the position is at or below $R$, the smallest number of batches that brings it above $R$; its position lives in the band $\{R+1, \dots, R+Q\}$ from the first order on. The performance measure is the long-run average cost rate $\frac{1}{T}\int_0^T g(y_{t-L})\,\mathrm{d}t$ as $T \to \infty$.

Formalization targets

Goal — Proposition 6.1

Almost surely, (1) for every policy $m$ and every $y_0$,

$$\liminf_{T\to\infty} \frac{1}{T}\int_0^T g\big(y^{m}_{t-L}\big)\,\mathrm{d}t \;\ge\; \frac{\bar g(R)}{Q},$$

and (2) the $(R,Q)$ policy attains it:

$$\frac{1}{T}\int_0^T g\big(y^{(R,Q)}_{t-L}\big)\,\mathrm{d}t \;\longrightarrow\; \frac{\bar g(R)}{Q}.$$

Supporting targets

Lemma 6.1, that $x \mapsto g(z + xQ)$ is convex and minimized at the representative of $z$ in the band; the closed form of the $(R,Q)$ position, $y_0 - S_n$ until the first order and the band representative of $y_0 - S_n$ afterwards; the uniform occupation of the band by the reduced process $y_t'$, the book's "the steady state distribution can be shown to be uniform", and its consequence that the long-run average of $g(y_t')$ is $\bar g(R)/Q$; Proposition 5.1 in the same ergodic form for the $(R,Q)$ policy; and the two halves of the goal as separate statements.

Significance

The result itself. Proposition 6.1 is what licenses the two-parameter policies on which the rest of the book's single-echelon theory is built, and it does so for the practically important case of batch ordering (pallets, containers, production lots). Its proof also explains why the policy works: the only quantity a policy controls is the residue class of the inventory position modulo $Q$, which no policy can influence, and the position within that class, which the $(R,Q)$ policy always sets to the cheapest possible value. The book extends the same reasoning to other cost structures and to periodic review.

Formalizing it. The proposition is a theorem about the class of all policies, and the book's proof is pathwise: Lemma 6.1 compares any policy with the reduced process instant by instant, and an ergodic statement about the reduced process does the rest. Formalizing it therefore forces the policy class, the demand process and the long-run average to be written down exactly, which the book never does. Nothing here is open; no statement has a machine-checked proof yet.

Difficulty

The pointwise comparison is elementary once Lemma 6.1 is available, and Lemma 6.1 is discrete convexity. The difficulty is entirely in the ergodic statement: that the reduced position $y_t' =$ (the band representative of $y_0 - S_{N(t)}$) spends a fraction $1/Q$ of the time at each point of the band, almost surely. In discrete time this is the convergence of occupation frequencies for an irreducible random walk on $\mathbb{Z}/Q\mathbb{Z}$ with step law $f$ modulo $Q$, where irreducibility is exactly the aperiodicity assumption on $f$, and the book's double-stochasticity argument (Eq. 5.33-5.34) identifies the uniform law as stationary. Passing to continuous time adds the exponential holding times: the time average is the arrival average weighted by i.i.d. holding times independent of the walk, which a strong law of large numbers turns back into the discrete statement. Mathlib has the strong law and the exponential law but no ergodic theorem for finite Markov chains, so that is the groundwork a solver must build. The naive route through the stationary distribution of the embedded chain at demand epochs is not enough on its own: for pure Poisson demand that chain is periodic, and the book itself notes it.

Formalization scope

A CompoundPoissonDemand on a probability space packages the rate, the size law with $f_0 = 0$ and the aperiodicity condition, and two sequences of random variables, the gaps and the sizes, with their laws (expMeasure lam, the given pmf), independence within each sequence, and independence between the sequences. Arrival times are partial sums of the gaps, count t is the supremum of $\{n : T_n \le t\}$, and cumDemand n is the partial sum of the sizes. A policy is a function m : ℕ → Ω → ℕ with no measurability requirement; ipPath and ipAt are the position after the $n$-th demand and at time $t$; rqIP and rqOrders are the $(R,Q)$ policy, with a theorem identifying rqOrders as a policy in the general sense. avgCost is $\frac{1}{T}\int_0^T g(y_{t-L})\,\mathrm{d}t$ with $y_s = y_0$ for $s < 0$. The cost function $g$ is sPolicyCost from the previous mission, applied to a DiscreteDemand that the hypotheses tie to the process as the law of the demand in $(0, L]$.

Conventions: $Q \ge 1$, $L \ge 0$, $h, b_1 > 0$; $R$ is any minimizer of $\bar g$ (it exists by the divergence of $g$, proved in the previous mission); $y_0$ is arbitrary. count and the interval integral take junk values on the null set where arrivals do not tend to infinity, which the almost-sure conclusions absorb. "$\liminf \ge c$" is stated as "for every $\varepsilon > 0$, eventually $\ge c - \varepsilon$", avoiding a liminf on $\mathbb{R}$ that could be junk.

Two readings that would trivialize the goal are excluded: the lower bound is over every rule, not over stationary or measurable ones, and the achievability half is a genuine limit, not a bound. The demand model and the occupation-frequency theorems are reusable for Proposition 10.1 and the batch-ordering models of Sect. 10.5; contributions establishing the ergodic theorem for irreducible chains on a finite cyclic group are welcome and would close most of this mission.

Selected references

• Sven Axsäter, Inventory Control, 3rd edition, International Series in Operations Research & Management Science 225, Springer, 2015, Sects. 5.3.1 and 6.2.1. DOI 10.1007/978-3-319-15729-0
• Fangruo Chen, Optimal Policies for Multi-Echelon Inventory Problems with Batch Ordering, Operations Research 48(3), 2000, pp. 376-389. DOI 10.1287/opre.48.3.376.12427
• Awi Federgruen and Yu-Sheng Zheng, An Efficient Algorithm for Computing an Optimal $(r,Q)$ Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4), 1992, pp. 808-813. DOI 10.1287/opre.40.4.808
• Evan L. Porteus, Foundations of Stochastic Inventory Theory, Stanford University Press, 2002.

Two decisions that are usually taken separately

An $(R,Q)$ policy has two parameters. Chapter 4 of Axsäter's Inventory Control chooses the batch quantity $Q$ from a deterministic model, and Chapter 5 chooses the reorder point $R$ from a stochastic one with $Q$ held fixed; the book presents this two-step practice as an adequate approximation. Section 6.1 asks what is lost by it and shows how to optimize both parameters jointly in one stochastic model. For discrete demand the answer, due to Federgruen and Zheng (1992), is an algorithm of remarkable simplicity: increase $Q$ one unit at a time, keep the reorder point optimal along the way by a one-line rule, and stop at the first $Q$ for which the cost goes up. The claim that this stopping rule finds the global optimum over all pairs $(R, Q)$ is the capstone of Sect. 6.1.1.1 and the goal of this mission. The same idea is reused in the book for $(s,S)$ policies (Sect. 6.1.1.2) and, in continuous form, for normally distributed demand (Sect. 6.1.2).

Setting

An item is controlled by a continuous review $(R,Q)$ policy with integral reorder point $R$ and batch quantity $Q \ge 1$. Demand is discrete and stationary; the lead-time demand $D(L)$ takes values in the nonnegative integers with probabilities $p_j = \Pr[D(L) = j]$ and has a finite mean $\mu'$. The average demand per unit of time is $\mu$. Costs are a holding cost $h$ and a shortage cost $b_1$, both per unit and time unit, and an ordering cost $A$ per batch.

The building block is the cost of an $(S-1,S)$ policy that keeps the inventory position at a fixed integer $k$. By the standard argument of Sect. 5.3.2 the inventory level a lead-time later is $k - D(L)$, and the average holding and shortage cost rate is (Eq. 6.3)

$$g(k) \;=\; -b_1\,(k - \mu') + (h + b_1)\sum_{j=1}^{k} j\,\Pr[D(L) = k - j].$$

Under the $(R,Q)$ policy the inventory position is uniformly distributed on $\{R+1, \dots, R+Q\}$ (Proposition 5.1), so the total average cost rate is (Eq. 6.4)

$$C(R, Q) \;=\; \frac{A\mu}{Q} + \frac{1}{Q}\sum_{k=R+1}^{R+Q} g(k),$$

and $C(Q) = \min_R C(R,Q)$ (Eq. 6.5), attained at an optimal reorder point $R^{*}(Q)$. The ready rate $S_3(R) = \Pr[IL > 0] = \frac{1}{Q}\sum_{k=R+1}^{R+Q}\Pr[D(L) \le k-1]$ links the cost to service: raising the reorder point by one unit changes the cost by $-b_1 + (h + b_1)S_3(R+1)$ (Eq. 5.60).

Formalization targets

Goal — the Federgruen-Zheng stopping rule is optimal

Let $Q^{*} \ge 1$ be the smallest batch quantity with $C(Q^{*}+1) \ge C(Q^{*})$ and let $R^{*}$ be an optimal reorder point for $Q^{*}$. Then

$$C(R^{*}, Q^{*}) \;\le\; C(R, Q) \qquad\text{for all } R \in \mathbb{Z},\ Q \ge 1.$$

Supporting targets

The increment identity $g(k+1) - g(k) = -b_1 + (h+b_1)\Pr[D(L) \le k]$; convexity of $g$ on $\mathbb{Z}$ together with $g(k) \to \infty$ as $|k| \to \infty$; Eq. (5.60) and the convexity of $C(\cdot, Q)$ in $R$; Eq. (5.61), that the largest $R$ with $S_3(R) \le b_1/(h+b_1)$ is optimal for its $Q$; existence of an optimal $R$ for every $Q$; the recursion (6.6)-(6.7), $R^{*}(Q+1) \in \{R^{*}(Q) - 1, R^{*}(Q)\}$ chosen by comparing $g(R^{*}(Q))$ with $g(R^{*}(Q)+Q+1)$, and $C(Q+1) = C(Q)\frac{Q}{Q+1} + \min\{g(R^{*}(Q)), g(R^{*}(Q)+Q+1)\}\frac{1}{Q+1}$; the equivalence $C(Q+1) \ge C(Q) \iff \min\{\cdot\} \ge C(Q)$ and the monotonicity of that minimum in $Q$; and the existence of some $Q$ at which the costs stop decreasing.

Significance

The result itself. Joint optimization typically enlarges the batch and lowers the reorder point relative to the two-step procedure, and the book's Example 6.1 puts the resulting cost saving at a few percent. The Federgruen-Zheng procedure makes the exact joint optimum for discrete demand as cheap to compute as the two-step approximation, because each step of the recursion evaluates $g$ at two points. It is the exact benchmark against which the book's approximate techniques for normal demand (Sects. 6.1.2 and 6.1.3) are judged, and its structural core, that the optimal window of $Q$ consecutive inventory positions grows one neighbour at a time, is the discrete-convexity fact behind the whole of Sect. 6.1.

Formalizing it. The mathematics is settled. What the mission produces is a Lean development in which the steps the book marks "evident" and "obvious" are separate statements: that the recursion preserves optimality, that the marginal cost of enlarging the batch is monotone, and that a minimum over $R$ exists at all. None of the statements has a machine-checked proof yet.

Difficulty

The obvious first idea, to argue that $C(Q)$ is convex in $Q$ and stop at its first increase, does not work as stated: $C(Q)$ is a minimum over $R$ of a ratio and is not convex in general. What is true, and what the proof uses, is that the marginal cost $(Q+1)C(Q+1) - QC(Q)$ is nondecreasing, because it equals the smaller of the two $g$-values adjacent to the optimal window. Establishing the recursion (6.6) is where discrete convexity is needed: one must show that the best window of $Q+1$ consecutive positions is obtained from the best window of $Q$ by adding a neighbour, which fails for non-convex $g$. The window sums $R \mapsto \sum_{k=R+1}^{R+Q} g(k)$ are themselves convex in $R$ with increments $g(R+Q+1) - g(R+1)$, and the argument compares a competing window with the optimal one through the end terms. The remaining steps are finite algebra and an induction on $Q$ from $Q^{*}$.

Formalization scope

A DiscreteDemand is a function $p : \mathbb{N} \to \mathbb{R}$ with $p \ge 0$, $\sum p = 1$ and a summable first moment; $\Pr[D(L) \le k]$ is a finite sum over $0 \le j \le k$, empty for $k < 0$. The reorder point ranges over $\mathbb{Z}$ and the batch quantity over $\mathbb{N}$, with $Q \ge 1$ assumed in every statement because Lean's division by $0$ is $0$. Convexity of a function on $\mathbb{Z}$ is stated as nondecreasing increments, and divergence as Tendsto g (cocompact ℤ) atTop.

$C(Q)$ enters the goal as a function CQ together with the hypothesis that CQ Q is the least value of $R \mapsto C(R, Q)$; the stopping index $Q^{*}$ is characterized by the two conditions that define "the smallest $Q$ with $C(Q+1) \ge C(Q)$", and $R^{*}$ by optimality at $Q^{*}$. That these objects exist is the content of two separate items, so the goal is not vacuous: a minimum over $R$ exists for every $Q$ because $g \to \infty$, and the costs cannot decrease forever because the average of the $Q$ smallest values of $g$ tends to infinity. The positivity of $A$ and $\mu$ is the book's setting and is assumed where it appears.

The uniform inventory position of Proposition 5.1, which needs the book's assumption that not all demands are multiples of an integer larger than one, is taken as given in the cost formula (6.4), as the book does; the proposition itself is the subject of the next mission of this series. The definitions are reusable for the $(s,S)$ optimization of Sect. 6.1.1.2 and for the multi-echelon batch-ordering results of Sect. 10.5; contributions formalizing the Zheng-Federgruen $(s,S)$ algorithm on top of them are welcome.

Selected references

• Sven Axsäter, Inventory Control, 3rd edition, International Series in Operations Research & Management Science 225, Springer, 2015, Sects. 5.9.1 and 6.1.1. DOI 10.1007/978-3-319-15729-0
• Awi Federgruen and Yu-Sheng Zheng, An Efficient Algorithm for Computing an Optimal $(r,Q)$ Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4), 1992, pp. 808-813. DOI 10.1287/opre.40.4.808
• Yu-Sheng Zheng and Awi Federgruen, Finding Optimal $(s,S)$ Policies Is About as Simple as Evaluating a Single Policy, Operations Research 39(4), 1991, pp. 654-665. DOI 10.1287/opre.39.4.654
• Paul Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000.

Where the reorder point comes from

Chapter 4 of Axsäter's Inventory Control fixes the batch quantity $Q$ from a deterministic model, and Chapter 5 asks the question that deterministic models cannot answer: with demand random and a replenishment lead-time $L$, when should the next batch be ordered? Under a continuous review $(R,Q)$ policy the answer is a single number, the reorder point $R$, and Sections 5.3 through 5.9 are one sustained computation of what a given $R$ buys. The chapter's own capstone is Eq. (5.67): if backorders are charged at $b_1$ per unit and time unit and stock at $h$, the cost-minimizing reorder point is exactly the one whose fill rate is $b_1/(h+b_1)$. The book calls the relationship "even more striking" than its discrete counterpart, and it is used in practice in both directions: a backorder cost prescribes a service level, and a chosen service level reveals the backorder cost a planner is implicitly assuming (Eq. 5.68).

Setting

An order for a fixed batch quantity $Q > 0$ is triggered whenever the inventory position (stock on hand plus outstanding orders minus backorders) falls to the reorder point $R$, and it arrives $L$ time units later. Demand is continuous and normally distributed; the demand over a lead-time has mean $\mu'$ and standard deviation $\sigma' > 0$. Two modelling facts from the book are taken as the definition of the steady state. First (Sect. 5.3.1), the inventory position $IP$ is uniformly distributed on $[R, R+Q]$; the book proves this for compound Poisson demand (Proposition 5.1) and adopts it as an accurate approximation for continuous demand. Second (Sect. 5.3.2, Eq. 5.35), the inventory level a lead-time later is the inventory position now minus the demand in between,

$$IL(t+L) \;=\; IP(t) - D(t, t+L),$$

with the two terms independent. The law of $IL$ is therefore the image of the product of a uniform and a normal law under subtraction, and everything in the chapter is a functional of it:

• the distribution function $F(x) = \Pr[IL \le x]$ and its density $f$;
• the ready rate $S_3 = \Pr[IL > 0]$, which for continuous demand equals the fill rate $S_2$, the fraction of demand met from stock on hand;
• the expected cost rate $C(R) = \mathbb{E}\big[h\,(IL)^{+} + b_1\,(IL)^{-}\big]$, holding cost on positive stock and backorder cost on negative stock, Eq. (5.56).

The closed forms run through the standard normal loss function $G(x) = \int_x^\infty (v-x)\varphi(v)\,\mathrm{d}v$ of Eq. (5.40), published with the newsboy mission and reused here, and through its integral, the second loss function $H(x) = \int_x^\infty G(v)\,\mathrm{d}v$ of Eq. (5.64). Both are tabulated in the book's Appendix 2, and both recur in Chapters 6, 9 and 10.

Formalization targets

Goal — Eq. (5.67)

For $h, b_1, Q, \sigma' > 0$ and any $\mu'$, a reorder point $R$ minimizes $C$ over $\mathbb{R}$ if and only if

$$S_2(R) \;=\; S_3(R) \;=\; \frac{b_1}{h + b_1}.$$

The biconditional carries both halves of the book's sentence: the stationary point is the optimum ("the optimal $R$ is obtained for $\mathrm{d}C/\mathrm{d}R = 0$") and the optimum is stationary ("in the optimal solution we have $S_2 = S_3 = b_1/(h+b_1)$").

Supporting targets

In the order the chapter builds them: Eq. (5.41), $G' = \Phi - 1$, with $G$ decreasing and convex; Eq. (5.39), the distribution function by conditioning on the inventory position; Eq. (5.42), its closed form $F(x) = \frac{\sigma'}{Q}[G(\frac{R-x-\mu'}{\sigma'}) - G(\frac{R+Q-x-\mu'}{\sigma'})]$; Eq. (5.43), the density; Eq. (5.52), the fill rate $1 - \frac{\sigma'}{Q}[G(\frac{R-\mu'}{\sigma'}) - G(\frac{R+Q-\mu'}{\sigma'})]$; Eq. (5.55), the expected backorders $\mathbb{E}(B)$ covered by one batch, and Eq. (5.54), that $1 - \mathbb{E}(B)/Q$ is the same fill rate; integrability of the cost rate and the mean $\mathbb{E}(IL) = R + Q/2 - \mu'$; Eq. (5.63), $\mathbb{E}(IL)^{-} = \int_{-\infty}^0 F$; Eq. (5.64), the closed form of $H$ and $H' = -G$; Eq. (5.65), the cost $C = h(R + Q/2 - \mu') + (h+b_1)\frac{\sigma'^2}{Q}[H(\frac{R-\mu'}{\sigma'}) - H(\frac{R+Q-\mu'}{\sigma'})]$; Eq. (5.66), $\mathrm{d}C/\mathrm{d}R = -b_1 + (h+b_1)S_2$; and the convexity of $C$ in $R$.

Significance

The result itself. The reorder point is the one parameter of an $(R,Q)$ policy that stochastic demand actually decides, and Eq. (5.67) says that deciding it by cost and deciding it by service level are the same decision, with an explicit dictionary between the two. That is why the book can present service-level constraints (Sect. 5.7) and shortage costs (Sect. 5.9) as interchangeable ways of specifying the same thing, and why it warns, immediately after Eq. (5.67), that the equivalence is only valid when $Q$ is given: with an ordering cost and a joint optimization of $R$ and $Q$ it fails, which is Chapter 6's problem.

The intermediate formulas have independent standing. Eq. (5.42) is the single expression from which every service measure of the chapter is computed, and Eq. (5.65) is the cost function that Chapter 6 extends by an ordering cost, Eq. (6.10), and optimizes iteratively. The second loss function $H$ returns in the periodic-review fill rate of Eq. (5.86) and in the two-echelon batch-ordering model of Sect. 10.5.

Formalizing it. Nothing here is open; the value is that the steady-state model becomes an explicit measure, so that formulas the book obtains by manipulating integrals whose existence it never questions become theorems about that measure. Integrability of the cost rate is a target of its own for exactly that reason. None of the statements has a machine-checked proof yet.

Difficulty

The obvious route is the book's, and it is not the hard part: once $F$ is known in closed form, every later identity is calculus on $G$ and $H$. The work is upstream of that. The distribution function (5.39) is a conditioning argument over the product measure, a Fubini step in which the inner probability is a Gaussian tail; the density (5.43) is a derivative of a parameter-dependent integral; and Eq. (5.63) exchanges the order of two integrals over an unbounded region, which needs integrability of $IL$ itself. The derivative (5.66) is then obtained from the closed form (5.65), not by differentiating under an expectation, which is what makes the goal reachable: $C$ is a smooth function of $R$ with an explicitly increasing derivative, and Eq. (5.67) follows from strict convexity together with the fact that the fill rate is a continuous, strictly increasing function of $R$ ranging over $(0,1)$. A solver who starts from the expectation and tries to differentiate it directly will meet the kink of $x^{+}$ at $0$ and a dominated-convergence argument; the integrated route avoids both.

Formalization scope

The inventory position is rqPosition R Q, Lebesgue measure conditioned on $[R, R+Q]$; the lead-time demand is newsboyDemand m s, Mathlib's gaussianReal m (s^2).toNNReal from the newsboy mission, with $m = \mu'$ and $s = \sigma'$; and rqLevel R Q m s is the pushforward of their product under $(u, d) \mapsto u - d$. Two lemmas in the definition file record that both are probability measures when $Q > 0$. The distribution function, ready rate and cost are the measure of $(-\infty, x]$, the measure of $(0, \infty)$, and a Bochner integral against this law.

Every statement assumes $Q > 0$ and $\sigma' > 0$. At $Q = 0$ the conditioned measure is the zero measure and every integral is $0$, so a statement without the hypothesis would be true and empty; at $\sigma' = 0$ the demand is a point mass and $F$ has jumps. The mean $\mu'$ is unrestricted, as none of the formulas depends on its sign, and reorder points may be negative, which the book explicitly allows in Sect. 5.8. Costs $h$ and $b_1$ are positive in every statement that involves them, and $\mathbb{E}(B)$ is stated for $Q \ge 0$ because its closed form holds there.

Two trivializing readings are ruled out. The cost is not defined as a formula in $H$ but as an expectation, so the closed form (5.65) has content; and because Lean's Bochner integral of a non-integrable function is $0$, integrability of the cost rate is stated as a theorem rather than assumed, otherwise a zero cost would make every reorder point optimal. The goal quantifies optimality over all real competing reorder points, not a neighbourhood.

A complete development needs Gaussian tail integrals, differentiation of parameter-dependent integrals, Fubini on a product of a bounded interval with the line, and the strict monotonicity of the Gaussian distribution function. The loss functions $G$ and $H$ and the inventory-level law are reusable across the rest of the series; contributions that establish the same identities for an arbitrary continuous lead-time demand with a finite mean, where Eqs. (5.39), (5.63) and (5.66) hold verbatim, are welcome.

Selected references

• Sven Axsäter, Inventory Control, 3rd edition, International Series in Operations Research & Management Science 225, Springer, 2015, Sects. 5.3, 5.7, 5.8 and 5.9. DOI 10.1007/978-3-319-15729-0
• George Hadley and Thomson M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• Paul Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000.
• Yu-Sheng Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1), 1992, pp. 87-103. DOI 10.1287/mnsc.38.1.87
• Kaj Rosling, Inventory Cost Rate Functions with Nonlinear Shortage Costs, Operations Research 50(6), 2002, pp. 1007-1017. DOI 10.1287/opre.50.6.1007.346

Motivation

A decision maker who does not want to be judged by expected loss alone needs a functional that weighs the bad outcomes more heavily than the good ones and still behaves well under optimization: monotone, convex, unchanged by shifting the loss, and scaling with it. Kusuoka's theorem (mission II) says every such law-invariant functional on an atomless space is a supremum of mixtures of Average Values-at-Risk. The mixtures themselves are the distortion risk functionals of Denneberg (Distorted probabilities and insurance premiums, Methods of Operations Research 63, 1990) and Acerbi (Spectral measures of risk: A coherent representation of subjective risk aversion, Journal of Banking and Finance 26, 2002, doi:10.1016/S0378-4266(02)00281-9), also called spectral risk measures: integrals of the quantile function against a nondecreasing density $\sigma$. They are the risk functionals used throughout Pflug and Pichler's book (doi:10.1007/978-3-319-08843-3) in the multistage objectives of Chapters 5 and 6, and the three representations proved in Sections 3.2 to 3.4 — as a supremum over densities $Z$, as a maximum over uniform variables, and as an infimum over convex-conjugate constraints — are what make them computable inside an optimization model. This mission formalizes those representations.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$. A random variable $Y:\Omega\to\mathbb R$ is a loss, and the functionals act on $L^\infty$, the bounded measurable ones. The Value-at-Risk at level $u\in(0,1]$ is the lower quantile $\mathsf{V@R}_u(Y)=\inf\{y:P(Y\le y)\ge u\}$ and the Average Value-at-Risk at level $\alpha\in[0,1)$ is $\mathsf{AV@R}_\alpha(Y)=\frac{1}{1-\alpha}\int_\alpha^1\mathsf{V@R}_u(Y)\,du$, extended to $\alpha=1$ by the essential supremum (mission II). A risk functional satisfies the four axioms (M), (C), (T), (H) of Definition 3.2.

A distortion function is a nonnegative, nondecreasing $\sigma:[0,1)\to[0,\infty)$ with $\int_0^1\sigma=1$, and the distortion risk functional with density $\sigma$ is

$$\mathcal R_\sigma(Y)\;=\;\int_0^1\sigma(u)\,\mathsf{V@R}_u(Y)\,du .$$

The Average Value-at-Risk is the case $\sigma_\alpha=(1-\alpha)^{-1}\mathbf 1_{[\alpha,1)}$. A random variable $Z$ is dominated by $\sigma$, $Z\preccurlyeq\sigma$, when $Z\in L^1$, $\mathbb E(Z)=1$ and $\mathsf{AV@R}_\alpha(Z)\le\frac{1}{1-\alpha}\int_\alpha^1\sigma$ for every $\alpha\in[0,1)$. A variable $U$ is uniformly distributed when $P(U\le u)=u$ on $[0,1]$. For $h:\mathbb R\to\mathbb R$ the conjugate is $h^*(s)=\sup_y(s\,y-h(y))\in(-\infty,+\infty]$.

Formalization targets

Goal — Theorem 3.16 (printed pp. 105–106)

$$\mathcal R_\sigma(Y)\;=\;\sup\bigl\{\mathbb E(Y\cdot Z)\ :\ Z\preccurlyeq\sigma\bigr\} \qquad(Y\in L^\infty).$$

The distortion functional is a risk functional (printed p. 99)

$\mathcal R_\sigma$ satisfies (M), (C), (T) and (H).

Representation (3.11) (printed p. 100)

There is a probability measure $\mu$ on $[0,1]$ with $\mathcal R_\sigma(Y)=\int_0^1\mathsf{AV@R}_\alpha(Y)\,\mu(d\alpha)$ for all $Y\in L^\infty$.

Corollary 3.18 (printed pp. 107–108)

For $\alpha<1$, $\mathsf{AV@R}_\alpha(Y)=\sup\{\mathbb E(YZ):\mathbb EZ=1,\ \mathsf{AV@R}_p(Z)\le\frac1{1-\alpha}\ \forall p\in[\alpha,1]\} =\sup\{\mathbb E(YZ):\mathbb EZ=1,\ 0\le Z\le\frac1{1-\alpha}\}$; for $\alpha=1$ the latter with the upper bound dropped.

Corollary 3.19 (printed p. 108)

On an atomless space, $\mathcal R_\sigma(Y)=\max\{\mathbb E(Y\cdot\sigma(U)):U\text{ uniform}\}$, the maximum attained.

Theorem 3.22 (printed p. 111)

$\mathcal R_\sigma(Y)=\inf\{\mathbb E(h(Y)):\int_0^1h^*(\sigma(u))\,du\le 0\}$ over measurable $h:\mathbb R\to\mathbb R$.

Significance

Theorem 3.16 identifies the conjugate of a distortion functional: $\mathcal R_\sigma^*(Z)$ is $0$ when $Z\preccurlyeq\sigma$ and $+\infty$ otherwise, so $\mathcal R_\sigma$ is the support function of an explicit convex set of densities. Everything else follows from that. Corollary 3.18 recovers the classical dual of the Average Value-at-Risk and shows that its constraints can be relaxed to the levels in $[\alpha,1]$; Corollary 3.19 turns the supremum into a maximum over couplings and identifies the maximizer, the co-monotone one, which is how distortion functionals are evaluated on scenario trees; Corollary 3.21, not stated here, combines the theorem with Kusuoka's representation to give the dual of every version independent risk functional. Theorem 3.22 goes the other way and writes $\mathcal R_\sigma$ as an infimum, which is what converts a minimax problem — minimize a supremum over $Z$ — into a plain minimization over the decision and an auxiliary function $h$, the form in which the book solves risk-averse programs in Chapters 5 and 6.

Everything here is proved in the source and in the cited papers; the platform has the finite-scenario Artzner–Delbaen representation of coherent risk measures but nothing on distortion functionals, and Mathlib has no risk-measure material and no quantile-based representation theory. The definitions of this mission sit on those of mission II and are reused as such.

Difficulty

The obvious route to Theorem 3.16 is Fenchel–Moreau duality: $\mathcal R_\sigma$ is convex and lower semicontinuous on $L^\infty$, so it equals its biconjugate, and the task is to compute $\mathcal R_\sigma^*(Z)=\sup_Y\,\mathbb E(YZ)-\mathcal R_\sigma(Y)$. The step where the naive computation stalls is bounding $\mathbb E(YZ)$ by a quantity that depends only on the distributions of $Y$ and $Z$: this is the rearrangement (Chebyshev, Hardy–Littlewood) inequality $\mathbb E(YZ)\le\int_0^1G_Y^{-1}(u)G_Z^{-1}(u)\,du$, with equality for co-monotone couplings. Given it, $\mathcal R_\sigma^*(Z)=\sup_Y\int_0^1G_Y^{-1}(G_Z^{-1}-\sigma)$, and testing with indicator-type $Y$ shows the supremum is $0$ exactly when the upper-tail averages of $Z$ are dominated by those of $\sigma$, which is the constraint $Z\preccurlyeq\sigma$. Neither the rearrangement inequality nor the identification of the conjugate is available in Mathlib.

For the corollaries the difficulties are concrete. Corollary 3.18 needs $Z\ge 0$ to be deduced from the constraints, which the source does by contradiction through the value $p=P(Z<0)$. Corollary 3.19 needs the co-monotone coupling to exist, which is where the atomless hypothesis enters, and needs $\sigma(U)$ to be feasible for (3.15), which uses $G_{\sigma(U)}^{-1}=\sigma$. Theorem 3.22 needs, besides the inequality $\mathbb E(h(Y))\ge\mathcal R_\sigma(Y)$ from Fenchel–Young, an admissible $h$ that nearly attains it; the source builds it from $\sigma$ and $G_Y^{-1}$ via Corollary 3.23.

Formalization scope

Random variables are functions $\Omega\to\mathbb R$ on an arbitrary measurable space with a probability measure, exactly as in mission II, whose MemLinfty, valueAtRisk, averageValueAtRisk, IsRiskFunctional, Atomless and IsKusuokaMeasure are imported and not redefined. The distortion density is a function on $\mathbb R$ constrained on $[0,1)$; its integrability on $(0,1)$ is part of the definition, and both $\int_0^1\sigma$ and $\mathcal R_\sigma$ integrate over the open interval, which excludes the level $0$ where the quantile formula is not meaningful and changes no value.

Every supremum and infimum is over a subtype of functions satisfying the constraints, and the prose of each item records why the family is nonempty and bounded, so that no real supremum takes its junk value. Pointwise constraints on $Z$ are almost sure. The constraint of (3.15) is stated for $\alpha\in[0,1)$: at $\alpha=1$ the source's expression is $0/0$ and means the limit, and the constraint there is implied by the others; (3.19) at $\alpha=1$ is stated separately with the upper bound dropped. The conjugate takes values in the extended reals, and admissibility in Theorem 3.22 requires $h^*(\sigma(u))$ finite almost everywhere, integrable, with integral at most $0$, and $h(Y)$ integrable — the conditions under which the expectations in (3.24) are the integrals the source means.

Two hypotheses are added beyond the printed statements and are flagged in the items: atomless for Corollary 3.19, because otherwise no uniform variable need exist and the maximum would be over an empty set; and integrability of $h(Y)$ in Theorem 3.22, without which Lean's integral of a non-integrable $h(Y)$ is $0$. Theorem 3.16 itself carries no atomless hypothesis, and the mission notes check the identity on two-point spaces by hand. A trivializing formalization — a constraint set that is empty or unbounded, so that the supremum is $0$ — is excluded by the constant density $Z\equiv 1$, feasible for every $\sigma$, and by $Z\ge 0$.

Welcome contributions beyond the milestones: Corollary 3.15 (the representation through the distribution function for $Y\ge 0$), Corollary 3.21 (the dual of a version independent risk functional through its Kusuoka set), Corollary 3.23, and the explicit mixing measure (3.12).

Selected references

• Georg Ch. Pflug and Alois Pichler, Multistage Stochastic Optimization, Springer, 2014, Sections 3.2–3.4. doi:10.1007/978-3-319-08843-3
• Carlo Acerbi, Spectral measures of risk: A coherent representation of subjective risk aversion, Journal of Banking and Finance 26 (2002). doi:10.1016/S0378-4266(02)00281-9
• Shigeo Kusuoka, On law invariant coherent risk measures, Advances in Mathematical Economics 3 (2001). doi:10.1007/978-4-431-67891-5_4
• Alois Pichler, The natural Banach space for version independent risk measures, Insurance: Mathematics and Economics 53 (2013). doi:10.1016/j.insmatheco.2013.07.005
• Georg Ch. Pflug and Werner Römisch, Modeling, Measuring and Managing Risk, World Scientific, 2007. doi:10.1142/6478