Motivation

A risk measure assigns to a random financial position $X$ a capital requirement $\rho(X)$: the amount of cash that must be added to $X$ to make it acceptable. The axiomatic theory of convex risk measures (Föllmer–Schied 2002; Frittelli–Rosazza Gianin 2002) treats this number as computed with no information beyond the model. In practice a regulator or a risk manager revises the requirement as information arrives, so the requirement becomes a random variable measurable with respect to the information available at the time of measurement. Detlefsen and Scandolo (SFB 649 Discussion Paper 2005-006; published in Finance and Stochastics 9(4), 2005, doi:10.1007/s00780-005-0159-6) develop this conditional theory: axioms, a robust representation, and a treatment of dynamic risk measurement.

The entropic risk measure is the standard example of a convex risk measure that is not coherent. It is the capital requirement of an agent with exponential utility $u_\gamma(x)=1-e^{-\gamma x}$, and its penalty function in the robust representation is the relative entropy $\frac1\gamma H(Q\mid P)$ (Föllmer–Schied, Stochastic Finance, Example 4.60, as cited by the paper). Section 5 of the paper carries this example to the conditional setting and shows that its penalty is a conditional relative entropy. The same identity appears in dynamic entropic risk measures, exponential-utility indifference pricing and recursive utility, where one-period conditional entropic measures are composed over time.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ and a sub-$\sigma$-algebra $\mathcal G\subseteq\mathcal F$, the information available at the time of measurement. $L^\infty$ is the space of essentially bounded random variables and $L^\infty_{\mathcal G}$ its $\mathcal G$-measurable part. All equalities and inequalities between random variables hold $P$-almost surely.

A conditional convex risk measure is a map $\rho:L^\infty\to L^\infty_{\mathcal G}$ that is translation invariant ($\rho(X+Z)=\rho(X)-Z$ for $Z\in L^\infty_{\mathcal G}$), monotone ($X\le Y\Rightarrow\rho(X)\ge\rho(Y)$), conditionally convex ($\rho(\Lambda X+(1-\Lambda)Y)\le\Lambda\rho(X)+(1-\Lambda)\rho(Y)$ for $\Lambda\in L^\infty_{\mathcal G}$, $0\le\Lambda\le1$), and satisfies $\rho(0)=0$.

The relevant probability models are

$$\mathcal P_{\mathcal G}=\{Q \text{ probability on } (\Omega,\mathcal F) : Q\ll P,\ Q(A)=P(A)\ \text{for all } A\in\mathcal G\}.$$

The essential supremum of a family $\mathcal X$ of $[-\infty,+\infty]$-valued random variables is the a.s. smallest random variable that dominates every member a.s.; the essential infimum is defined symmetrically. The minimal penalty of $\rho$ is

$$\alpha^*(Q)=\operatorname{ess.sup}_{X\in L^\infty}\{-E_Q(X\mid\mathcal G)-\rho(X)\},\qquad Q\in\mathcal P_{\mathcal G}.$$

For a risk aversion $\gamma>0$, the conditional entropic risk measure is

$$\rho_\gamma(X)=\frac1\gamma\log E_P\big(e^{-\gamma X}\mid\mathcal G\big),$$

the capital requirement for the acceptance set $A_\gamma=\{X\in L^\infty : E_P(e^{-\gamma X}\mid\mathcal G)\le1\}$. For $Q\in\mathcal P_{\mathcal G}$ with density $\varphi=dQ/dP$, the conditional relative entropy is

$$H_{\mathcal G}(Q\mid P)=E_P(\varphi\log\varphi\mid\mathcal G)\in[0,+\infty],\qquad 0\log0=0.$$

Formalization targets

Goal: Proposition 5.4

For every $\gamma>0$:

$$\rho_\gamma(X)=\operatorname{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\Big\{-E_Q(X\mid\mathcal G)-\tfrac1\gamma H_{\mathcal G}(Q\mid P)\Big\}\quad(X\in L^\infty),\qquad \alpha^*(Q)=\tfrac1\gamma H_{\mathcal G}(Q\mid P)\quad(Q\in\mathcal P_{\mathcal G}).$$

The first identity is representability with the minimal penalty as the penalty; the second identifies that penalty.

Milestones

1. (Section 5, p. 12) $\rho_\gamma$ is a conditional convex risk measure.
2. (Section 5, p. 12) $\rho_\gamma(X)=\operatorname{ess.inf}\{Y\in L^\infty_{\mathcal G}: X+Y\in A_\gamma\}=\operatorname{ess.inf}\{Y\in L^\infty_{\mathcal G}: E_P(e^{-\gamma X}\mid\mathcal G)\le e^{\gamma Y}\}$.
3. (Proof of Proposition 5.4) $\rho_\gamma$ is continuous from above: $X_n\searrow X$ implies $\rho_\gamma(X_n)\nearrow\rho_\gamma(X)$.
4. (Section 5, p. 13) For $Q\in\mathcal P_{\mathcal G}$: $E_P(\varphi\mid\mathcal G)=1$ and $H_{\mathcal G}(Q\mid P)=E_Q(\log\varphi\mid\mathcal G)$.
5. (Proof of Proposition 5.4) $\alpha^*(Q)=\frac1\gamma\operatorname{ess.sup}_{Z\in L^\infty}\{E_Q(Z\mid\mathcal G)-\log E_P(e^Z\mid\mathcal G)\}$.
6. (Lemma 5.5) The conditional Donsker–Varadhan formula

$$\operatorname{ess.sup}_{Z\in L^\infty}\{E_Q(Z\mid\mathcal G)-\log E_P(e^Z\mid\mathcal G)\}=H_{\mathcal G}(Q\mid P),\qquad Q\in\mathcal P_{\mathcal G}.$$

Significance

The result gives the conditional entropic risk measure an explicit dual description: the capital requirement is a worst case over conditional models, each penalized by its conditional relative entropy. This duality is what makes entropic risk measures computable in dynamic settings. Recursive compositions of $\rho_\gamma$ over a filtration are time consistent, and their penalties add up by the chain rule for conditional relative entropy. Lemma 5.5 is also the conditional form of the Donsker–Varadhan (Gibbs) variational principle, which is used on its own in large deviations and in PAC-Bayesian bounds.

On status: the results are proved in the paper, and the unconditional versions are textbook material. Mathlib has unconditional Kullback–Leibler divergence, tilted measures, conditional Jensen's inequality and a $[0,+\infty]$-valued conditional expectation. As far as the platform search could establish, neither the conditional relative entropy nor the conditional Donsker–Varadhan formula nor any conditional risk measure has been formalized. This mission produces the first machine-checked conditional version, with $H_{\mathcal G}$ allowed to be infinite.

Difficulty

In the unconditional case both sides of Lemma 5.5 are numbers, and the supremum is a supremum over reals. Conditionally, both sides are random variables. The supremum over the uncountable family indexed by $L^\infty$ must be taken in the essential sense, and a pointwise supremum is neither measurable nor meaningful. The conditional relative entropy can be $+\infty$ on a set of positive probability. The integrand $\varphi\log\varphi$ need not be integrable, so the usual conditional expectation of $L^1$ is not available for it, and the "$\ge$" direction must reach an unbounded target through bounded test variables while controlling $\log E_P(e^{Z}\mid\mathcal G)$ at the same time. The ess.sup in the goal ranges over measures, not random variables, and each $E_Q(\cdot\mid\mathcal G)$ is a conditional expectation under a different measure. These are identified with $P$-a.s. objects through the condition $Q=P$ on $\mathcal G$.

Formalization scope

• $(\Omega,\mathcal F,P)$ is a probability space (IsProbabilityMeasure P), and $\mathcal G$ is m : MeasurableSpace Ω with hm : m ≤ mΩ. Payoffs are real functions with MemLp X ⊤ P. $L^\infty_{\mathcal G}$ membership is StronglyMeasurable[m] plus MemLp ⊤. Every (in)equality between random variables is $P$-a.e.
• $\mathcal P_{\mathcal G}$ is the subtype of probability measures $Q\ll P$ with $Q(A)=P(A)$ for all $A\in\mathcal G$. This is equality on $\mathcal G$, not equivalence of measures.
• $E_P(\cdot\mid\mathcal G)$ and $E_Q(\cdot\mid\mathcal G)$ on bounded variables are Mathlib's conditional expectations P[·|m] and Q[·|m]. Bounded variables are integrable under every $Q\ll P$, so no junk value arises.
• $\rho_\gamma$ is the paper's closed form $\frac1\gamma\log E_P(e^{-\gamma X}\mid\mathcal G)$. The ess.inf descriptions are a milestone, and no positivity hypothesis on $X$ is imposed.
• $\varphi$ is the real part of the Radon–Nikodym derivative Q.rnDeriv P. $H_{\mathcal G}(Q\mid P)$ and $E_Q(\log\varphi\mid\mathcal G)$ are generalized conditional expectations, $E(f^+\mid\mathcal G)-E(f^-\mid\mathcal G)$, built from Mathlib's $[0,+\infty]$-valued condLExp and valued in EReal. The negative parts are integrable, so $+\infty-(+\infty)$ never arises. In EReal, a real number minus $+\infty$ is $-\infty$, which is how a model with infinite entropy drops out of the supremum.
• Essential suprema and infima are predicates (IsEssSup, IsEssInf) on a candidate $P$-a.e. measurable EReal-valued function. The candidate must dominate every member a.s. and lie a.s. below every a.s. upper bound.
• Continuity from above means: a.s. monotone convergence $X_n\searrow X$ in $L^\infty$ implies a.s. monotone convergence $\rho(X_n)\nearrow\rho(X)$.
• $\gamma$ is a real constant with $\gamma>0$. The random risk aversion of Remark 5.6 is not formalized.
• Ruled out: defining $H_{\mathcal G}$ through the Bochner conditional expectation P[φ * log φ | m] (which returns $0$ when $\varphi\log\varphi$ is not integrable) or $\alpha^*$ through a pointwise supremum would make the goal false or vacuous, and so would stating it for an abstract convex risk measure in place of $\rho_\gamma$. The formalization uses the extended-valued $H_{\mathcal G}$, the essential supremum, and the explicit $\rho_\gamma$.
• The mission is self-contained. It redefines conditional convex risk measures, $\mathcal P_{\mathcal G}$ and the essential supremum in its own namespace CondConvexRisk.Entropic and does not assume the general representation theorem (Theorem 3.2). The generalized conditional expectation and the conditional Donsker–Varadhan formula are reusable beyond risk measures. Contributions are welcome on the ess.sup API (existence, upward-directed families), on conditional monotone convergence for condExp, and on the conditional Jensen step for $x\log x$.

Selected references

• S. Detlefsen, G. Scandolo, Conditional and Dynamic Convex Risk Measures, SFB 649 Discussion Paper 2005-006, Humboldt-Universität zu Berlin, 2005 (the version formalized; published in Finance and Stochastics 9(4), 2005, https://doi.org/10.1007/s00780-005-0159-6).
• H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, de Gruyter, Berlin, 2002 (reference [8] of the paper).
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6:429–447, 2002. https://doi.org/10.1007/s007800200072
• M. D. Donsker, S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time, III, Comm. Pure Appl. Math. 29:389–461, 1976. https://doi.org/10.1002/cpa.3160290405

Motivation

Von Neumann's minimax theorem says that in a zero-sum game with real payoffs, Player I can guarantee an expected gain of at least the value $v$ and Player II can hold it to at most $v$. In a long series of plays, the law of large numbers turns this into a statement about the average payoff: I can make it exceed $v-\varepsilon$, II can keep it below $v+\varepsilon$, with probability approaching one.

Blackwell's 1956 paper asks the same question when the payoff of each play is a vector in $\mathbb R^N$ rather than a number. A single player then cannot optimize "the" payoff, and the natural question becomes geometric: can a player force the running average of the payoff vectors to converge to a prescribed set $S$, whatever the opponent does? The resulting notion, approachability, became a basic tool in repeated games with incomplete information (Aumann–Maschler), in the theory of calibration and regret minimization (Foster–Vohra; Hart–Mas-Colell), and in online learning, where no-regret algorithms and Blackwell approachability are known to be equivalent (Abernethy–Bartlett–Hazan 2011).

Timeline.

• 1928: von Neumann's minimax theorem for matrix games.
• 1954: Blackwell's maximal inequality for sums with negative conditional drift (On optimal systems, Ann. Math. Statist.), quoted in this paper as THEOREM 2.
• 1956: this paper. A sufficient condition for approachability (THEOREM 1), a complete characterization for closed convex sets (THEOREM 3) and for $N=1$, an example of a set that is neither approachable nor excludable, and a conjecture on weak approachability.
• 1992: Vieille proved Blackwell's conjecture that every set is weakly approachable or weakly excludable.

Setting

Fix integers $N\ge0$ and $r,s\ge1$, and a closed, bounded, convex set $X\subseteq\mathbb R^N$. The game is an $r\times s$ matrix $M=\|m(i,j)\|$ whose entries are probability distributions concentrated on $X$. Write $\bar m(i,j)$ for the mean of $m(i,j)$, $P$ for the simplex of mixed actions $p=(p_1,\dots,p_r)$ of Player I, and $Q$ for that of Player II.

A strategy $f=\{f_n\}_{n\ge0}$ of I is a sequence of measurable maps from the $n$-tuples $(x_1,\dots,x_n)$ of past outcomes to $P$; $f_0$ is a point of $P$. Strategies $g=\{g_n\}$ of II take values in $Q$. A play of $(f,g)$ is a sequence of random vectors $x_1,x_2,\dots$ such that, given $x_1,\dots,x_n$, the players draw $i$ and $j$ independently from $f_n(x_1,\dots,x_n)$ and $g_n(x_1,\dots,x_n)$, and $x_{n+1}$ is drawn from $m(i,j)$. The average payoff is $\bar x_n=\frac1n\sum_{i=1}^n x_i$, and $\delta_n$ is its distance from $S$.

A set $S\subseteq\mathbb R^N$ is approachable with $f^*$ if for every $\varepsilon>0$ there is $N_0$ such that for every strategy $g$ of II,

$$\mathrm{Prob}\{\delta_n\ge\varepsilon\text{ for some }n\ge N_0\}<\varepsilon .$$

It is excludable with $g^*$ if there is $d>0$ such that for every $\varepsilon>0$ there is $N_0$ such that for every strategy $f$ of I,

$$\mathrm{Prob}\{\delta_n\ge d\text{ for all }n\ge N_0\}>1-\varepsilon .$$

$S$ is approachable (excludable) if some strategy approaches (excludes) it. Finally, for $p\in P$ and $q\in Q$,

$$R(p)=\operatorname{conv}\Big\{\textstyle\sum_i p_i\bar m(i,j)\Big\}_{j=1}^{s},\qquad T(q)=\operatorname{conv}\Big\{\textstyle\sum_j q_j\bar m(i,j)\Big\}_{i=1}^{r}:$$

$R(p)$ is the set of expected payoffs I can guarantee to stay in by playing $p$, and $T(q)$ the set II can confine them to by playing $q$.

Formalization targets

Goal: THEOREM 3

For a closed convex set $S\subseteq\mathbb R^N$,

$$S\text{ is approachable}\iff S\cap T(q)\neq\emptyset\ \text{ for every }q\in Q,$$

and if $S\cap T(q_0)=\emptyset$ then $S$ is excludable with the stationary strategy $g_n\equiv q_0$. In particular every closed convex set is either approachable or excludable. Both sentences are part of the goal.

Milestones, in the paper's order

1. THEOREM 2: for $|z_k|\le1$ with $E(z_k\mid z_1,\dots,z_{k-1})\le-u\,E(|z_k|\mid z_1,\dots,z_{k-1})$ and $0<u<1$,

$$\mathrm{Prob}\{z_1+\dots+z_k\ge t\text{ for some }k\}\le\Big(\tfrac{1-u}{1+u}\Big)^t .$$

2. The LEMMA: a sequence satisfying the almost-supermartingale conditions (5), (6), (7) converges to $0$ at a rate depending only on the constants $a,b,c$.
3. In the proof of THEOREM 1, the squared distances $\delta_n^2$ satisfy (5)–(7) uniformly in II's strategy.
4. THEOREM 1: if every $x\notin S$ admits $p(x)\in P$ such that the hyperplane through a closest point $y\in S$, perpendicular to $xy$, separates $x$ from $R(p(x))$, then $S$ is approachable with any strategy playing $p(\bar x_n)$ when $\bar x_n\notin S$.
5. No set is both approachable and excludable.
6. If a closed $S$ is approachable in the transpose $M'$ with $f$, then every closed $T$ disjoint from $S$ is excludable in $M$ with $f$.
7. A closed convex $S$ meeting every $T(q)$ satisfies THEOREM 1's hypothesis.
8. Every $T(q_0)$ is approachable in $M'$ with $f_n\equiv q_0$.

Significance

The result. THEOREM 3 is the vector analogue of the minimax theorem. For a closed convex target it reduces an infinite-horizon stochastic question, about every strategy of the opponent over all histories, to a finite family of one-shot conditions on the mean matrix $\bar M$, and it shows that the game is determined for convex targets: one of the two players always wins. Its sufficient condition, THEOREM 1, is the origin of the "Blackwell strategy", which steers the average toward the target by playing, at each step, a mixed action that pushes the expected next payoff across the supporting hyperplane. Regret-matching, calibration algorithms and the reductions between online linear optimization and approachability are instances of this construction.

Formalizing it. The result is proved in the paper; to the best of available knowledge no machine-checked proof of it exists. This mission produces one: the stochastic model of a repeated game with vector payoffs, the probabilistic estimates (THEOREM 2 and the LEMMA) with the uniform rate the paper claims, and the minimax reduction for convex sets. A related platform mission, Introduction to Online Convex Optimization XIII, states a deterministic, sufficiency-only textbook variant for bounded sets; the present mission covers the stochastic model, unbounded convex targets, and the excludability half.

Difficulty

The obvious argument shows that the expected squared distance $E\delta_n^2$ decreases like $1/n$. That is not approachability: the definition asks for the probability that the average is ever again $\varepsilon$-far after time $N_0$, uniformly over the opponent's strategies. Controlling the whole tail of the path, with a threshold $N_0$ that does not depend on the opponent, is the step that fails for a naive expectation bound and is why the paper needs a maximal inequality for sums with negative conditional drift. On the geometric side, the "only if" direction is not automatic: it requires that approachability and excludability be incompatible, which in turn requires that a play of every pair of strategies exists.

Formalization scope

Points live in EuclideanSpace ℝ (Fin N); pure actions are Fin r and Fin s; mixed actions are elements of stdSimplex. The game is a structure carrying $X$ (closed, bounded, convex) and the distributions $m(i,j)$ (probability measures with $m(i,j)(X^{c})=0$). A play is described by the conditional law of the next outcome given the past, and approachability and excludability quantify over every probability space in Type carrying such a play. Distances are extended (Metric.infEDist), equal to $+\infty$ to the empty set.

Conventions and disclosed additions:

• $r,s\ge1$ where a statement needs both players to have strategies;
• strategies are measurable in the history;
• outcomes are indexed from $1$; (5) and (7) start at $n=2$, (6) at $n=1$;
• "the closest point" in THEOREM 1 is some closest point, and "separates" is weak separation;
• THEOREM 2 is stated with $E(|z_k|\mid\cdot)$ in place of the printed "max" (the weaker hypothesis, as in the cited source), and with $u<1$ so that $((1-u)/(1+u))^t$ is a real power.

$S$ is not assumed bounded or nonempty. With the real-valued distance, the empty set would be approachable with every strategy and THEOREM 3 would be false; the extended distance rules this out. Stating only the sufficiency direction, fixing the approaching strategy in the hypotheses, or assuming a play exists would each trivialize the goal, and none is done.

A complete development needs: conditional laws of the next outcome from a strategy pair (Ionescu–Tulcea, Kernel.traj in Mathlib), a nonnegative-supermartingale maximal inequality, the metric projection onto closed convex sets, and the minimax theorem (Mathlib's Sion theorem). The maximal inequality of THEOREM 2 and the LEMMA are reusable beyond this mission. Contributions to any milestone, and to a construction of plays, are welcome.

Selected references

• D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific J. Math. 6(1):1–8, 1956. https://doi.org/10.2140/pjm.1956.6.1
• D. Blackwell, On optimal systems, Ann. Math. Statist. 25(2):394–397, 1954. https://doi.org/10.1214/aoms/1177728796
• N. Vieille, Weak approachability, Math. Oper. Res. 17(4):781–791, 1992. https://doi.org/10.1287/moor.17.4.781
• J. Abernethy, P. Bartlett, E. Hazan, Blackwell approachability and no-regret learning are equivalent, COLT 2011. https://arxiv.org/abs/1011.1936
• S. Hart, A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68(5):1127–1150, 2000. https://doi.org/10.1111/1468-0262.00153

Motivation

A linear program is solved with known data, but in planning problems the data are often only known in distribution when the main decision is taken: demands, yields and requirements are revealed later, and a corrective action is taken after they are. E. M. L. Beale's 1955 paper On Minimizing a Convex Function Subject to Linear Inequalities formulates this situation in its §5, "Linear Programming with Random Coefficients", as what is now called a two-stage stochastic linear program with recourse. Beale's motivating example is the transportation problem of Hitchcock (1941) with random requirements at the destinations, where every unit of shortage or excess incurs a loss. The same model was put forward in the same year by Dantzig, Linear Programming under Uncertainty (Management Science, 1955), as the paper's note added in proof acknowledges.

Timeline:

• 1955. Beale (§5, Theorems 2 and 3) and Dantzig independently introduce two-stage linear programs with random data; Beale proves that the expected cost is convex in the first-stage decision, and that the cost is convex in the random data for fixed decision.
• 1967. Walkup and Wets, Stochastic Programs with Recourse, study the domain of the expected recourse function and its properties under fixed recourse.
• 1974. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, gives the systematic treatment of convexity, finiteness and polyhedrality of the expected recourse function, now textbook material (Birge and Louveaux, Introduction to Stochastic Programming, Ch. 3).

Setting

Constants $c\in\mathbb R^n$, $f\in\mathbb R^p$ and an $m\times p$ matrix $D=(d_{ik})$ are given. The data $A=(\alpha_{ij})$, an $m\times n$ matrix, and $\beta\in\mathbb R^m$ are random variables on a probability space $(\Omega,P)$: their distribution is known when the first-stage decision $x\in\mathbb R^n$, $x\ge0$, is chosen, and their values are known when the second-stage decision $y\in\mathbb R^p$, $y\ge0$, is chosen. The cost is

$$C=c'x+f'y,\qquad Ax+Dy=\beta. \qquad(5.3),(5.4)$$

For a right-hand side $b\in\mathbb R^m$ the second-stage value is

$$Q(b)=\min\{f'y : y\ge0,\ Dy=b\},$$

and for fixed data the cost of a first-stage decision is $C(x)=c'x+Q(\beta-Ax)$. The expected cost is

$$E(C)(x)=\int_\Omega \bigl(c'x+Q(\beta(\omega)-A(\omega)x)\bigr)\,dP(\omega).$$

The problem is to choose $x\ge0$ minimising $E(C)$. In Lean the value is secondStageValue D f b, the cost is cost c f D A β x, and the expected cost is expectedCost P c f D A β x, all in the namespace BealeConvexMin.RandomLP.

Formalization targets

Goal: Theorem 2 (p. 182)

Assume that for every $x\ge0$ the second-stage minimum is attained for almost every outcome and that $\omega\mapsto C(x,\omega)$ is integrable. Then

$$E(C)(\lambda_1x_1+\lambda_2x_2)\le\lambda_1E(C)(x_1)+\lambda_2E(C)(x_2)\qquad(x_1,x_2\ge0,\ \lambda_1,\lambda_2\ge0,\ \lambda_1+\lambda_2=1),$$

that is, $E(C)$ is convex on the non-negative orthant. The statement fixes no distribution class: it is claimed for any known distribution of $(A,\beta)$.

Milestones

1. Pointwise convexity (last display of the proof of Theorem 2, p. 182): for fixed data $(A,\beta)$, with the minimum attained at every $x\ge0$,

$$C(\lambda_1x_1+\lambda_2x_2)\le\lambda_1C(x_1)+\lambda_2C(x_2).$$

2. Theorem 3 (p. 182): for fixed $x$, the cost $(A,\beta)\mapsto c'x+Q(\beta-Ax)$ is jointly convex on every convex set of data on which the second-stage minimum is attained.
3. Eqs. (5.5)–(5.6) (p. 182): for a finitely supported distribution, $A=A_r$ and $\beta=\beta_r$ with probability $p_r$, the value $E(C)(x)$ is the minimum of $c'x+\sum_r p_r f'y_r$ over non-negative $y_r$ with $A_rx+Dy_r=\beta_r$ for all $r$; minimising $E(C)$ is then a linear program.

Significance

The result. Theorem 2 is the basic structural fact of two-stage stochastic linear programming: the first-stage problem is a convex program in $x$, whatever the distribution of the data. It is what makes local optimality global for the first-stage problem, what justifies cutting-plane and decomposition methods that approximate $E(C)$ from below by supporting hyperplanes, and what makes sample-average approximations convex programs. Theorem 3, joint convexity in the data, gives through Jensen's inequality the comparison between the stochastic problem and its mean-value problem that Beale draws on p. 182. The discrete reformulation (5.5)–(5.6) is the deterministic-equivalent linear program used for finitely many scenarios.

Formalizing it. The theorems are proved in the paper, and their content is classical. The mission produces machine-checked statements of the model with its implicit hypotheses made explicit (attainment of the second stage, integrability of the cost), and proofs of the three results in Lean. The platform already has related statements in other models (finite scenario sets with extended-real recourse, and a complete-recourse, finite-second-moment version); none has Beale's hypotheses, and none states convexity of $c'x+E\,Q$ for an arbitrary distribution.

Difficulty

The mathematics is short; the difficulty is in the encoding. The second-stage value is a minimum that may fail to exist: the second stage may be infeasible for some $x$ and some outcomes, or unbounded below. A real-valued infimum then takes an arbitrary default value, and convexity would become a statement about that default. Similarly, the mean value only exists when the cost is integrable. A faithful statement has to carry attainment and integrability exactly where the paper tacitly assumes them, on the domain $x\ge0$ the paper uses, and no stronger condition (such as complete recourse or moment bounds) that the paper does not make. In the discrete reformulation, the minimum over the whole family $(y_r)_r$ has to be matched with the probability-weighted sum of per-scenario minima.

Formalization scope

• Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, inner products dotProduct, and $y\ge0$ is the componentwise order. The random data are functions A : Ω → Matrix (Fin m) (Fin n) ℝ and β : Ω → Fin m → ℝ on a measurable space with a probability measure P; no measurability of the data is assumed beyond integrability of the cost.
• The second-stage value is the real infimum of $f'y$ over the feasible set. It equals $0$ on an infeasible or unbounded-below second stage, so each theorem assumes attainment of the minimum where it is evaluated (the paper's "value of $y$ that minimizes $C$"). The goal assumes attainment for almost every outcome at every $x\ge0$.
• $E(C)$ is the Bochner integral, which is $0$ for a non-integrable integrand, so the goal assumes integrability of $C(x,\cdot)$ at every $x\ge0$ (the paper's "mean value $E(C)$").
• Convexity is claimed on $\{x : x\ge0\}$, the paper's domain, not on all of $\mathbb R^n$. Theorem 3 is stated for fixed non-negative $x$ (the model's first-stage domain) and on every convex set of data on which the minimum is attained, since the paper names no domain.
• A formalization in which the value is an unconstrained infimum without attainment, or the expectation is taken without integrability, is trivially convex on the region where the default values apply and does not state Beale's theorem; such variants are ruled out.
• Reusable beyond this mission: basic facts on the optimal value of a parametric linear program in its right-hand side and cost data, and convexity of integrals of pointwise-convex integrands. Proofs of the milestones and of the goal, and alternative formulations in extended reals, are welcome.

Selected references

• E. M. L. Beale, On Minimizing a Convex Function Subject to Linear Inequalities, Journal of the Royal Statistical Society, Series B 17(2):173–184, 1955. https://doi.org/10.1111/j.2517-6161.1955.tb00191.x
• G. B. Dantzig, Linear Programming under Uncertainty, Management Science 1(3–4):197–206, 1955. https://doi.org/10.1287/mnsc.1.3-4.197
• F. L. Hitchcock, The Distribution of a Product from Several Sources to Numerous Localities, Journal of Mathematics and Physics 20:224–230, 1941. https://doi.org/10.1002/sapm1941201224
• D. W. Walkup and R. J.-B. Wets, Stochastic Programs with Recourse, SIAM Journal on Applied Mathematics 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
• R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

Many computations in scientific computing, statistics and machine learning need the trace of a matrix $A$ that is never formed explicitly: $A$ may be $f(B)$ for a large sparse $B$, an inverse $B^{-1}$, or a product of operators, and the only access to it is the ability to compute products $Az$ for chosen vectors $z$. Examples are log-determinant estimation in Gaussian process regression, counting triangles in graphs through $\mathrm{trace}(B^3)$, computing charge densities in electronic structure calculations, and generalized cross-validation in regularized regression. For such matrices the $n$ diagonal entries are not available, and computing them one at a time costs $n$ matrix–vector products.

Randomized trace estimators replace this by a small number $M$ of products: draw random vectors $z_1,\ldots,z_M$ from a fixed distribution with $\mathrm{E}(z_i^T A z_i) = \mathrm{trace}(A)$ and average the quadratic forms. Hutchinson (1989) introduced the estimator with Rademacher vectors and computed its variance; Silver and Röder (1997) used Gaussian vectors. Before Avron and Toledo (2011), the analyses of these estimators were variance computations, which do not say how many samples guarantee a given relative accuracy with a given probability. Avron and Toledo gave the first such sample bounds for several estimators, stated in terms of an $(\epsilon,\delta)$ guarantee; this mission formalizes their bound for the Gaussian estimator. Later work (Roosta-Khorasani and Ascher 2015; Cortinovis and Kressner 2022) sharpened these bounds and extended them to indefinite matrices.

Setting

Let $A \in \mathbb{R}^{n\times n}$ be symmetric positive semi-definite, and write $\tau = \mathrm{trace}(A)$. Fix a number of samples $M \ge 1$. Let $z_1, \ldots, z_M \in \mathbb{R}^n$ be random vectors whose $Mn$ entries are independent standard normal random variables. The Gaussian trace estimator (Definition 3.1) is

$$G_M = \frac{1}{M}\sum_{i=1}^{M} z_i^T A z_i .$$

Each term $z_i^TAz_i$ has expectation $\mathrm{trace}(A)$, so $G_M$ is unbiased. A randomized trace estimator $T$ is an $(\epsilon,\delta)$-approximator of $\mathrm{trace}(A)$ (Definition 4.1) if

$$\Pr\bigl(|T - \mathrm{trace}(A)| \le \epsilon\,\mathrm{trace}(A)\bigr) \ge 1-\delta ,$$

that is, if its relative error is at most $\epsilon$ except on an event of probability at most $\delta$.

The analysis uses the eigenvalues $\lambda_1,\ldots,\lambda_n \ge 0$ of $A$, listed with multiplicity, and the polynomial $h(t) = \sum_{s=2}^{n}(-2)^s t^s \sum_{|S| = s}\prod_{i\in S}\lambda_i$, where $S$ ranges over subsets of $\{1,\ldots,n\}$; it satisfies $\prod_i(1-2\lambda_i t) = 1 - 2\tau t + h(t)$.

Formalization targets

Goal: Theorem 5.2 (corrected)

For every symmetric positive semi-definite $A$, every $0 < \epsilon \le 1/10$, every $0<\delta<1$ and every natural number $M$ with

$$M \ge 20\,\epsilon^{-2}\ln(2/\delta),$$

the estimator $G_M$ is an $(\epsilon,\delta)$-approximator of $\mathrm{trace}(A)$. The sample count depends on neither $n$ nor $A$.

Milestones

1. Lemma 5.1. For symmetric $A$, $\mathrm{E}(G_1) = \mathrm{trace}(A)$ and $\mathrm{Var}(G_1) = 2\|A\|_F^2$.
2. Eq. (1). For symmetric $A$ and every $t$ with $2\lambda_i t < 1$ for all $i$, the moment generating function of $Z = MG_M$ is

$$m_Z(t) = \prod_{i=1}^{n}(1-2\lambda_i t)^{-M/2} = (1 - 2\tau t + h(t))^{-M/2}.$$

3. Elementary symmetric sums (p. 8:8). For non-negative $x_1,\ldots,x_n$ and $1\le i\le n$, $\sum_{|S|=i}\prod_{j\in S}x_j \le (\sum_j x_j)^i$; hence $|h(t)| \le \sum_{j=2}^{n}(2\tau t)^j$ for $t\ge0$ when all $\lambda_i\ge0$.
4. Upper tail (pp. 8:8–8:9). If $\tau > 0$, $M\ge1$ and $0<\epsilon\le 0.1$, then

$$\Pr\bigl(G_M \ge \tau(1+\epsilon)\bigr) \le \exp(-M\epsilon^2/20).$$

5. Both tails (p. 8:9). If $\tau>0$, $0<\epsilon\le0.1$ and $M \ge 20\epsilon^{-2}\ln(2/\delta)$, then $\Pr(G_M \ge \tau(1+\epsilon)) \le \delta/2$ and $\Pr(G_M \le \tau(1-\epsilon)) \le \delta/2$.

Significance

The theorem gives a number of matrix–vector products, $O(\epsilon^{-2}\ln(1/\delta))$, that suffices for a relative-error guarantee on the trace of any positive semi-definite matrix, independent of its dimension and spectrum. It is the reference row of the paper's Table I, against which the Hutchinson, normalized Rayleigh-quotient and unit-vector estimators are compared, and it is the form in which trace estimation enters the analysis of randomized algorithms for log-determinants, spectral densities and matrix functions.

The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The mission produces a machine-checked version with the constant $20$ and the range of $\epsilon$ made explicit, and with the misprints of the printed argument resolved (see Formalization scope). It also produces reusable pieces: the moment generating function of a Gaussian quadratic form, and the bound on elementary symmetric sums by powers of the power sum. Sharper constants, the removal of the restriction $\epsilon\le 0.1$, or a direct formalization of the lower tail through a $\chi^2$ tail bound are welcome as further theorems.

Difficulty

Unbiasedness and the variance formula do not give the result: Chebyshev's inequality with $\mathrm{Var}(G_M) = 2\|A\|_F^2/M \le 2\tau^2/M$ yields $M \ge 2\epsilon^{-2}\delta^{-1}$, with a polynomial rather than logarithmic dependence on $1/\delta$. A logarithmic bound needs exponential moments of $G_M$, and the exponential moment of $z^TAz$ is finite only for $t$ below $1/(2\lambda_{\max})$; the argument has to choose $t$ inside that range uniformly in the spectrum, using only $\lambda_{\max}\le\tau$. The second obstacle is distributional: $z^TAz$ is not a sum of independent terms in the coordinates of $z$, and reducing it to a weighted sum of independent $\chi^2$ variables requires the rotation invariance of the standard Gaussian vector. The paper proves only the upper tail with an explicit constant and states that the lower tail follows "using the same technique"; that step has to be supplied.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; "symmetric positive semi-definite" is A.PosSemidef, "symmetric" is A.IsHermitian, and eigenvalues are Matrix.IsHermitian.eigenvalues. The sample space is Fin M → Fin n → ℝ with the product measure of $Mn$ copies of gaussianReal 0 1, so the law of the samples is constructed, not assumed; $G_M(\omega) = (M:\mathbb{R})^{-1}\sum_i \omega_i\cdot(A\omega_i)$. Probabilities are Measure.real; the moment generating function is Mathlib's mgf; the variance is Mathlib's variance, and Lemma 5.1 asserts square integrability so that neither the integral nor the variance takes its default value. The sample count is a natural number $M\ge1$; $\epsilon$ and $\delta$ are real.

Corrections of the printed text, each recorded in the item's Formalization Note:

• Theorem 5.2 is printed without a range for $\epsilon$ and is false without one (for rank-one $A$, $\epsilon=100$, $\delta=e^{-400}$ the threshold allows $M=1$, while $\Pr(\chi^2_1>101)\approx e^{-50}>\delta$). The proof gives its key bound "for $\epsilon\le0.1$"; the goal is stated for $0<\epsilon\le 1/10$.
• Eq. (1) is printed for $|\lambda_i t|\le\frac12$, which admits $1-2\lambda_it = 0$, where the moment generating function is infinite. It is stated for $2\lambda_i t<1$. The page's sum over subsets of "the set $\Lambda$ of eigenvalues" is taken over index sets, so repeated eigenvalues count with multiplicity.
• The last paragraph of the proof prints $\Pr(G_M\le\tau(1+\epsilon))\le\delta/2$ for the upper tail and $\Pr(|G_M-\tau|\le\tau(1+\epsilon))\le\delta$ for the conclusion; the intended statements are $\Pr(G_M\ge\tau(1+\epsilon))\le\delta/2$ and $\Pr(|G_M-\tau|>\epsilon\tau)\le\delta$. Milestone 5 states the upper and lower tail bounds.
• Lemma 5.1 is followed by the remark that it "also applies when $A$ is non-symmetric"; this is false for the variance and is not formalized. Definition 3.1 says "positive-definite"; the estimator is defined for every matrix and each theorem carries its own hypothesis.
• The one-sided tail milestones assume $\mathrm{trace}(A)>0$; for $A=0$ their events are certain, while the goal holds trivially.

A formalization that makes the goal trivial is ruled out: the estimator's law is the explicit product Gaussian measure rather than a hypothesis, $M$ ranges over all natural numbers above the threshold, and the approximator predicate is evaluated on the genuine event $|G_M - \mathrm{trace}(A)|\le\epsilon\,\mathrm{trace}(A)$.

A complete development needs rotation invariance of the standard Gaussian on $\mathbb{R}^n$ (Mathlib's stdGaussian_map), the moment generating function of a squared standard normal, independence of products of Gaussian vectors, and a Chernoff bound from the moment generating function. The Gaussian quadratic-form results (milestones 1 and 2) are reusable for the other Gaussian estimators of the paper, such as the rank estimator of Lemma 5.3. Proofs of any milestone, alternative proofs of the lower tail, and helper lemmas on $\chi^2$ moment generating functions are welcome.

Selected references

• H. Avron and S. Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, Journal of the ACM 58(2), Article 8, 2011. https://doi.org/10.1145/1944345.1944349
• M. F. Hutchinson, A stochastic estimator of the trace of the influence matrix for Laplacian smoothing splines, Communications in Statistics – Simulation and Computation 18(3), 1059–1076, 1989. https://doi.org/10.1080/03610918908812806
• R. N. Silver and H. Röder, Calculation of densities of states and spectral functions by Chebyshev recursion and maximum entropy, Physical Review E 56(4), 4822–4829, 1997. https://doi.org/10.1103/PhysRevE.56.4822
• F. Roosta-Khorasani and U. Ascher, Improved bounds on sample size for implicit matrix trace estimators, Foundations of Computational Mathematics 15, 1187–1212, 2015. https://doi.org/10.1007/s10208-014-9220-1
• A. Cortinovis and D. Kressner, On randomized trace estimates for indefinite matrices with an application to determinants, Foundations of Computational Mathematics 22, 875–903, 2022. https://doi.org/10.1007/s10208-021-09525-9

Motivation

Retailers of fashion and seasonal goods sell at a premium price early in the season and mark down later. When customers anticipate the markdown, some of them wait, and the seller's pricing problem becomes a game between the seller and a population of forward-looking (strategic) customers. Aviv and Pazgal (MSOM 10(3), 2008) study this game in a model with limited inventory, stochastic arrivals and valuations that decline over the season, under two classes of seller policies: contingent pricing, where the discount depends on the inventory left, and announced fixed-discount pricing, where the seller commits to both prices upfront. Their numerical study (§7.3) compares the two classes and finds that precommitment can raise expected revenue by up to about 8%.

That comparison needs, for every announced price path, the customers' equilibrium response. Theorem 2 of the paper (p. 348) supplies it: a threshold purchasing policy, pinned down by a scalar fixed-point equation for the probability that a waiting customer is served. This mission formalizes Theorem 2. A companion mission of the same series formalizes Theorem 1, the contingent-pricing counterpart.

Setting

A seller has $Q \ge 1$ units to sell over a season $[0, H]$, split at a fixed time $T$ with $0 < T \le H$. Customers arrive by a Poisson process with rate $\lambda > 0$. Customer $j$ has a base valuation $V_j$ drawn from a continuous distribution $F$ (tail $\bar F = 1 - F$), and at time $t$ values the product at $V_j(t) = V_j e^{-\alpha t}$, where the decline factor $\alpha \ge 0$ is common to all customers.

Under an announced price path the seller commits to a premium price $p_1$ on $[0, T)$ and a discount price $p_2 \le p_1$ from $T$ on; $p_2$ does not depend on the remaining inventory. Customers know the initial inventory but not the current one.

A customer arriving at $t < T$ buys immediately if and only if (i) the current surplus $V(t) - p_1$ is nonnegative and (ii) it is at least the expected surplus of waiting,

$$\omega\cdot\max\{V(T) - p_2, 0\},$$

where $\omega$ is the probability that a unit will be allocated to the customer at time $T$. Units left at $T$ are rationed at random among the customers who request one.

For a threshold function $\psi$ on $[0, T)$ the paper defines three segment rates: $\Lambda_I(\psi)$, the expected number of customers who buy at $p_1$; $\Lambda_S(\psi, p_1, p_2)$, those who could buy at $p_1$ but wait and want to buy at $p_2$; and $\Lambda_W(p_1, p_2)$, those whose valuation was below $p_1$ and who want to buy at $p_2$. Each is $\lambda$ times an integral over $[0, T]$ of $\bar F$ at scaled prices (p. 345). With $P(x \mid \Lambda)$ the Poisson probabilities, the allocation probability of $q$ units is

$$A(q \mid \Lambda) = \sum_{y=0}^{\infty} \frac{q}{\max\{1+y, q\}}\,P(y \mid \Lambda).$$

Formalization targets

Goal: Theorem 2 (p. 348)

For $w \in [0,1]$ let

$$\psi_A(t) = \max\left\{p_1, \frac{p_1 - wp_2}{1 - we^{-\alpha(T-t)}}\right\},\qquad 0 \le t < T, \tag{7}$$

and suppose $w$ solves

$$w = \sum_{x=0}^{Q-1} P\big(x \mid \Lambda_I(\psi_A)\big)\cdot A\big(Q-x \mid \Lambda_S(\psi_A, p_1, p_2) + \Lambda_W(p_1, p_2)\big). \tag{8}$$

Then, when all other customers use $\psi_A$ (so that a waiting customer is served with the probability on the right of (8)), every customer arriving at $t \in [0, T)$ buys immediately if and only if $V(t) \ge \psi_A(t)$: the symmetric threshold profile is a Nash equilibrium.

Milestones: the two cases of the proof (p. 358)

1. If $e^{-\alpha(T-t)} \le p_2/p_1$, the threshold is $p_1$.
2. If $e^{-\alpha(T-t)} > p_2/p_1$, the threshold is $(p_1 - wp_2)/(1 - we^{-\alpha(T-t)}) \ge p_1$.

Significance

Theorem 2 reduces the customers' equilibrium under an announced path to a single scalar $w$. Everything downstream in §5 and §7 rests on it: the seller's expected revenue $\pi_{A/S}(p_1, p_2)$ (p. 348) is written in terms of $\psi_A$, the seller's optimal announced path maximizes it, and the comparison between announced and contingent pricing uses the resulting value $\pi^*_{A/S}$. The theorem also explains the qualitative prediction of the model: the threshold exceeds $p_1$ exactly when the announced discount is deep relative to the decline of valuations, and it rises with the perceived availability $w$.

The result is proved in the paper; to the best of our search it has no machine-checked proof. A formal development contributes the model objects (segment rates for threshold policies, the allocation probability for random rationing among Poisson requesters) in a form reusable by the rest of the series and by other strategic-customer pricing models, and a checked proof of the equilibrium property. The existence of a solution to (8) is not proved in the paper and is a natural further target.

Difficulty

The best-response part of the argument is elementary once the availability is known. The substance of the statement lies in the availability itself: the probability that a waiting customer is served is not a free parameter but the one generated, through (8), by the other customers' use of the same threshold. A formalization must connect the segment rates, the Poisson counts and random rationing into one expression and keep the fixed-point coupling between $w$ and $\psi_A$ intact; dropping it turns the theorem into a one-line inequality about an arbitrary $w$. The division by $1 - we^{-\alpha(T-t)}$ also degenerates when $w = 1$ and $\alpha = 0$, and has to be excluded explicitly.

Formalization scope

The Lean development lives in namespace SeasonalPricing.Announced. Conventions:

• Time is real; base valuations have law μ : Measure ℝ with IsProbabilityMeasure μ, $F$ = ProbabilityTheory.cdf μ, and continuity of $F$ (the paper's "continuous distribution") is a hypothesis of the goal. No support condition on $[0,\infty)$ is imposed; the statement quantifies over every real base valuation $V$.
• $\Lambda_I, \Lambda_S, \Lambda_W$ are interval integrals over $[0, T]$ exactly as printed. $P(x \mid \Lambda) = e^{-\Lambda}\Lambda^x/x!$ is written out; $A(q\mid\Lambda)$ is the infinite series (tsum) as printed, not its closed form.
• availability is the right-hand side of (8), with $\psi_A$ built from $w$ by (7).

Readings of the paper's informal words:

• "Nash equilibrium" is read as the best-response property the paper's proof checks: against the availability generated by (8), the immediate-purchase rule of p. 344 coincides with the threshold $\psi_A$ at every $t \in [0, T)$ and every valuation. The paper defines no strategy space beyond threshold rules.
• "$w$ is a solution to (8)": the theorem is conditional on a solution; its existence is neither assumed elsewhere nor claimed. The conditional statement has content only when (8) has a solution, which the paper does not prove.
• $w$ as a likelihood: $0 \le w \le 1$ is a hypothesis (it also follows from (8)).
• Added hypothesis: $\alpha > 0$ or $w < 1$, which keeps $1 - we^{-\alpha(T-t)} > 0$ for $t < T$; the paper's formula is undefined when it fails. In the milestones the same condition appears as $we^{-\alpha(T-t)} < 1$, and $0 < p_1$ is added so that $p_2/p_1$ is meaningful.
• The rule on $[T, H]$ (buy at $T$ iff $V(T) > p_2$) is part of the model and is not restated; $H$ does not enter the statements.

A formalization in which $w$ is an arbitrary number in $[0,1]$, not tied to (8), is ruled out: it is the best-response lemma alone, not Theorem 2. Contributions welcome: proofs of the two milestones and the goal; lemmas such as $0 \le A(q\mid\Lambda) \le 1$ and summability of its series; the closed form of $A(q \mid \Lambda)$ printed on p. 346; and an existence result for (8).

Selected references

• Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• X. Su, Intertemporal Pricing with Strategic Customer Behavior, Management Science 53(5):726–741, 2007. https://doi.org/10.1287/mnsc.1060.0667