Operations Research

Motivation

Firms that sell new products (consoles, books, films) often take preorders before release. A preorder serves two purposes at once. It lets the firm charge early adopters a different price from later buyers, a form of price discrimination, and the number of preorders is advance demand information: an early signal of how large regular-season demand will be. Li and Zhang (MSOM 15(1), 2013) ask whether better advance information always helps a seller who runs a preorder, when consumers are strategic and anticipate the seller's stocking decision. Their answer is no. The second-period stocking decision improves, but the preorder price can fall. Whether the net effect is positive depends on the low-type margin and the size of the early-adopter segment.

This mission formalizes that answer, §4 of the paper: the preorder profit as a function of the demand correlation $\rho$.

Setting

A seller sells a perishable product over two periods. High-type consumers, with valuation $v_H$, arrive in the first period and may preorder at price $p_1$. Low-type consumers, with valuation $v_L < v_H$, arrive in the second period, when the price is $p_2$. A high type who waits values the product at $\delta v_H$, where $\delta \le 1$ and $\delta v_H > v_L$. The unit cost is $c$, with $0 < c < v_L$. Unsold units have no salvage value and unmet demand carries no penalty. Write $\Delta = \delta v_H - v_L$.

The demands are jointly normal with correlation $\rho \in [0,1)$. The high-type demand has mean $\mu_H$, and $X$ denotes its standardization, a standard normal variable. The low-type demand has mean $\mu_L$, standard deviation $\sigma_L$ and $\lambda_L = \mu_L/\sigma_L$. Given $X = x$, the updated low-type demand $\tilde X_L(x)$ is normal with mean $\tilde\mu_L(x) = \mu_L + \rho\sigma_L x$ and standard deviation $\tilde\sigma_L = \sigma_L\sqrt{1-\rho^2}$. $\Phi$ and $\phi$ are the standard normal distribution function and density, and $z_L$ solves $\Phi(z_L) = (v_L - c)/v_L$.

In the second period the seller charges $p_2 = v_L$ and solves a newsvendor problem. It orders

$$Q(x) = \tilde\mu_L(x) + z_L\tilde\sigma_L \qquad (1)$$

and earns $\Pi_L(x) = (v_L - c)(\mu_L + \rho\sigma_L x) - v_L\phi(z_L)\sigma_L\sqrt{1-\rho^2}$ (2). A waiting high type believes half of the remaining consumers will be served before her, so her belief of product availability is

$$\xi(\rho) = \mathbb E\Big[\Pr\Big(\tfrac{\tilde X_L(X)}{2} < Q(X)\Big)\Big]. \qquad (3)$$

In the rational-expectations equilibrium every high type preorders at $p_1 = v_H - \Delta\xi$. The preorder profit is

$$\Pi^p(\rho) = (v_H - \Delta\xi(\rho) - c)\mu_H + \Pi_L(0). \qquad (4)$$

The threshold is

$$\tilde\mu(\rho) = -\frac{v_L\phi(z_L)\sigma_L}{2\Delta z_L\,\phi\big(2z_L\sqrt{1-\rho^2} + \lambda_L\big)}. \qquad (6)$$

Formalization targets

Goal: PROPOSITION 2

$$\begin{aligned} &\text{(i) } c < v_L < 2c:\ \Pi^p \text{ strictly increases on every interval where } \mu_H < \tilde\mu(\rho),\\ &\qquad\text{and strictly decreases on every interval where } \mu_H \ge \tilde\mu(\rho);\\ &\text{(ii) } v_L \ge 2c:\ \Pi^p \text{ strictly increases on } [0,1). \end{aligned}$$

Milestones

1. (1)–(2): $Q(x)$ is the unique maximizer of $\mathbb E[v_L\min(Q,\tilde X_L(x)) - cQ]$, and its value is $\Pi_L(x)$.
2. (3): $\xi(\rho) = \mathbb E\big[\Phi\big((\lambda_L + \rho X)/\sqrt{1-\rho^2} + 2z_L\big)\big]$.
3. LEMMA 1(i): if $c < v_L < 2c$, then $z_L < 0$ and $\xi$ is strictly increasing in $\rho$.
4. LEMMA 1(ii): if $v_L \ge 2c$, then $z_L \ge 0$ and $\xi$ is non-increasing in $\rho$, strictly so when $v_L > 2c$.
5. After (5): $\dfrac{d}{d\rho}\Pi_L(0) = v_L\phi(z_L)\sigma_L\,\rho/\sqrt{1-\rho^2} > 0$ for $\rho \in (0,1)$.
6. PROPOSITION 2(i), pointwise: for $\rho \in (0,1)$, $d\Pi^p/d\rho > 0 \iff \mu_H < \tilde\mu(\rho)$ and $d\Pi^p/d\rho < 0 \iff \mu_H > \tilde\mu(\rho)$.
7. LEMMA 2(i): if $-\lambda_L/2 < z_L < 0$, then $\tilde\mu$ is strictly increasing in $\rho$.
8. LEMMA 2(ii): if $z_L \le -\lambda_L/2$, then $\tilde\mu$ is quasi-convex in $\rho$.

Significance

The proposition splits the value of advance demand information into two effects with opposite signs. Better information always raises the second-period profit (milestone 5). Its effect on the preorder price depends on the margin. When $v_L < 2c$, the seller stocks below the conditional mean. A more precise forecast then raises the stock and the availability $\xi$, and waiting becomes more attractive, which lowers the preorder price. The threshold $\tilde\mu(\rho)$ says which effect wins, and LEMMA 2 describes its shape. This is the basis for the paper's later comparisons of preorder, price-guarantee and no-preorder strategies.

The paper states these results and leaves the proofs to an online appendix. None of them has a machine-checked proof. A complete development would also give reusable facts about normal laws: the expectation $\mathbb E[\Phi(a + bX)]$ for standard normal $X$, the normal newsvendor solution with its closed-form optimal profit, and derivatives of Gaussian integrals with respect to a correlation parameter.

Difficulty

The model is explicit, so the difficulty is not in modelling. It is in turning the two expectations into closed forms and differentiating them. The availability $\xi$ is an integral over $X$ of a normal probability whose mean and variance both move with $\rho$. The expected newsvendor profit involves $\mathbb E[\min(Q, Y)]$ for a normal $Y$. Neither closed form is in Mathlib, and neither is a derivative in $\rho$ of a Gaussian integral. The obvious route, differentiating under the integral sign in (3), needs domination estimates that are uniform in $\rho$ near each point, and these degenerate as $\rho \to 1$.

Signs are the second difficulty. $z_L$ changes sign at $v_L = 2c$, $\tilde\mu$ carries a leading minus and divides by $z_L$, and the derivative of $\Pi^p$ vanishes at $\rho = 0$ and wherever $\tilde\mu(\rho) = \mu_H$. Strict monotonicity on an interval has to be recovered from a derivative that is positive except at finitely many points.

Formalization scope

Everything lives in the namespace PreorderADI.Correlation. A structure Params holds $v_H, v_L, c, \delta, \mu_H, \mu_L, \sigma_L, z_L$. The predicate Params.Standing records the model's assumptions: $v_H > v_L$, $c < v_L$, $\delta \le 1$ and $\delta v_H > v_L$, together with $\Phi(z_L) = (v_L-c)/v_L$. $\sigma_H$ is omitted because nothing in §4 uses it after standardization. $\Phi$ is ProbabilityTheory.cdf (gaussianReal 0 1) and $\phi$ is gaussianPDFReal 0 1. The normal law with mean $m$ and standard deviation $s$ is gaussianReal m (s^2).

The formalization commits to the following conventions and additions:

• Added hypotheses. Four hypotheses are added to the page's assumptions:
  • $c > 0$, so that $z_L$ exists;
  • $\sigma_L > 0$, so that the conditional law is a genuine normal law;
  • $\mu_L > 0$, so that $\lambda_L > 0$, as LEMMA 2 presupposes;
  • $\mu_H > 0$, which PROPOSITION 2(ii) needs.
• $z_L$. $z_L$ is a parameter pinned down by $\Phi(z_L) = (v_L-c)/v_L$, not an inverse function with junk values.
• Range of $\rho$. $\rho$ ranges over $[0,1)$, the paper's "we will focus on $\rho \ge 0$" together with $\rho < 1$. Derivative statements use $(0,1)$.
• $\xi$ and $\Pi^p$. $\xi$ is defined as the first expression of (3), the expected probability, so that no closed form is assumed. $\Pi^p$ is defined by (4). PROPOSITION 1, which derives (4) as the unique equilibrium profit, is not formalized: the paper defines the equilibrium only through conditions that already assume every high type preorders.
• Monotonicity. "Increases in $\rho$ when $\mu_H < \tilde\mu(\rho)$" is formalized as strict monotonicity on every order-connected $I \subseteq [0,1)$ on which the condition holds. "Decreasing" in LEMMA 1(ii) is non-strict, since $\xi$ is constant when $v_L = 2c$. Quasi-convexity is Mathlib's QuasiconvexOn.
• The ε_v sentence is omitted. PROPOSITION 2(i) also claims that some $\varepsilon_v > 0$ makes $\Pi^p$ always decrease when $v_L < c + \varepsilon_v$. That claim is false in the paper's own model. As $v_L \downarrow c$, $\tilde\mu(\rho) \to \infty$ for $\rho$ below roughly $\sqrt 3/2$, so $\Pi^p$ increases there for every fixed $\mu_H$. The paper's Figure 1 shows the same behaviour.
• Out of scope. §5 rests on an approximation that treats normal demands as nonnegative, so it is excluded. §§6–7 depend on models given only in the online appendix and are excluded too.

A statement about the closed form $\Phi(\lambda_L + 2z_L\sqrt{1-\rho^2})$ in place of $\xi$ would make LEMMA 1 a one-line monotonicity fact. So would a definition of $\Pi^p$ that bypasses (3). The definitions rule both out.

Welcome contributions include proofs of the milestones, general Mathlib-style lemmas on Gaussian expectations of $\Phi$ and of $\min(Q, Y)$, and a formalization of PROPOSITION 1 from conditions (i)–(v).

Selected references

• C. Li and F. Zhang, Advance Demand Information, Price Discrimination, and Preorder Strategies, Manufacturing & Service Operations Management 15(1):57–71, 2013. https://doi.org/10.1287/msom.1120.0398
• G. P. Cachon and R. Swinney, Purchasing, Pricing, and Quick Response in the Presence of Strategic Consumers, Management Science 55(3):497–511, 2009. https://doi.org/10.1287/mnsc.1080.0948
• X. Su and F. Zhang, On the Value of Commitment and Availability Guarantees When Selling to Strategic Consumers, Management Science 55(5):713–726, 2009. https://doi.org/10.1287/mnsc.1080.0967

Motivation

Value-at-Risk (VaR) is the loss level that a portfolio exceeds with probability at most $\varepsilon$. It is the standard risk measure of banking regulation, and its classical computation assumes Gaussian returns: for a Gaussian return vector with mean $\hat x$ and covariance $\Gamma$ it equals $-\Phi^{-1}(\varepsilon)\sqrt{w^\top\Gamma w} - \hat x^\top w$, where $\Phi$ is the standard normal distribution function. Real returns are not exactly Gaussian, and a VaR computed from a misspecified distribution can badly understate risk.

El Ghaoui, Oks and Oustry (Oper. Res. 51(4), 2003) replace the single distribution by a class $\mathcal P$ of distributions and define the worst-case VaR as the smallest loss level whose probability is at most $\varepsilon$ under every distribution of the class. Their first class, distributions with a given mean and covariance, leads to the Chebyshev-type bound of their Theorem 1, whose worst case is attained by discrete distributions. §4.2 of the paper asks instead for distributions that stay close to a Gaussian, measured by relative entropy (Kullback–Leibler divergence). Such balls are the basic uncertainty sets of distributionally robust optimization and of robust control in economics (Hansen and Sargent's multiplier and constraint preferences), and they give a smooth worst case. Theorem 9 computes the resulting worst-case VaR in closed form.

Setting

Returns are random vectors $x \in \mathbb R^n$ and a portfolio is a vector $w \in \mathbb R^n$ with $w \neq 0$; its return is $r(w,x) = w^\top x$. For a level $\gamma \in \mathbb R$ the loss set is $\mathcal S_\gamma = \{x : \gamma \le -x^\top w\}$ (Eq. 13 of the paper).

Given a class $\mathcal P$ of probability distributions on $\mathbb R^n$ and $\varepsilon \in (0,1)$, the worst-case Value-at-Risk (Eq. 4) is

$$V_{\mathcal P}(w) = \min\Big\{\gamma \in \mathbb R : \sup_{P \in \mathcal P} P(\mathcal S_\gamma) \le \varepsilon\Big\}.$$

Fix a mean $\hat x \in \mathbb R^n$ and a positive definite covariance $\Gamma \succ 0$, and let $P_0 = \mathcal N(\hat x, \Gamma)$ be the reference Gaussian. For $d \ge 0$ the relative-entropy class (Eq. 43) is

$$\mathcal P_d = \Big\{P \text{ probability on } \mathbb R^n : \mathrm{KL}(P, P_0) = \int \log\frac{dP}{dP_0}\,dP \le d\Big\},$$

with $\mathrm{KL}(P,P_0) = +\infty$ unless $P$ is absolutely continuous with respect to $P_0$.

The risk factor (Eq. 45) is

$$f(\varepsilon,d) = \sup_{\lambda>0}\frac{e^{\varepsilon/\lambda - d} - 1}{e^{1/\lambda} - 1}, \qquad \kappa(\varepsilon,d) = -\Phi^{-1}\big(f(\varepsilon,d)\big),$$

and the Gaussian tail of the loss set is $\phi(\gamma) = P_0(\mathcal S_\gamma) = 1 - \Phi\big((\gamma + w^\top\hat x)/\sqrt{w^\top\Gamma w}\big)$.

Formalization targets

Goal: Theorem 9 (p. 553)

For $\Gamma \succ 0$, $w \neq 0$, $d \ge 0$ and $0 < \varepsilon < 1$, the minimum in (4) over $\mathcal P_d$ exists and

$$V_{\mathcal P_d}(w) = \kappa(\varepsilon,d)\sqrt{w^\top\Gamma w} - \hat x^\top w. \tag{44}$$

Milestones

The milestones follow the proof of Theorem 9 on pp. 553–554, in attack order.

1. Eq. (45). The two expressions of $f$ agree: $\sup_{\lambda>0}\frac{e^{\varepsilon/\lambda-d}-1}{e^{1/\lambda}-1} = \sup_{v>0}\frac{e^{-d}(v+1)^\varepsilon - 1}{v}$.
2. Gaussian tail. $P_0(\mathcal S_\gamma) = 1 - \Phi\big((\gamma + w^\top\hat x)/\sqrt{w^\top\Gamma w}\big)$.
3. Eq. (47). For $\lambda > 0$, the Lagrangian $L(Q) = Q(\mathcal S_\gamma) + \lambda_0(1 - Q(\mathbb R^n)) + \lambda(d - \mathrm{KL}\text{-integral})$ is maximised over finite measures $Q \ll P_0$ by the exponentially tilted density $dQ^\star/dP_0 = \exp((\chi_{\mathcal S} - \lambda_0)/\lambda - 1)$, with value

$$\theta(\lambda_0,\lambda) = \lambda_0 + \lambda d + \lambda e^{-\lambda_0/\lambda - 1}\big((e^{1/\lambda}-1)\phi(\gamma) + 1\big).$$

4. Eq. (48). $\min_{\lambda_0\in\mathbb R}\theta(\lambda_0,\lambda) = \lambda d + \lambda\log\big((e^{1/\lambda}-1)\phi(\gamma)+1\big)$.
5. Duality. $\sup_{P\in\mathcal P_d} P(\mathcal S_\gamma) = \inf_{\lambda>0}\big(\lambda d + \lambda\log((e^{1/\lambda}-1)\phi(\gamma)+1)\big)$.
6. Inversion. For $d > 0$: some $\lambda > 0$ makes the dual value at most $\varepsilon$ if and only if $\gamma \ge \kappa(\varepsilon,d)\sqrt{w^\top\Gamma w} - w^\top\hat x$.
7. Remark after Theorem 9. $f(\varepsilon, 0) = \varepsilon$, so $\kappa(\varepsilon,0) = -\Phi^{-1}(\varepsilon)$. The risk factor $\kappa(\varepsilon, d)$ is strictly increasing in $d \ge 0$.

Significance

Theorem 9 says that an entropy ball around a Gaussian leaves the form of the Gaussian VaR unchanged: only the risk factor moves, from $-\Phi^{-1}(\varepsilon)$ to $\kappa(\varepsilon,d)$, a scalar computed by a one-dimensional maximisation. The worst-case VaR therefore stays a convex function of $w$ whenever $\kappa \ge 0$, and minimising it over a polytope of portfolios is a second-order cone program (problem (3) of the paper). The number $f(\varepsilon,d)$ is the largest $p$ with $\mathrm{KL}(\mathrm{Bernoulli}(\varepsilon)\,\|\,\mathrm{Bernoulli}(p)) \le d$, which ties the result to the binary-divergence bounds used throughout information theory.

The theorem was proved in 2003. The worst-case-probability step (milestone 5) is an instance of the Donsker–Varadhan / Gibbs variational duality for relative-entropy balls, which the paper imports from the literature (Smith 1995). No machine-checked proof of Theorem 9 or of this duality on $\mathbb R^n$ is known. A formalization would give a verified closed form for a relative-entropy distributionally robust chance constraint, and the duality and tilting lemmas would serve any mission on KL-ball robust optimization.

Difficulty

The obvious argument is Lagrangian duality for the infinite-dimensional problem $\sup\{P(\mathcal S_\gamma) : \mathrm{KL}(P,P_0) \le d\}$. Weak duality and the pointwise maximisation that produces the tilted density are elementary. The difficulty is the step the paper cites rather than proves: that the duality gap is zero, and that the supremum over distributions equals the infimum of the dual over $\lambda > 0$. The feasible set is a set of measures, the objective is an indicator, and the constraint is a divergence that is $+\infty$ off a set of absolutely continuous measures, so a finite-dimensional Slater argument does not apply as stated.

The second difficulty is at the boundary of the parameters. At $d = 0$ the supremum defining $f(\varepsilon,0)$ is approached only as $\lambda \to \infty$, so the final inversion step behaves differently from $d > 0$. At $\varepsilon = 1$ the theorem is false, since every level $\gamma$ is feasible and (4) has no minimum.

Formalization scope

Returns live in EuclideanSpace ℝ (Fin n). $P_0$ is Mathlib's multivariateGaussian xhat Γ with Γ.PosDef, and $\mathrm{KL}$ is InformationTheory.klDiv, which is $\infty$ unless $P \ll P_0$ with integrable log-likelihood ratio and equals $\int\log\frac{dP}{dP_0}\,dP$ otherwise for probability measures. The class $\mathcal P_d$ requires IsProbabilityMeasure P. $\Phi$ is cdf (gaussianReal 0 1), and $\Phi^{-1}(p)$ is defined as $\inf\{t : p \le \Phi(t)\}$, which inverts $\Phi$ on $(0,1)$. The quadratic form $w^\top\Gamma w$ is a double sum, and $\|\Gamma^{1/2}w\|_2$ is written $\sqrt{w^\top\Gamma w}$.

Conventions the Lean statements commit to:

• "min" in (4) is IsLeast of the feasible set $\{\gamma : P(\mathcal S_\gamma) \le \varepsilon \ \forall P \in \mathcal P_d\}$. "$\sup_{P}P(\mathcal S_\gamma) \le \varepsilon$" is written "for every $P$", with probabilities compared in $[0,\infty]$.
• The paper prints $\varepsilon \in (0,1]$. The mission assumes $0 < \varepsilon < 1$, because the goal is false at $\varepsilon = 1$.
• $w \neq 0$ is the paper's assumption that the admissible set of portfolios excludes $0$.
• $f(\varepsilon,d)$ is a Lean sSup of a set that is nonempty and bounded above by $1$ for $\varepsilon \le 1$, $d \ge 0$.
• The duality of milestone 5 is stated as the existence of one real number that is both the least upper bound of the worst-case probabilities and the greatest lower bound of the dual values, not as an equality of Lean's sSup and sInf.
• Eq. (48) is stated as an attained minimum (IsLeast), which the calculus gives.
• Milestone 3 works with finite measures $Q \ll P_0$ with integrable log-likelihood ratio in place of the paper's densities $p$. It uses the complement of $\mathcal S_\gamma$ where the paper writes $\{\gamma \ge -x^\top w\}$, which differs by a $P_0$-null hyperplane.
• Milestone 6 assumes $d > 0$; the goal keeps $d \ge 0$.

Restricting $\mathcal P_d$ to $\{P_0\}$, dropping IsProbabilityMeasure, or taking an arbitrary reference measure would trivialize or change the theorem. The class is the full KL ball around the nondegenerate Gaussian.

Infrastructure a complete development needs: the pushforward of a multivariate Gaussian under a linear functional (a one-dimensional Gaussian), the Gibbs variational principle for relative entropy, the strong duality for KL balls, and properties of $\Phi$ and its quantile (continuity, strict monotonicity, symmetry $\Phi(-t) = 1 - \Phi(t)$). The Gaussian-quantile and KL-ball duality lemmas are reusable beyond this mission. Contributions of any of these as separate lemmas are welcome.

Selected references

• L. El Ghaoui, M. Oks, F. Oustry, Worst-Case Value-at-Risk and Robust Portfolio Optimization: A Conic Programming Approach, Operations Research 51(4):543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101
• J. E. Smith, Generalized Chebychev Inequalities: Theory and Applications in Decision Analysis, Operations Research 43(5):807–825, 1995. https://doi.org/10.1287/opre.43.5.807
• M. D. Donsker, S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time, I, Communications on Pure and Applied Mathematics 28(1):1–47, 1975. https://doi.org/10.1002/cpa.3160280102
• L. P. Hansen, T. J. Sargent, Robust Control and Model Uncertainty, American Economic Review 91(2):60–66, 2001. https://doi.org/10.1257/aer.91.2.60

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality $F(x) = F_0 + \sum_i x_i F_i \succeq 0$. When the data $F_i$ are uncertain, El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) proposed to optimize against the worst case over a norm-bounded family of perturbations: the robust SDP. Their Theorem 3.1 shows that, for unstructured ("full") perturbations, the robust SDP is itself an SDP in the enlarged variable $(x,\tau)$. Section 4 of the paper then asks what robustification does to the solution. Nominal SDPs are often ill-posed: the optimal set can be a whole face, and optimal points can jump under small data changes. Section 4 shows that, under explicit hypotheses, the robust problem has a unique solution with quadratic growth, which is the sense in which the paper describes robustness as a regularization of SDPs. This mission formalizes that result, Theorem 4.2.

Setting

Fix natural numbers $m, n, p, q$, matrices $F_0, \dots, F_m \in \mathbb{R}^{n\times n}$ (symmetric), $R_0, \dots, R_m \in \mathbb{R}^{q\times n}$, $L \in \mathbb{R}^{n\times p}$, and an objective vector $c \in \mathbb{R}^m$, $c \neq 0$. Write $F(x) = F_0 + \sum_{i=1}^m x_iF_i$ and $R(x) = R_0 + \sum_{i=1}^m x_iR_i$.

With full perturbations, uncertainty level $\rho = 1$ and $D = 0$ (the standing choices of §4), the robust SDP is the SDP

$$\text{minimize } c^Tx \quad\text{subject to}\quad \mathcal{F}(x,\tau) = \begin{bmatrix} F(x) - \tau LL^T & R(x)^T \\ R(x) & \tau I\end{bmatrix} \succeq 0 \tag{15}$$

in the variables $y = (x,\tau) \in \mathbb{R}^m \times \mathbb{R}$. A point is feasible if $\mathcal{F}(x,\tau) \succeq 0$ (symmetric positive semidefinite) and optimal if it is feasible and minimizes $c^Tx$ over all feasible $(x',\tau')$. The solution is the pair $(x,\tau)$.

The paper's hypotheses (§4.1):

• H1 (Slater): $\mathcal{F}(x,\tau) \succ 0$ for some $(x,\tau)$.
• H2 (inf-compactness): every sublevel set $\{(x,\tau)\ \text{feasible} : c^Tx \le M\}$ is bounded.
• H3(a): the nullspace of the pencil $\lambda R_0 + \sum_i x_iR_i$ is one and the same proper subspace $N \subsetneq \mathbb{R}^n$ for every $(\lambda,x) \neq (0,0)$.
• H3(b): for every $x$ the stacked matrix $\begin{bmatrix} L^T \\ R(x)\end{bmatrix}$ has full column rank.

For $\tau > 0$ put $G(x,\tau) = F(x) - \tau LL^T - \frac{1}{\tau}R(x)^TR(x)$, the Schur complement of the block $\tau I$ in $\mathcal{F}(x,\tau)$.

The quadratic growth condition (QGC) holds at an optimal point $y^\star = (x^\star,\tau^\star)$ if there are $\alpha, \varepsilon > 0$ with

$$c^Tx \ \ge\ c^Tx^\star + \alpha\,\|y - y^\star\|^2 \qquad \text{for every feasible } y = (x,\tau),\ \|y - y^\star\| < \varepsilon .$$

Formalization targets

Goal: Theorem 4.2 (p. 39)

Under $c \neq 0$, symmetry of the $F_i$, H1, H2, H3(a) and H3(b):

$$\bigl(\forall\, y^\star \text{ optimal for (15)}:\ \text{QGC holds at } y^\star\bigr)\quad\text{and}\quad \exists!\, y = (x,\tau) \text{ optimal for (15)} .$$

Both halves are stated; uniqueness is of the pair $(x,\tau)$, and existence is part of the claim.

Milestones, in the order the paper's proof uses them

1. §4.1 (p. 38): H3(a) implies $R(x) \neq 0$ for every $x$.
2. §4.2 (p. 39): under H3(a), every feasible $\tau$ is positive; in particular $\tau_{\mathrm{opt}} > 0$.
3. §4.2, Eq. (16): for $\tau > 0$, $\mathcal{F}(x,\tau) \succeq 0 \iff G(x,\tau) \succeq 0$.
4. Appendix A (p. 49): at every optimal $(x,\tau)$ there is a dual matrix $Z \succeq 0$, $Z \neq 0$, with $\operatorname{Tr} ZG(x,\tau) = 0$, $\operatorname{Tr} Z\,\partial G/\partial x_i = c_i$ and $\tau^2\operatorname{Tr}LL^TZ = \operatorname{Tr}R(x)^TR(x)Z$.
5. Appendix A (p. 49): H3(b) rules out $\operatorname{Tr}LL^TZ = \operatorname{Tr}R(x)^TR(x)Z = 0$ for $Z \succeq 0$, $Z \neq 0$, hence $\operatorname{Tr}R(x)^TR(x)Z > 0$.
6. Appendix A (pp. 49–50): under H3(a), with $\tau > 0$, $Z \succeq 0$ and $\operatorname{Tr}R(x)^TR(x)Z > 0$, the Hessian of the Lagrangian $c^Tx - \operatorname{Tr} Z\,G(x,\tau)$ is positive definite.

Significance

The result. Theorem 4.2 turns the robust SDP into a well-posed problem: a unique solution with quadratic growth. Quadratic growth is the property from which the paper's Hölder-stability results (Theorem 4.3, Corollaries 4.1–4.2) follow through the perturbation theory of Bonnans, Cominetti and Shapiro, and it is what justifies using the robust SDP as a regularization of ill-conditioned SDPs (§5.4). The remark after the theorem notes a geometric reading: the growth holds for every objective, so the boundary of the robust feasible set contains no facets.

Formalizing it. The theorem has a published proof (Appendix A), which relies on a second-order sufficient condition for nonlinear SDPs cited from Bonnans, Cominetti and Shapiro. There is no machine-checked proof of it or of any second-order optimality result for SDPs that we know of. A formalization provides a complete account of the dual attainment, complementarity and second-order steps for this concrete problem class, and it checks the paper's computations; one of them, the intermediate display for the second derivative in Appendix A, has a factor error in its cross term that does not affect the conclusion.

Difficulty

The feasible set of (15) is a spectrahedron, and linear objectives over spectrahedra do not in general have unique minimizers, since optimal faces can be flat. Uniqueness therefore cannot come from convexity alone. It has to come from curvature of the boundary at the optimum, and that curvature is carried only by the nonlinear term $\frac{1}{\tau}R(x)^TR(x)$ of the Schur complement, which is degenerate along some directions. Positive definiteness of the Hessian must be recovered from the structural hypotheses H3(a) and H3(b), which interact with a dual matrix $Z$ that is known only to exist. The natural first attempt is to use $\tau > 0$ and the positive semidefiniteness of $Z$ directly. That attempt fails: the second derivative is $\operatorname{Tr} Z\,\mathcal{R}^T\mathcal{R}$ for a direction-dependent matrix $\mathcal{R}$, which vanishes on the kernel of $Z$, so it is not positive without H3(a) relating the kernels of all members of the pencil. Dual attainment and complementarity for (15) also have to be established, and the local second-order bound then has to be converted into a statement about every nearby feasible point.

Formalization scope

• Representation. Data are bundled in RobustSDP.Uniqueness.SDPData m n p q; decision points are pairs y : (Fin m → ℝ) × ℝ; the coefficient Fs i, i : Fin m, is the paper's $F_{i+1}$. $\succeq 0$ and $\succ 0$ are Mathlib's Matrix.PosSemidef and Matrix.PosDef, which include symmetry, as the paper's notation does.
• Conventions fixed. §4's standing choices $D = 0$ and $\rho = 1$ are built into (15). The standing assumptions $c \neq 0$ and symmetric $F_i$ (p. 33) are explicit hypotheses. H2 is read as bounded sublevel sets of the feasible set in $(x,\tau)$; the paper's wording ("any unbounded sequence of feasible points produces an unbounded sequence of objectives") is meant in this sense, as its claim that H1 and H2 give existence of optimal points shows. H3(b)'s full column rank is injectivity of $\xi \mapsto (L^T\xi, R(x)\xi)$. The QGC uses the Euclidean norm on $\mathbb{R}^{m+1}$ in its local form, which is equivalent to the paper's $o(\|y - y_{\mathrm{opt}}\|^2)$ form. It is stated for (15) rather than for the paper's reformulation (16), with which (15) coincides near the optimum because $\tau_{\mathrm{opt}} > 0$. The auxiliary constraint $\tau \ge 0.99\,\tau_{\mathrm{opt}}$ of (16) is not formalized. $G$ uses Lean's τ⁻¹, which is $0$ at $\tau = 0$, so every statement about $G$ assumes $\tau > 0$ or $\tau \ne 0$.
• No trivializing reading. The goal cannot be satisfied by stating only uniqueness of $x$, by reading H2 as "the objective is bounded below", or by reading H3(a) as "$R(x) \neq 0$". The statement quantifies over the pair $(x,\tau)$, and both the quadratic growth and the existence and uniqueness halves are required. The hypotheses are jointly satisfiable: for example $m = 1$, $n = p = 2$, $q = 4$, $F(x) = \mathrm{diag}(3+x, 3-x)$, $L = I_2$, $R(x) = [1; x]\otimes I_2$ and $c = 1$.
• Infrastructure. A complete development needs Schur complements for positive semidefinite block matrices (available in Mathlib), strong duality with dual attainment for inequality-form SDPs under Slater's condition (ConvexOptimization.sdp_strong_duality on the platform, in another Mathlib environment), existence of minimizers on closed bounded sets, second derivatives of matrix-valued maps, and a local second-order argument for convex problems. The duality and second-order parts can be reused beyond this mission. Contributions to any milestone, or alternative proofs that avoid the general Bonnans–Cominetti–Shapiro theory, are welcome.

Selected references

• L. El Ghaoui, F. Oustry and H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1), 33–52, 1998. https://doi.org/10.1137/S1052623496305717
• J. F. Bonnans, R. Cominetti and A. Shapiro, Sensitivity analysis of optimization problems under second order regular constraints, Math. Oper. Res. 23(4), 806–831, 1998 (the paper's reference [10]). https://doi.org/10.1287/moor.23.4.806
• A. Shapiro, First and second order analysis of nonlinear semidefinite programs, Math. Programming Ser. B 77, 301–320, 1997. https://doi.org/10.1007/BF02614439
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Many firms learn part of future demand before it has to be served: customers place orders days or weeks ahead of the date they need the goods, or commit to delivery dates in contracts. Advance demand information of this kind reduces the uncertainty the inventory manager has to protect against, and the question is how replenishment decisions should use it. Gallego and Özer (Management Science 47(10), 2001) model orders placed up to $N$ periods ahead and a supply lead time $L$. They show that, with a fixed ordering cost, the classical $(s,S)$ structure survives with parameters that depend on the observed future demand, and they identify when that dependence disappears.

The classical theory this builds on is the finite-horizon inventory model with a set-up cost. Scarf (1960) introduced $K$-convexity to prove that $(s,S)$ policies are optimal there. Veinott (1966) and Iglehart (1963) bounded the optimal policy parameters by myopic quantities. Gallego and Özer extend both results to a state that carries a vector of observed demands.

Setting

Periods are $t = 1, \dots, T$. In period $t$ customers place orders $D_t = (D_{t,t}, \dots, D_{t,t+N})$ for periods $t, \dots, t+N$; $D_t$ is a random vector with law $\mu_t$ and nonnegative components. The lead time $L$ and the information horizon $N$ satisfy $N > L+1$; write $M = N - L - 1 \ge 1$. The state at the start of period $t$ is a pair $(x_t, o_t)$: the modified inventory position $x_t \in \mathbb{R}$, and the vector

$$o_t = (o_{t,t+L+1}, \dots, o_{t,t+N-1}) \in \mathbb{R}^M$$

of demands already observed for the periods beyond the protection period $t, \dots, t+L$.

The manager raises $x_t$ to an order-up-to level $y \ge x_t$, paying a set-up cost $K_t > 0$ if $y > x_t$. After $D_t$ is observed, the state moves to

$$x_{t+1} = y - \sum_{s=t}^{t+L+1} D_{t,s} - o_{t,t+L+1},\qquad o_{t+1,s} = o_{t,s} + D_{t,s}\ \ (s = t+L+2,\dots,t+N),$$

with $o_{t,t+N} = 0$. With a convex single-period cost $G_t$, discount factors $\alpha_t > 0$ and $\delta(z) = \mathbf 1\{z > 0\}$, the optimal cost satisfies $J_{T+1} \equiv 0$ and

$$J_t(x, o) = \min_{y \ge x}\{K_t\delta(y - x) + V_t(y, o)\},\qquad V_t(y, o) = G_t(y) + \alpha_{t+1}\,\mathbb E\,J_{t+1}(x_{t+1}, o_{t+1}).$$

Let $H_t(x, o) = K_t + \min_{y\ge x}V_t(y,o) - V_t(x,o)$. The order-up-to level $S_t(o)$ is the least minimizer of $V_t(\cdot, o)$, and the reorder point is $s_t(o) = \max\{x : H_t(x,o) \le 0\}$.

A function $g$ is $(a,b)$-convex, $g \in C(a,b)$, if $g(\theta x_1 + (1-\theta)x_2) \le \theta(a + g(x_1)) + (1-\theta)(b + g(x_2))$ for all $x_1 \le x_2$ and $\theta \in [0,1]$; $C(0,K)$ is Scarf's $K$-convexity. In the stationary problem $G_t = G$, $K_t = K$, $\alpha_t = \alpha$ and $\mu_t = \nu$, and the myopic levels are

$$S^m = \min\{y : G(y) \le G(x)\ \forall x\},\quad s^m = \max\{y \le S^m : G(y) \ge K + G(S^m)\},\quad \overline S = \inf\{y > S^m : G(y) > G(S^m) + \alpha K\}.$$

Formalization targets

Goal: Theorem 2 (p. 1350)

For the stationary problem, every $1 \le t \le T$ and every observed-demand vector $o_t \ge 0$,

$$o_{t,t+L+1} \ge \overline S - s^m \implies S_t(o_t) = S^m.$$

Only the observed demand for the first period beyond the protection period is compared with the threshold; the other components of $o_t$ are free.

Milestones

• Lemma 1, Parts 1, 2, 4, 5 (p. 1349): inclusion, positive combinations, expectations, and $g(\max(x,s))$ for $(a,b)$-convex functions.
• Lemma 2 and Corollary 1 (p. 1350): for $V \in C(0,K)$ with a minimizer $S$, $H$ changes sign once from $-$ to $+$, and (for continuous $V$) $J(x) = V(\max(s,x))$.
• Theorem 1, Parts 1–3 (p. 1350): $V_t(\cdot, o_t) \in C(0, K_t)$ is coercive, a state-dependent $(s_t(o_t), S_t(o_t))$ policy is optimal, and $J_t(\cdot, o_t) \in C(0, K_t)$ with its limits at $\pm\infty$.
• Lemma 3 (p. 1351): $S^m \le S_t(o_t) \le \overline S$ and $s^m \le s_t(o_t)$.

Significance

Theorem 1 says that advance demand information does not destroy the $(s,S)$ structure: the optimal policy is still a reorder point and an order-up-to level, now functions of $o_t$. Theorem 2 is a horizon result. Once enough demand is already booked for period $t+L+1$, the order-up-to level is the myopic one, computed from $G$ alone, and the rest of the information vector can be ignored. The threshold $\overline S - s^m$ grows with the set-up cost. In practice the manager then orders only to cover demand up to period $t+L$, knowing another order will be placed in period $t+1$, and the search for state-dependent policies is confined to states with little booked demand.

The results are proved in the paper, with some steps argued informally (the unit forward difference in Lemma 3, a minimum over an open set in the definition of $\overline S$). As far as the platform's catalog shows, no $(s,S)$ optimality theorem of this form has a machine-checked proof: the platform has $K$-convexity lemmas for a single constant, not for $(a,b)$-convexity or a dynamic program with a vector state. A formal proof would check the infinite-state induction and the conditions under which the expectation in (9) is finite. The $(a,b)$-convexity layer and the one-period results (Lemma 2, Corollary 1) are reusable for any set-up cost model.

Difficulty

The obvious induction proves $K$-convexity of $V_t$ and then applies Scarf's argument. The vector state makes each step conditional on facts the scalar case gets for free. The expectation in (9) mixes a random shift of $x$ with a random update of $o$, so preserving $K$-convexity needs Lemma 1, Part 4 rather than the scalar version. Coercivity and continuity of $V_t(\cdot, o)$, and measurability and integrability of $D \mapsto J_{t+1}(x_{t+1}, o_{t+1})$, must be carried through the induction jointly in $(x, o)$. They cannot be assumed.

For Theorem 2, $V_t$ is not a function of $G$ alone, and a comparison of $S_t(o_t)$ with $S^m$ has to control $\mathbb E J_{t+1}$. That requires the lower bound $s^m \le s_{t+1}(o_{t+1})$ at the next period, which holds only on the nonnegative state space.

Formalization scope

Everything is stated about the functional equation (8)–(9). The paper derives it in Appendix A from a control problem over history-dependent policies, citing Özer (2000); that reduction is out of scope. The demand vector is Fin (L + M + 2) → ℝ and $o$ is Fin M → ℝ, with component $j$ equal to $o_{t,t+L+1+j}$. $J$ is defined by backward recursion, minima over $y \ge x$ are infima over $\{y : x \le y\}$, and expectations are Bochner integrals. $G_t$ is an abstract primitive, not built from holding and penalty costs.

The paper's hypotheses are $G_t$ convex with $G_t(y) \to \infty$ as $|y| \to \infty$ (stated for $\widetilde G_t$, used for $G_t$), $K_t > 0$ (Section 4), and $\alpha_{t+1}K_{t+1} \le K_t$. The formalization adds hypotheses the paper uses without stating:

• positive discount factors;
• demands nonnegative almost surely;
• every demand component has a finite mean, and $|G_t(y)| \le a_t + b_t|y|$ (so the expectation in (9) is finite);
• continuity of $V$ in the abstract Corollary 1;
• nonnegative observed demands $o_t$ in Lemma 3 and Theorem 2, where the lower bound fails for negative $o_{t,t+L+1}$.

All hypotheses are placed on the primitives; nothing is assumed about the derived $V_t$ or $J_t$. A Solutions/verification instance ($G(y) = |y|$, $K = 1$, $\alpha = 1/2$, zero demand) shows these hypotheses can be met together.

The definition of $\overline S$ is read as an infimum: the paper prints a minimum over an open set. $S_t(o_t)$ and $s_t(o_t)$ appear through IsLeast and IsGreatest, never as sInf/sSup values. A default value therefore cannot satisfy a conclusion, and vacuous readings (an empty minimizer set, an unbounded reorder set) are excluded. The infinite-horizon results (Lemma 4, Theorem 3, Corollary 2) and the zero set-up cost case are not part of this mission. Contributions are welcome at every level, and most of all a reusable library for $(a,b)$-convex functions.

Selected references

• G. Gallego, Ö. Özer, Integrating Replenishment Decisions with Advance Demand Information, Management Science 47(10):1344–1360, 2001. https://doi.org/10.1287/mnsc.47.10.1344.10261
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• A. F. Veinott, On the Optimality of (s,S) Inventory Policies: New Conditions and a New Proof, SIAM Journal on Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259

Motivation

A correlated equilibrium (Aumann 1974) is a joint distribution over the players' strategy profiles such that no player gains by deviating from the strategy the distribution recommends to them. It is the equilibrium notion that learning dynamics in repeated games most naturally reach, and a basic question in learning in games is which simple rules, played repeatedly, drive the empirical distribution of play to the set of correlated equilibria.

Foster and Vohra (1997) answer this with a hypothesis on forecasts instead of a particular algorithm. Each player forecasts the other's next move and best-responds to the forecast. They only require the forecasts to be calibrated in the sense of Dawid (1982): among the rounds in which a player forecast a given probability vector, the empirical frequencies of the opponent's moves must approach that vector. Their Theorem 1 says that this already forces the empirical joint distribution of play to approach the set of correlated equilibria. The paper uses this to argue that Bayesian players under a common prior, whose forecasts are calibrated by Dawid's theorem, end up playing a correlated equilibrium. That is an alternative to Aumann's (1987) derivation of correlated equilibrium from common priors and rationality.

Timeline:

• Aumann (1974, 1987) introduces correlated equilibrium and derives it from Bayesian rationality.
• Dawid (1982) proposes calibration as a minimal requirement on probability forecasts.
• Foster and Vohra (1997) prove Theorem 1 (this mission) and show that calibrated forecasts exist once the forecaster may randomize.
• Hart and Mas-Colell (2000) give regret matching, an adaptive procedure with the same limit set.

Setting

A finite two-player game $G$ has strategy sets $S(1) = \{0, \dots, m-1\}$ and $S(2) = \{0, \dots, n-1\}$ and payoff matrices $u_1, u_2 : S(1) \times S(2) \to \mathbb{R}$, which the players maximize. A joint distribution $D$ is a nonnegative $m \times n$ matrix with entries summing to $1$. It is a correlated equilibrium if

$$\sum_{x,y} D(x,y)\, u_1(\Phi(x), y) \le \sum_{x,y} D(x,y)\, u_1(x,y) \quad \text{for all } \Phi : S(1) \to S(1),$$

and symmetrically for player 2. The set of correlated equilibria is $\pi(G)$.

The game is played in rounds $s = 0, 1, 2, \dots$. In round $s$ player 1 issues a forecast $f_1(s)$, a probability vector over $S(2)$, and player 2 issues a forecast $f_2(s)$ over $S(1)$. Each player then plays a best response to its forecast, $x(s) = R_1(f_1(s))$ and $y(s) = R_2(f_2(s))$. Here $R_1$ and $R_2$ are best-reply functions: $R_1(p)$ maximizes $\sum_y p_y u_1(\cdot, y)$ for every probability vector $p$, and $R_1$ is a fixed function of the forecast alone. This is the paper's standing assumption of a stationary, deterministic tie-breaking rule.

For a forecast sequence $f$ and the opponent's plays $z$, $N(p,t)$ counts the rounds among the first $t$ in which $f$ forecast $p$. $\rho(p,j,t)$ is the fraction of those rounds in which the opponent played $j$, and $0$ if there are none. The forecast is calibrated with respect to $z$ if for every $j$

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

The empirical joint distribution $D_t(x,y)$ is the fraction of the first $t$ rounds in which player 1 played $x$ and player 2 played $y$.

Formalization targets

Goal: Theorem 1

If $f_1$ is calibrated with respect to $y$ and $f_2$ is calibrated with respect to $x$, then

$$\min_{D \in \pi(G)} \ \max_{x \in S(1),\, y \in S(2)} |D_t(x,y) - D(x,y)| \longrightarrow 0 \qquad (t \to \infty).$$

The goal fixes no rate and no particular forecasting method: it asserts only convergence of $D_t$ to the set $\pi(G)$, for every calibrated forecast.

Milestones: the steps of the proof (pp. 44–45)

1. $D_t$ lies in the simplex for $t \ge 1$.
2. For each $x \in S(1)$, the set $M_b(x)$ of mixtures to which $x$ is a best response is closed and convex.
3. The mixtures $M_p(x)$ at which player 1 actually plays $x$ satisfy $M_p(x) \subseteq M_b(x)$.
4. The identity writing $D_t(x,y)$ as a forecast-weighted term plus a calibration error.
5. Calibration makes the error term vanish.
6. The weighted average of the forecasts at which player 1 plays $x$ lies in $M_b(x)$.
7. For a convergent subsequence $D_{t_i} \to D$, every row of $D$ with positive mass, normalized, lies in $M_b(x)$.
8. Every subsequential limit of $D_t$ is a correlated equilibrium.

Further result: matching pennies (p. 46)

With the constant forecast $(1/2, 1/2)$ and the non-stationary tie-break "heads on even rounds, tails on odd rounds", both forecasts are calibrated and every play is a best reply, yet $D_t$ does not approach $\pi(G)$. The stationarity assumption cannot be dropped.

Significance

The result. Theorem 1 separates what learning needs from how it is achieved. Any forecasting procedure that is calibrated, combined with myopic best responses, yields correlated equilibrium behaviour in the long run. The paper's Theorem 3 constructs a randomized calibrated forecaster, so the theorem gives an uncoupled learning procedure for correlated equilibrium, one that needs no knowledge of the opponent's payoffs. The converse direction, that every correlated equilibrium arises this way for almost every game, is the paper's Theorem 2 (a separate mission of this series).

Formalizing it. The theorem is proved in the paper and has no machine-checked proof on Prove2Me or, to the knowledge of this mission, elsewhere. The platform's existing correlated-equilibrium results (the Algorithmic Game Theory swap-regret development, AGT.swap_regret_correlated_equilibrium) reach correlated equilibrium through swap regret of mixed strategies, a different hypothesis and a different object. This mission adds a formal notion of calibration and the convergence argument, both reusable for the paper's Theorems 2 and 3 and for later work on calibration and learning.

Difficulty

The obvious reading of calibration is that each player's forecast converges to the opponent's empirical distribution; if that held, best responses to it would give convergence. It does not hold. Calibration constrains the opponent's frequencies only conditionally on the forecast issued, and the forecasts need not converge at all. What must be shown is a statement about the conditional distributions of the joint play given each strategy of player 1, while the set of forecasts issued keeps growing. Rows of the limit with zero mass carry no conditional distribution. The "min → 0" form also asks for more than a property of limit points: it is a uniform statement about all large $t$.

Formalization scope

• Strategies are Fin m and Fin n; payoffs are real matrices; forecasts are real vectors required to be probability vectors in every round.
• A correlated equilibrium is the joint-distribution form of p. 44 (the correlated strategy on a finite probability space is represented by its law). It is the $\varepsilon = 0$, two-player, payoff (not cost) instance of the published AGT.IsCorrelatedEquilibrium, restated rather than imported.
• The stationary deterministic tie-break is modelled by arbitrary best-reply functions $R_i$ of the forecast. They do not depend on the round, and the statements quantify over all of them, which includes the lowest-index rule.
• Forecasts are sequences $f_i : \mathbb{N} \to \mathbb{R}^k$. The theorem uses only the realized forecasts, and every sequence is realized by a rule reading the round number from the history.
• Rounds are indexed from $0$: "the first $t$ rounds" are $0, \dots, t-1$. $D_0 = 0$ by Lean's division convention; only $t \ge 1$ and limits are used.
• The calibration sum runs over the forecasts issued in the first $t$ rounds, which is the paper's sum over all $p$ with its zero terms removed. $\rho(p,j,t) = 0$ when $N(p,t) = 0$, as on the page.
• "min … → 0" is stated as: for every $\varepsilon > 0$, eventually some $D \in \pi(G)$ is within $\varepsilon$ of $D_t$ in every coordinate. The two forms are equivalent because $\pi(G)$ is compact and nonempty. The formalization avoids an infimum over $\pi(G)$, which Lean would evaluate to $0$ on an empty set.
• A statement that drops the best-reply property, the probability-vector condition on forecasts, or the stationarity of $R_i$ is not Theorem 1: the matching pennies example shows the last one is essential. Swapping the calibration hypotheses (player 1's forecast calibrated against player 1's own plays) type-checks when $m = n$ and is not the theorem.
• Only the two-player case is claimed. The paper says the results "generalize easily to the $n$-person case" without proof.

Proofs of any milestone, and reusable lemmas about calibration scores and compactness of the simplex of joint distributions, are welcome.

Selected references

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