All missions

Motivation

Linear second-order parabolic equations such as $u_t + Lu = f$ model diffusion with advection, growth or decay, and external sources. The heat equation is the prototype. For coefficients that are only bounded and measurable, classical solutions need not exist, and the natural well-posedness theory is the $L^2$ energy theory of weak solutions. In that theory the solution is a curve $t \mapsto u(t)$ in a Sobolev space, and the equation holds in the dual space. This framework, developed by J.-L. Lions and others in the 1950s–60s (Lions–Magenes 1972), underlies the numerical analysis of parabolic problems through finite elements and spectral Galerkin methods. It also underlies the existence theory for nonlinear evolution equations such as the Navier–Stokes equations (Temam 1977).

This mission formalizes Chapter 6 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014): the existence, uniqueness and energy estimate for weak solutions of the parabolic initial–boundary value problem, proved by the Galerkin method. It also formalizes the vector-valued calculus on Hilbert triples that the proof rests on, and the Ehrling and Aubin–Lions compactness results of §6.6.

Setting

Let $\Omega \subset \mathbb{R}^n$ be a bounded open set and $T > 0$. $H^1_0(\Omega)$ is the closure of $C_c^\infty(\Omega)$ in the norm $\|u\|_{H^1_0}^2 = \int_\Omega (u^2 + |Du|^2)\,dx$. $H^{-1}(\Omega)$ is its dual, with pairing $\langle f, v\rangle$. Every $u \in L^2(\Omega)$ acts on $H^1_0(\Omega)$ by $v \mapsto \int_\Omega uv\,dx$.

The operator is $Lu = -\sum_{i,j}\partial_i(a^{ij}\partial_j u) + \sum_j b^j\partial_j u + cu$. Its coefficients satisfy Assumption 6.1: $a^{ij}, b^j, c \in L^\infty(\Omega\times(0,T))$, $a^{ij} = a^{ji}$, and uniform ellipticity $\sum a^{ij}\xi_i\xi_j \ge \theta|\xi|^2$ for some $\theta > 0$. The associated form is

$$a(u, v; t) = \sum_{i,j}\int_\Omega a^{ij}\partial_i u\,\partial_j v\,dx + \sum_j\int_\Omega b^j\partial_j u\,v\,dx + \int_\Omega c\,uv\,dx.$$

A function $u : [0,T] \to H^1_0(\Omega)$ has weak time derivative $u_t = w$ if $\int_0^T \phi'(t)u(t)\,dt = -\int_0^T\phi(t)w(t)\,dt$ for all $\phi \in C_c^\infty(0,T)$, with Bochner integrals in $H^{-1}(\Omega)$. Given $f \in L^2(0,T;H^{-1}(\Omega))$ and $g \in L^2(\Omega)$, $u$ is a weak solution of

$$u_t + Lu = f \ \text{in } \Omega\times(0,T), \qquad u = 0 \ \text{on } \partial\Omega, \qquad u(0) = g$$

when three conditions hold. First, $u \in L^2(0,T;H^1_0)$ and $u_t \in L^2(0,T;H^{-1})$. Second, $\langle u_t(t), v\rangle + a(u(t), v; t) = \langle f(t), v\rangle$ for every $v \in H^1_0(\Omega)$ and a.e. $t$. Third, $u(0) = g$, where the value at $0$ is that of the continuous representative in $C([0,T];L^2(\Omega))$.

The Galerkin approximations use an $L^2$-orthonormal basis $\{w_k\}$ of Dirichlet eigenfunctions and the spaces $E_N = \langle w_1, \dots, w_N\rangle$. The approximation $u_N : [0,T] \to E_N$ solves the projected equation $(u_{Nt}, v)_{L^2} + a(u_N, v; t) = \langle f, v\rangle$ for $v \in E_N$, with $u_N(0) = P_N g$.

A Hilbert triple $\mathcal{V} \hookrightarrow \mathcal{H} \hookrightarrow \mathcal{V}'$ consists of two separable Hilbert spaces $\mathcal{V}$, $\mathcal{H}$ and the dual $\mathcal{V}'$, with dense continuous injective embeddings and $\langle f, v\rangle = (f, v)_{\mathcal{H}}$ for $f \in \mathcal{H}$. The model is $H^1_0 \hookrightarrow L^2 \hookrightarrow H^{-1}$.

Formalization targets

Goal: Theorem 6.3

For every $f \in L^2(0,T;H^{-1}(\Omega))$ and $g \in L^2(\Omega)$ there is a unique weak solution $u \in C([0,T];L^2) \cap L^2(0,T;H^1_0)$ with $u_t \in L^2(0,T;H^{-1})$. There is also a constant $C = C(\Omega, T, L)$ such that

$$\|u\|_{L^\infty(0,T;L^2)} + \|u\|_{L^2(0,T;H^1_0)} + \|u_t\|_{L^2(0,T;H^{-1})} \le C\big(\|f\|_{L^2(0,T;H^{-1})} + \|g\|_{L^2}\big).$$

Milestones

• Theorem 6.41. If $u \in L^2(0,T;\mathcal{V})$ and $u_t \in L^2(0,T;\mathcal{V}')$, then $u \in C([0,T];\mathcal{H})$. Moreover $\frac{d}{dt}(u,v)_{\mathcal{H}} = \langle u_t, v\rangle$, $\frac{d}{dt}\|u\|^2_{\mathcal{H}} = 2\langle u_t, u\rangle$, and $\|u\|_{L^\infty(\mathcal{H})} \le C(\|u\|_{L^2(\mathcal{V})} + \|u_t\|_{L^2(\mathcal{V}')})$.
• Theorem 6.42. $\int_0^T\langle u_t, v\rangle\,dt = (u(T),v(T))_{\mathcal{H}} - (u(0),v(0))_{\mathcal{H}} - \int_0^T\langle u, v_t\rangle\,dt$.
• Proposition 6.5. Each Galerkin problem has a unique solution $u_N$.
• Proposition 6.6. The energy estimate above holds for $u_N$ with $C$ independent of $N$.
• Proposition 6.7. A subsequence of $u_N$ converges weakly to a weak solution satisfying the estimate.
• Lemma 6.10 (Ehrling) and Theorem 6.9 (Aubin–Lions). These are further results of the chapter, stated for Banach spaces $X \hookrightarrow Y \hookrightarrow Z$ with $X$ compactly embedded in $Y$.

Significance

Theorem 6.3 is the basic well-posedness theorem for linear parabolic equations with rough coefficients. It gives existence and uniqueness, and continuous dependence on the data through the linear estimate. The same argument gives the Galerkin convergence that justifies spectral and finite-element semi-discretizations. The Hilbert-triple calculus of Theorems 6.41–6.42 is the standard setting for linear and nonlinear evolution equations. The Aubin–Lions lemma is the compactness tool for nonlinear problems, such as the semilinear heat equation of §6.6 and the Navier–Stokes equations of §6.7.

All of these results are classical and proved in the notes, except that Theorem 6.41's proof leans on vector-valued mollification. As far as a search of the platform shows, none of them is formalized there. Mathlib has the Bochner integral, $L^p$ spaces of Banach-valued functions and Gronwall's inequality. It does not have weak derivatives of vector-valued functions, Hilbert triples, or evolution-equation existence theorems. The work here is therefore to formalize known proofs, and in doing so to build reusable infrastructure for time-dependent PDEs.

Difficulty

The main obstacle is that the natural objects are equivalence classes of vector-valued functions, not functions. The initial condition $u(0) = g$ is meaningless for an element of $L^2(0,T;H^1_0)$ until Theorem 6.41 provides a continuous representative. Its proof needs extension across the endpoints and mollification of $\mathcal{V}$-valued functions. Passing to the limit in the Galerkin scheme needs weak compactness in $L^2(0,T;H^1_0)$ and $L^2(0,T;H^{-1})$, identified with a dual Bochner space. Proposition 6.5 is a linear ODE system whose coefficients are only $L^\infty$ in time, so the Picard–Lindelöf theorem for continuous right-hand sides does not apply directly. The $H^{-1}$ bound on $u_{Nt}$ needs the projection $P_N$ to be bounded on $H^1_0$ as well as on $L^2$, which is why the basis is taken to be eigenfunctions. Uniqueness needs the energy identity (6.46) and a Gronwall argument in weak form.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n), with 0-based coordinates. H10 n Ω is the closure of the jets $(\phi, \nabla\phi)$, $\phi \in C_c^\infty(\Omega)$, in $L^2(\Omega;\mathbb{R}\times\mathbb{R}^n)$, so its norm is the full $H^1$ norm. Hm1 n Ω is StrongDual ℝ (H10 n Ω). l2Embed is the embedding $H^1_0 \hookrightarrow L^2 \hookrightarrow H^{-1}$.
• $L^p(0,T;X)$ is MemLp for Lebesgue measure on $(0,T)$, and norms are eLpNorm with values in $[0,\infty]$. Constants are finite nonnegative reals. Every constant is quantified before the data it must not depend on: before $f$, $g$ in Theorem 6.3, and before the basis, $f$, $g$, $N$ in Propositions 6.6–6.7.
• The weak time derivative is (6.14) in its standard form $\int\phi' u = -\int\phi w$. The page prints $\phi$ and $\phi'$ interchanged, which is a typo.
• Weak solutions take $g \in L^2(\Omega)$ as in Assumption 6.1(3). The printed Theorem 6.3 says $g \in H^1_0(\Omega)$, a special case. $u(0) = g$ is read through a continuous representative $\tilde u \in C([0,T];L^2)$, and uniqueness means equality for a.e. $t$.
• Coefficient conditions and ellipticity hold almost everywhere on $\Omega\times(0,T)$. The Galerkin basis is a hypothesis: an orthonormal basis of $L^2(\Omega)$ of weak Dirichlet eigenfunctions.
• Proposition 6.7 states weak convergence of $u_{N_k}$ in $L^2(0,T;H^1_0)$ and of $u_{N_k t}$ in $L^2(0,T;H^{-1})$, in the explicit integral form of p. 186. This is at least as strong as the printed claim.
• Hilbert triples are structures with two continuous injective dense-range embeddings, separability, and the compatibility identity. Reflexivity in Theorem 6.9 is surjectivity of the canonical map into the bidual.
• Ruling out trivializations. Every Bochner integral in a definition has an integrable integrand under the stated $L^2$ hypotheses, so no weak-derivative or weak-solution condition holds through the integral's junk value $0$. The initial condition is imposed on a continuous representative, so it is not vacuous on a null set.
• Reusable infrastructure welcome: vector-valued mollification and extension, the Hilbert-triple calculus, and dual identification of $L^2(0,T;X)'$.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, Chapter 6. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• L. C. Evans, Partial Differential Equations, 2nd ed., Graduate Studies in Mathematics 19, AMS, 2010, §7.1. https://doi.org/10.1090/gsm/019
• J.-L. Lions and E. Magenes, Non-Homogeneous Boundary Value Problems and Applications I, Springer, 1972. https://doi.org/10.1007/978-3-642-65161-8
• R. Temam, Navier–Stokes Equations: Theory and Numerical Analysis, North-Holland, 1977; AMS Chelsea reprint 2001. https://doi.org/10.1090/chel/343
• J. Simon, Compact sets in the space $L^p(0,T;B)$, Ann. Mat. Pura Appl. 146 (1987), 65–96. https://doi.org/10.1007/BF01762360

Motivation

Milgrom and Shannon's theory of quasi-supermodularity, developed for monotone comparative statics in economics, showed that many of the consequences of lattice submodularity survive under a much weaker, purely ordinal relaxation of the defining inequality. Chapter 7's final section imports this idea into discrete convex analysis: does L-convexity's optimality and proximity theory survive when the additive submodularity inequality is relaxed to an ordinal condition on the sign pattern of the two relevant differences, rather than their sum? This mission formalizes the chapter's answer for the strongest of the relevant relaxations, (SSQSB) (semistrict quasi submodularity): yes, and the class is large enough to include every strictly increasing rescaling of an L-convex function — exactly mirroring chunk 07's result for the M-convex side, and completing the "quasi" theory on both halves of the exchange-axiom framework before chapter 8 unifies them under conjugacy.

Setting

Let $V$ be a finite ground set and $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$. Building on chunk 08's submodularity axiom (SBF[Z]), this section introduces four ordinal relaxations. $g$ is quasi submodular, satisfying (QSB), if for every $p, q \in \mathbb Z^V$, $g(p \wedge q) \le g(p)$ or $g(p \vee q) \le g(q)$. $g$ is semistrictly quasi submodular, satisfying (SSQSB), if additionally $g(p \vee q) \ge g(q) \implies g(p \wedge q) \le g(p)$ and symmetrically. The weak variants (QSBw) and (SSQSBw) restrict attention to points of the effective domain and compare $\max(g(p), g(q))$ against $\min(g(p \wedge q), g(p \vee q))$ directly, with (SSQSBw) additionally allowing the four-way tie $g(p) = g(q) = g(p\wedge q) = g(p \vee q)$. The linear perturbation of $g$ by $x : V \to \mathbb R$ is $g[x](p) = g(p) + \langle p, x \rangle$.

Formalization targets

Goal: Theorem 7.54 (the quasi L-proximity theorem)

Let $g$ satisfy (SSQSB) and $g(p) = g(p + \mathbf 1)$ for all $p$, $n = |V|$, $\alpha$ a positive integer. If $p_\alpha \in \operatorname{dom} g$ satisfies $g(p_\alpha) \le g(p_\alpha + \alpha \chi_Y)$ for all $Y \subseteq V$, then $\arg\min g \ne \emptyset$ and there is $p^* \in \arg\min g$ with the componentwise bound $p_\alpha \le p^* \le p_\alpha + (n-1)(\alpha-1) \mathbf 1$ — verbatim the same conclusion, and the same exact bound, as chunk 08's Theorem 7.18(1), now established for the strictly larger class satisfying (SSQSB) rather than (SBF[Z]).

Milestones: Theorems 7.49, 7.53

Theorem 7.49: the full nesting chain (SBF[Z]) $\Rightarrow$ (SSQSB) $\Rightarrow$ (QSB), (SSQSB) $\Rightarrow$ (SSQSBw) $\Rightarrow$ (QSBw), together with the collapse theorem that (SBF[Z]) holds if and only if every linear perturbation of $g$ satisfies (QSBw) — precisely quantifying how weak (QSBw) is pointwise and how the classes reunite under universal perturbation. Theorem 7.53 (the quasi L-optimality criterion): the direct analogue of chunk 08's Theorem 7.14, showing that global (or, for the weaker (QSBw) case, unique-up-to-translation) optimality still reduces to a purely local check against the $2^n - 2$ nontrivial sign-pattern neighbors $p + \chi_X$.

Significance

The result itself. As with the M-convex case (chunk 07), the proximity theorem is what algorithms actually need: an L-convex-flavored objective transformed by any strictly increasing scalar rescaling (a common device — expressing a network-flow cost in a different currency, or applying a monotone risk adjustment) retains a scaling algorithm's correctness guarantee with exactly the same distance bound, even though the rescaled function is generally no longer L-convex itself.

Formalizing it. No matching item exists on the platform for quasi submodularity or quasi L-convexity in any form. Together with chunk 07 (the M-side quasi-convexity theory), this mission completes the "quasi" relaxation on both halves of the exchange-axiom framework the book develops, immediately before chapter 8 unifies M-convexity and L-convexity under a single conjugacy relationship.

Difficulty

As with chunk 07's quasi M-proximity theorem, the temptation is to imitate chunk 08's L-proximity proof line by line. The overall architecture does survive — translate so $p_\alpha = 0$, find a lattice-minimal sufficiently-good point, and bound the gap using submodularity — but chunk 08's proof uses (SBF[Z])'s additive inequality directly to compare four function values at once, while this proof must instead route every such comparison through (SSQSB)'s two one-directional implications (Proposition 7.50's quasi-version of the same two-sided inequality), which only ever license moving in one direction at a time depending on which side of a comparison is tight. The book's proof handles this by working with the specific implications (7.43)–(7.44) in place of the L♮-approach property used in chunk 08's proof — an ordinal substitute for the same additive step, at the cost of a case analysis chunk 08's proof did not need.

Formalization scope

This mission builds directly on chunk 08's published items (SBF, DomZ, ArgMin, IndicatorVec), per the platform's textbook convention that a later chapter section of the same book imports an earlier one's definitions; its own namespace DiscreteConvex.LConvexFunctions.Quasi nests under chunk 08's DiscreteConvex.LConvexFunctions accordingly. Note the sign convention of the linear perturbation here, $g[x](p) = g(p) + \langle p,x\rangle$, is the opposite of the M-side's $f[p](x) = f(x) - \langle p,x\rangle$ (chunks 06–07) — verified against the book's own formula rather than assumed by analogy.

A trivializing formalization of the goal would silently strengthen (SSQSB) back to plain (SBF[Z]) (making this mission redundant with chunk 08's Theorem 7.18) or loosen the exact bound $(n-1)(\alpha-1)$; neither is done. Only (QSB), (SSQSB), (QSBw), (SSQSBw) are drafted, matching exactly what the chosen three items need; the polyhedral L-convex-function bridge (§7.8–7.9, Theorems 7.40–7.46) and the level-set characterizations (Theorems 7.51–7.52) are left for a follow-on mission. Contributions building the 0L ↔ S correspondence (Theorem 7.40, a bridge back to chunk 04's submodular-set-function vocabulary) or the scaled quasi L-minimizer-cut analogue are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• P. Milgrom, C. Shannon, "Monotone comparative statics," Econometrica, 62(1), 1994, pp. 157–180.

Motivation

Many linear partial differential equations of evolution type — the heat equation, the Schrödinger equation, linear wave and Klein–Gordon equations, linearized reaction–diffusion and Kuramoto–Sivashinsky equations — can be written as an ordinary differential equation

$$u_t = Au, \qquad u(0) = f,$$

in a Banach space $X$ of functions, where $A$ is a spatial differential operator. When $A$ is bounded, the solution is the operator exponential $e^{tA}f$. Differential operators are unbounded, however, and then the solution operators $f \mapsto u(t)$ are only continuous in time in the strong sense and may exist only forward in time. Semigroup theory makes this picture rigorous: it characterizes exactly which operators $A$ generate a well-posed evolution, and it is the standard route from energy estimates to existence and uniqueness for linear and semilinear evolution equations (Duhamel's formula, §5.4.5 of the notes, used for the semilinear heat equation in §5.5).

This mission formalizes §5.4 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014): uniformly continuous groups, strongly continuous semigroups and their generators, the Hille–Yosida theorem, the Lumer–Phillips theorem and Stone's theorem.

Timeline. The generation theorem for contraction semigroups is due independently to E. Hille (1948) and K. Yosida (1948); the general version with constants $M$, $a$ to Feller, Miyadera and Phillips (1952–53). G. Lumer and R. S. Phillips (1961) recast the contraction case in terms of dissipative operators. Stone's theorem on one-parameter unitary groups dates from 1930–32. Standard modern accounts are Pazy (1983) and Engel–Nagel (2000).

Setting

Let $X$ be a Banach space over $\mathbb{K} = \mathbb{R}$ or $\mathbb{C}$, and $\mathcal{L}(X)$ the Banach space of bounded linear operators on $X$ with the operator norm.

A uniformly continuous group is a family $\{T(t) : t \in \mathbb{R}\} \subset \mathcal{L}(X)$ with $T(0) = I$, $T(s)T(t) = T(s+t)$, and $T(h) \to I$ in operator norm as $h \to 0$. A strongly continuous (C₀) semigroup is a family $\{T(t) : t \ge 0\} \subset \mathcal{L}(X)$ with $T(0) = I$, $T(s)T(t) = T(s+t)$ for $s, t \ge 0$, and $T(h)f \to f$ as $h \to 0^+$ for every $f \in X$; it is a contraction semigroup if $\|T(t)\| \le 1$ for all $t \ge 0$. A C₀ group has the same properties for all $s, t \in \mathbb{R}$; on a complex Hilbert space it is unitary if every $T(t)$ is unitary.

An operator $A : \mathcal{D}(A) \subset X \to X$ is a linear map defined on a subspace $\mathcal{D}(A)$. The generator of a C₀ semigroup is the operator $A$ whose domain is the set of $f$ for which

$$Af = \lim_{h \to 0^+} \frac{T(h)f - f}{h}$$

exists in norm, with $Af$ this limit. $A$ is closed if its graph $\{(f, Af) : f \in \mathcal{D}(A)\}$ is closed in $X \times X$, and densely defined if $\mathcal{D}(A)$ is dense. A scalar $\lambda$ is in the resolvent set of $A$ if $\lambda I - A : \mathcal{D}(A) \to X$ is a bijection, and then $R(\lambda, A) = (\lambda I - A)^{-1}$ is the resolvent. $A$ is dissipative if $\lambda\|f\| \le \|(\lambda I - A)f\|$ for all real $\lambda > 0$ and $f \in \mathcal{D}(A)$, and m-dissipative if in addition $\lambda I - A$ is onto $X$ for some $\lambda > 0$. On a complex Hilbert space $\mathcal{H}$, $A$ is self-adjoint if $\mathcal{D}(A)$ is dense, $\mathcal{D}(A) = \mathcal{D}(A^*)$, and $(x, Ay) = (Ax, y)$ for $x, y \in \mathcal{D}(A)$.

Formalization targets

Goal: the Lumer–Phillips theorem (Theorem 5.38)

For an operator $A : \mathcal{D}(A) \subset X \to X$,

$$A \text{ generates a C₀ contraction semigroup on } X \iff A \text{ is closed, densely defined and m-dissipative.}$$

Milestones

1. Theorem 5.24. A uniformly continuous group is smooth in operator norm, $A = T'(0) \in \mathcal{L}(X)$ exists, and $T(t) = e^{tA}$ for all $t \in \mathbb{R}$.
2. Theorem 5.32. The generator of a C₀ semigroup is closed and densely defined.
3. Theorem 5.35 (Hille–Yosida). $A$ generates a C₀ semigroup if and only if, for some $M \ge 1$ and $a \in \mathbb{R}$, $A$ is closed and densely defined, $(a, \infty)$ lies in the resolvent set, and

$$\|R(\lambda, A)^n\| \le \frac{M}{(\lambda - a)^n} \qquad (\lambda > a,\ n \in \mathbb{N});$$

in that case $\|T(t)\| \le M e^{at}$ for $t \ge 0$. 4. Corollary 5.36. The contraction case: $M = 1$, $a = 0$, with $\|R(\lambda, A)\| \le 1/\lambda$. 5. Theorem 5.42 (Stone). On a complex Hilbert space, $iA$ generates a C₀ unitary group if and only if $A$ is self-adjoint.

Significance

The result itself. The Lumer–Phillips theorem is the working form of generation theory for PDEs: to show that $u_t = Au$ is well posed with $\|u(t)\| \le \|u(0)\|$, it suffices to prove an energy inequality (dissipativity) and to solve a single resolvent equation $\lambda f - Af = g$. The notes apply it to the Laplacian on $H^2(\mathbb{R}^n) \subset L^2(\mathbb{R}^n)$ and, after a shift, to the linearized Kuramoto–Sivashinsky operator; later chapters use the resulting semigroups in Duhamel's formula to construct solutions of semilinear heat and Schrödinger equations. Hille–Yosida gives the general growth bound $\|T(t)\| \le Me^{at}$, and Stone's theorem identifies unitary quantum dynamics with self-adjoint Hamiltonians.

Formalizing it. All results are classical and proved in the literature; the notes themselves state 5.32, 5.35, 5.36, 5.38 and 5.42 without proof, referring to standard texts. Mathlib currently has the operator exponential on Banach algebras, partially defined linear maps (LinearPMap) with closedness, closures and adjoints, but no theory of C₀ semigroups or their generators. A complete development would give Lean a reusable generation theory for unbounded operators, on which parabolic and dispersive PDE existence results can rest.

Difficulty

The central obstacle is the passage from resolvent information to a semigroup. Formally $T(t) = e^{tA}$, but for unbounded $A$ the exponential series is meaningless, and the necessity directions require showing that the resolvent is a Laplace transform of the semigroup, which needs integration of strongly (not norm) continuous operator-valued functions. The sufficiency directions must construct a semigroup from $A$ by an approximation of the unbounded generator and a limit that converges only strongly, and then identify the generator of the limit with $A$ — including its domain, which is where most careless arguments fail. In the Lumer–Phillips theorem, surjectivity of $\lambda I - A$ is assumed for a single $\lambda > 0$ and must be propagated to every $\lambda > 0$. In Stone's theorem both directions need domain arguments for unbounded operators on Hilbert space; symmetry of $A$ alone is not enough.

Formalization scope

• Scalars: a field 𝕜 with [RCLike 𝕜] (ℝ or ℂ), and X a Banach space over it ([NormedAddCommGroup X] [NormedSpace 𝕜 X] [CompleteSpace X]). Stone's theorem is over ℂ on an InnerProductSpace ℂ H with [CompleteSpace H]. Theorem 5.24 additionally equips X with a compatible real structure ([NormedSpace ℝ X] [IsScalarTower ℝ 𝕜 X]) so that $t \mapsto T(t)$ can be differentiated; $e^{tA}$ is Mathlib's NormedSpace.exp, and $C^\infty$ is ContDiff ℝ ∞.
• Operators $A : \mathcal{D}(A) \subset X \to X$ are X →ₗ.[𝕜] X (LinearPMap); closedness is LinearPMap.IsClosed (closed graph).
• Semigroups are functions T : ℝ → X →L[𝕜] X; for semigroups only the values at $t \ge 0$ enter. Composition is multiplication in X →L[𝕜] X.
• The generator relation IsGenerator T A states, for all $f, g$: the right difference quotient $h^{-1}(T(h)f - f)$ tends to $g$ as $h \to 0^+$ if and only if $f \in \mathcal{D}(A)$ and $Af = g$. So "$A$ generates a semigroup" means that $A$ equals the generator including its domain; a formalization in which $A$ merely agrees with the limit on some subspace, or in which the generator is a restriction, would make the theorems different (and false) statements, and is ruled out.
• Resolvent norm bounds $\|R(\lambda, A)^n\| \le c$ are stated pointwise, $\|R(\lambda,A)^n g\| \le c\|g\|$ for all $g$, which is equivalent. In (5.24) $n = 0$ is included, which adds nothing because $M \ge 1$. The "in that case" clause of Theorem 5.35 is a second conjunct: for every semigroup generated by $A$ and every $M, a$ satisfying the three conditions, $\|T(t)\| \le Me^{at}$.
• Closedness and density, which the notes build into the definitions of the resolvent set and of dissipativity, are stated explicitly wherever they are used (they appear as condition (1) in every theorem).
• The generator of a C₀ group (Stone) is the generator of its forward part, as in Definition 5.30; the operator $iA$ is Complex.I • A, with the same domain as $A$. Self-adjointness is Definition 5.41 as printed, not Mathlib's IsSelfAdjoint for LinearPMap, although the two agree.
• Useful infrastructure, reusable beyond this mission: Riemann/Bochner integration of strongly continuous operator families, the Laplace-transform representation of the resolvent, Yosida approximations, and dissipativity–resolvent equivalences. Contributions of any of these as separate lemmas are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §5.4. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• A. Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Springer, 1983. https://doi.org/10.1007/978-1-4612-5561-1
• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Springer GTM 194, 2000. https://doi.org/10.1007/b97696
• G. Lumer and R. S. Phillips, Dissipative operators in a Banach space, Pacific J. Math. 11 (1961), 679–698. https://doi.org/10.2140/pjm.1961.11.679
• M. H. Stone, On one-parameter unitary groups in Hilbert space, Ann. of Math. 33 (1932), 643–648. https://doi.org/10.2307/1968538
• K. Yosida, On the differentiability and the representation of one-parameter semigroup of linear operators, J. Math. Soc. Japan 1 (1948), 15–21. https://doi.org/10.2969/jmsj/00110015

Motivation

A gambler watching a sequence unfold has to decide, at each moment and knowing only the past, whether to take what is on the table or wait for something better. That is the whole of optimal stopping, and it is one of the few problems in stochastic control with a clean and completely general answer: the value of the problem is the smallest superharmonic function dominating the immediate payoff. Snell (1952) proved the martingale form; the dynamic-programming form is due to Chow, Robbins and Siegmund. It is the structure behind the pricing of American options, the secretary problem, sequential hypothesis testing, and the bandit problems of Chapter 5.

Bäuerle and Rieder's Chapter 10 (Markov Decision Processes with Applications to Finance, Springer, 2011) derives this from their own Markov-decision machinery rather than from martingale theory, which makes the whole development elementary and self-contained: a stopping problem is a Markov Decision Problem whose action space is {continue, stop}, so Chapter 2's finite-horizon theory and Chapter 7's unbounded-horizon theory apply to it verbatim. The chapter then runs the resulting theory on three classical problems and solves each one in closed form.

Setting

The problem. A Markov process (X_n) on a Borel space E is observed. A stopping time is a random time τ with {τ ≤ n} ∈ F_n — "upon observing the process until time n we can decide whether or not τ has already occurred". Stopping at τ collects

$$R_\tau := \sum_{k=0}^{\tau-1} c_k(X_k) + g_\tau(X_\tau),$$

a running reward c_k while continuing and a stopping reward g_τ at the end, and the problem is to find V_N^*(x) := sup_{τ ≤ N} E_x[R_τ] (10.1). Assumption (B_N) — finiteness of the supremum of the positive parts — is what makes this well posed.

The reduction (Theorem 10.1.2). Take A = {0,1}, let a = 0 mean continue and a = 1 mean stop, and make the transition law uncontrollable on continuation and absorbing on stopping. A policy π = (f_0,…,f_{N-1}) induces the stopping time τ_π = inf{n | f_n(X_n) = 1} ∧ N, and conversely every stopping time is a history-dependent policy. The theorem says the two suprema agree: the extra history buys nothing.

The recursion (Theorems 10.1.3, 10.1.5). The Bellman operator becomes a two-branch maximum,

$$\mathcal{T}v(x) = \max\Big\{g(x),\ c(x) + \beta\int v(x')Q^X(dx'|x)\Big\},$$

with no action variable left in it. In the stationary case J_0 = g, J_n = \mathcal{T}J_{n-1}; the J_n increase, the sets S_n^* = {J_n = g} shrink — "the tendency to stop is non-decreasing as time goes by" — and the optimal rule is "stop on first entry into S_{N-n}^*".

The unbounded horizon (§10.2). Now the reward is discounted, R_τ = Σ β^k c(X_k) + β^τ g(X_τ) for τ < ∞, the value is V_∞^*(x) = sup_{τ<∞} E_x[R_τ], and there is no terminal condition to induct from. Three candidate values present themselves: V_∞^*; G = sup_π liminf_n J_{nπ}, a supremum over policies of limits of finite-horizon values; and J = lim_n J_n, which exists by monotonicity. Theorem 10.2.2, the goal, says all three coincide, that the common value solves J = \mathcal{T}J and satisfies 0-free bounds, and — the characterization — that it is the smallest c-superharmonic function majorizing g.

Turning the value into a rule (Theorems 10.2.3, 10.2.7, Corollaries 10.2.6, 10.2.8). Knowing the value is not knowing when to stop. Theorem 10.2.3 produces the stopping region as S^* = {J = g} = {d ≥ 0} where d = lim_n d_n, under two conditions that Corollary 10.2.6 then gives three checkable sufficient conditions for. Theorem 10.2.7 is the practical one, the One-Step-Look-Ahead Rule: if the set where stopping now beats stopping one step later is closed under the transition law, then the myopic rule is globally optimal. Corollary 10.2.8 adds monotonicity and gets a threshold.

Three applications (§10.3). The house seller who receives i.i.d. offers and pays maintenance on each rejection should accept the first offer above an explicit threshold, obtained as the maximiser of a one-dimensional function (Theorem 10.3.1). The secretary problem's value function is computed exactly (Proposition 10.3.2), giving the classical rule — reject the first k^*, then take the first leader — with success probability (k^*/N)h(k^*) and k^*(N)/N → 1/e (Theorem 10.3.3). And when the offers' distribution has an unknown parameter, MTP_2 of the likelihood propagates into monotonicity of the value in the information state (Theorem 10.3.4), with a fully explicit solution for the exponential/Inverse-Gamma conjugate pair (Theorem 10.3.6).

What is being asked

Formalize Theorem 10.2.2 in full: the three-way equality of V_∞^*, G and J, the fixed point equation, and — the part that carries the theorem — minimality among all functions that are both c-superharmonic and above g. Asserting only that J is such a function, or only one of the two conditions, is a strictly weaker and different claim.

The twelve milestones are the rest of the chapter, in attack order: the reduction and the two recursions, then the unbounded-horizon apparatus, then the three worked problems.

The stopping-time apparatus is built rather than assumed — the chain's law pinned by its finite-dimensional distributions, stopping times valued in ℕ ∪ {∞}, rewards vanishing at ∞ — because every theorem here is the identification of a supremum over stopping times with something computable, and carrying the value as an abstract function would make them vacuous. Every supremum is taken as a least upper bound against an explicit set of achievable values rather than by sSup, so that a set unbounded above is not silently given the value 0.

Motivation

Poisson's equation $-\Delta u = f$ is the model elliptic partial differential equation. It describes the electrostatic potential of a charge density, the gravitational potential of a mass density, and the steady temperature of a body with internal heat sources. Its solution on the whole space by convolution with a point-source potential, and the fact that this solution has exactly two more derivatives than the data when smoothness is measured in Hölder norms, are the starting point of the regularity theory of second-order elliptic equations.

This mission formalizes §2.6–2.7 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014), which follow the classical line: the fundamental solution, the Newtonian potential, an integral representation of its second derivatives, and the Hölder estimate. The estimate goes back to J. Schauder (1934), who used it to build an existence theory for elliptic equations with Hölder continuous coefficients, now called Schauder theory (Gilbarg–Trudinger, Ch. 4 and 6). The singular integral operators that appear in the second derivatives were later placed in a general framework by A. P. Calderón and A. Zygmund (1952), whose theory gives the $L^p$ analogue.

Setting

Throughout, $n \ge 2$ and $\mathbb{R}^n$ carries the Euclidean norm $|x|$ and Lebesgue measure. Let $\alpha_n$ be the volume of the open unit ball. The fundamental solution of Laplace's equation is

$$\Gamma(x) = \frac{1}{n(n-2)\alpha_n}\,\frac{1}{|x|^{n-2}} \quad (n \ge 3), \qquad \Gamma(x) = -\frac{1}{2\pi}\log|x| \quad (n = 2),$$

defined for $x \neq 0$. With this sign convention (as in Evans, opposite to Gilbarg–Trudinger) $\Gamma$ is harmonic away from the origin and $-\Delta\Gamma = \delta$ in the sense of distributions. $\Gamma$ is locally integrable, and so is its gradient, but its second derivatives behave like $|x|^{-n}$ and are not.

For a smooth function $f$ with compact support, $f \in C_c^\infty(\mathbb{R}^n)$, the Newtonian potential of $f$ is the convolution

$$u(x) = (\Gamma * f)(x) = \int_{\mathbb{R}^n} \Gamma(x - y)\, f(y)\, dy.$$

Partial derivatives are written $\partial_i$, with $\partial_{ij} = \partial_i \partial_j$, and $\delta_{ij}$ is the Kronecker delta. For $0 < \alpha \le 1$ the Hölder seminorm of $v : \mathbb{R}^n \to \mathbb{R}$ is

$$[v]_{0,\alpha} = \sup_{x \neq y} \frac{|v(x) - v(y)|}{|x - y|^{\alpha}} \in [0, \infty].$$

In the Lean development these objects are fundamentalSolution n, unitBallVolume n, newtonianPotential n f, partialDeriv u i, secondPartial u i j and holderSeminorm α Set.univ v, all in the namespace HunterPDE.Newtonian.

Formalization targets

Goal: the Hölder estimate (Theorem 2.28)

For $0 < \alpha < 1$ there is a constant $C$, depending only on $\alpha$ and $n$, such that for every $f \in C_c^\infty(\mathbb{R}^n)$ and all indices $i, j$,

$$[\partial_{ij}(\Gamma * f)]_{0,\alpha} \le C\,[f]_{0,\alpha}.$$

The constant is not specified: the goal asserts the shape of the estimate, not a numerical value.

Milestones

1. Eq. (2.14). $\Gamma$ is $C^\infty$ on $\mathbb{R}^n \setminus \{0\}$ and $\partial_i\Gamma(x) = -\dfrac{1}{n\alpha_n}\dfrac{1}{|x|^{n-1}}\dfrac{x_i}{|x|}$ for $x \neq 0$.
2. Eq. (2.23). $\Gamma * (\Delta f) = -f$ for $f \in C_c^\infty(\mathbb{R}^n)$.
3. Theorem 2.25. $u = \Gamma * f$ is well defined, $u \in C^\infty(\mathbb{R}^n)$, and $-\Delta u = f$.
4. Corollary 2.27. For every $x$ and every open ball $B_R(x)$ containing the support of $f$,

$$\partial_{ij} u(x) = \int_{B_R(x)} \partial_{ij}\Gamma(x - y)\,[f(y) - f(x)]\,dy - \frac{1}{n} f(x)\,\delta_{ij},$$

with the integral absolutely convergent.

Significance

Theorem 2.25 is the existence theorem for Poisson's equation on the whole space. Corollary 2.27 expresses $D^2 u$ as a singular integral operator applied to $f$ plus a multiple of $f$; it is the prototype of the representations behind both the Hölder (Schauder) and the $L^p$ (Calderón–Zygmund) theories. Theorem 2.28 is the first Schauder estimate. With it, a priori estimates for equations with variable Hölder coefficients follow by freezing the coefficients, and existence follows by the method of continuity. The notes point out that the Hölder scale is essential: there are continuous compactly supported $f$ for which $\Gamma * f$ is not $C^2$, so no estimate of $D^2 u$ by the maximum of $|f|$ holds. The endpoint $\alpha = 1$ is excluded from the theorem.

All four statements are classical and proved in the notes; none is new mathematics. As far as the Prove2Me corpus and Mathlib show, none has been machine-checked. Mathlib has the Laplacian on inner product spaces, convolution, and the volume of Euclidean balls, but no fundamental solution of the Laplacian in general dimension, no Newtonian potential, and no Hölder estimates for it. A formalization would supply reusable infrastructure: the fundamental solution with its derivative formulas, differentiation under the integral sign with a locally integrable kernel, and estimates for kernels homogeneous of degree $-n$ with mean zero on spheres.

Difficulty

The obvious route to the second derivatives, differentiating twice under the integral sign, fails: $\partial_{ij}\Gamma$ is of order $|x|^{-n}$ near the origin and is not locally integrable, so $\int \partial_{ij}\Gamma(x-y) f(y)\,dy$ need not exist. Corollary 2.27 is precisely the statement that the correct formula carries a subtracted value $f(x)$ and a boundary contribution $-\frac1n f(x)\delta_{ij}$, and computing that contribution needs integrals over spheres, which Mathlib supports only indirectly. For the goal, a pointwise bound on the kernel is not enough. Estimating $|\partial_{ij}\Gamma(x-y)|\,|f(y)-f(x)|$ in absolute value gives a bound that grows with the radius of the ball containing the support of $f$, while the theorem's constant must be uniform over all $f$, all indices and all pairs of points. The estimate depends on cancellation in the kernel, and the maximum-norm version of the same statement is false.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with volume. Every theorem assumes 2 ≤ n; the definition of $\Gamma$ returns junk values for $n = 0, 1$, which the book excludes.
• $\Gamma(0)$ is undefined in the book; in Lean it equals $0$ (from $1/0 = 0$ and $\log 0 = 0$), one point of measure zero.
• Coordinates are 0-based (i : Fin n). $\partial_i u(x)$ is fderiv ℝ u x (EuclideanSpace.single i 1), and $\partial_{ij} u = \partial_i(\partial_j u)$. fderiv is $0$ where $u$ is not differentiable, so $\partial_{ij}\Gamma(x-y)$ in Corollary 2.27 has an arbitrary value at the single point $y = x$.
• "Smooth" is ContDiff ℝ ∞ ($C^\infty$). In this Mathlib ContDiff ℝ ⊤ means analytic, and it is not used. Compact support is HasCompactSupport, and "the support of $f$" is the closed support tsupport f.
• $\Delta$ is Mathlib's InnerProductSpace.laplacian.
• The convolution $\Gamma * f$ is the Lebesgue integral $\int \Gamma(x-y) f(y)\,dy$, with no integrability assumed of $\Gamma$. Lean's Bochner integral is $0$ for a non-integrable integrand, so Theorem 2.25 asserts integrability of $y \mapsto \Gamma(x-y)f(y)$ for every $x$, and Corollary 2.27 asserts integrability of its integrand on the ball. Both are true and are implicit in the book's formulas; they rule out reading an identity between junk values as the theorem.
• The Hölder seminorm is a supremum in $[0,\infty]$ over all pairs of distinct points of $\mathbb{R}^n$, not Mathlib's HolderWith, which fixes a constant. In the goal $C$ is a finite nonnegative real quantified before $f$, $i$ and $j$. The inequality therefore also asserts that $\partial_{ij} u$ is uniformly $\alpha$-Hölder, because $[f]_{0,\alpha} < \infty$ for $f \in C_c^\infty$. A formalization that takes $C$ after $f$, lets it depend on the support of $f$, or includes the excluded endpoint $\alpha = 1$ is not the theorem.
• Theorem 2.26 of the notes (the same representation over an arbitrary smooth domain, with a surface integral over $\partial\Omega$) is not stated, because a faithful statement needs a surface measure on general smooth boundaries. The singular-integral discussion of §2.8 is commentary and is not stated.

Useful infrastructure, all reusable beyond this mission: differentiation of $\Gamma$ away from the origin; integration in polar coordinates and integrals of $|x|^{-a}$ over balls and annuli; surface integrals over spheres, or the divergence theorem on balls; differentiation under the integral sign for convolutions with a locally integrable kernel. Contributions of any of these as separate lemmas are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §2.6–2.8 and Definition 1.1. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• L. C. Evans, Partial Differential Equations, 2nd ed., Graduate Studies in Mathematics 19, AMS, 2010, §2.2. https://doi.org/10.1090/gsm/019
• D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Springer, 2001 (reprint of the 1998 ed.), Ch. 4. https://doi.org/10.1007/978-3-642-61798-0
• J. Schauder, Über lineare elliptische Differentialgleichungen zweiter Ordnung, Mathematische Zeitschrift 38 (1934), 257–282. https://doi.org/10.1007/BF01170635
• A. P. Calderón and A. Zygmund, On the existence of certain singular integrals, Acta Mathematica 88 (1952), 85–139. https://doi.org/10.1007/BF02392130

Motivation

Two problems in this mission, both about markets that do not behave the way the textbook Black–Scholes market does, and both solved by the same technique.

The first is portfolio choice in a pure jump market. Prices move by jumps at the epochs of a Poisson process, not by continuous Brownian fluctuation. This is not a technical variation: the market is incomplete, there is no replicating portfolio, and the machinery of stochastic analysis that makes the diffusion case tractable is unavailable. What is available instead is that the wealth process is piecewise deterministic — between jumps it follows an ODE, and all the randomness is in when the jumps happen and how big they are. Chapter 8's technique embeds such a process in its jump chain and turns the continuous-time control problem into a discrete-time Markov Decision Model with infinite horizon; Chapter 7's contracting theory then solves that.

The second is trade execution in an illiquid market. An agent must sell a large block of shares by a deadline. Placing the whole order at once moves the price against them, and in a traditional order book other participants can see the intention and trade against it — so the order goes to a dark pool, where there is no order book and matches arrive at random. The agent can only sell when a counterparty happens to appear, and whatever is unsold at the deadline must be dumped on the traditional market at once. The question is how much to offer at each opportunity.

The two problems have opposite curvature — the first is a concave maximisation of utility, the second a convex minimisation of cost — and the section is a good demonstration that the same embedding technique handles both, with each problem's structure entering only through which set of functions the value function is sought in.

Setting

The jump market (§9.3). The bond is S⁰_t = e^{ρt}; the risky assets follow dS^k_t = S^k_{t-}(μ_k dt + dC^k_t) where C_t = Σ_{n≤N_t} Y_n is a compound Poisson process of intensity λ whose jumps Y_n are supported in (-1,∞)^d, which keeps prices positive. Short-sellings are prohibited, so the admissible fractions of wealth form the compact set 𝒰 = {u ≥ 0, u·e ≤ 1}, and the wealth follows

$$dX_t = X_{t-}\big((\rho + \pi_t\cdot(\mu-\rho e))dt + \pi_t dC_t\big). \tag{9.10}$$

The investor maximises E^π_{tx}[U(X_T)] for a strictly increasing, strictly concave U.

The embedded model's state is (t,x) — a jump time and the wealth just after it — and its action is a whole control path α : [0,T] → 𝒰, followed until the next jump. Between jumps the wealth is φ^α_t(x) = x exp(∫₀^t (ρ + α_s·(μ-ρe))ds) (9.13), and the transition kernel is substochastic: with probability e^{-λ(T-t)} no further jump arrives before the horizon, and the reward r(t,x,α) = e^{-λ(T-t)}U(φ^α_{T-t}(x)) is collected instead.

The trade execution model (§9.4). A Poisson process of intensity λ delivers the trading epochs; selling a shares costs C(a) with C strictly increasing and strictly convex (the discrete form (9.19)), C(0) = 0; the inventory X_t = x₀ - ∫₀^t π_s dN_s is what remains, and C(X_T) is the terminal dump. Here the flow is uncontrolled — the inventory does not move between epochs — which makes the embedded model simpler.

What is being asked

The goal is Theorem 9.3.4, the main result for the terminal wealth problem, in all six of its parts: the value function is the limit of the value iteration and lies in IM_cv; it is the unique fixed point of the dynamic programming operator there; value iteration converges at the explicit geometric rate α_b^n/(1-α_b); there exists an optimal Markov portfolio strategy given by a single decision rule; policy iteration holds; and Howard's policy improvement algorithm holds. Parts a)–c) describe the value; parts d)–f) produce the strategy, and a formalization of the first three alone would omit the entire control half of the theorem.

The seven milestones are the rest of §9.3–9.4: the reduction from continuous to discrete time, the bounding function and its explicit contraction modulus, the invocation of Chapter 7's Structure Theorem, the iff-characterization of when holding only the bond is optimal, the stability of the value and of the optimal policies under perturbation of the utility, and then the trade execution problem's own bounding function and its monotone, unit-Lipschitz optimal execution rate.

Two formalization conventions run through everything here. The operator of §9.3 is a supremum over a space of control paths, and since Mathlib's sSup of a set unbounded above is 0 — with an unbounded reward that is a live risk, not a formality — it is carried as a relation defined by least upper bounds against explicit sets of achievable values, with its iterates a chain of such relations. And the continuous-time side is built, not assumed: Theorem 9.3.1 is the identification of the continuous-time value with the discrete-time one, so the law of the embedded jump chain is pinned by the one-step conditional law the book displays, and the terminal wealth is read off that chain.

Motivation

A correlated equilibrium (Aumann, 1974) is a joint distribution over the players' strategy profiles from which no player gains by deviating from a recommended strategy. A central question of learning in games is which equilibria repeated play of simple, myopic rules can reach. Foster and Vohra (1997) answered it for calibrated forecasting: if each player forecasts the opponent with a calibrated rule and best-responds to the forecast, the empirical distribution of play approaches the set of correlated equilibria (their Theorem 1). That result has become a basic reference point for no-regret and calibration-based learning in games (Hart and Mas-Colell, 2000).

This mission formalizes the paper's converse. Theorem 1 says calibrated learning ends up in the correlated equilibria; the converse says it can end up at any of them, for almost every game. Together the two results characterize exactly which long-run outcomes calibrated learning with best responses can produce.

Setting

Two players choose strategies from finite sets $S(1)$ with $m$ elements and $S(2)$ with $n$ elements; player $i$ receives payoff $u_i(x,y)\in\mathbb{R}$ and maximizes it. A game $G=(u_1,u_2)$ is a pair of real $m\times n$ matrices, that is, a point of $\mathbb{R}^{2mn}$; a set of games has measure zero if it is Lebesgue-null in $\mathbb{R}^{2mn}$.

A joint distribution $D$ on $S(1)\times S(2)$ is a correlated equilibrium if for every map $\Phi:S(1)\to S(1)$, $\sum_{x,y}D(x,y)u_1(\Phi(x),y)\le\sum_{x,y}D(x,y)u_1(x,y)$, and symmetrically for player 2. $\pi(G)$ is the set of correlated equilibria.

Play is repeated in rounds $t=0,1,2,\dots$. Before each round, player 1 issues a forecast $f_1(t)$, a probability vector over $S(2)$, produced by a deterministic forecasting rule from the history of play so far; player 2 likewise forecasts player 1. For a forecast sequence $f$ and the opponent's plays $z$, let $N(p,t)$ be the number of the first $t$ rounds with forecast $p$, and $\rho(p,j,t)$ the fraction of those rounds in which the opponent played $j$ (zero if $N(p,t)=0$). The forecasts are calibrated if for every $j$

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

Each player then plays $R_i$ of its forecast, where the best-reply function $R_i$ picks a best response to every forecast and does not depend on the round. $D_t(x,y)$ is the fraction of the first $t$ rounds in which $(x,y)$ was played.

$\lambda(G)$, the set of limit points of calibrated forecasts, consists of the $D$ for which some best-reply functions $R_1,R_2$ and some calibrated forecasting rules make $D_t(x,y)\to D(x,y)$ for all $(x,y)$.

Formalization targets

Goal: Theorem 2 (p. 47)

$$\text{for Lebesgue-almost every } G\in\mathbb{R}^{2mn}:\qquad \lambda(G)=\pi(G).$$

Milestones

1. $\lambda(G)\subseteq\pi(G)$ for every game (Theorem 1 restated, p. 46).
2. Every joint distribution $D$ is the limiting empirical distribution of a deterministic play sequence supported on $\{D>0\}$ (p. 47).
3. Along such a sequence the conditional forecasts $p_{1,t}=D(x_t,\cdot)/\sum_yD(x_t,y)$ and $p_{2,t}=D(\cdot,y_t)/\sum_xD(x,y_t)$ are calibrated (p. 47).
4. In a correlated equilibrium each recommended strategy is a best response to its conditional forecast (p. 47).
5. For almost every payoff matrix, each set $M_b(x)$ of forecasts to which $x$ is a best response is either empty or contains a forecast in the open simplex at which $x$ is the unique best response (p. 47).
6. The perturbed forecasts $p_i=(1-1/i)p^*+(1/i)q$ converge to $p^*$ and keep a unique best reply (p. 48).
7. For the $3\times3$ game of p. 48, a correlated equilibrium lies outside $\lambda(G)$, and $\lambda(G)$ is the single point mass on $(C,2)$.

Significance

Theorem 1 by itself leaves open whether calibration selects among correlated equilibria, for instance toward Nash equilibria or toward particular payoffs. Theorem 2 closes that question negatively for generic games: every correlated equilibrium is the genuine limit, not merely an accumulation point, of calibrated play with stationary best replies. As the paper notes, adding the assumption that the limit exists therefore does not refine the equilibrium reached, in contrast with Fudenberg and Kreps's result for asymptotically myopic Bayesian play. The $3\times3$ example shows that the genericity hypothesis cannot be dropped.

The results are proved in the 1997 paper; none is formalized. A complete development produces a reusable layer for repeated two-player games (calibration, empirical distributions, best-reply maps, correlated equilibria), a genericity lemma for best-response regions that is useful beyond this paper, and a machine-checked version of an argument that the paper gives only in outline.

Difficulty

The natural construction takes a correlated equilibrium $D$, a play sequence realizing $D$, and forecasts equal to the conditional distributions of $D$. The forecasts are then calibrated and each played strategy is a best response. What fails is the best-reply function: two strategies $x'\ne x''$ can have the same conditional forecast $p^*$, while a stationary $R_1$ maps $p^*$ to only one strategy. Separating them needs forecasts near $p^*$ at which each is the unique best response, and that exists only when the best-response regions have nonempty relative interior, a property that fails on a null set of games (the $3\times3$ example) and whose genericity must be proved. The perturbed forecasts are no longer exactly equal to the conditional frequencies, so calibration has to be re-established with errors that vanish along the sequence.

Formalization scope

• Strategies are Fin m and Fin n; payoffs are real matrices; players maximize. A game is a point of (Fin m → Fin n → ℝ) × (Fin m → Fin n → ℝ) with Mathlib's volume (Lebesgue measure on $\mathbb{R}^{2mn}$), and "almost every" is ∀ᵐ.
• A correlated equilibrium is the joint-distribution form of p. 44 (a joint distribution with the two deviation inequalities).
• Forecasting rules map finite histories to probability vectors; the play is generated recursively from the rules and the best-reply functions. Best-reply functions are arbitrary stationary selections of a best response at every probability vector; they may not depend on the round, since round-dependent tie-breaking enlarges $\lambda(G)$ (the matching pennies example of p. 46).
• Rounds are $0,\dots,t-1$; $D_0=0$. The calibration sum runs over the forecasts issued so far, which is the paper's sum over all $p$ since the other terms vanish.
• $\lambda(G)$ requires convergence of $D_t$, not a subsequence. Replacing the limit by a limit point, or stating only $\pi(G)\subseteq\lambda(G)$, does not formalize the theorem.
• The page's sentence "Almost every game has the property that all the sets $M_b(x)$ have non-empty interior" is false for dominated strategies ($M_b(x)=\emptyset$ on an open set of games). Milestone 5 states the dichotomy the page's argument proves: empty or with relative interior.
• The page prints the denominator of $p_{2,t}$ as $\sum_{x}D(x_t,y)$; the mission uses $\sum_xD(x,y_t)$.

The theorems are stated from the mission's own definitions of the game, calibration and $\lambda(G)$; no statement is vacuous: at $m=0$ or $n=0$ both sides of the goal are empty, and the $3\times3$ example exercises every definition. Contributions welcome: proofs of the milestones in any order, the genericity lemma (Lebesgue-null sets of linear degeneracies), and the calibration estimates for the perturbed forecasts.

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
• 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
• 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
• D. Fudenberg and D. M. Kreps, Learning mixed equilibria, Games and Economic Behavior 5 (1993), 320–367. https://doi.org/10.1006/game.1993.1021
• 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

Convexity on the integer lattice cannot be defined by the classical secant-line inequality alone: a function can be midpoint-convex along every line and still admit no useful global optimality theory, because integer points off a chosen line are invisible to it. M-convex functions, introduced by Murota, resolve this by replacing the secant condition with an exchange axiom directly generalizing the basis-exchange property of matroids and the convex-hull structure of network flows: a function on the integer lattice is M-convex if, whenever two points can be improved by moving one coordinate up and a compensating coordinate down, at least one such move weakly improves the sum of the two function values. This single axiom turns out to be equivalent to several strikingly different-looking properties — invariance under a wide family of domain operations, supermodularity in the M♮ (translation-invariant) case, and, most importantly, a local-to-global optimality principle: a point is a global minimizer of an M-convex function if and only if no single coordinate exchange improves it. This mission develops the algebraic core of that theory — the exchange axiom's basic consequences, its equivalent local and dynamic reformulations, and the operations that preserve it — building toward the theorem that recasts M-convexity itself as an algorithmically meaningful local-search guarantee.

Companion mission 06-mconvex-functions-i (Discrete Convex Analysis V) covers this chapter's own primary line of development: the equivalence of M-convexity and M♮-convexity with their respective exchange axioms (Theorem 6.2), the M-optimality criterion (Theorem 6.26), a minimizer-cut lemma (Theorem 6.28), and the M-proximity theorem (Theorem 6.37, its goal). This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the results that chapter leaves for a second pass: the domain structure of M- and M♮-convex functions, worked examples (quadratic forms, quasi-separable functions), the operations that preserve M-convexity, supermodularity of the M♮-convex case, the descent-direction property, and — this mission's goal — the equivalence of the exchange axiom with a dynamic sequential-improvement property.

Setting

Fix a finite ground set $V$. A function $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain $\operatorname{dom} f$ is M-convex if it satisfies the exchange axiom (M-EXC[Z]): for $x, y \in \operatorname{dom} f$ and $u \in \operatorname{supp}^+(x-y)$ (coordinates where $x$ exceeds $y$), there is $v \in \operatorname{supp}^-(x-y)$ with

$$f(x) + f(y) \ge f(x - \chi_u + \chi_v) + f(y + \chi_u - \chi_v).$$

Writing $\tilde f(x_0, x) = f(x)$ when $x_0 = -x(V)$ and $+\infty$ otherwise (a lift to one extra coordinate), $f$ is M$^\natural$-convex if $\tilde f$ is M-convex; M♮-convexity is a genuine generalization of M-convexity (every M-convex function is M♮-convex, but not conversely) and coincides with it exactly when $\operatorname{dom} f$ lies on a single hyperplane. The linear-weighted function $f[p](x) = f(x) - \langle p, x \rangle$ (for $p \in \mathbb R^V$) is the standard device for testing local optimality under an arbitrary reweighting.

Formalization targets

Goal: the exchange axiom as sequential improvement

$$f \text{ is M-convex} \iff \forall p \in \mathbb R^V,\ \forall x, y \in \operatorname{dom} f,\ f[p](x) > f[p](y) \implies f[p](x) > \min_{u \in \operatorname{supp}^+(x-y)}\ \min_{v \in \operatorname{supp}^-(x-y)} f[p](x - \chi_u + \chi_v),$$

with the analogous statement for M♮-convexity (Theorem 6.24). This is the weakest stable form: it makes no reference to a specific algorithm, only to the existence of an improving single exchange whenever the current point is suboptimal under any linear reweighting — a property a faster algorithm could exploit without invalidating the characterization itself.

Supporting structural targets

Eleven further results build the vocabulary and toolkit this goal draws on: the domain structure of M-convex and M♮-convex functions (Propositions 6.1, 6.7), the equivalence of the exchange axiom with a local, bounded-distance version (Theorem 6.4), worked examples establishing M-convexity for quadratic forms, univariate, conservation-law, and quasi-separable functions (Propositions 6.8-6.9), the domain and range operations preserving M-convexity (Theorem 6.13, Proposition 6.14), supermodularity of the M♮-convex case (Theorem 6.19), the descent-direction property (Proposition 6.23) that Theorem 6.24 generalizes, and a discrete subgradient inequality (Proposition 6.25).

Significance

Theorem 6.24 is the bridge between the static exchange axiom (a property of function values at pairs of points) and the dynamic behavior of local-search algorithms: it says a greedy single-coordinate-exchange step, applied to any linearly reweighted version of an M-convex function, always finds a strict improvement when one exists. This is exactly the guarantee that makes steepest-descent-type algorithms for M-convex function minimization correct, and it is the theorem chapter 10's algorithmic analysis (Schrijver-type methods) relies on implicitly whenever it argues that local exchange steps make global progress. The descent-direction property (Proposition 6.23) is the special case $p=0$, isolating the core combinatorial fact before the reweighting machinery is added. The operations catalog (Theorem 6.13) is the practical toolkit that lets later chapters build complex M-convex functions (network flow costs, matroid rank functions composed with linear maps) from simple pieces without re-verifying the exchange axiom from scratch each time.

None of these results are open — they are Murota's own systematic development of the exchange- axiom theory, with worked examples drawn from classical quadratic and separable function theory. What this mission contributes is a faithful, machine-checked formal statement of each, sharing the Lean vocabulary (MExchangeAxiom, MNaturalConvex, LinearWeight) the rest of the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The forward direction of Theorem 6.24 (M-convex $\implies$ sequential improvement) follows in one step from Proposition 6.23 applied to $f[p]$, itself M-convex by Theorem 6.13(3) — routine once those two pieces are in hand. The converse is the substantial direction: it must derive the full static exchange axiom from a property that only ever exhibits some improving exchange at some linear weighting, for every pair of suboptimal points — the proof constructs an explicit adversarial weighting $p$ designed so that failure of the local exchange step at that specific $p$ forces the domain itself to be M-convex (via Theorem 4.3) and then forces the local exchange axiom (M-EXCloc[Z]) via a bipartite-matching argument on the coordinates that differ, finally invoking Theorem 6.4 to lift locality to the full exchange axiom. No shortcut bypasses this two-stage reduction (domain structure, then local exchange) — attempting to verify (M-EXC[Z]) directly from (M-SI[Z]) without first pinning down that $\operatorname{dom} f$ is M-convex fails because the exchange axiom's own statement presupposes a well-structured domain.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; functions are (V → ℤ) → WithTop ℝ. SuppPos/SuppNeg are Finset V (not Set V), matching how the (M-SI[Z])/(M♮-SI[Z]) axioms and the descent-direction property use Finset.inf, whose value on an empty index set is ⊤ — exactly the book's own stated convention for an empty minimum. No Module ℝ or ConvexOn machinery is used for WithTop ℝ-valued arithmetic; scalar actions by positive reals (PosScalarMul, Theorem 6.13(1)) and by naturals (FCheck's flow coefficients, Proposition 6.25) are built directly from the native order and AddMonoid structure. No numeric constants are hard-coded anywhere in this mission (rule 7 is vacuous); Proposition 6.8's quadratic-form conditions are stated with the book's own literal coefficients ($0$, and the min/≥ structure of Eq. (6.25)-(6.28)), not a special case. Theorem 6.13's parts (7) (aggregation) and (8) (integer infimal convolution) are not restated here since the book itself proves them only later via Chapter 9's network-transformation machinery — see the Difficulty note and MODERATION_NOTES.md; this is not a trivializing omission, since the six operations that are included already exercise every domain- and range-transformation technique this mission's goal needs. This mission's definitions (MExchangeAxiom, MNaturalConvex, CharVec, DomZ, SuppPos, SuppNeg, CharVecOpt) are redeclared from chunk 06-mconvex-functions-i rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the twelve sorrys are welcome; the goal's converse direction and Theorem 6.13's operations are the two with the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 (the exchange axiom and its equivalent local/dynamic reformulations).

Motivation

Financial regulators and risk managers summarise the loss distribution of a position by a single number, the capital that must be held against it. The two standards in practice are Value-at-Risk (VaR), a quantile of the loss, and expected shortfall (ES), an average of the upper quantiles; ES is the standard of the Basel framework. Both depend on the position only through its probability law, a property called law invariance, which is what allows them to be estimated from data.

The axiomatic theory of risk measures, starting with Artzner, Delbaen, Eber and Heath (1999) and Föllmer and Schied (2002), centres on convex risk measures. VaR is not convex, however, and neither are its robust variants used in practice: the maximum or the median of VaR over a set of scenario models, or the benchmark-loss VaR of Bignozzi, Burzoni and Munari (2020). Castagnoli, Cattelan, Maccheroni, Tebaldi and Wang (Operations Research 70(5), 2022) propose star-shapedness as the common property of all of these measures: doubling the exposure to a risky position at least doubles the required capital. Their Section 7 identifies exactly which law-invariant risk measures are star-shaped.

Timeline:

• 1999: Artzner et al. introduce coherent risk measures and show that ES-type measures dominate VaR (doi:10.1111/1467-9965.00068).
• 2002: Föllmer and Schied introduce convex risk measures.
• 2020: Mao and Wang characterise the risk measures consistent with second-order stochastic dominance as infima of ES-based functionals.
• 2022: Castagnoli et al. prove Theorem 5, the corresponding characterisation of star-shaped law-invariant risk measures through VaR.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space with $P$ atomless: every event of positive probability contains an event of strictly smaller positive probability. A position is a bounded measurable function $X:\Omega\to\mathbb R$, read as a loss: $X(\omega)>0$ is money lost in state $\omega$. The positions form a linear space $\mathcal X$ that contains the constants and carries the pointwise order $X\geqq Y$.

A risk measure is a function $\rho:\mathcal X\to\mathbb R$ that is monotone ($X\geqq Y\Rightarrow\rho(X)\ge\rho(Y)$), translation invariant ($\rho(X-m)=\rho(X)-m$ for real $m$) and normalized ($\rho(0)=0$). It is star-shaped if $\rho(\lambda X)\ge\lambda\rho(X)$ for all $X$ and all $\lambda>1$, and law-invariant if $X$ and $Y$ with the same law under $P$ satisfy $\rho(X)=\rho(Y)$. Its acceptance set is $\mathcal A_\rho=\{X\mid\rho(X)\le 0\}$. A set $S$ in a vector space is star-shaped if $\lambda s\in S$ whenever $s\in S$ and $\lambda\in[0,1]$.

For $\alpha\in(0,1)$ the Value-at-Risk of $X$ is

$$\mathrm{VaR}_\alpha(X)=\inf\{x\in\mathbb R : P(X>x)\le 1-\alpha\}.$$

Write $F_X(x)=P(X\le x)$. A loss $X$ first-order stochastically dominates $Y$, written $X\succsim_{\mathrm{FSD}}Y$, if $F_X\ge F_Y$ pointwise, so $X$ is the smaller loss.

Formalization targets

Goal: Theorem 5, (i) ⇔ (ii)

For a function $\rho:\mathcal X\to\mathbb R$ the following are equivalent:

1. $\rho$ is a star-shaped and law-invariant risk measure;
2. there is a star-shaped set $\mathcal G$ of increasing functions $g:(0,1)\to\mathbb R$ with $g(0+)\le 0$ such that

$$\rho(X)=\inf_{g\in\mathcal G}\ \sup_{\alpha\in(0,1)}\ \{\mathrm{VaR}_\alpha(X)-g(\alpha)\}\qquad X\in\mathcal X.\tag{25}$$

The goal fixes neither $\mathcal G$ nor any constant. The paper's "Moreover" clause, closure of the class under the operations of Theorem 1, is excluded: its proof is a citation of Liu et al. (2020, Theorem 2) plus "the rest is straightforward".

Milestones

• Eq. (7): $\rho(X)=\min\{m\in\mathbb R\mid X-m\in\mathcal A_\rho\}$ for every risk measure.
• Proposition 2: for a risk measure $\rho$, the following are equivalent: $\rho$ is star-shaped; $\mathcal A_\rho$ is star-shaped; $\rho=\rho_{\mathcal A}$ for a star-shaped acceptance set $\mathcal A$.
• Eq. (A.1): $F_X\ge F_Y$ if and only if $\mathrm{VaR}_\alpha(X)\le\mathrm{VaR}_\alpha(Y)$ for all $\alpha\in(0,1)$.
• FSD consistency (proof of Theorem 5): if $P$ is atomless and $\rho$ is monotone and law-invariant, then $X\succsim_{\mathrm{FSD}}Y\Rightarrow\rho(X)\le\rho(Y)$.

Significance

Theorem 5 says that the star-shaped law-invariant risk measures are exactly the robustifications of VaR: each benchmark $g$ in $\mathcal G$ gives a capital requirement $\sup_\alpha\{\mathrm{VaR}_\alpha(X)-g(\alpha)\}$, and $\rho$ takes the most favourable benchmark. The class contains VaR, ES, their scenario-based maxima and the benchmark-loss VaR. The theorem parallels Theorem 4 of the same paper, derived from Mao and Wang (2020), in which ES replaces VaR and SSD-consistency replaces law invariance. Together the two results separate the two classes: VaR is star-shaped and law-invariant but not SSD-consistent. Section 7 also records that star-shaped law-invariant measures are in general not minima of law-invariant convex risk measures, which is why a representation specific to VaR is needed.

On the formal side, the result is proved in the paper; no machine-checked proof is known. The mission yields a Lean library of law-invariant risk measures on bounded measurable positions, a quantile-based Value-at-Risk with its basic order properties, and the FSD-consistency of monotone law-invariant functionals on atomless spaces. That last statement is the probabilistic core that other law-invariant representation theorems reuse.

Difficulty

The direction (ii) ⇒ (i) is a direct computation. The direction (i) ⇒ (ii) rests on FSD consistency. The obvious argument writes $X\succsim_{\mathrm{FSD}}Y$ as $X\le Y$ and applies monotonicity, but first-order dominance compares only laws, and two positions ordered in law need not be ordered state by state. One must construct positions with the laws of $X$ and $Y$ that are ordered pointwise, and this uses atomlessness in an essential way: on a space with atoms, the construction can fail. The remaining steps are bookkeeping of extended-real infima and suprema, including levels $\alpha$ near $0$ where $g$ may diverge.

Formalization scope

Positions are the bounded measurable functions $\Omega\to\mathbb R$ (a Submodule ℝ (Ω → ℝ), definition Positions) with the pointwise order, rather than equivalence classes in $L^\infty(\Omega,\mathcal F,P)$. For a law-invariant $\rho$ the two readings agree: almost surely equal positions have the same law, and a position that dominates another almost surely has a pointwise modification with the same law that dominates it everywhere. Atomlessness is defined locally (IsAtomless), because Mathlib's NoAtoms only states that singletons are null, which is weaker. Law invariance compares push-forward measures P.map X; measurability is part of Positions, so these are never degenerate.

VaR is an sInf of reals and is applied only to bounded positions at levels in $(0,1)$, where the infimum is over a nonempty set that is bounded below. In (25) each function $g$ has domain exactly $(0,1)$, "increasing" means weakly increasing, and $g(0+)\le 0$ is stated as $\inf_{\alpha\in(0,1)}g(\alpha)\le 0$ in the extended reals. Both sides of (25) are compared in the extended reals, since the inner supremum can be $+\infty$. The minimum in Eq. (7) is an attained minimum (IsLeast), and the supremum condition on acceptance sets is a least upper bound (IsLUB).

These choices rule out the trivialising formalizations of (25). A real-valued supremum would read an unbounded supremum as $0$. Dropping monotonicity of $g$ or the condition $g(0+)\le 0$ describes a larger class that includes non-normalized functionals. Allowing $\mathcal G=\emptyset$ is excluded because the left side of (25) is a real number and the right side would be $+\infty$.

The following are not part of the mission: the "Moreover" clause of Theorem 5, Theorem 4 (its main direction is Mao and Wang 2020, Theorem 3.1), and Proposition 7 (ES as the smallest SSD-consistent risk measure dominating $\mathrm{VaR}_\alpha$), which would need second-order dominance and ES as additional definitions.

Reusable infrastructure: VaR on bounded measurable functions and its homogeneity and translation properties; the equivalence (A.1); existence of a uniform random variable on an atomless probability space and the quantile coupling it provides. Proofs of these as separate lemmas are welcome.

Selected references

• E. Castagnoli, G. Cattelan, F. Maccheroni, C. Tebaldi, R. Wang, Star-Shaped Risk Measures, Operations Research 70(5):2637–2654, 2022. https://doi.org/10.1287/opre.2022.2303
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, 4th ed., De Gruyter, 2016. https://doi.org/10.1515/9783110463453
• T. Mao, R. Wang, Risk Aversion in Regulatory Capital Principles, SIAM Journal on Financial Mathematics 11(1):169–200, 2020 (cited as Mao and Wang 2020 in the source paper).
• V. Bignozzi, M. Burzoni, C. Munari, Risk Measures Based on Benchmark Loss Distributions, Journal of Risk and Insurance, 2020 (cited as Bignozzi et al. 2020 in the source paper).