Motivation

An insurance company's surplus grows with premiums and falls with claims. In the Cramér–Lundberg model with a positive safety loading, the surplus drifts to $+\infty$ with probability one. De Finetti (1957) objected that a company does not accumulate capital indefinitely: surplus above some level is paid out to shareholders. He proposed choosing the payout policy to maximize the expected discounted dividends paid before ruin. This is the optimal dividend problem. It is one of the basic stochastic control problems of actuarial mathematics and corporate finance, and it serves as a test case for singular control of processes with jumps.

The classical answer is a barrier strategy: pay out whatever lifts the surplus above a level $a$ and nothing else. Jeanblanc and Shiryaev (1995) proved this optimal when the surplus is a Brownian motion with drift, and Gerber and Shiu studied the same Brownian setting. Azcue and Muler (2005) showed that it can fail in the Cramér–Lundberg model, where the optimal policy may be a band strategy. Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007) 156–180) treated a general spectrally negative Lévy process, a process with stationary independent increments and only downward jumps. They found the value of every barrier strategy in closed form through the scale function of the process and identified the best barrier level $c^*$. They also gave a verification condition under which the barrier at $c^*$ is optimal among all strategies. Loeffen (2008) later showed that the condition holds whenever the Lévy measure has a completely monotone density.

Setting

Let $X=(X_t)_{t\ge0}$ be a spectrally negative Lévy process on a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ with $X_0=0$ and Lévy triplet $(c,\sigma,\nu)$. Its Laplace exponent is $\psi(\theta)=\log\mathbf E[e^{\theta X_1}]$, finite for $\theta\ge0$:

$$\psi(\theta)=c\theta+\tfrac{\sigma^2}{2}\theta^2+\int_{(-\infty,0)}\bigl(e^{\theta y}-1-\theta y\mathbf 1_{\{|y|<1\}}\bigr)\nu(dy).$$

Increments after time $s$ are independent of $\mathcal F_s$. Initial capital $x$ is added to $X$. The standing assumptions are the following: $X$ does not have monotone paths, $\mathbf E[X_1]>-\infty$, and either $\sigma>0$, $\int_{(-1,0)}|y|\,\nu(dy)=\infty$, or $\nu$ has a density.

A dividend strategy is a nondecreasing, left-continuous, adapted process $L$ with $L_0=0$. The risk process is $U_t=x+X_t-L_t$ and the ruin time is $\sigma^L=\inf\{t\ge0:U_t<0\}$. The strategy is admissible ($L\in\Pi$) if no lump sum exceeds the current reserves. Its value is

$$v_L(x)=\mathbf E\Bigl[\int_0^{\sigma^L}e^{-qt}\,dL_t\Bigr],\qquad v_*(x)=\sup_{L\in\Pi}v_L(x),$$

with discount rate $q>0$. For $C\in[0,\infty]$, $\Pi_{\le C}$ consists of the admissible strategies that keep $U_t\le C$ for $t>0$.

The $q$-scale function $W=W^{(q)}$ is the unique continuous nondecreasing function on $[0,\infty)$ with $\int_0^\infty e^{-\theta y}W(y)\,dy=1/(\psi(\theta)-q)$ for large $\theta$. It is extended by $W=0$ on $(-\infty,0)$. The barrier strategy $\pi_a$ reflects $x+X$ at the level $a$, paying $(x-a)^+$ at time $0$. The paper computes its value

$$v_a(x)=\frac{W(x)}{W'(a)}\ (0\le x\le a),\qquad v_a(x)=x-a+\frac{W(a)}{W'(a)}\ (x>a),$$

and the optimal barrier level is $c^*=\inf\{a>0: W'(a)\le W'(x)\ \forall x>0\}$, read as $0$ when this set is empty and $W'(0+)\le W'(x)$ for all $x>0$. The generator is

$$\Gamma f(x)=\tfrac{\sigma^2}{2}f''(x)+cf'(x)+\int_{(-\infty,0)}[f(x+y)-f(x)-f'(x)y\mathbf 1_{\{|y|<1\}}]\,\nu(dy).$$

Formalization targets

Goal: Theorem 2 (p. 14)

Assume $\sigma>0$, or $X$ has bounded variation, or $v_{c^*}\in C^2(0,\infty)$. Then $c^*<\infty$ and:

$$\text{(i)}\quad \pi_{c^*}\in\Pi_{\le c^*},\qquad v_{\pi_{c^*}}(x)=v_{c^*}(x)=\sup_{\pi\in\Pi_{\le c^*}}v_\pi(x)\quad(x\ge0);$$ $$\text{(ii)}\quad (\Gamma v_{c^*}-qv_{c^*})(x)\le0\ \ \forall x>c^*\ \Longrightarrow\ v_*(x)=v_{c^*}(x)\ (x\ge0),\ \ \pi_*=\pi_{c^*}.$$

The goal fixes no constants: the barrier level and the value function are both given by the scale function of the given process.

Milestones

• Proposition 1 (p. 7): $v_{\pi_a}(x)=W(x)/W'(a)$ for $a>0$, $x\in[0,a]$.
• Lemma 2(i) (p. 15): $c^*<\infty$.
• Proposition 3(i) (p. 15): $v_a(x)\le v_{c^*}(x)$ for $x\in[0,c^*]$, $a\ge0$.
• Lemma 3(i) (p. 16): $v_{c^*}'(x)\ge1$ for $x>0$.
• Proposition 4(i) (p. 18): a $C^2$ (unbounded variation) or $C^1$ (bounded variation) solution $w$ of $\max\{\Gamma w-qw,1-w'\}=0$ on $(0,C)$ dominates $\sup_{\Pi_{\le C}}v_\pi$.
• Lemma 4 (p. 20): $(\Gamma v_{c^*}-qv_{c^*})(x)=0$ on $(0,c^*)$ when $c^*>0$.

Significance

The theorem gives an explicit solution to a singular control problem for a general Lévy model. The candidate value function and barrier level are expressed through one special function, $W^{(q)}$, and optimality over all strategies reduces to one inequality on $(c^*,\infty)$. It is the basis of the later literature on scale-function methods in dividend problems (Loeffen 2008, Kyprianou–Rivero–Song 2010, and the refracted and Parisian variants). Part (i) holds with no condition on the Lévy measure. Part (ii) shows exactly where barrier optimality can fail.

The paper's proofs use fluctuation identities (exit problems, excursion theory) and Itô's formula for semimartingales with jumps. None of these is in Mathlib. As far as is known, none of these results has been machine-checked. A formalization would produce a Lévy-process and scale-function layer, a formal model of singular control with jumps and lump-sum payments, and a checked verification argument. Each of these can be reused beyond this paper.

Difficulty

The analytic part is elementary once the value formula (5.1) is available: the choice of $c^*$, Proposition 3(i) and Lemma 3(i) follow from the shape of $W'$. The difficulty lies in the two probabilistic steps. Proposition 1 identifies the value of a reflected process through exit identities for $X$. Those identities rest on excursion theory, or on the martingale property of $e^{-qt}W(X_t)$ up to exit. The verification step, Proposition 4(i), needs Itô's formula for $w(U_t)$. Here $U$ is a jump process controlled by a left-continuous finite-variation process that may itself jump. The change-of-variables formula must also run under only $C^1$ regularity when $X$ has bounded variation. Just proving that $\Gamma w-qw\le0$ and $w'\ge1$ imply a supermartingale inequality does not settle the question: the lump-sum payments and the jumps of $X$ enter the Itô expansion separately and must each be bounded.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0). $X$ is a structure carrying the triplet $(c,\sigma,\nu)$ and pathwise càdlàg paths with only downward jumps. It also carries independence of increments from the filtration and stationarity. Its law is fixed by the Laplace transform $\mathbf E[e^{\theta X_t}]=e^{t\psi(\theta)}$ for $\theta\ge0$. The standing assumptions of §2 and (3.3) are bundled as one predicate. The scale function is a hypothesis on a function argument $W$ (it is unique). $W'(0+)$ is an extended real, since it is $+\infty$ for unbounded variation without a Gaussian part.

Values of strategies and value functions lie in $[0,\infty]$. The dividend integral is a Lebesgue–Stieltjes integral over $[0,\sigma^L)\cup\{0\}$: it counts the lump sum at time $0$ and excludes a payment at the ruin instant.

Several conventions are fixed, and each is disclosed in the item it affects:

• Admissibility. The paper requires $L_{t+}-L_t<U_t$. The formalization uses $\le$, because the paper's own strategy of paying out everything at once needs it.
• Barrier level (5.2). Printed over $a>0$ and "all $x$", the defining set is empty for Brownian motion with nonpositive drift. The printed set (with $x>0$) is kept whenever it is nonempty; when it is empty and $W'(0+)\le W'(x)$ for all $x>0$ — the second alternative in the proof of Lemma 2(i) — $c^*=0$, and otherwise $c^*=\infty$.
• Printed slips. The integral $\int_{-1}^0 x\,\nu(dx)$ in (3.3) is read as $\int|x|\,\nu(dx)$. In (3.4), $e^{-\theta x}$ is read as $e^{-\theta y}$, and in Theorem 2(i), $\pi^*_c$ is read as $\pi_{c^*}$.
• Proposition 4(i) is stated for initial capital $x\le C$. Beyond $C$, $w$ is unconstrained and the printed claim fails.
• Lemma 4 carries the smoothness proviso of Theorem 2 on $(0,c^*)$.

A trivializing encoding is ruled out: the value is not a real supremum, the barrier strategy is constructed rather than assumed, and $c^*<\infty$ is a conclusion.

A complete development needs:

• Lévy processes and their Laplace exponents;
• scale functions and the exit identity $\mathbf E_x[e^{-qT}\mathbf 1_{\{X_T=a\}}]=W(x)/W(a)$;
• reflected processes;
• Itô's formula for jump semimartingales with finite-variation controls.

The Lévy and scale-function layer is shared with the companion mission on the bail-out problem. Contributions of general lemmas (Stieltjes integration by parts, optional stopping for càdlàg martingales) are welcome.

Selected references

• F. Avram, Z. Palmowski, M. R. Pistorius, On the optimal dividend problem for a spectrally negative Lévy process, Ann. Appl. Probab. 17 (2007) 156–180. https://arxiv.org/abs/math/0702893
• P. Azcue, N. Muler, Optimal reinsurance and dividend distribution policies in the Cramér–Lundberg model, Math. Finance 15 (2005) 261–308.
• M. Jeanblanc-Picqué, A. N. Shiryaev, Optimization of the flow of dividends, Russian Math. Surveys 50 (1995) 257–277.
• R. L. Loeffen, On optimality of the barrier strategy in de Finetti's dividend problem for spectrally negative Lévy processes, Ann. Appl. Probab. 18 (2008) 1669–1680.
• A. E. Kyprianou, Introductory Lectures on Fluctuations of Lévy Processes with Applications, Springer, 2006. https://doi.org/10.1007/978-3-540-31343-4

Motivation

Before a queueing network's stability can be studied in any depth, a much cruder question has to be settled: is stability even possible for the given arrival rates and service capacities, under any control policy at all? For a single M/M/1 queue the answer is the familiar $\lambda < \mu$, but a general stochastic processing network (SPN) — many buffers, many activities, servers that can be pooled or shared across job classes — has no single scalar "utilization" to compare against a threshold. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) answers this with a linear program: the static planning problem, first formulated by Harrison (2000). This mission formalizes the theorem that answers the crude question in one direction — no control policy can stabilize a network outside the region that program identifies — which is why, as the book puts it, "throughout the remainder of this book, attention is essentially restricted to subcritical networks."

Setting

An SPN has $I$ buffers, indexed by $i \in \mathcal{I}$, and $J$ activities, indexed by $j \in \mathcal{J}$. Its first-order data — the quantities that matter for a capacity calculation, as opposed to full stochastic detail — are: the $I \times J$ material requirement matrix $B$ ($B_{ij}$ = number of class-$i$ items one type-$j$ service consumes), the $I \times J$ mean output matrix $\Gamma$ (its $j$th column is the expected output vector of a type-$j$ service), the mean service times $m_j > 0$, the $K \times J$ capacity consumption matrix $A$ (server pool $k$ against activity $j$), and the server-pool capacities $b \in \mathbb{R}_+^K$. From these,

$$R := (B - \Gamma)M^{-1}, \qquad M := \operatorname{diag}(m_1, \dots, m_J),$$

so that $R_{ij}$ is the long-run average rate at which activity $j$ depletes buffer $i$'s content.

Given an arrival-rate vector $\lambda \in \mathbb{R}_+^I$, the static planning problem (SPP) is the linear program

$$\gamma^\ast(\lambda) := \min_{x \ge 0,\, \gamma} \ \gamma \quad \text{s.t.} \quad Rx = \lambda, \quad Ax \le \gamma b,$$

whose decision variable $x_j$ is a long-run average activity rate and whose objective $\gamma$ upper-bounds every server pool's utilization. The network is subcritical at $\lambda$ if $\gamma^\ast(\lambda) < 1$, and the subcritical region is $\Lambda := \{\lambda : \gamma^\ast(\lambda) < 1\}$.

An SPN is stable (Definition 3.6, mission I) when its ambient Markov chain is positive recurrent, equivalently has a unique stationary distribution, equivalently its buffer contents converge in distribution to a non-defective limit. This mission's chapter portion (Chapters 4-5) also treats three extensions used elsewhere in the book: a Markovian arrival process replacing independent Poisson arrivals; alternate routing with immediate commitment, where arrivals must be routed into an eligible buffer at the instant they arrive, with routing rates constrained by an augmented version of the SPP; and processor sharing (PS) networks, whose service discipline falls outside the book's ordinary relaxed-control framework and is instead analyzed through an equivalent head-of-line (EHL) model built to have the same generator.

Formalization targets

Goal: Theorem 5.2 — only subcritical networks can be stable

$$\text{(baseline stochastic assumptions)} \ \wedge \ \text{(Markov representation)} \ \wedge \ \text{(SPN stable)} \implies \lambda \in \Lambda.$$

This is the weakest target that captures the chapter's content: it asserts nothing about which policy achieves stability, or whether subcriticality is sufficient (Chapters 6 onward answer that, case by case, and Chapter 5 itself gives two counterexamples where it is not) — only that subcriticality is unconditionally necessary.

Further results (milestones)

Proposition 4.1 (a strong law of large numbers for class-level arrivals under randomized routing), Proposition 4.4 (PS-network stability reduces to EHL-model stability), Proposition 5.1 (for a unitary network, subcriticality reduces to the classical load condition $\rho < b$), and Corollaries 5.4-5.6 (the same necessity conclusion under a Markovian arrival process, under alternate routing, and its consequence for maximally stable policies).

Significance

The result itself. Theorem 5.2 converts "can this network be stabilized at all?" from an open-ended search over control policies into a single linear-program feasibility check on first-order data alone. Corollary 5.6 turns this into the standard proof template every later chapter uses: exhibit a policy whose implementation does not reference $\lambda$, show it is stable throughout the subcritical region, and conclude maximal stability — without having to separately characterize the true stability region $\Lambda^\ast$, which the book calls "a deep mathematical problem" in general.

Formalizing it. A search of the platform for "processing network," "static planning problem," and "linear program" returned no hits: the SPN-specific static planning problem — its decision variables $x$ tied to a network's material-balance matrix $R$ and capacity matrix $A$ — has no existing counterpart, though the platform's linear-optimization field (16 missions) has general LP duality substrate a future proof of Proposition 5.1 or Theorem 5.2 could draw on. This mission is a from-scratch formalization of the SPP, the subcritical region, and the necessity theorem.

Difficulty

The natural first attempt states Theorem 5.2 as a claim about the buffer-contents process $Z(t)$ directly. This fails to separate cleanly from the proof, because the actual argument passes through an auxiliary quantity — the stationary mean $x := \mathbb{E}_\pi[N(0)]$ under the chain's (unique, by stability) stationary distribution $\pi$ — that has no meaning outside a specific proof strategy. The formalization instead states the goal purely in terms of the data $(R, A, b)$ and the hypothesis of stability, exactly as the book's own statement does, leaving $x$'s construction to the (currently sorry) proof. A second difficulty is Corollary 5.4's Markovian arrival process: naively reusing BaselineAssumptions with a non-Poisson arrival process is impossible, since Poisson-ness is a mandatory structural field of that definition, not an optional hypothesis — the corollary needs its own hypothesis structure that changes exactly the one clause Assumption 2.1(a) contributes and nothing else.

Formalization scope

Buffers and activities are Fin I, Fin J; matrices are Matrix over ℝ. The subcritical region is defined via the optimal SPP value $\gamma^\ast$, formalized with Mathlib's IsLeast (attained infimum, matching the book's own "$\gamma^\ast \le 1$ iff $x$ exists" phrasing, which presupposes attainment) rather than a bare existential — a formalization using, say, sInf would silently commit to junk values on an infeasible or unbounded LP and would not obviously match the book's own usage of $\gamma^\ast$ as literally attained. The basic SPN model's full state-process construction (Sections 2.3-2.4) is not re-derived from scratch here; Theorem 5.2 instead takes the structural facts its own proof invokes — the capacity constraint $AN(t) \le b$ (Eq. 2.11) and the material-requirement matrix $B$ — as explicit data, reusing mission I's BaselineAssumptions and MarkovRepresentation for the stochastic and Markov-chain apparatus. Proposition 4.4's shared- generator fact between a PS network and its EHL model (the actual content the book's construction of Section 4.4 establishes) is likewise taken as an explicit hypothesis rather than rebuilt from the refined-class/phase-type machinery of Eqs. (4.19)-(4.29); reconstructing that machinery from scratch, or reproving Proposition 4.1's SLLN from the chain's strong Markov property at regeneration times, are both welcome future contributions. A formalization that stated Theorem 5.2 with $\Lambda$ replaced by an unconstrained existential (dropping the LP structure entirely) would trivialize the chapter's actual content — the LP-feasibility characterization is what makes $\Lambda$ checkable, and is preserved here in full.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• J. M. Harrison, "Brownian models of open processing networks: canonical representation of workload," Annals of Applied Probability 10 (2000), 75-103.
• J. G. Dai and W. Lin, "Maximum pressure policies in stochastic processing networks," Operations Research 53 (2005), 197-218.

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 forecaster who announces "70% chance of rain" is calibrated if, among the days on which that number was announced, it rained on about 70% of them. Dawid (The well-calibrated Bayesian, JASA 1982) proposed calibration as the minimal requirement of an honest probability forecaster. Oakes (Self-calibrating priors do not exist, JASA 1985) showed that no deterministic forecasting rule can be calibrated against every sequence of outcomes: an adversary who knows the rule can always choose the outcome that contradicts the forecast.

Foster and Vohra (Calibrated learning and correlated equilibrium, Games Econ. Behav. 21 (1997) 40–55) use calibration as the bridge between learning and equilibrium in repeated games. Their Theorem 1 says that if each player best-responds to calibrated forecasts of the opponent, the empirical distribution of play converges to the set of correlated equilibria. That theorem is only useful if calibrated forecasts can actually be produced whatever the opponent does. Theorem 3 of the paper, credited to an unpublished 1991 manuscript of the same authors and proved in the paper's Appendix, says they can, provided the forecaster randomizes.

Timeline. Dawid (1982) defines calibration. Oakes (1985) rules out deterministic calibrated forecasting against arbitrary sequences. Foster and Vohra (1991 manuscript; 1997 paper, Theorem 3 and Appendix) give a randomized forecaster calibrated against any opponent, through a pairwise ("internal") no-regret property. The full argument appeared in Foster and Vohra, Asymptotic calibration, Biometrika 85 (1998). Hart and Mas-Colell (A simple adaptive procedure leading to correlated equilibrium, Econometrica 2000) later made internal regret the standard route to correlated equilibrium.

Setting

Player 2 has $n\ge 1$ pure strategies $j\in\{0,\dots,n-1\}$. In every round, player 1 announces a forecast $p\in\mathbb R^n$, a probability vector ($p_j\ge 0$, $\sum_j p_j = 1$), and player 2 plays a strategy $j$. The two moves are simultaneous: player 2 does not see the current forecast.

A history $h$ of length $t$ is the list of the $t$ pairs (forecast, play), oldest first. For a forecast vector $p$ and a strategy $j$:

• $N(p,t)$ is the number of rounds of $h$ in which $p$ was forecast;
• $\rho(p,j,t)$ is the fraction of those rounds in which player 2 played $j$ (and $0$ if $N(p,t)=0$);
• the calibration score (Eq. (1), p. 49) is

$$C_t = \sum_p\sum_j \bigl|\rho(p,j,t) - p_j\bigr|\,\frac{N(p,t)}{t}.$$

A randomized forecaster $F$ maps each history to a probability distribution on forecasts. A learning rule $A$ of player 2 maps each history to a probability distribution on strategies. In round $t+1$ the forecast is drawn from $F(h)$ and the play from $A(h)$, independently given the history $h$ of the first $t$ rounds. This defines the law $\mathbb P_{F,A}$ of the first $t$ rounds (histLaw F A t).

For the Appendix: with $k$ forecasts, losses $L_t^i$ and mixing weights $w_t^i$, the pairwise regret of replacing forecast $i$ by forecast $j$ is

$$R_T^{i\to j} = \max\Bigl\{0,\ \sum_{t=1}^T w_t^i\,(L_t^i - L_t^j)\Bigr\}.$$

Formalization targets

Goal: Theorem 3 (p. 49)

There is a forecaster $F$, with probability-vector forecasts, such that for every learning rule $A$ of player 2 and every $\varepsilon>0$,

$$\lim_{t\to\infty}\mathbb P_{F,A}\bigl(C_t<\varepsilon\bigr) = 1.$$

The forecaster is fixed before the opponent; no rate is claimed, and the rate may depend on $A$.

Milestones, in the order the Appendix uses them

1. Flow conservation is solvable (p. 52). For every nonnegative $k\times k$ matrix $R$, $k\ge 1$, there is a probability vector $w$ with $w^i\sum_j R^{i\to j} = \sum_j w^j R^{j\to i}$ for all $i$.
2. Lemma 1 (No-Regret) (p. 52). With losses in $[0,1]$ and weights solving flow conservation for the previous regrets,

$$R_T^{i\to j}\le\sqrt{2kT}\quad\text{for all } i,j,T.$$

3. Regrets sandwich L-2 calibration (p. 54). For a grid $p^1,\dots,p^k$ that is $\varepsilon$-dense in squared distance and losses $L_t^i = |X_t - p^i|^2$,

$$\sum_i\max_j \frac{R_T^{i\to j}}{T}\ \le\ C_{2,w}(T)\ \le\ \varepsilon + \sum_i\max_j\frac{R_T^{i\to j}}{T},$$

with $C_{2,w}$ the fractional L-2 calibration score. 4. L-1 versus L-2 (p. 54). For each $j$, $\sum_p|\rho(p,j,t)-p_j|\,N(p,t)/t \le \sqrt{\sum_p(\rho(p,j,t)-p_j)^2 N(p,t)/t}$.

Significance

The result. Theorem 3 makes the hypothesis of Theorem 1 attainable: combined, they show that there are learning procedures under which play converges in probability to the set of correlated equilibria of any finite game (the paper's Corollary, p. 49). The intermediate Lemma 1 is an early internal-regret bound; internal (swap) regret minimization later became the standard algorithmic route to correlated equilibria and to calibrated prediction in online learning.

Formalizing it. The result is proved, in the 1997 Appendix in telegraphic form and in full in Foster and Vohra (1998). The Appendix leaves several steps informal (see Formalization scope), so a machine-checked proof must supply them. No formalization of calibration or of internal regret was found on Prove2Me as of 2026-09-26. The mission produces a formal model of randomized forecasters against adaptive opponents, a checked internal-regret bound with an explicit constant, and the passage from regret to calibration.

Difficulty

The obvious approach is to pick, at each round, a forecast that corrects the current miscalibration. This is a deterministic rule, and by Oakes' theorem an opponent can defeat it. Randomization alone does not help either: the forecaster must randomize in a way that controls every pairwise regret $R^{i\to j}$ at once, not only the regret against the best fixed forecast. External no-regret does not imply calibration.

Two further gaps separate Lemma 1 from Theorem 3. First, the Appendix controls a fractional score in which the event "forecast $p^i$ was issued" is replaced by its probability $w_t^i$. The realized calibration score involves the random choices, so a concentration argument is needed against an adaptive opponent. Second, a fixed grid gives calibration only up to its mesh $\varepsilon$. Exact convergence requires letting the grid size $k$ grow and $\varepsilon$ shrink over time, and the scores of the different phases must be combined.

Formalization scope

• Model. Strategies are Fin n; forecasts are vectors Fin n → ℝ that are probability vectors (IsDist). Histories are Lean lists of (forecast, play) pairs, oldest first. Forecaster and opponent are maps from histories to Mathlib PMFs. The history law is built with PMF.bind/PMF.map, with the two draws independent given the past. $\mathbb P(C_t<\varepsilon)$ is the toOuterMeasure of the law, in ℝ≥0∞; no σ-algebra on histories is used.
• Opponent. The opponent may be randomized and may depend on all past forecasts and plays; fixed sequences and deterministic rules are special cases. The opponent never sees the current forecast. Letting it see the current forecast would make the goal false, and restricting to fixed sequences would make it weaker than the paper.
• Quantifiers. The forecaster is chosen before the opponent (∃ F, ∀ A). The reverse order is trivial, since one can forecast $A$'s next play.
• Conventions. Rounds are counted from $0$, so the paper's rounds $1,\dots,t$ are the first $t$ list entries. The paper's $R_{t-1}$ is the regret over the $0$-based rounds before $t$. Forecasts are grouped by exact equality of real vectors. Sums over $p$ run over the forecasts that occur, and every other term vanishes. Scores divide by the history length, and are $0$ for the empty history. "Converges in probability" is the $\lim\mathbb P(C_t<\varepsilon)=1$ form the page states. The grid of milestone 3 is indexed $1,\dots,k$ (the page writes $i = 0,\dots,k$ on p. 53 and $1,\dots,k$ in Lemma 1), and "within $\varepsilon$" is read in squared Euclidean distance.
• Pinned reading. The page writes the middle term of milestone 3 as $E(C_2(t))$ with a garbled formula. The mission states the inequality for the fractional score $C_{2,w}$, for which it holds.
• Steps the paper leaves informal, not stated as milestones. (a) "$E(C_2(t))\le\varepsilon + O(k/\sqrt2)$" when the weights solve flow conservation; the $O$-term is garbled and should decay in $t$. (b) "if we let $k$ grow slowly and $\varepsilon$ go slowly to zero … $C_2(t)\to 0$ in expectation which implies $C_2(t)\to0$ in probability by Jensen's inequality", together with the passage from the fractional score to the realized one. Solvers will have to formalize these steps on the way to the goal.
• Not included. The Corollary on p. 49 (convergence in probability of play to the correlated equilibria when both players use the scheme). It needs the game layer and a quantitative form of Theorem 1, and the page gives no proof.
• Infrastructure welcome. Finite Markov chain stationary distributions (for milestone 1), for which Prove2Me has MarkovChain.exists_isStationary for row-stochastic matrices. Also useful: martingale concentration for PMF-built processes, and Cauchy–Schwarz with weights. The history-law construction is reusable for any repeated forecasting game.

Selected references

• D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997) 40–55. https://doi.org/10.1006/game.1997.0595
• D. P. Foster and R. V. Vohra, Asymptotic calibration, Biometrika 85 (1998) 379–390. https://doi.org/10.1093/biomet/85.2.379
• A. P. Dawid, The well-calibrated Bayesian, J. Amer. Statist. Assoc. 77 (1982) 605–613. https://doi.org/10.1080/01621459.1982.10477856
• D. Oakes, Self-calibrating priors do not exist, J. Amer. Statist. Assoc. 80 (1985) 339. https://doi.org/10.1080/01621459.1985.10478117
• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000) 1127–1150. https://doi.org/10.1111/1468-0262.00153

Motivation

Classical non-cooperative game theory randomizes with objective, independent devices: each player spins a private wheel whose odds everyone agrees on. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) asks what changes when the randomizing events are ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. The paper introduced correlated equilibrium, and it also separates two effects that the classical model fuses: subjectivity (players disagree about probabilities) and correlation (players peg their choices on common or dependent events).

This mission formalizes the paper's result on subjectivity without correlation. Example 2.3 of the paper exhibits a three-person game in which strategies pegged on subjective but mutually secret events form an equilibrium that every player prefers to every classical mixed equilibrium. Proposition 5.1 shows that this cannot happen with two players.

Setting

A game has a finite set $N=\{1,\dots,n\}$ of players, a finite set $S_i$ of pure strategies for each player, a finite set $X$ of outcomes and an outcome function $g$ from $S=\times_{i\in N}S_i$ onto $X$. Player $i$ has a utility $u_i:X\to\mathbb R$; write $h_i(a)=u_i(g(a))$ for $a\in S$.

A randomizing structure consists of a set $\Omega$ of states of the world with a $\sigma$-field $\mathcal B$ of events, a sub-$\sigma$-field $\mathcal J_i\subseteq\mathcal B$ for each player (the events $i$ is informed about), and a probability measure $p_i$ on $\mathcal B$ for each player (the subjective probability of $i$). A strategy of $i$ is a map $s_i:\Omega\to S_i$ whose level sets $\{s_i=a\}$ lie in $\mathcal J_i$. For a profile $s=(s_1,\dots,s_n)$ of strategies the payoff of $i$ is

$$H_i(s)=\int_\Omega h_i\big(s(\omega)\big)\,dp_i(\omega),$$

computed under player $i$'s own beliefs. An equilibrium point is a profile $s$ with $H_i(s)\ge H_i(s_1,\dots,t_i,\dots,s_n)$ for every player $i$ and every strategy $t_i$ of $i$.

An event $A$ is $i$-secret if $A\in\mathcal J_i$ and every other player $j$ regards $A$ as independent of every event in the $\sigma$-field generated by the $\mathcal J_k$, $k\ne i$: $p_j(A\cap B)=p_j(A)p_j(B)$. A strategy is mixed if its level sets are $i$-secret, and objective if each level set has the same probability under every $p_j$. A measure is non-atomic on a $\sigma$-field $\mathcal R$ if every event of $\mathcal R$ of positive measure contains an event of $\mathcal R$ of strictly smaller positive measure; a roulette is a sub-$\sigma$-field of $\mathcal B$ on which every $p_j$ is non-atomic. Throughout, Assumption II holds: every player $i$ has a $\sigma$-field $\mathcal R_i$ of $i$-secret events on which every $p_j$ is non-atomic.

For distributions $\sigma_i$ on $S_i$ the classical payoff is $F_i(\sigma)=\sum_{a\in S}h_i(a)\prod_j\sigma_j(a_j)$, and $\sigma$ is a Nash equilibrium point if no player gains by switching to another distribution.

Formalization targets

Goal: Proposition 5.1 (p. 78)

Let $n=2$ and assume

$$p_1(B)=0\iff p_2(B)=0\qquad\text{for every }B\in\mathcal B.\tag{5.2}$$

Then for every equilibrium point $s$ in mixed strategies there is an equilibrium point $t$ in objective mixed strategies with

$$H(s)=H(t).$$

The game need not be zero-sum.

Milestones

1. Lemma 7.1 (p. 81): in a roulette $\mathcal R$, for events $B^1,\dots,B^l$ and $\alpha\in[0,1]$, there is an objective $A\in\mathcal R$ with $p_i(A)=\alpha$ and $p_i(A\cap B^k)=p_i(A)p_i(B^k)$ for all $i,k$.
2. Lemma 4.1 (p. 77): every distribution $\sigma_i$ on $S_i$ is realised by an objective mixed strategy $s_i$ with $p\{s_i=a\}=\sigma_i(a)$.
3. Lemma 7.3 (p. 82): if every $s_j$, $j\ne i$, is mixed, then $p_i\{s=a\}=p_i\{s_i=a_i\}\,p_i\{s_j=a_j\ \forall j\ne i\}=\prod_j p_i\{s_j=a_j\}$.
4. Corollary 7.4 (p. 83): mixed strategies are independent under every $p_k$.
5. Proposition 4.3 (p. 77): $\{F(\sigma):\sigma\text{ Nash}\}=\{H(s): s\text{ an equilibrium point in objective mixed strategies}\}$.

Significance

The result. Proposition 5.1 isolates correlation as the source of the new equilibrium payoffs of the subjective model in two-person games: disagreement about probabilities alone, with strategies pegged on secret events, reproduces only payoffs already achievable by classical mixed strategies (by Proposition 4.3, only Nash equilibrium payoffs). The paper uses it to explain Example 2.9, where two zero-sum players both expect more than the value, as an effect of subjectivity combined with correlation. Proposition 4.3 is the bridge that embeds classical Nash theory in the subjective model; with Nash's theorem it gives existence of equilibrium points in every game.

Formalizing it. The results are proved in the paper; to our knowledge none of them has been machine-checked. The mission produces a reusable measure-theoretic model of randomized strategies with private information and subjective beliefs (secret events, mixed and objective strategies, roulettes), a non-atomicity notion relative to a sub-$\sigma$-field, and the Lyapunov-type construction of Lemma 7.1, none of which exists in Mathlib at the pinned revision.

Difficulty

The equilibrium conditions quantify over all strategies of the deviator, i.e. all $\mathcal J_i$-measurable maps, and the deviator may know events on which the opponent's mixed strategy is pegged. The obvious computation of $H_1(t_1,s_2)$ as a sum of products of marginal probabilities is valid only because the opponent's strategy is pegged on secret events, which is the content of Lemma 7.3; for correlated strategies it fails, and Example 2.9 shows the proposition then fails. A second obstacle is that the replacement $t_1$ must reproduce player 2's beliefs about $s_1$, while player 1's own equilibrium condition is stated under $p_1$; condition (5.2) is what transfers "$a$ is played with positive probability" from one player's beliefs to the other's. Constructing objective strategies with prescribed probabilities (Lemmas 7.1 and 4.1) needs the convexity of the range of a non-atomic vector measure (Lyapunov's theorem), which is not in Mathlib.

Formalization scope

Players are a finite type (Fin 2 in the goal, players $1,2\mapsto 0,1$); the $S_i$ and $X$ are finite types, and $g$ is surjective. The $\sigma$-field $\mathcal B$ is an explicit parameter mΩ of the structure RandomizingStructure ι Ω mΩ, which carries the $\mathcal J_i$ and the probability measures $p_i$. Probabilities are $[0,\infty]$-valued Mathlib measures. Utilities and $p_i$ are data (Assumption I is used only to compare lotteries by expected utility; the uniqueness of $p_i$ is not encoded). $H_i$ is a Bochner integral; for strategy profiles the integrand has finitely many values and is measurable, hence integrable. Non-atomicity on a sub-$\sigma$-field is defined directly; Mathlib's NoAtoms (singletons are null) would trivialize Assumption II and is not used. "Mixed" means pegged on the family of all $i$-secret events, not on the $\sigma$-field $\mathcal R_i$ of Assumption II. Classical distributions, $F_i$ and Nash equilibrium points are AGT.IsLottery, AGT.expectedPayoff and AGT.IsMixedNash from the published definition agt_games.

A formalization that restricted deviations to mixed or objective strategies, or dropped "mixed" from the hypothesis on $s$, would state a different theorem and is ruled out.

Useful contributions: Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures (or the special case needed for Lemma 7.1), the factorization of Lemma 7.3, and the payoff identities used in the proof of Proposition 4.3. The model definitions are shared in meaning with the companion mission on two-person zero-sum games.

Selected references

• 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
• J. Nash, Non-Cooperative Games, Annals of Mathematics 54 (1951) 286–295. https://doi.org/10.2307/1969529
• A. Liapounoff, Sur les fonctions-vecteurs complètement additives, Izv. Akad. Nauk SSSR Ser. Mat. 4 (1940) 465–478.
• L. J. Savage, The Foundations of Statistics, Wiley, 1954.