Missions · Prove2Me

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

A Soft Robust Model for Optimization Under Ambiguity: For Every δ > 0, Soft Robust Feasibility Is a Convex Risk Measure Constraint, and Every Normalized Convex Risk Measure Arises This WayResearch Paper

Motivation

Optimization under uncertainty usually fixes one probability distribution $\mathbb P$ for the uncertain data and optimizes an expected payoff, or fixes a set $\mathcal Q$ of distributions and protects against the worst one (robust optimization). The first is sensitive to a misspecified $\mathbb P$ ; the second can be very conservative, because it treats a barely plausible distribution exactly like the nominal one. Ben-Tal, Bertsimas and Brown (Oper. Res. 58(4), 2010) propose a graded alternative, the soft robust model: the decision maker accepts a loss of at most $\varepsilon$ in expected payoff under every distribution of a set $\mathcal Q(\varepsilon)$ , simultaneously for all levels $\varepsilon$ up to a budget $\delta$ . Larger sets of distributions are allowed a larger shortfall.

The paper's central result, Theorem 2.1, shows that this model is exactly a constraint on a convex risk measure in the sense of Föllmer and Schied (Finance Stoch. 6, 2002), and that every normalized convex risk measure arises from some soft robust model. This connects distributionally robust optimization with the theory of monetary risk measures, and gives a tractable convex reformulation of soft robust constraints. Related earlier work connected coherent risk measures with standard robust optimization (Bertsimas and Brown, Oper. Res. 57(6), 2009).

Setting

Let $(\Omega,\mathcal F)$ be a measurable space and $\mathcal P$ the set of all probability measures on it. A decision $x$ ranges over a nonempty, closed, convex set $X\subseteq\mathbb R^n$ ; a random variable $u:\Omega\to\mathbb R^m$ carries the uncertain parameters, and $f(x,u(\omega))$ is the payoff, concave in $x\in X$ for every $\omega$ . For each $x\in X$ the random variable $f(x)=f(x,u(\cdot))$ is assumed bounded and measurable.

A family of measures is $\mathbf Q=\{\mathcal Q(\varepsilon)\subseteq\mathcal P:\varepsilon\ge0\}$ . It is nondecreasing if $\mathcal Q(\varepsilon_1)\subseteq\mathcal Q(\varepsilon_2)$ for $\varepsilon_1\le\varepsilon_2$ , and convex if $\mathbb Q_i\in\mathcal Q(\varepsilon_i)$ implies $\lambda\mathbb Q_1+(1-\lambda)\mathbb Q_2\in\mathcal Q(\lambda\varepsilon_1+(1-\lambda)\varepsilon_2)$ for $\lambda\in[0,1]$ . The standing assumptions are that $\mathbf Q$ is nondecreasing and convex and that $\mathcal Q(0)\neq\emptyset$ . The soft robust feasible set at level $\delta\ge0$ is

X^Q(\delta)=\Big\{x\in X:\ \inf_{\mathbb Q\in\mathcal Q(\varepsilon)}\mathbb E_{\mathbb Q}[f(x)]\ \ge\ -\varepsilon\quad\forall\,\varepsilon\in[0,\delta]\Big\}.\tag{5}

A risk measure, on the space $\mathcal Y$ of bounded payoffs, is a map $\rho:\mathcal Y\to\mathbb R$ with $Y_1\ge Y_2\Rightarrow\rho(Y_1)\le\rho(Y_2)$ and $\rho(Y+c)=\rho(Y)-c$ for $c\in\mathbb R$ ; it is convex if $\rho(\lambda Y_1+(1-\lambda)Y_2)\le\lambda\rho(Y_1)+(1-\lambda)\rho(Y_2)$ . It is generated by a convex penalty $\alpha:\mathcal P\to[0,\infty]$ if $\rho(Y)=\sup_{\mathbb Q\in\mathcal P}\{-\mathbb E_{\mathbb Q}[Y]-\alpha(\mathbb Q)\}$ , and normalized if in addition $\alpha(\mathbb Q)=0$ for some $\mathbb Q$ . A family and a penalty determine each other:

\alpha^Q(\mathbb Q)=\inf\{\varepsilon\ge0:\mathbb Q\in\mathcal Q(\varepsilon)\},\qquad \mathcal Q^\alpha(\varepsilon)=\{\mathbb Q\in\mathcal P:\alpha(\mathbb Q)\le\varepsilon\},

and $\rho^Q$ denotes the risk measure generated by $\alpha^Q$ .

Formalization targets

Goal: Theorem 2.1 for $\delta>0$

For every nondecreasing, convex family $\mathbf Q$ with $\mathcal Q(0)\ne\emptyset$ , $\rho^Q$ is a convex risk measure generated by the normalized convex penalty $\alpha^Q$ , the minimum below is attained for every $x\in X$ , and

X^Q(\delta)=\Big\{x\in X:\ \min_{\lambda\ge0}\Big\{\lambda\delta+(\lambda+1)\,\rho^Q\Big(\frac{f(x)}{\lambda+1}\Big)\Big\}\le0\Big\}.\tag{6}

Conversely, for every convex risk measure $\rho$ generated by a normalized convex penalty $\alpha$ , the family $\mathbf Q^\alpha$ is nondecreasing and convex with $\mathcal Q^\alpha(0)\ne\emptyset$ , and (6) holds with $\rho$ on the right and $\mathbf Q^\alpha$ on the left.

Milestones: the steps of the proof (p. 1224)

The soft robust infimum $\inf\{\mathbb E_{\mathbb Q}[f(x)]+\varepsilon:\varepsilon\in[0,\delta],\ \mathbb Q\in\mathcal Q(\varepsilon)\}$ equals $\inf\{\mathbb E_{\mathbb Q}[f(x)]+\alpha^Q(\mathbb Q):\alpha^Q(\mathbb Q)\le\delta\}$ .
Strong duality with an attained multiplier: that infimum equals $\max_{\lambda\ge0}\{-\lambda\delta+\inf_{\mathbb Q}\{\mathbb E_{\mathbb Q}[f(x)]+(\lambda+1)\alpha^Q(\mathbb Q)\}\}$ .
The scaling identity $\inf_{\mathbb Q}\{\mathbb E_{\mathbb Q}[Y]+(\lambda+1)\alpha^Q(\mathbb Q)\}=-(\lambda+1)\rho^Q(Y/(\lambda+1))$ .
$\rho^Q$ is a convex risk measure generated by the convex, normalized penalty $\alpha^Q$ .
For a convex normalized $\alpha$ , $\mathbf Q^\alpha$ is nondecreasing and convex with $\mathcal Q^\alpha(0)\ne\emptyset$ .
$\alpha^{Q^\alpha}=\alpha$ .

Significance

Theorem 2.1 makes the soft robust constraint usable: the right side of (6) is a single constraint in $(\lambda,x)$ , and the function $(\lambda+1)\rho(f(x)/(\lambda+1))$ is jointly convex in $(\lambda,x)$ for $\lambda\ge0$ , so soft robust problems are convex programs whenever the risk measure can be evaluated. Read in the other direction, it gives every normalized convex risk measure an interpretation as a graded robustness requirement over the level sets of its penalty, which is how the paper derives soft robust counterparts of optimized certainty equivalents, CVaR and entropic risk, and its later bounds on the probability of a loss.

The theorem is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a Lean development of convex risk measures generated by penalties on an arbitrary measurable space, with extended-valued penalties and mixtures of probability measures, and a one-constraint Lagrange duality theorem over a convex set of probability measures. Mathlib does not currently provide Lagrange duality in this form.

Difficulty

The equalities of the proof read as routine, and two of them are not. The first equality is described as "the definition of $\alpha^Q$ ", but a measure with $\alpha^Q(\mathbb Q)=\delta$ need not belong to $\mathcal Q(\delta)$ , because the infimum defining $\alpha^Q$ need not be attained; the equality relies on the convexity of the family, the nonemptiness of $\mathcal Q(0)$ and the boundedness of $f(x)$ . The second equality is Lagrange duality with dual attainment for a convex program whose variable is a probability measure and whose objective and constraint are extended-valued; the classical theorem applies to convex subsets of vector spaces, and transferring it to mixtures of probability measures with $[0,\infty]$ -valued penalties is the main formal work. Attainment of the minimum in (6), which the paper asserts by writing "min", is exactly dual attainment and does not follow from the inequality alone.

Formalization scope

The probability measures are ProbabilityMeasure Ω on a measurable space; a family is a map from levels $\varepsilon\in\mathbb R_{\ge0}$ to sets of probability measures, and mixtures are built from the measures $t\,\mathbb Q_1+(1-t)\,\mathbb Q_2$ . Penalties, including $\alpha^Q$ , take values in $[0,\infty]$ , so that a measure in no $\mathcal Q(\varepsilon)$ has penalty $+\infty$ ; a real-valued $\alpha^Q$ would give such measures penalty $0$ through the junk value of an empty infimum, and is excluded. Risk measures are real functions whose axioms are imposed on bounded measurable payoffs, "generated by" includes the least-upper-bound property of the supremum, and "min" in (6) is attainment on $[0,\infty)$ together with a nonpositive minimum. The decision set and payoff carry the paper's assumptions; concavity of the payoff and closedness and convexity of $X$ are kept although Theorem 2.1 does not use them. Infima over measures in the milestones are taken in the extended reals.

The case $\delta=0$ is excluded. The paper states Theorem 2.1 for $\delta\ge0$ , but at $\delta=0$ its proof interchanges a limit in $\lambda$ with a supremum over measures without justification, and (6) fails: on $\Omega=\{a,b\}$ with $\mathcal Q(0)$ the measures giving $a$ mass at most $1/4$ and $\mathcal Q(\varepsilon)$ those giving it mass at most $1/2$ for $\varepsilon>0$ , the payoff $f(a)=-2$ , $f(b)=1$ is soft robust at level $0$ while the right side of (6) is empty. The goal and the milestones therefore fix $\delta>0$ , the case the paper's main argument treats.

A complete development needs: convex risk measures and their generation by penalties, mixtures of probability measures, Lagrange duality with Slater's condition over convex sets of measures, and the scaling identity for $\rho^Q$ . The duality theorem and the risk-measure layer are reusable beyond this mission. Contributions of any milestone are welcome, as are general convex-duality lemmas that the strong-duality step can import.

Selected references

A. Ben-Tal, D. Bertsimas, D. B. Brown, A Soft Robust Model for Optimization Under Ambiguity, Operations Research 58(4, Part 2):1220–1234, 2010. https://doi.org/10.1287/opre.1100.0821
H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072
H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, 2nd ed., de Gruyter, 2004. https://doi.org/10.1515/9783110212075
D. G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969, Chapter 8.
D. Bertsimas, D. B. Brown, Constructing Uncertainty Sets for Robust Linear Optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0695

10 thms3 active usersReviewed

Completed

Mathematical Logic Model Theory·Captain: Lucas

Continuum Hypothesis: Independence from ZFCTextbook

Motivation

The continuum hypothesis (CH) asks how large the set of real numbers is. Cantor proved that $|\mathbb Z|=|\mathbb Q|<|\mathbb R|$ , and in 1878 he conjectured that no set has cardinality strictly between that of the integers and that of the reals. Settling CH was the first of Hilbert's problems at the 1900 International Congress of Mathematicians. The question was answered by showing that it cannot be answered from the standard axioms: CH is independent of Zermelo–Fraenkel set theory with choice (ZFC).

Timeline (as recorded in the source):

1878 — Cantor formulates the (weak) continuum hypothesis; in 1882 he states CH in its modern form.
1900 — Hilbert lists CH as the first of his problems.
1906 — Kőnig proves a theorem that, combined with Hausdorff's notion of cofinality (1908), shows $2^{\aleph_0}\neq\aleph_\alpha$ whenever $\alpha$ has cofinality $\omega$ .
1930 — Patai: if $2^\kappa$ is the $\gamma$ -th successor of $\kappa$ for every infinite $\kappa$ , then $\gamma$ is finite.
1938/1940 — Gödel proves that AC and GCH hold in the constructible universe $L$ , so $\mathrm{Con}(\mathrm{ZF})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\mathrm{GCH})$ .
1947 — Sierpiński proves that ZF + GCH implies AC.
1963 — Cohen invents forcing and proves $\mathrm{Con}(\mathrm{ZFC})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\neg\mathrm{CH})$ .
1986 — Freiling shows that $\neg$ CH is equivalent to his axiom of symmetry.

Setting

A cardinal measures the size of a set; $|A|\le|B|$ means there is an injection $A\to B$ , and $|A|=|B|$ a bijection. $\aleph_0=|\mathbb N|$ , $2^\kappa=|\mathcal P(X)|$ for $|X|=\kappa$ , so $|\mathbb R|=2^{\aleph_0}$ . $\aleph_\alpha$ is the $\alpha$ -th infinite cardinal, $\beth_\alpha$ is defined by $\beth_0=\aleph_0$ , $\beth_{\alpha+1}=2^{\beth_\alpha}$ and suprema at limits, and $\mathrm{cf}$ denotes cofinality.

CH: there is no $S\subseteq\mathbb R$ with $\aleph_0<|S|<2^{\aleph_0}$ (CH).
GCH: for every infinite cardinal $\kappa$ there is no cardinal strictly between $\kappa$ and $2^\kappa$ (GCH).

Independence is a statement about a first-order theory. The language of set theory has one binary relation symbol $\in$ (setLang). ZF (ZF) consists of extensionality, foundation, pairing, union, power set, infinity, and all instances of the separation and replacement schemas; ZFC (ZFC) adds the axiom of choice (acSentence). CH and GCH are also written as first-order sentences (chSentence, gchSentence): CH says that every subset of $\mathcal P(\omega)$ injects into $\omega$ or receives an injection from $\mathcal P(\omega)$ . A theory is consistent if it has a model, and $T\models\sigma$ means $\sigma$ holds in every model of $T$ ; by Gödel's completeness theorem these coincide with the proof-theoretic notions.

Formalization targets

Goal: independence of CH from ZFC

\mathrm{Con}(\mathrm{ZFC})\ \Longrightarrow\ \mathrm{ZFC}\not\models\mathrm{CH}\ \text{ and }\ \mathrm{ZFC}\not\models\neg\mathrm{CH}.

Milestones

$|\mathbb Z|=|\mathbb Q|<|\mathbb R|$ .
$\mathrm{CH}\iff 2^{\aleph_0}=\aleph_1$ .
(Gödel) $\mathrm{Con}(\mathrm{ZF})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\mathrm{GCH})$ .
$\mathrm{ZFC}+\mathrm{GCH}\models\mathrm{CH}$ .
(Cohen) $\mathrm{Con}(\mathrm{ZFC})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\neg\mathrm{CH})$ .
(Kőnig) $2^{\aleph_0}\neq\aleph_\alpha$ when $\mathrm{cf}(\alpha)=\omega$ ; and $\mathrm{cf}(2^{\aleph_0})>\aleph_0$ .
(Sierpiński) $\mathrm{ZF}+\mathrm{GCH}\models\mathrm{AC}$ .
$\mathrm{GCH}\iff\forall\alpha,\ 2^{\aleph_\alpha}=\aleph_{\alpha+1}\iff\forall\alpha,\ \aleph_\alpha=\beth_\alpha$ .
Under GCH: $A<B\Rightarrow 2^A<2^B$ for infinite $A$ , and the three-case formula for $\aleph_\alpha^{\aleph_\beta}$ .
(Patai) $\forall\alpha,\ 2^{\aleph_\alpha}=\aleph_{\alpha+\gamma}$ implies $\gamma<\omega$ .
(Freiling) the axiom of symmetry is equivalent to $\neg$ CH.

Significance

The independence theorem shows that the ZFC axioms do not determine the size of the continuum, and it was among the first independence results for a mathematical statement. Its two halves introduced the two main tools of modern set theory: inner models (Gödel's $L$ ) and forcing (Cohen). Many statements in analysis, topology and measure theory were subsequently shown to be independent by the same methods.

For formalization, the goal requires a model theory of ZF inside Lean: interpreting the first-order theory, building $L$ inside an arbitrary model of ZF, and building forcing extensions of an arbitrary model of ZFC. The independence of CH was formalized in Lean 3 by the Flypitch project (Han and van Doorn, 2019–2020); no Lean 4 / Mathlib formalization is known to this mission. The cardinal-arithmetic milestones (2, 6, 8–11) are theorems of ZFC that can be proved directly in Lean's cardinal library.

Difficulty

Neither half follows from cardinal arithmetic in Lean: Lean's foundations prove that models of ZFC exist, but (assuming they are consistent) they prove neither CH nor its negation about Lean's own Cardinal, so an argument inside Lean's cardinal arithmetic alone cannot produce the required models. Gödel's half needs relativization of formulas to a definable inner class and absoluteness of the construction of $L$ ; Cohen's half needs a generic extension in which a new family of $\aleph_2$ reals is added while cardinals are preserved (the countable chain condition). Both require a theory of definability inside arbitrary, possibly non-well-founded, models of a first-order theory.

Formalization scope

Syntax and semantics are Mathlib's first-order logic (FirstOrder.Language, Theory.IsSatisfiable, Theory.ModelsBoundedFormula written ⊨ᵇ). Formulas name their variables by natural numbers; close φ is the universal closure. Equality is the built-in equality of first-order logic.
Consistency is satisfiability and provability is semantic consequence over models with universe in Type. By the completeness theorem these agree with the syntactic notions.
The first-order CH uses $\mathcal P(\omega)$ in place of $\mathbb R$ (they are equinumerous in ZF). The first-order GCH is the choice-free form " $|S|\le|T|\le|\mathcal P(S)|\Rightarrow|T|=|S|$ or $|T|=|\mathcal P(S)|$ , for $S$ infinite".
The consistency results carry their hypotheses $\mathrm{Con}(\mathrm{ZF})$ or $\mathrm{Con}(\mathrm{ZFC})$ explicitly, even though these are provable in Lean. A solution may not replace a model of ZF by Lean's own universe in a way that assumes CH or its negation.
Results that need large-cardinal hypotheses or class forcing (Easton, Solovay, Foreman–Woodin, Merimovich) are not part of this mission.

Reusable infrastructure: the language of set theory with standard abbreviations (pairs, functions, $\omega$ , power set), satisfaction lemmas for the abbreviations, relativization, absoluteness, the constructible hierarchy, and forcing over models of ZFC.

Selected references

G. Cantor, Ein Beitrag zur Mannigfaltigkeitslehre, J. Reine Angew. Math. 84 (1878) 242–258. https://doi.org/10.1515/crll.1878.84.242
K. Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis, PNAS 24 (1938) 556–557. https://doi.org/10.1073/pnas.24.12.556
K. Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory, Annals of Math. Studies 3, Princeton, 1940.
P. J. Cohen, The independence of the Continuum Hypothesis I, II, PNAS 50 (1963) 1143–1148; 51 (1964) 105–110. https://doi.org/10.1073/pnas.50.6.1143, https://doi.org/10.1073/pnas.51.1.105
C. Freiling, Axioms of symmetry: throwing darts at the real number line, J. Symbolic Logic 51 (1986) 190–200. https://doi.org/10.2307/2273955
L. Gillman, Two classical surprises concerning the Axiom of Choice and the Continuum Hypothesis, Amer. Math. Monthly 109 (2002) 544–553. https://doi.org/10.2307/2695444
K. Kunen, Set Theory: An Introduction to Independence Proofs, North-Holland, 1980.
Wikipedia, Continuum hypothesis (revision 1376315189). https://en.wikipedia.org/w/index.php?title=Continuum_hypothesis&oldid=1376315189

33 thms3 active usersReviewed

Number Theory·Captain: Lucas

Class Number Formula: Continuation of the Dedekind Zeta Function and Dirichlet's FormulaTextbook

Motivation

The class number formula connects the analytic behaviour of the Dedekind zeta function $\zeta_K(s)$ of a number field $K$ at $s = 1$ with the basic arithmetic invariants of $K$ : its class number, regulator, number of roots of unity and discriminant. It is the main tool for computing and bounding class numbers analytically, and its quadratic case, Dirichlet's class number formula, came out of Dirichlet's proof of his theorem on primes in arithmetic progressions.

Timeline.

1801: Gauss appears to have known the quadratic case, stated for binary quadratic forms (MathOverflow 109330).
1839: Dirichlet publishes a proof of the formula for quadratic discriminants, in the language of binary quadratic forms.
Later in the 19th century: Dedekind introduces $\zeta_K$ for an arbitrary number field, and the residue formula is established in general.

Setting

Let $K$ be a number field of degree $n = r_1 + 2r_2$ , where $r_1$ is the number of real embeddings and $2r_2$ the number of complex embeddings of $K$ . Write $h_K$ for the class number (the order of the ideal class group), $\mathrm{Reg}_K$ for the regulator, $w_K$ for the number of roots of unity in $K$ , and $D_K$ for the discriminant of $K/\mathbb Q$ . The Dedekind zeta function is the Dirichlet series

\zeta_K(s) = \sum_{n \ge 1} \frac{a_n}{n^s}, \qquad a_n = \#\{\mathfrak a \subseteq \mathcal O_K : N(\mathfrak a) = n\}.

For the quadratic case, let $d$ be a fundamental discriminant, let $h(d)$ be the number of proper ( $\mathrm{SL}_2(\mathbb Z)$ ) equivalence classes of binary quadratic forms $ax^2 + bxy + cy^2$ of discriminant $b^2 - 4ac = d$ (positive definite ones if $d < 0$ ), and let $\chi(m) = \left(\frac{d}{m}\right)$ be the Kronecker symbol, a Dirichlet character modulo $|d|$ with $L$ -function $L(s,\chi)$ . For $d < 0$ let $w = 2, 4, 6$ according as $d < -4$ , $d = -4$ , $d = -3$ . For $d > 0$ let $t, u > 0$ solve $t^2 - du^2 = 4$ with $u$ minimal, and put $\varepsilon = \frac12(t + u\sqrt d)$ .

Formalization targets

Goal: the class number formula

\zeta_K(s) \text{ converges absolutely for } \operatorname{Re}(s) > 1, \text{ and extends meromorphically to } \mathbb C \text{ with a single simple pole at } s=1,

\lim_{s\to 1}(s-1)\,\zeta_K(s) = \frac{2^{r_1}(2\pi)^{r_2}\,\mathrm{Reg}_K\,h_K}{w_K\sqrt{|D_K|}} .

Milestones

Dirichlet's unit theorem, and the reduction of the residue to the average of the coefficients of $\zeta_K$ .
The case $K = \mathbb Q(i)$ : coefficients as sums of two squares, the lattice-point count in a quarter circle, and the residue $\pi/4$ .
The general ideal count $\#\{\mathfrak a : N(\mathfrak a) \le N\} \sim \rho_K N$ , and the residue at $s = 1$ approached from the right.
Dirichlet's formula:

h(d) = \frac{w\sqrt{|d|}}{2\pi}\,L(1,\chi)\ \ (d<0), \qquad h(d) = \frac{\sqrt d}{\ln\varepsilon}\,L(1,\chi)\ \ (d>0),

with the supporting facts that $\chi$ is a Dirichlet character, that $\zeta_K(s) = \zeta(s)L(s,\chi)$ for a quadratic field, that the Pell equation $t^2 - du^2 = 4$ is solvable, and that $\varepsilon$ is a fundamental unit or its square. 5. Finite forms of $L(1,\chi)$ for prime conductor $q$ :

L(1,\chi) = -\frac{\pi}{q^{3/2}}\sum_{m=1}^{q-1} m\left(\frac mq\right)\ (q\equiv3\bmod 4), \qquad L(1,\chi) = -\frac{1}{q^{1/2}}\sum_{m=1}^{q-1}\left(\frac mq\right)\ln\sin\frac{m\pi}{q}\ (q\equiv1\bmod 4).

Significance

The result. The formula makes $h_K \mathrm{Reg}_K$ computable from $L$ -values. In the quadratic case it gives closed formulas for class numbers, and it implies that $L(1,\chi) \neq 0$ for real characters, which is the hardest step in Dirichlet's theorem on primes in arithmetic progressions. Its refinements for cyclotomic fields relate class numbers to cyclotomic units and lead into Iwasawa theory.

Formalizing it. The result is classical. Mathlib already proves the residue as a one-sided real limit, $(s-1)\zeta_K(s) \to \rho_K$ as $s \to 1^+$ , and that statement is available on the platform as a proved theorem. What is not formalized is the meromorphic continuation of $\zeta_K$ to all of $\mathbb C$ with a single simple pole, which is what the goal requires. Dirichlet's formula in terms of binary quadratic forms, its supporting facts, and the finite forms of $L(1,\chi)$ are not formalized either.

Difficulty

The residue formula follows from counting ideals of bounded norm, but that only controls $\zeta_K$ for real $s > 1$ . Continuing $\zeta_K$ to all of $\mathbb C$ needs a separate analytic input, such as theta functions or Hecke's integral representation with a functional equation, or a decomposition into Hecke $L$ -functions. Mathlib has such continuations for the Riemann zeta function and Dirichlet $L$ -functions, but not for $\zeta_K$ in general. For Dirichlet's formula, the hard part is connecting classes of binary quadratic forms (proper equivalence, positive definiteness for $d<0$ ) with ideal classes of the quadratic order, keeping track of the unit and automorph conventions that decide the constants $w$ and $\varepsilon$ .

Formalization scope

The goal uses Mathlib's NumberField.dedekindZeta (the Dirichlet series, meaningful for $\operatorname{Re}(s) > 1$ ) together with nrRealPlaces, nrComplexPlaces, regulator, classNumber, torsionOrder and discr. The continuation is stated as an entire function $G$ with $\zeta_K(s) = G(s)/(s-1)$ on $\operatorname{Re}(s)>1$ and $G(1)$ equal to the residue. Since the residue is positive, this rules out the trivial reading where $\zeta_K$ is continued with no pole.
$L(s,\chi)$ is DirichletCharacter.LFunction, the analytic continuation, so $L(1,\chi)$ is its value at $s=1$ and not the (conditionally convergent) series. The character is a hypothesis agreeing with the Kronecker symbol, and a separate milestone shows that such a character exists.
$h(d)$ counts $\mathrm{SL}_2(\mathbb Z)$ -classes of integral forms of discriminant $d$ , positive definite when $d < 0$ (Davenport's convention, which the source follows).
Corrections to the source. Two displayed constants in the source are off by a factor $2$ and are corrected here: the $d>0$ case of Dirichlet's formula uses $\ln\varepsilon$ in place of $2\ln\varepsilon$ (as in Davenport, Ch. 6), and the $q \equiv 1 \pmod 4$ finite form uses $-q^{-1/2}$ in place of $-\frac12 q^{-1/2}$ . Each affected milestone checks the case $d = q = 5$ explicitly.
Not included: the sections on Galois and abelian extensions (Artin $L$ -functions, Kummer's cyclotomic formulas). Mathlib has no Artin $L$ -functions, and the source states those results only informally.
Reusable outputs: the Kronecker symbol, binary quadratic forms with proper equivalence, the Pell unit $\varepsilon$ , and the continuation of $\zeta_K$ .

Selected references

Wikipedia, "Class number formula", revision 1366411311. https://en.wikipedia.org/w/index.php?title=Class_number_formula&oldid=1366411311
H. Davenport, Multiplicative Number Theory, 3rd ed., rev. H. L. Montgomery, Graduate Texts in Mathematics 74, Springer, 2000, Ch. 6, pp. 43–53. https://books.google.com/books?id=U91lsCaJJmsC
W. Narkiewicz, Elementary and Analytic Theory of Algebraic Numbers, 2nd ed., Springer/PWN, 1990, pp. 324–355. https://archive.org/details/elementaryanalyt0000nark
"Did Gauss know Dirichlet's class number formula in 1801?", MathOverflow, 2012. https://mathoverflow.net/q/109330

18 thms3 active usersReviewed

Number Theory·Captain: Lucas

Ramanujan–Petersson Conjecture (Wikipedia): Coefficient Bounds for Holomorphic Cusp FormsTextbook

Motivation

The Fourier coefficients of modular forms are among the most studied arithmetic functions in number theory. In 1916 Srinivasa Ramanujan studied the coefficients $\tau(n)$ of the discriminant modular form $\Delta$ and conjectured three properties: multiplicativity, a three-term recursion on prime powers, and the bound $|\tau(p)|\le 2p^{11/2}$ for primes $p$ (Ramanujan 1916). Hans Petersson extended the size bound to the coefficients of holomorphic cusp forms for congruence subgroups (Petersson 1930). The resulting Ramanujan–Petersson conjecture for holomorphic cusp forms is now a theorem of Deligne (weight $k\ge 2$ ) and Deligne–Serre (weight $k=1$ ). Its analogues for Maass forms and for general automorphic representations remain open.

Timeline (as recorded in the source article, Wikipedia: Ramanujan–Petersson conjecture):

1916: Ramanujan conjectures that $\tau$ is multiplicative, that it satisfies the prime-power recursion, and that $|\tau(p)|\le 2p^{11/2}$ .
1917: Mordell proves the first two statements, using what are now called Hecke operators.
1930: Petersson formulates the coefficient bound for holomorphic cusp forms for congruence subgroups.
1937: Hecke extends Mordell's method to holomorphic cusp forms in general.
1971: Deligne, building on Kuga, Sato, Shimura and Ihara, reduces the conjecture for weight $k\ge 2$ to the Weil conjectures via the Eichler–Shimura isomorphism (Deligne 1971).
1974: Deligne proves the Riemann hypothesis part of the Weil conjectures, which settles the case $k\ge 2$ and in particular $|\tau(p)|\le 2p^{11/2}$ (Deligne 1974). Deligne and Serre treat weight $k=1$ (Deligne–Serre 1974).

Setting

Let $\mathbb H=\{z\in\mathbb C:\operatorname{Im}z>0\}$ and $q=e^{2\pi i z}$ . The Dedekind eta function is $\eta(z)=q^{1/24}\prod_{n\ge1}(1-q^n)$ . The discriminant modular form is

\Delta(z)=q\prod_{n>0}(1-q^n)^{24}=\eta(z)^{24}.

It is a holomorphic cusp form of weight $12$ and level $1$ . Ramanujan's tau function $\tau:\mathbb N\to\mathbb C$ is defined by the Fourier expansion

\Delta(z)=\sum_{n\ge1}\tau(n)q^n=q-24q^2+252q^3-1472q^4+4830q^5-\cdots.

Its Ramanujan $L$ -function is the Dirichlet series $L(s,\tau)=\sum_{n\ge1}\tau(n)n^{-s}$ .

More generally, let $\Gamma\subseteq SL(2,\mathbb Z)$ be a congruence subgroup, meaning that $\Gamma$ contains the principal congruence subgroup $\Gamma(N)$ for some $N\ge1$ . A holomorphic cusp form of weight $k$ for $\Gamma$ is a holomorphic function $f:\mathbb H\to\mathbb C$ with $f(\gamma z)=(cz+d)^k f(z)$ for every $\gamma=\begin{pmatrix}a&b\\c&d\end{pmatrix}\in\Gamma$ , which vanishes at every cusp. Such an $f$ is periodic with some least period $h>0$ , and it has a Fourier expansion $f(z)=\sum_{n\ge1}a_n q_h^n$ with $q_h=e^{2\pi i z/h}$ . When $\Gamma$ contains $z\mapsto z+1$ (for example $\Gamma_0(N)$ , $\Gamma_1(N)$ , or $SL(2,\mathbb Z)$ itself), $h=1$ and $q_h=q$ .

Formalization targets

Goal: the Ramanujan–Petersson conjecture for holomorphic cusp forms

For every congruence subgroup $\Gamma$ , every weight $k\ge1$ , every cusp form $f$ of weight $k$ for $\Gamma$ with coefficients $a_n$ , and every $\varepsilon>0$ ,

a_n=O_\varepsilon\!\left(n^{(k-1)/2+\varepsilon}\right).

The goal splits by weight into Deligne's theorem ( $k\ge2$ ) and the Deligne–Serre theorem ( $k=1$ ), both listed as milestones.

The tau function

Values: $\tau(1)=1$ , $\tau(2)=-24$ , $\tau(3)=252$ , $\tau(4)=-1472$ , $\tau(5)=4830$ .
Multiplicativity (Mordell): $\tau(mn)=\tau(m)\tau(n)$ whenever $\gcd(m,n)=1$ .
Recursion (Mordell): $\tau$ is not completely multiplicative, and $\tau(p^{j+1})=\tau(p)\tau(p^j)-p^{11}\tau(p^{j-1})$ for primes $p$ and $j\ge2$ .
Ramanujan's bound (Deligne): $|\tau(p)|\le 2p^{11/2}$ for all primes $p$ .
Consequences: $|\tau(n)|\le d(n)n^{11/2}$ for all $n\ge1$ , where $d(n)$ is the number of divisors, and hence $\tau(n)=O(n^{11/2+\varepsilon})$ .

The Ramanujan $L$ -function

$\sum_{k\le n}\tau(k)=O(n^{13/2+\varepsilon})$ , and $L(s,\tau)$ converges absolutely for $\operatorname{Re}s>13/2$ .
$L(s,\tau)$ continues to an entire function satisfying $\dfrac{\Gamma(s)L(s,\tau)}{(2\pi)^s}=\dfrac{\Gamma(12-s)L(12-s,\tau)}{(2\pi)^{12-s}}$ .
Euler product: $L(s,\tau)=\prod_p\sum_{n\ge0}\tau(p^n)p^{-ns}=\prod_p\big(1-\tau(p)p^{-s}+p^{11-2s}\big)^{-1}$ for $\operatorname{Re}s>13/2$ .

Significance

The bound $|\tau(p)|\le 2p^{11/2}$ says that the roots of $1-\tau(p)u+p^{11}u^2$ have equal absolute value $p^{-11/2}$ , an analogue of the Riemann hypothesis for the local factors of $L(s,\tau)$ . The bounds for general cusp forms are used throughout analytic number theory to control sums of Fourier coefficients. They are also used in the explicit construction of Ramanujan graphs by Lubotzky, Phillips and Sarnak, which are optimal expander graphs. The generalized conjecture for $GL(n)$ implies Selberg's $1/4$ conjecture on Laplace eigenvalues.

All targets in this mission are proved theorems in the literature. At the pinned Mathlib revision, none of them is formalized except the identity $\tau(1)=1$ . Mathlib does contain the definitions they need: $\eta$ , $\Delta$ as a cusp form of weight 12 and level 1, $q$ -expansions, congruence subgroups, and the $L$ -function of a cusp form. Mathlib also proves the analytic continuation of that $L$ -function. The remaining work is to formalize Hecke theory for $\Delta$ , the elementary consequences of Deligne's bound, the $L$ -function statements, and ultimately Deligne's and Deligne–Serre's theorems.

Difficulty

The algebraic statements about $\tau$ (multiplicativity, the recursion, the Euler product) and the functional equation are classical, but formalizing them needs infrastructure that Mathlib does not yet have, such as Hecke operators on cusp forms. The size bounds are of a different kind. Estimates from the Petersson inner product or from Hecke's method give only the exponent $k/2$ (Hecke's bound). That exponent is attainable by complex analysis alone, but the improvement to $(k-1)/2$ is not. In the literature it depends on arithmetic geometry: Deligne's proof of the Weil conjectures for $k\ge2$ , and Galois representations for $k=1$ . The analytically similar statement for Maass forms is still open.

Formalization scope

$\tau(n)$ is defined as the $n$ -th coefficient of Mathlib's $q$ -expansion of ModularForm.discriminant with period $1$ , as a complex number. The source's description of $\tau$ is taken as the definition, and integrality is not assumed.
Absolute values are complex norms. $n^{11/2}$ and similar powers are real powers of nonnegative reals.
$O(\cdot)$ is Mathlib's big-O along atTop on $\mathbb N$ , with the constant allowed to depend on $\varepsilon$ .
In the general goal, the coefficients are taken with respect to $q_h=e^{2\pi i z/h}$ , where $h$ is the strict width of the cusp $\infty$ for $\Gamma$ (Subgroup.strictWidthInfty). This equals $1$ whenever $z\mapsto z+1$ lies in $\Gamma$ . A congruence subgroup is CongruenceSubgroup.IsCongruenceSubgroup.
The functional equation is stated only at points $s$ where neither $s$ nor $12-s$ is a pole of $\Gamma$ . This avoids Mathlib's convention that $\Gamma$ is $0$ at its poles.
The recursion is stated for $j\ge2$ , exactly as in the source.
The Maass-form and automorphic-representation versions, the function-field results and the bounds towards Ramanujan over number fields are outside this mission's scope. Mathlib lacks the definitions they need.

Selected references

S. Ramanujan, On certain arithmetical functions, Trans. Cambridge Philos. Soc. 22 (1916), 159–184. http://ramanujan.sirinudi.org/Volumes/published/ram18.pdf
H. Petersson, Theorie der automorphen Formen beliebiger reeller Dimension …, Math. Ann. 103 (1930), 369–436. https://doi.org/10.1007/BF01455702
P. Deligne, Formes modulaires et représentations l-adiques, Sém. Bourbaki 1968/69, LNM 179 (1971). https://doi.org/10.1007/BFb0058801
P. Deligne, La conjecture de Weil. I, Publ. Math. IHÉS 43 (1974), 273–307. https://doi.org/10.1007/BF02684373
P. Deligne, J.-P. Serre, Formes modulaires de poids 1, Ann. Sci. ÉNS 7 (1974), 507–530. https://doi.org/10.24033/asens.1277
P. Sarnak, Notes on the generalized Ramanujan conjectures, Clay Math. Proc. 4 (2005). http://www.claymath.org/publications/Harmonic_Analysis/chapter9.pdf

15 thms3 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XC: Structural Corporate Default and Rating-Migration Credit ValuationTextbook

Motivation

Credit risk matters to insurer bond holdings, pension scheme fixed-income investment and counterparty guarantees. Merton's corporate debt model derives terminal shareholder and bondholder payoffs from limited liability and asset value. Jarrow–Lando–Turnbull introduces observable ratings with Markov state migrations and default, motivating a second, independently defined view of risky fixed-income valuation.

Setting

A firm has nonnegative terminal assets and a single promise of face-value debt. Creditors are paid no more than the promise and no more than available assets; equity gets the residual. Finite genuine probability masses attach to terminal asset scenarios and yield discounted debt and equity claim valuations. Separately, a three-state rating matrix contains two non-default ratings and a terminal default state, with nonnegative row probabilities and full row-sum constraints.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Merton limited liability and terminal default payoffs

Strict asset deficit is equivalent to zero equity except for solvent zero-cashflow special cases.

E_T=(V_T-D)^+,\quad B_T=\min(V_T,D)

Finite default risk premiums and risk-neutral debt pricing

A bond priced equally to risk-free debt has zero model spread.

B_0=e^{-rT}\mathbb E^{\mathbb Q}[\min(V_T,D)]

Three-state rating migration and recoverable default claims

Structural terminal solvency and an independent absorbing-rating transition system reconcile riskier defaultable debt prices, nonnegative credit value deductions and genuinely two-period probability conservation.

\sum_j P_{ij}=1,\quad P_{\text{default,default}}=1

Capstone theorem

Structural terminal solvency and an independent absorbing-rating transition system reconcile riskier defaultable debt prices, nonnegative credit value deductions and genuinely two-period probability conservation.

\sum_j P_{ij}=1,\quad P_{\text{default,default}}=1

Significance

As discussed in Merton's corporate-credit model, The mission connects terminal firm claims to an actual finite risk-neutral weighted value: equity plus debt exhaust firm assets, expected discounted defaultable debt is bounded above by its risk-free counterpart, and credit value deductions are nonnegative. The genuine two-step rating migration law preserves total probability mass. These independently defined results jointly give an actuarial foundation for pricing defaultable corporate securities and recognising credit exposures in asset-liability valuation.

Difficulty

It must be proved that the limited-liability payoffs partition total assets, with exact boundary conditions where assets equal or fall below face value. The pricing theorem must distinguish actual discounted expected creditor payments from assuming a closed-form Black–Scholes price; no lognormal risk-neutral firm distribution is postulated. Credit spreads require positive debt prices and maturities. A rating transition matrix must be proved stochastic under composition, and an absorbing default state is a model condition rather than automatically true for arbitrary matrices.

Formalization scope

Limited liability and rating-migration probabilities are distinct mathematical constructs in this model. The complete diffusion-based Merton option value and continuous-time rating default models remain future mathematical research. The current target is nontrivial because it derives the bond valuation from limited-liability terminal payouts and an actual probability space, and the migration law from an independent finite transition kernel. Existing bond-present-value and state-reward missions are useful, but they do not identify shareholder and debt recovery claims. Its expected payoff and finite rating matrix infrastructure is reusable in asset-liability modelling and insurer counterparty credit valuation.

A firm's terminal assets must be partitioned consistently between equity and creditor payoffs. Above the promised debt face amount bondholders receive the promise and owners receive remaining assets. At the strict default threshold the owners' limited liability makes equity worthless and bondholders recover the remaining assets. The source values these payoffs using a proper finite risk-neutral scenario law, proving that discounted risky debt is no more valuable than the risk-free debt promise. The other branch builds a genuinely stochastic three-state rating transition matrix and derives two-step migration probabilities from matrix multiplication. Those observed or risk-neutral migration probabilities are not interchangeable without an additional measure-change argument. This is precise finite corporate credit mathematics; it is not a fabricated full closed-form structural diffusion model or a continuous-time default-intensity theory.

The new credit mission establishes exact one-period finite-state structural debt/equity payoff pricing and two-step rating probability conservation. It does not claim Merton's Black–Scholes closed-form equity value, stochastic diffusion replication, or the full continuous-time JLT risk-neutral generator model. The default-state absorbing property needs additional row restrictions and is not asserted for unrestricted transition matrices. Those are substantial extensions, and the current theorem bodies remain unproved.

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

Robert C. Merton (1974), On the Pricing of Corporate Debt: The Risk Structure of Interest Rates, Journal of Finance 29(2), 449–470. https://doi.org/10.1111/j.1540-6261.1974.tb03058.x
Robert A. Jarrow, David Lando and Stuart M. Turnbull (1997), A Markov Model for the Term Structure of Credit Risk Spreads, Review of Financial Studies 10(2), 481–523. https://doi.org/10.1093/rfs/10.2.481

48 thms3 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics LXXXIX: Expected Utility, Certainty Equivalents and Stochastic Risk OrdersTextbook

Motivation

Insurance economics prices risk using the utility of wealth rather than merely its variance. Pratt's seminal work derives risk aversion and the certainty-equivalent insurance premium, while Rothschild and Stiglitz connect comparative risk to probability order. Earlier actuarial entropic premium missions contain special finite retention objectives but do not derive an independently constructed expected wealth utility with premium indifference and finite stochastic dominance.

Setting

Losses are monetary outcomes on a genuinely finite scenario probability model, whose masses are nonnegative and sum to one. The exponential CARA wealth utility is strictly increasing and concave for positive aversion. The certainty-equivalent premium is constructed from the actual exponential moment of loss. Full insurance replaces the uncertain loss with a fixed premium and its utility is compared with the truly weighted uninsured outcome.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Expected exponential utility and absolute risk aversion

Utility of deterministic wealth equals its scenario expectation.

u_a(w)=-e^{-aw},\quad A(w)=-u''_a(w)/u'_a(w)=a

Actuarial insurance certainty equivalents and premium indifference

Risk-averse exponential expected utility demands at least the expected claim cost.

\pi_a(X)=\frac{1}{a}\log\mathbb E[e^{aX}]

Genuine pathwise coupling and finite first-order stochastic dominance

The actuarial insurer and policyholder indifference premium follows from genuinely averaged utility, with positive risk loading and a finite-scenario stochastic risk ordering.

X\le Y\ \text{a.s.}\Longrightarrow \mathbb E[\phi(X)]\le\mathbb E[\phi(Y)]

Capstone theorem

The actuarial insurer and policyholder indifference premium follows from genuinely averaged utility, with positive risk loading and a finite-scenario stochastic risk ordering.

X\le Y\ \text{a.s.}\Longrightarrow \mathbb E[\phi(X)]\le\mathbb E[\phi(Y)]

Significance

As discussed in Pratt's utility-risk treatment, The capstone proves a complete indifference premium identity, not merely its algebraic definition, and derives risk loading above expected loss from convexity of the exponential. A coupled stochastic order implies both the ordering of actual finite distribution functions and higher expected utility for increasing utility functions. The same ordering is related to excess-of-loss premiums through statewise monotonicity. These results supply core insurer and policyholder pricing foundations.

Difficulty

The logarithmic certainty equivalent requires strictly positive exponential moments and a nonzero risk-aversion parameter. The actual expected utility factorization must account for the sign of negative exponential utility. Risk loading requires Jensen's inequality or an equivalent discrete exponential-convexity argument, not the assertion that every risk is profitable to insure. The comparison of finite CDFs must reverse the inequality for higher wealth, while a higher loss severity raises stop-loss costs. Pathwise coupling is stronger than the entire stochastic-dominance order and is identified as such.

Formalization scope

Certainty-equivalent premium and stochastic risk ordering are distinct mathematical constructs in this model. A future generalisation will derive second-order stochastic dominance via integrals of real CDFs and concave expected utility, not merely a pathwise coupling. The current project is nontrivial because the CARA indifference identity follows by differentiating and averaging the actual utility, and the insurer's risk loading is derived from Jensen's inequality. Existing specialised exponential risk-price examples provide a useful benchmark but do not replace these general sources. The premium and coupling functions are reusable for nonproportional reinsurance, risk classification and comparative risk analysis.

Under constant absolute risk aversion the negative exponential utility function is increasing and concave in wealth when risk aversion is positive, even though its numerical utility level is negative. A fair premium is not obtained by simply assuming a desired level of profit. The expected uninsured utility is calculated from true scenario probabilities, the utility with full insurance is calculated using a fixed premium and the resulting indifference equation is solved from the loss exponential moment. The log moment premium must then be compared against expected claim cost using convexity, and the sign of this loading depends on risk aversion. Finite distribution functions and expected excess claims are independently defined for comparison. The pathwise coupling order in the source is stronger than first-order stochastic dominance, so no false claim of characterising all stochastic orders is made. Second-order dominance requires a separate distribution-integral analysis.

This is a genuine finite-probability CARA model with exactly derived insured/uninsured premium indifference. The stochastic order is proven for explicit statewise couplings and thus yields a strong sufficient condition for first-order stochastic dominance, not a complete characterisation of arbitrary second-order stochastic dominance. General concave utility risk orders, mean-preserving spreads, Arrow–Pratt comparative aversion for all utility families, and infinite random variables are future developments. All proof obligations are open.

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

John W. Pratt (1964), Risk Aversion in the Small and in the Large, Econometrica 32, 122–136. https://doi.org/10.2307/1913738
Michael Rothschild and Joseph E. Stiglitz (1970), Increasing Risk: I. A Definition, Journal of Economic Theory 2, 225–243. https://doi.org/10.1016/0022-0531(70)90038-4

46 thms3 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XCI: Joint-Life Mortality Profit and Contingent Survivor BenefitsTextbook

Motivation

Mortality experience in joint-life assurance and pensions depends not only on whether someone died, but on which insured life survives and which survivor or joint reserve must then be held. Standard multiple-life actuarial valuations motivate last-survivor, reversionary and guaranteed pension benefits. Earlier actuarial missions XLV and XLVI treat basic reversionary annuities and single-life mortality profit separately; this connects them through a genuine four-outcome death-strain model.

Setting

Two members start alive and experience independent yearly survival outcomes. Exactly four mutually exclusive joint states follow: both survive, only the first survives, only the second survives, or neither survives. Their probabilities use product and complement survival factors. The year-end reserve and any benefits can differ for every one of these states. Opening reserves plus premiums earn the annual return before payment and the next state contingent reserve is recognized.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Independent joint-life outcomes and probabilities

Each valid joint-life outcome has nonnegative mass.

p_{xy}=p_xp_y,\quad p_{x\dagger y}=(1-p_x)p_y

Outcome-dependent reserves, benefits and death strain

Additional state-specific benefit claims add to expected death strain.

D_{s}=B_s+V_s-(V_0+P)(1+i)

Joint mortality profit and limited-contingent survivor benefits

An exhaustive, correctly normalized two-life outcome model makes the mortality experience profit mean zero, retaining separate survivor reserves, death benefits and guaranteed payment conventions.

\Pi_{\text{mort}}=\sum_s p_s D_s-D_{\text{observed}}

Capstone theorem

An exhaustive, correctly normalized two-life outcome model makes the mortality experience profit mean zero, retaining separate survivor reserves, death benefits and guaranteed payment conventions.

\Pi_{\text{mort}}=\sum_s p_s D_s-D_{\text{observed}}

Significance

As discussed in Dickson, Hardy and Waters' multiple-life analysis, The capstone derives actual four-state normalization and reconciles joint mortality profit as expected death strain less observed state-specific death strain, whose expected result is zero under its own properly normalized law. The state-specific reserve functions distinguish the two possible remaining single-life liabilities rather than collapsing them into a single average. Limited-reversionary and certain guarantee payments are represented as separate conditional benefits.

Difficulty

Four disjoint probabilities must be normalized with exact endpoint treatment. Reserve releases after each death outcome may have opposite signs to death-benefit payments, so the state strain must include both payout and next-state reserve less the accumulated starting fund. Expected mortality profit cannot be asserted by defining it to have zero mean: it must follow from the actual weighted expectation of the observed strain. Independence is an explicit current assumption; arbitrary dependent lives need a separate four-state probability law.

Formalization scope

Joint-life mortality profit and state-dependent death strain are distinct mathematical constructs in this model. A future mission could introduce dependent lifetimes and within-year order of deaths, then compute first-to-die and last-survivor benefit present values directly from the joint survival law. The present work is nontrivial because both survivor reserves and actual death claims differ across the four states, while the mean mortality profit emerges from their normalised probability distribution. Existing joint-life annuity and single-life profit missions do not establish this combination. The outcome-specific reserve and mortality gain functions are reusable for spouse's pensions, death-in-service benefits and multi-life experience analysis.

Four disjoint annual outcomes must be considered for a policy whose two insured lives begin the year alive. They are both alive, only the first alive, only the second alive and both dead. Each outcome has a separate year-end reserve and may have a different death or survivor benefit. Accordingly, its actual death strain includes the benefit paid plus the new reserve less accumulated beginning-year funds. Expected strain is a genuine probability-weighted average of those four observed strains. The mortality experience profit for any one realised outcome equals the expected strain less that outcome's actual strain. Its expectation must be shown to vanish under the normalised four-outcome probability distribution, rather than by assuming zero mean. This framework supplies an actuarial bridge from joint-life/reversionary benefits to experience profit analysis and guarantee-period pensions. Within-year timing and dependent life outcomes require additional formal work.

This is a complete one-year joint mortality-experience model with explicit separate survivor reserves, not a full continuous-time ordering of first and second deaths inside the same policy year. Guarantee-period timing is represented by a separate deterministic indicator input. Exact age differences, policy options, death-payment timing and dependence-copula extensions can build on these definitions later. All theorem statements remain unproved.

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2020), Actuarial Mathematics for Life Contingent Risks, Cambridge University Press. https://www.cambridge.org/core/books/actuarial-mathematics-for-life-contingent-risks/
S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Wiley. https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521

54 thms3 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics LXXVII: Compound Aggregate Masses and the Full Finite Panjer RecursionTextbook

Motivation

Panjer's original 1981 result derives the aggregate claims recursion from a special frequency probability law and arbitrary nonnegative-integer severity mass distribution, including claims worth zero. The original article and the Sundt–Jewell extension underpin the mission. Earlier actuarial mission LIV handles direct recurrence algebra, while LXXIII derives the Bernoulli first positive aggregate mass identity. This mission formalises a full positive-aggregate-severity recursion for a genuinely constructed compound law.

Setting

A claim count N has probability weights p_n supported on {0,...,m}, with no artificial truncation of an otherwise infinite count distribution. Independent severity masses f_j on nonnegative integer amounts admit a genuine n-fold convolution, with count-zero convolution equal to a unit atom at zero. Thus g_k=Σ_{n=0}^m p_n(f^{*n})k is defined independently of Panjer's formula. The count recursion p_n=(a+b/n)p{n−1} is assumed only for 1≤n≤m+1, including its boundary p_{m+1}=0, and p_n=0 above m. No conclusion about the aggregate g is assumed.

Formalization targets

Aggregate claims from an actual frequency distribution

Write $p_n$ for the probability of exactly $n$ claims and $f_j$ for the probability that one claim has size $j$ . The frequency law is genuinely supported on $0,\ldots,m$ ; an infinite Poisson distribution is not silently truncated. The empty portfolio has aggregate size zero, while $f^{*n}$ denotes the distribution obtained by summing $n$ independent severities.

The first group constructs the aggregate probability $g_k$ directly from the frequency and severity laws:

g_k=\sum_{n=0}^{m}p_n(f^{*n})_k,\qquad (f^{*0})_0=1.

It also proves the zero-severity convolution identities, nonnegative mass preservation, and finite frequency and severity generating-function relationships.

The Panjer law and its upper support boundary

The count probabilities obey a Panjer recurrence with coefficients $a$ and $b$ . Crucially, the finite-support model includes the transition from $m$ to the compulsory zero probability at $m+1$ :

p_n=\left(a+\frac{b}{n}\right)p_{n-1}, \qquad 1\le n\le m+1,\qquad p_{m+1}=0.

This makes the assumed count law compatible with the finite aggregate distribution. For a claim size that may equal zero, the aggregate zero atom involves every possible claim count:

g_0=G_N(f_0)=\sum_{n=0}^{m}p_n f_0^{\,n}.

Corrected aggregate recursion and valuation

The central target is the entire positive-aggregate-size Panjer recurrence, not merely its first positive atom. For every integer $k\ge1$ , the result is

(1-af_0)g_k= \sum_{j=1}^{k}\left(a+\frac{bj}{k}\right) f_jg_{k-j}.

The factor $1-af_0$ is essential because a positive number of claims may still produce aggregate size zero. Further targets establish properties of cumulative aggregate probabilities, capital exceedance tails and finite stop-loss expectations. Every aggregate probability is defined independently of the recurrence it is subsequently required to satisfy.

Significance

The original Panjer paper gives the classical aggregate-loss setting. The capstone derives (1-a f_0)g_k=Σ_{j=1}^k(a+bj/k) f_j g_{k-j} for every positive aggregate amount from the actual random sum, together with g_0=G_N(f_0). The generator gives a count-supported finite Panjer family; it does not claim an infinite Poisson/negative-binomial count law. The exact zero claim-size correction is essential even when count N is positive, because multiple claims may all have zero monetary size. The authoring graph also includes frequency PGFs, severity convolution, CDF/tail and stop-loss identities.

Difficulty

Existing actuarial probability and Panjer steps are established subject areas. Every formal result introduced in this mission is an open Lean theorem target; none has an accepted proof. A vacuous or trivial definition of the aggregate as the recurrence solution is explicitly ruled out. The proof must rearrange nested severity convolutions, differentiate coefficient identities or establish the equivalent frequency recursion, and manage the zero-severity term that multiplies g_k itself. The count-support cutoff must satisfy the Panjer multiplier at m+1 to avoid invalid boundary terms. The recurrence at k=0 is not defined due to division by k; zero aggregate mass follows separately from the frequency PGF. Because f_0 may be positive, truncating the count sum at arbitrary m with an infinite count law would be mathematically invalid; we avoid that by using a genuine finite count distribution.

Formalization scope

This mission supplies a full k≥1 Panjer relation under an exact finite-support frequency model, not general infinite Poisson or geometric counts and not continuous claim severities. Positivity and mass normalisation require additional explicit probability conditions beyond the purely algebraic count recurrence, so the capstone is a valid algebraic identity even before imposing proper probability weights. All formal results remain Lean theorem targets without accepted proofs. The finite model is a reusable foundation for formal-power-series and analytic infinite-frequency cases.

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

Harry H. Panjer (1981), Recursive Evaluation of a Family of Compound Distributions, ASTIN Bulletin 12(1), 22–26. https://doi.org/10.1017/S0515036100006796
Bjørn Sundt and William S. Jewell (1981), Further Results on Recursive Evaluation of Compound Distributions, ASTIN Bulletin 12(1), 27–39. https://doi.org/10.1017/S0515036100006802
S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapter 21, section 21.11. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml

58 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Convergence Analysis of Sampling-Based Decomposition Methods for Risk-Averse Multistage Stochastic Convex Programs 2: Subdifferential of the Value Function of a Convex ProgramResearch Paper

Why subgradients of value functions matter

Stochastic dual dynamic programming (SDDP) and related decomposition methods solve multistage stochastic programs by approximating each stage's recourse function from below by a maximum of affine cuts. Every cut needs a value and a slope: the value of a convex subproblem at a trial point, and a subgradient of that subproblem's optimal value as a function of the trial point. For linear subproblems the slope is a vector of dual multipliers. For convex subproblems in which the trial point enters the objective and the nonlinear constraints, the slope requires a formula for the subdifferential of the value function of a parametric convex program.

Vincent Guigues, in Convergence Analysis of Sampling-Based Decomposition Methods for Risk-Averse Multistage Stochastic Convex Programs (arXiv:1408.4439v4, SIAM J. Optim. 2016), states such a formula as Lemma 2.1 and announces it in the abstract and in contribution (C) as a result of independent interest. Earlier convergence proofs for convex SDDP (Girardeau, Leclère and Philpott, Math. Oper. Res. 2015) avoid the question by copying the trial point into new variables and linear constraints, so that only the classical formula for a value function of right-hand-side perturbations is needed. Lemma 2.1 removes that device.

This mission is the second in the series on Guigues' paper. The first mission formalizes the almost-sure convergence of the risk-averse algorithm (Theorem 4.1) and takes the subgradient property of cut slopes as part of its model, so the two missions are independent.

Setting

Write $\mathbb R^k$ for Euclidean space with the scalar product $\langle x,y\rangle = x^\top y$ , and pair $\mathbb R^m\times\mathbb R^n$ by $\langle (s,t),(x,y)\rangle=\langle s,x\rangle+\langle t,y\rangle$ . Let $A\in\mathbb R^{q\times m}$ , $B\in\mathbb R^{q\times n}$ , $b\in\mathbb R^q$ , let $f:\mathbb R^m\times\mathbb R^n\to\mathbb R\cup\{+\infty\}$ , let $g=(g_1,\dots,g_p)$ be constraint functions on $\mathbb R^m\times\mathbb R^n$ , and let $X\subseteq\mathbb R^m$ and $Y\subseteq\mathbb R^n$ be nonempty, compact and convex. The value function (2.1) is

\mathcal Q(x)=\inf\{\,f(x,y):\ y\in S(x)\,\},\qquad S(x)=\{y\in Y:\ Ax+By=b,\ g(x,y)\le 0\},

defined for every $x\in\mathbb R^m$ , with $\mathcal Q(x)=+\infty$ when $S(x)=\emptyset$ . The solution set is $\operatorname{Sol}(x)=\{y\in S(x): f(x,y)=\mathcal Q(x)\}$ and the active set is $I(x,y)=\{i: g_i(x,y)=0\}$ .

The subdifferential of an extended-real function $h$ at $z_0$ is $\partial h(z_0)=\{s: h(z_0)\in\mathbb R,\ h(z)\ge h(z_0)+\langle s,z-z_0\rangle\ \forall z\}$ , and the normal cone of a set $C$ at $z_0\in C$ is $\mathcal N_C(z_0)=\{v:\langle v,z-z_0\rangle\le0\ \forall z\in C\}$ . The Lagrangian dual (2.3) maximizes

\theta_x(\lambda,\mu)=\inf_{y\in Y}\ f(x,y)+\lambda^\top(Ax+By-b)+\mu^\top g(x,y)

over $\lambda\in\mathbb R^q$ , $\mu\in\mathbb R^p_+$ ; its solution set is $\Lambda(x)$ .

Assumption (H): $f$ is lower semicontinuous, proper and convex; each $g_i$ is convex and lower semicontinuous with values in $\mathbb R\cup\{+\infty\}$ ; and $X^\varepsilon\times Y\subseteq\operatorname{dom} f$ for some $\varepsilon>0$ , where $X^\varepsilon=X+\varepsilon B_m$ .

Formalization targets

Goal: Lemma 2.1, formula (2.4), repaired

Assume (H) and the repaired Slater condition: every $g_i$ is real-valued (R1), and there is $(\bar x,\bar y)\in X\times\operatorname{ri}(Y)$ with $A\bar x+B\bar y=b$ , $g_i(\bar x,\bar y)<0$ for all $i$ (R2), and $(\bar x,\bar y)\in\operatorname{ri}(\operatorname{dom} f)$ (R3). For $x_0\in X$ with $S(x_0)\ne\emptyset$ , the set $\operatorname{Sol}(x_0)$ is nonempty and for every $y_0\in\operatorname{Sol}(x_0)$

s\in\partial\mathcal Q(x_0)\iff (s,0)\in\partial f(x_0,y_0)+\{[A^\top;B^\top]\lambda\}+\Big\{\sum_{i\in I(x_0,y_0)}\mu_i\,\partial g_i(x_0,y_0):\mu_i\ge0\Big\}+\{0\}\times\mathcal N_Y(y_0).

Differentiable case

If $f$ and the $g_i$ are real-valued, convex and differentiable, then under (R2)

\partial\mathcal Q(x_0)=\Big\{\nabla_x f(x_0,y_0)+A^\top\lambda+\sum_{i\in I(x_0,y_0)}\mu_i\nabla_x g_i(x_0,y_0):\ (\lambda,\mu)\in\Lambda(x_0)\Big\}.

Steps of the proof (milestones)

$\mathcal Q(x)=\inf_y f(x,y)+\mathbb I_{\operatorname{Gr}(S)}(x,y)$ , and $s\in\partial\mathcal Q(x_0)\iff(s,0)\in\partial(f+\mathbb I_{\operatorname{Gr}(S)})(x_0,y_0)$ — (2.5).
The sum rule $\partial(f+\mathbb I_{\operatorname{Gr}(S)})=\partial f+\mathcal N_{\operatorname{Gr}(S)}$ under (2.6) — (2.5)-(a).
$\mathcal N_{\operatorname{Gr}(S)}=\mathcal N_{C_1}+\mathcal N_{C_2}+\mathcal N_{\mathbb R^m\times Y}$ and $\mathcal N_{\mathbb R^m\times Y}=\{0\}\times\mathcal N_Y$ .
$\mathcal N_{C_1}(x_0,y_0)=\{(A^\top\lambda,B^\top\lambda)\}$ .
$\mathcal N_{C_2}(x_0,y_0)=\{\sum_{i\in I}\mu_i\partial g_i(x_0,y_0):\mu_i\ge0\}$ (repaired).
Primal-dual solutions satisfy (2.7)-(b), and (2.7)-(b) with $\mu\ge0$ yields $(\lambda,\mu)\in\Lambda(x_0)$ .
The differentiable case above.

Significance

Formula (2.4) yields cut slopes for SDDP applied to convex multistage programs directly from a primal solution and multipliers of the stage subproblem, without auxiliary copies of the state, and it is the source of the subgradient property used in the convergence analysis of the paper's Algorithm 1. The differentiable case is the form an implementation uses: any optimal dual pair gives a subgradient, and every subgradient arises this way.

For formalization, the result is a self-contained piece of finite-dimensional convex analysis: infimal projection, the subdifferential sum rule under a relative-interior condition, normal cones of intersections, of affine sets and of convex sublevel sets, and Lagrangian duality under Slater's condition. None of these steps is in Mathlib in the extended-real form needed here. No machine-checked proof of Lemma 2.1 or of its differentiable case exists. The platform has Shor's subgradient formula for value functions (ShorNonsmooth.Decomposition.value_function_convex_and_subgradient, subgradient_formula, subgradient_formula_differentiable, proved). Those statements cover real-valued data with inequality constraints only and prove one inclusion. They have no equality block $Ax+By=b$ , no set $Y$ and no converse, so they are related to this mission but are not instances of it.

Difficulty

The printed lemma is false. Two steps of its proof fail. First, the formula for $\mathcal N_{C_2}$ needs a strict Slater point: for $g(x,y)=y^2$ , $C_2=\mathbb R\times\{0\}$ equals its own relative interior, but $\mathcal N_{C_2}(0,0)=\{0\}\times\mathbb R$ is not generated by $\partial g(0,0)=\{0\}$ . With $f(x,y)=y$ , $X=Y=[-1,1]$ and $A=B=0$ , all printed hypotheses hold, $\mathcal Q\equiv0$ , and no $s$ satisfies (2.4). Second, $X^\varepsilon\times Y\subseteq\operatorname{dom} f$ does not give $\operatorname{ri}(X^\varepsilon\times Y)\subseteq\operatorname{ri}(\operatorname{dom}f)$ : with $Y=\{0\}$ , $g\equiv-1$ and $f(x,y)=-\sqrt y$ , $\partial f(x_0,0)=\emptyset$ while $\partial\mathcal Q(x_0)=\{0\}$ . The repair (R1)–(R3) adds hypotheses and leaves every step of the printed proof valid.

The remaining work is the relative-interior calculus. The sum rule and the intersection formula for normal cones hold only under qualification conditions phrased with relative interiors, and the converse direction of (2.4) needs that the qualification passes from $(\bar x,\bar y)$ to $\operatorname{Gr}(S)$ . A proof that uses only interiors fails as soon as $Y$ is lower-dimensional, which the hypotheses allow.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin k). The product $\mathbb R^m\times\mathbb R^n$ is the Lean product type, and subgradients and normal cones on it use the explicit pairing $\langle s,x\rangle+\langle t,y\rangle$ . No norm of the product is involved. Extended values are EReal. $\mathcal Q$ is an EReal infimum on all of $\mathbb R^m$ , and $\partial\mathcal Q(x_0)$ is its subdifferential on $\mathbb R^m$ , not relative to $X$ . An encoding of $\mathcal Q$ on $X$ only, or of $\partial\mathcal Q$ relative to $X$ , would describe a different function, whose subdifferential is unbounded at boundary points of $X$ ; it is excluded. Subdifferentials require a finite value at the base point, so the equivalence cannot hold vacuously at a point where a function is $+\infty$ . $X^\varepsilon$ is Metric.cthickening ε X; relative interiors are intrinsicInterior ℝ. Indices are 0-based (Fin p, Fin q). The sums in (2.4) are written with explicit witnesses $\mu_i\ge0$ , $w_i\in\partial g_i$ indexed by the active set, which avoids the convention $0\cdot\emptyset=\emptyset$ .

Repaired statements, each labelled "(repaired)" in its title:

Lemma 2.1 (2.4): adds (R1) real-valued $g_i$ , (R2) strict Slater point, (R3) Slater point in $\operatorname{ri}(\operatorname{dom}f)$ , and concludes $\operatorname{Sol}(x_0)\ne\emptyset$ , which the printed "where $y_0$ is any element" presupposes.
$\mathcal N_{C_2}$ formula: assumes (R1) and (R2) instead of a point of $\operatorname{ri}(C_2)$ .
Differentiable case: " $f$ and $g$ differentiable" is read as real-valued and differentiable on the whole space, and (R2) replaces the printed condition.

The sum-rule milestone keeps (2.6) as a hypothesis, as the page states it. The dual-solution milestone reads "primal-dual solution" as $y_0\in\operatorname{Sol}(x_0)$ , $(\lambda,\mu)\in\Lambda(x_0)$ with zero duality gap, assumes only primal feasibility of $y_0$ for the converse (as the page does), and extends $\mu$ by zero outside the active set.

A complete development needs: the subdifferential sum rule for proper convex extended-real functions under a relative-interior condition; normal cones of intersections of convex sets with one affine set; normal cones of sublevel sets of finite convex functions under Slater's condition; existence of minimizers of lower semicontinuous functions on compact sets; and a zero-duality-gap (minimax) theorem for Lagrangians of convex programs over a compact convex set. These are reusable well beyond this mission. Contributions of any of these lemmas, in the generality of an arbitrary finite-dimensional inner product space, are welcome.

Selected references

V. Guigues, Convergence Analysis of Sampling-Based Decomposition Methods for Risk-Averse Multistage Stochastic Convex Programs, arXiv:1408.4439v4, 2016; SIAM J. Optim. 26(4), 2016. https://arxiv.org/abs/1408.4439
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorems 23.8, 24(a), 28.2; Corollary 23.8.1). https://doi.org/10.1515/9781400873173
P. Girardeau, V. Leclère, A. B. Philpott, On the Convergence of Decomposition Methods for Multistage Stochastic Convex Programs, Math. Oper. Res. 40(1), 2015. https://doi.org/10.1287/moor.2014.0664
M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Programming 52, 1991. https://doi.org/10.1007/BF01582895
N. Z. Shor, Nondifferentiable Optimization and Polynomial Problems, Kluwer, 1998. https://doi.org/10.1007/978-1-4757-6015-6

11 thms3 active usersReviewed

Completed

Differential Geometry Mathematical Physics·Captain: Lucas

Uhlenbeck, Equations of Gauge Theory I: Self-Dual Connections Minimize Yang-MillsTextbook

Motivation

The Yang–Mills functional measures the total curvature of a connection on a principal bundle. Its critical points, the Yang–Mills connections, are the non-abelian generalization of solutions of Maxwell's equations, and in four dimensions the most important among them are the self-dual and anti-self-dual connections (instantons), whose moduli spaces underlie Donaldson theory of smooth four-manifolds. A basic and frequently used fact, recorded as Proposition 3.1.1 in K. Uhlenbeck's lectures Equations of Gauge Theory (notes by L. Fredrickson, Temple University, 2012), is that instantons are not merely critical points: within a fixed topological class and with fixed boundary data they are absolute minimizers of the Yang–Mills energy. The same "energy identity" argument is the template the notes later apply to the Kapustin–Witten equations (Proposition 3.1.5).

Timeline of the ideas involved: Yang and Mills introduce the equations (1954); Belavin, Polyakov, Schwartz and Tyupkin observe the topological lower bound on the energy and its saturation by self-dual fields (1975); Atiyah, Hitchin and Singer study the deformation theory of instantons (1977–78); Donaldson uses the instanton moduli space in four-manifold topology (1983).

Setting

Work on the trivial principal $SU(n)$ -bundle over a closed box $\Omega=[a,b]=\prod_{\mu=0}^{3}[a_\mu,b_\mu]\subset\mathbb R^4$ with the Euclidean metric. A connection is $D_A=d+A$ with $A=\sum_\mu A_\mu\,dx^\mu$ , where each $A_\mu$ is a smooth map into the Lie algebra $\mathfrak{su}(n)$ of traceless skew-Hermitian $n\times n$ complex matrices. Its curvature is the $\mathfrak{su}(n)$ -valued two-form $F_A=dA+A\wedge A$ with coefficients

(F_A)_{\mu\nu}=\partial_\mu A_\nu-\partial_\nu A_\mu+[A_\mu,A_\nu].

The Hodge star on two-forms is $(\star F)_{\mu\nu}=\tfrac12\sum_{\rho,\sigma}\varepsilon_{\mu\nu\rho\sigma}F_{\rho\sigma}$ , with $\varepsilon$ the Levi-Civita symbol. A two-form is self-dual if $\star F=F$ and anti-self-dual if $\star F=-F$ . The pointwise norm is $|F|^2=\sum_{\mu<\nu}\operatorname{Re}\operatorname{tr}(F_{\mu\nu}F_{\mu\nu}^{*})$ , and the Yang–Mills functional on $\Omega$ is

\mathrm{Ym}_\Omega(A)=\int_\Omega |F_A|^2\,d\mathrm{vol}.

The Chern–Weil density $\operatorname{tr}(F\wedge F)$ is the coefficient $\tfrac14\sum\varepsilon_{\mu\nu\rho\sigma}\operatorname{tr}(F_{\mu\nu}F_{\rho\sigma})$ of $dx^0\wedge dx^1\wedge dx^2\wedge dx^3$ , and the Chern–Simons three-form is $CS(A)=\operatorname{tr}(A\wedge dA+\tfrac23A\wedge A\wedge A)$ , with flux components $K^\mu=\sum\varepsilon_{\mu\nu\rho\sigma}\operatorname{tr}(A_\nu\partial_\rho A_\sigma+\tfrac23A_\nu A_\rho A_\sigma)$ .

Formalization targets

Goal (Proposition 3.1.1, box version)

If $A$ and $B$ are smooth $SU(n)$ -connections on $\Omega$ that agree on $\partial\Omega$ , and $F_A$ is self-dual on all of $\Omega$ or anti-self-dual on all of $\Omega$ , then

\mathrm{Ym}_\Omega(A)\le \mathrm{Ym}_\Omega(B).

Milestones

Lemma 3.1.2. For an $\mathfrak{su}(n)$ -valued two-form $F$ : $|F\pm\star F|^2=2|F|^2\mp2\operatorname{tr}(F\wedge F)$ .
Fact 3.1.3, local form. $\operatorname{tr}(F_A\wedge F_A)=\sum_\mu\partial_\mu K^\mu$ , i.e. $\operatorname{tr}(F_A\wedge F_A)=d\,CS(A)$ .
Fact 3.1.3, box form. $\int_\Omega\operatorname{tr}(F_A\wedge F_A)=\int_{\partial\Omega}CS(A)$ (the topological term vanishes for the trivial bundle).
Energy bound (proof of Proposition 3.1.1). $\mathrm{Ym}_\Omega(A)\ge \mp\int_{\partial\Omega}CS(A)$ .
Equality case (proof of Proposition 3.1.1). On a non-degenerate box, $\mathrm{Ym}_\Omega(A)=-\int_{\partial\Omega}CS(A)$ iff $F_A$ is self-dual on $\Omega$ , and $\mathrm{Ym}_\Omega(A)=\int_{\partial\Omega}CS(A)$ iff $F_A$ is anti-self-dual on $\Omega$ .

Significance

The energy identity turns a second-order variational problem into a first-order one: any connection satisfying the first-order self-duality equation is automatically a Yang–Mills connection, and in fact a global minimizer in its class. This is the reason instanton moduli spaces are the natural objects of four-dimensional gauge theory, and it is the model for the corresponding minimization statements for the Kapustin–Witten equations treated later in the same notes. The result is classical and its proof is known; the remaining work is formal: a machine-checked development of the curvature, Hodge star, Chern–Simons transgression and the boundary integration on boxes, none of which are currently packaged in this form in Mathlib.

Difficulty

The algebraic identity of Lemma 3.1.2 is a finite computation. The substantive step is the transgression formula $\operatorname{tr}(F_A\wedge F_A)=d\,CS(A)$ , a cancellation between derivative terms and cubic terms that depends on cyclicity of the trace and on the antisymmetry of $\varepsilon$ , followed by Stokes' theorem on the box with correct face orientations. The naive approach of comparing $|F_A|^2$ and $|F_B|^2$ pointwise fails: the two connections agree only on the boundary, and only the integrated topological term is boundary-determined.

Formalization scope

The general setting of the notes (a $G$ -bundle over a compact oriented Riemannian four-manifold with boundary, topological class $c_2(P)=k$ ) is replaced by the trivial $SU(n)$ -bundle over a closed axis-parallel box in Euclidean $\mathbb R^4$ , so the topological term $8\pi^2c_2(P)$ is zero. Connections are smooth on all of $\mathbb R^4$ (equivalently, smooth up to the boundary of the box) and every coefficient takes values in $\mathfrak{su}(n)$ . Two-forms are stored as antisymmetric $4\times4$ families of matrices; partial derivatives are taken entrywise; integrals are Lebesgue integrals over the box and over its faces. "Fixed boundary data" means $A=B$ at every point of $\partial\Omega$ . Self-duality is $\star F=F$ , matching $F=\star F$ in Section 2.2 of the notes.

Two sign/normalization corrections relative to the printed notes are made deliberately: Lemma 3.1.2 is stated with the sign obtained in its own proof on p. 32 ( $\mp$ rather than the printed $\pm$ , because $B^*=-B$ on $\mathfrak{su}(n)$ ), and the Chern–Simons form uses the standard coefficient $\tfrac23$ in $\operatorname{tr}(A\wedge dA+\tfrac23A^3)$ , i.e. $\operatorname{tr}(A\wedge F_A)-\tfrac13\operatorname{tr}(A^3)$ , for which $d\,CS=\operatorname{tr}(F\wedge F)$ holds, instead of the printed $\tfrac16$ .

A trivializing formalization would make the boundary condition or the self-duality hypothesis unsatisfiable; here the zero connection is self-dual and satisfies every hypothesis, and the statements are not vacuous.

Reusable infrastructure: Levi-Civita symbol and Hodge star on $\Lambda^2\mathbb R^4$ with matrix coefficients, curvature of matrix-valued connections, the Chern–Simons transgression, and Stokes' theorem for flux forms on boxes (Mathlib's divergence theorem on boxes is the natural tool). Contributions to any milestone are welcome.

Selected references

K. Uhlenbeck, Equations of Gauge Theory, notes by L. Fredrickson, Emil Grosswald Lectures, Temple University, 2012 (the source of all statements; Section 3.1, pp. 29–32).
C. N. Yang, R. L. Mills, Conservation of isotopic spin and isotopic gauge invariance, Phys. Rev. 96 (1954), 191–195. https://doi.org/10.1103/PhysRev.96.191
A. A. Belavin, A. M. Polyakov, A. S. Schwartz, Yu. S. Tyupkin, Pseudoparticle solutions of the Yang–Mills equations, Phys. Lett. B 59 (1975), 85–87. https://doi.org/10.1016/0370-2693(75)90163-X
S. K. Donaldson, An application of gauge theory to four-dimensional topology, J. Differential Geom. 18 (1983), 279–315. https://doi.org/10.4310/jdg/1214437665

9 thms3 active usersReviewed

Completed

Combinatorics Group Theory Number Theory·Captain: Lucas

Landau's Function: Growth of the Maximal Order of a PermutationResearch Paper

Motivation

How large can the order of a single permutation of $n$ objects be? The answer, Landau's function $g(n)$ , is a basic invariant of the symmetric group $S_n$ : it is the maximum number of times a permutation can be iterated before it returns to the identity. Because the order of a permutation is the least common multiple of its cycle lengths, $g(n)$ is also the largest least common multiple of the parts of a partition of $n$ , which ties the question to the distribution of prime numbers.

Timeline.

1902–1903. E. Landau proved that $\ln g(n)\sim\sqrt{n\ln n}$ .
1968. J.-L. Nicolas showed that $g$ is constant on arbitrarily long runs of consecutive integers.
1984. J.-P. Massias proved the explicit bound $\ln g(n)\le 1.05313836\sqrt{n\ln n}$ for all $n\ge 1$ .
1988. Massias, Nicolas and Robin obtained a three-term asymptotic expansion of $\ln g(n)$ , its expression through the inverse logarithmic integral, and the equivalence of a one-sided inequality with the Riemann hypothesis.
2002. K. Ford's bounds for the Riemann zeta function give the error term $x\exp(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5})$ in the prime number theorem, which can be fed into the 1988 result.

Setting

For a natural number $n$ , let $S_n$ be the group of all permutations of an $n$ -element set. The order of $\sigma\in S_n$ is the least $k\ge 1$ with $\sigma^k=\mathrm{id}$ . Landau's function is

g(n)=\max_{\sigma\in S_n}\operatorname{ord}(\sigma).

A partition of $n$ is a multiset of positive integers summing to $n$ . The prime counting function $\pi(x)$ is the number of primes $p\le x$ , the (offset) logarithmic integral is $\mathrm{Li}(x)=\int_2^x\frac{dt}{\ln t}$ , and $\mathrm{Li}^{-1}$ is its inverse on $[2,\infty)$ . Throughout, $\ln$ is the natural logarithm.

Formalization targets

Goal: Landau's theorem (1902)

\lim_{n\to\infty}\frac{\ln g(n)}{\sqrt{n\ln n}}=1.

Supporting milestones

Partition characterization: $g(n)=\max\{\operatorname{lcm}(\lambda):\lambda\vdash n\}$ .
Initial values $g(0),\dots,g(8)=1,1,2,3,4,6,6,12,15$ .
Nicolas (1968): for every $m$ there is $n$ with $g(n)=g(n+1)=\dots=g(n+m)$ .
Massias–Nicolas–Robin (1988): $\ln g(n)=\sqrt{n\ln n}\Bigl(1+\frac{\ln\ln n-1}{2\ln n}-\frac{(\ln\ln n)^2-6\ln\ln n+9}{8(\ln n)^2}+O\bigl((\tfrac{\ln\ln n}{\ln n})^3\bigr)\Bigr)$ .
Ford (2002): $\pi(x)-\mathrm{Li}(x)=O\bigl(x\exp(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5})\bigr)$ for some $c>0$ .
Massias–Nicolas–Robin (1988): if $\pi(x)-\mathrm{Li}(x)=O(R(x))$ with $R(x)=x\exp(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5})$ , then $\ln g(n)=\sqrt{\mathrm{Li}^{-1}(n)}+O\bigl(R(\sqrt{n\ln n})\ln n\bigr)$ .
Riemann hypothesis criterion: $\ln g(n)<\sqrt{\mathrm{Li}^{-1}(n)}$ for all large $n$ $\iff$ RH.
$g(n)\le e^{n/e}$ for all $n$ , with equality only at $n=0$ .
Massias (1984): $g(n)\le\exp(1.05314\sqrt{n\ln n})$ .

Significance

Landau's theorem pins down the growth rate of the largest element order in $S_n$ , which bounds, for example, how long any fixed shuffle of $n$ cards can be repeated before the deck returns to its starting order. The refined statements quantify the second-order behaviour and connect it to the error term in the prime number theorem; the criterion in milestone 7 is one of the known elementary reformulations of the Riemann hypothesis, and is included as a faithful statement of the source, not as an expected deliverable. The other results are proved in the literature; formalizing them requires building the partition/lcm description of element orders in $S_n$ and quantitative prime-counting estimates on top of Mathlib.

Difficulty

The order of a permutation is easy to compute from its cycle type, but maximizing an lcm over all partitions is a non-linear optimization: the optimum uses prime powers whose sizes are dictated by the distribution of primes, so even the leading-order asymptotics need Chebyshev-type or prime number theorem estimates, and the refined milestones need the prime number theorem with an explicit error term.

Formalization scope

$S_n$ is Equiv.Perm (Fin n); $g(n)$ is the supremum of orderOf σ over the finite group (a natural number; $g(0)=1$ ).
Partitions are Mathlib's Nat.Partition n; the lcm of a partition is the Multiset.lcm of its parts.
Real logarithms use Real.log (which returns $0$ at $0$ and is defined for negative input); all asymptotic statements are about $n\to\infty$ , so the values at small $n$ are irrelevant there. The bounds in milestones 8–9 are stated for every $n$ and are true at $n=0,1$ .
$\pi(x)$ for real $x$ is Nat.primeCounting ⌊x⌋₊; $\mathrm{Li}$ is the offset logarithmic integral $\int_2^x dt/\ln t$ ; $\mathrm{Li}^{-1}(y)$ is the least $x\ge2$ with $\mathrm{Li}(x)\ge y$ , which for $y\ge0$ is the inverse function value. Replacing $\mathrm{Li}$ by the full integral $\mathrm{li}$ changes the inverse by $O(\ln n)$ and does not affect any of the asymptotic statements.
The Riemann hypothesis is Mathlib's RiemannHypothesis.

Contributions of reusable infrastructure (cycle-type lcm, prime-counting error terms, the logarithmic integral) are welcome.

Selected references

E. Landau, Über die Maximalordnung der Permutationen gegebenen Grades, Arch. Math. Phys. Ser. 3, vol. 5, 1903.
J.-L. Nicolas, Sur l'ordre maximum d'un élément dans le groupe $S_n$ des permutations, Acta Arithmetica 14 (1968), 315–332.
J.-P. Massias, Majoration explicite de l'ordre maximum d'un élément du groupe symétrique, Ann. Fac. Sci. Toulouse Math. (5) 6 (1984), 269–281.
J.-P. Massias, J.-L. Nicolas, G. Robin, Évaluation asymptotique de l'ordre maximum d'un élément du groupe symétrique, Acta Arithmetica 50 (1988), 221–242.
K. Ford, Vinogradov's integral and bounds for the Riemann zeta function, Proc. London Math. Soc. 85 (2002), 565–633. https://doi.org/10.1112/S0024611502013655
W. Miller, The maximum order of an element of a finite symmetric group, Amer. Math. Monthly 94 (1987), 497–506.
OEIS A000793. https://oeis.org/A000793

13 thms3 active usersReviewed

Completed

Economics·Captain: Lucas

Marginal Utility I: The Law of Diminishing Marginal UtilityTextbook

Motivation

Marginal utility is the change in utility (pleasure or satisfaction) that results from consuming one more unit of a good or service. It is the basic quantity of the marginalist theory of value, which explains prices and consumer choice by the additional satisfaction provided by each extra unit rather than by total usefulness. The law of diminishing marginal utility states that, other things being equal, the utility a consumer derives from additional units of a commodity goes on decreasing as the amount consumed increases; economists regard it as reflected in the concave shape of most utility functions.

Timeline. Gabriel Cramer (private letter, 1728) and Daniel Bernoulli (Specimen theoriae novae de mensura sortis, 1738) proposed that the desirability of money decreases as it accumulates, measuring it by the square root (Cramer) and the natural logarithm (Bernoulli), in order to resolve the St. Petersburg paradox. W. F. Lloyd (1833), N. W. Senior (1836), J. Dupuit (1844) and H. H. Gossen (1854) stated marginal-utility ideas with little contemporary influence. The theory entered the mainstream in the Marginal Revolution of Jevons (1862/1871), Menger (1871) and Walras (1874), and was consolidated by Marshall's Principles of Economics (1890), which treats utility as quantified. Ordinalist reformulations (Edgeworth 1881, Slutsky 1915, Hicks–Allen 1934) moved to indifference-curve analysis; cardinal utility returned with expected-utility theory (Ramsey 1926, von Neumann–Morgenstern 1944, Savage 1954), where diminishing marginal utility is linked to risk aversion.

Setting

A utility function of one quantified variable is a map $U:\mathbb R\to\mathbb R$ , where $g$ is the quantity of a single good and every other variable is held fixed (ceteris paribus, "c.p."). The change in utility from state $s_1$ to state $s_2$ is

\Delta U(s_1\to s_2)=U(s_2)-U(s_1).

The marginal utility at $g$ is the limit of the ratio of the change in utility to the size of the change in $g$ ,

\frac{\partial U}{\partial g}=\lim_{\Delta g\to 0}\left.\frac{\Delta U}{\Delta g}\right|_{c.p.},

which mainstream neoclassical economics assumes to exist. The function $U$ has diminishing marginal utility on a set $D$ of quantities when

\frac{\partial^2 U}{\partial g^2}<0\quad\text{on }D.

In the Lean development these are utilityChange, marginalUtility and HasDiminishingMarginalUtility in the namespace MarginalUtility.

Formalization targets

Goal: the law of diminishing marginal utility

For $D$ an open interval and $U$ with diminishing marginal utility on $D$ :

g_1<g_2 \text{ in } D\;\Longrightarrow\; \frac{\partial U}{\partial g}(g_2)<\frac{\partial U}{\partial g}(g_1),\qquad U(x+2h)-U(x+h)<U(x+h)-U(x)\ \ (h>0,\ x,x+2h\in D).

The first clause is the law as stated ("marginal utility goes on decreasing"); the second is its reading in terms of successive equal gains.

Milestones

Marginal utility is the limit of $\Delta U/\Delta g$ wherever $U$ is differentiable.
Positive marginal utility on an interval makes utility strictly increasing there; negative marginal utility makes it strictly decreasing.
Diminishing marginal utility makes marginal utility strictly decreasing.
Diminishing marginal utility makes $U$ strictly concave.
For a strictly concave $U$ , each equal gain adds strictly less utility than the previous one.
If marginal utility reaches zero at $x_0$ , total utility is maximal at $x_0$ and marginal utility is negative beyond $x_0$ .
Bernoulli's $\log x$ and Cramer's $\sqrt x$ have diminishing marginal utility on $(0,\infty)$ .

Significance

The law underlies the marginalist explanation of demand, the resolution of the water–diamond paradox, and, through the concavity of utility, the modelling of risk aversion in expected-utility theory. The concave-shape and satiation statements are the forms in which the law is used in consumer theory: under diminishing marginal utility, total utility is maximal exactly where marginal utility vanishes.

The mathematical content is classical single-variable calculus and is fully known. What this mission adds is a precise, machine-checked dictionary between the economic vocabulary ("marginal utility", "diminishing", "concave shape", "satiation") and standard analytic statements, on which later missions about consumer choice and risk aversion can build.

Difficulty

None of the statements is deep. The care required is in the hypotheses: the law is a statement about an open interval of quantities, marginal utility only makes sense where $U$ is differentiable, and mere (non-strict) concavity gives only non-strict decrease of successive gains. The source's verbal statements must be matched exactly in strength (strict versus non-strict inequalities) and in domain.

Formalization scope

Utility is a function $U:\mathbb R\to\mathbb R$ of one real quantity; the domain of interest is an open convex set $D\subseteq\mathbb R$ (an open interval, possibly unbounded), passed as a hypothesis. Marginal utility is deriv U, which Lean sets to $0$ where $U$ is not differentiable; every statement that uses it assumes the needed differentiability. Diminishing marginal utility means $U$ and $U'$ are differentiable on $D$ and $U''<0$ on $D$ . A statement that only assumed $U''<0$ without differentiability would be weaker than intended, because of the value- $0$ convention; the definition rules this out. Multivariate utility, ordinal utility and the qualitative assumptions listed in the source (identical units, constant tastes, and so on) are outside the scope of this mission. Proofs may use Mathlib's one-variable calculus and convexity libraries freely.

Selected references

Wikipedia, Marginal utility. https://en.wikipedia.org/wiki/Marginal_utility
D. Bernoulli, Specimen theoriae novae de mensura sortis (1738); English translation: Exposition of a New Theory on the Measurement of Risk, Econometrica 22 (1954) 23–36. https://doi.org/10.2307/1909829
A. Marshall, Principles of Economics, Macmillan, 1890.

9 thms3 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Second Law of Thermodynamics (Wikipedia) I: Carnot's Theorem and the Thermodynamic Temperature ScaleTextbook

Motivation

The second law of thermodynamics is a physical law based on universal empirical observation concerning heat and energy interconversions. Two of its classical statements are impossibility statements about machines. Rudolf Clausius (1854): "Heat can never pass from a colder to a warmer body without some other change, connected therewith, occurring at the same time." Lord Kelvin: "It is impossible for any system to operate in a thermodynamic cycle and deliver a net amount of energy by work to its surroundings while receiving energy by heat transfer from a single thermal reservoir." The Wikipedia article Second law of thermodynamics records that these two have been shown to be equivalent.

The law is not only prohibitive. Sadi Carnot's analysis of heat engines (1824) yields an upper bound on the efficiency of any engine running between two heat reservoirs, attained by reversible engines and strictly missed by irreversible ones, and — crucially — the same for all reversible engines whatever the working substance. That substance-independence is what makes a thermodynamic temperature possible: as the article puts it, "The second law allows a distinguished temperature scale, which defines an absolute, thermodynamic temperature, independent of the properties of any particular reference thermometric body."

This mission formalizes that chain: from the two impossibility statements, through Carnot's theorem, to the existence and uniqueness of the absolute temperature scale normalized by the Kelvin convention at the triple point of water.

Setting

A cyclically operating device is recorded by the heat it exchanges with thermal reservoirs over one complete cycle. Reservoirs are labelled by empirical temperature, an element of a linearly ordered type $\Theta$ ( $s<t$ : the reservoir at $s$ is colder). A cycle is a finitely supported function $c:\Theta\to\mathbb R$ , where $c(t)$ is the net heat absorbed by the device from the reservoir at $t$ (negative if rejected). Because the device returns to its initial state, the first law makes the net work delivered equal to the total heat absorbed:

W(c)=\sum_{t}c(t).

The cycles that can actually be realized form a set $\mathcal C$ , assumed to be a convex cone: the null cycle is realizable; two realizable devices can be run side by side, their heat exchanges adding; and a realizable device can be scaled by any factor $r\ge0$ . A cycle is reversible when $c\in\mathcal C$ and $-c\in\mathcal C$ , and operates between $h$ and $k$ when it exchanges heat with no other reservoir. A Carnot engine between a hot $h$ and a cold $k$ is a reversible cycle operating between them with $c(h)>0$ , $c(k)<0$ and $W(c)>0$ . The efficiency relative to the hot reservoir is $\eta=W(c)/c(h)$ .

In this language:

Clausius statement. For $k<h$ : every realizable cycle operating between $h$ and $k$ with $W(c)=0$ satisfies $c(k)\le0$ .
Kelvin statement. Every realizable cycle exchanging heat with a single reservoir satisfies $W(c)\le0$ .
$\mathcal C$ admits Carnot engines when a Carnot engine exists between every pair of reservoirs at different temperatures.

Formalization targets

Goal: the thermodynamic temperature scale

Assume $\mathcal C$ is a convex cone satisfying the Clausius statement and admitting Carnot engines, and fix a reference reservoir $T_0$ . Then there is exactly one $T:\Theta\to\mathbb R$ with

T>0,\qquad T(T_0)=273.16,\qquad \frac{|e(k)|}{|e(h)|}=\frac{T(k)}{T(h)}\quad\text{for every Carnot engine } e \text{ between } k<h.

The content is that the left-hand ratio, a property of an engine, depends on the engine only through its two reservoirs, and does so as a ratio of numbers attached to the reservoirs. The normalization $273.16$ at $T_0$ is the Kelvin convention; as the article notes, "any reference temperature and any positive numerical value could be used".

The two impossibility statements

\text{Clausius}(\mathcal C)\iff\text{Kelvin}(\mathcal C)

for a convex cone admitting Carnot engines over at least two reservoir temperatures.

Carnot's theorem

For $k<h$ and a Carnot engine $e$ between them, every realizable engine $c$ between the same two reservoirs satisfies $\eta(c)\le\eta(e)$ , with strict inequality when $c$ is irreversible ( $-c\notin\mathcal C$ ); and any two Carnot engines between $h$ and $k$ have equal efficiency.

Significance

The goal makes explicit which features of the realizable processes are used when a textbook defines absolute temperature. The three hypotheses — convex cone, Clausius statement, existence of Carnot engines — are exactly what the derivation needs; the working substance, the equation of state, and the mechanism of a device never appear. Uniqueness is the part that is usually left implicit: the Kelvin normalization at one reservoir pins the scale completely.

The milestones follow the article's own order: equation (1) for the efficiency of an arbitrary engine; the equivalence of the Clausius and Kelvin statements; the three clauses of Carnot's theorem; the composition law $f(T_1,T_3)=f(T_1,T_2)f(T_2,T_3)$ for the reversible heat ratio across an intermediate reservoir; the conversion of that law into a scale; and the resulting Carnot efficiency $\eta=1-T_{\mathrm C}/T_{\mathrm H}$ .

Difficulty

The mathematics is elementary — convex cones in a space of finitely supported real functions, and one functional equation — but the bookkeeping is where faithfulness is won or lost. Carnot's theorem is proved by scaling a candidate engine against a reversed Carnot engine so that the composite does no net work, which makes the Clausius statement applicable; the equality case has to identify the candidate as a positive multiple of the Carnot engine before concluding that it is reversible. The composition law requires the intermediate reservoir to be exactly balanced, so that the composite is again a two-reservoir engine — the article's remark that "the heat $q_2$ flown from the engine 2 to the intermediate reservoir must be equal to the heat $q_2^*$ flown out from the reservoir to the engine 3". The functional equation must be solved without assuming the reference reservoir is the hottest or the coldest, so the scale is defined by $f(T_0,\cdot)$ below $T_0$ and by $1/f(\cdot,T_0)$ above it, and the composition law is applied in four different orderings.

Formalization scope

Reservoir temperatures form an arbitrary linearly ordered type; the order is the empirical hotter/colder relation and nothing else is assumed of it.
Heat is positive into the device. Work is the sum of the heats, which is the first law for a cycle; the first law is therefore built into the model rather than stated.
A device is recorded only by its heat exchanges. Working substance, the states traversed, quasi-staticity and the internal construction do not appear; "reversible" means exactly that the reversed heat exchange pattern is also realizable.
The Clausius statement is formalized for a cycle with zero net work exchanging heat with exactly two reservoirs: that is the article's "without some other change, connected therewith, occurring at the same time".
Out of scope for this mission: the Clausius inequality $\oint \delta Q/T_{\mathrm{surr}}\le0$ , the definition of entropy as a state function, Carathéodory's and Planck's formulations, the statistical-mechanical derivations, and the Clausius–Duhem inequality for continua.

Selected references

Wikipedia, Second law of thermodynamics, revision oldid=1378607758. https://en.wikipedia.org/w/index.php?title=Second_law_of_thermodynamics&oldid=1378607758
S. Carnot, Réflexions sur la puissance motrice du feu, 1824.
R. Clausius, Über eine veränderte Form des zweiten Hauptsatzes der mechanischen Wärmetheorie, Annalen der Physik 93 (1854), 481–506.

15 thms3 active usersReviewed

Completed

Differential Geometry Mathematical Physics·Captain: Lucas

Einstein Field Equations I: Local Energy–Momentum Conservation in D DimensionsTextbook

Motivation

The Einstein field equations (EFE) are the field equations of general relativity. They relate the curvature of spacetime, encoded in the metric $g_{\mu\nu}$ , to its matter–energy content, encoded in the stress–energy tensor $T_{\mu\nu}$ :

G_{\mu\nu}+\Lambda g_{\mu\nu}=\kappa T_{\mu\nu},\qquad \kappa=\frac{8\pi G}{c^4}.

They were published by Einstein in 1915. A structural requirement on any such equation is that it be compatible with the local conservation of energy and momentum, $\nabla_\beta T^{\alpha\beta}=0$ . For the EFE this compatibility is automatic: the left-hand side is identically divergence-free by the contracted Bianchi identity, so the field equations force conservation of the right-hand side. This mission formalizes that implication together with the standard algebraic reformulations of the equations, following the Wikipedia article Einstein field equations (revision 1374672993).

Setting

Everything is written in one coordinate chart. A point is $x\in\mathbb{R}^D$ , where $D$ is the spacetime dimension (not fixed to $4$ ). A 2-tensor field is a matrix-valued function $x\mapsto T_{ab}(x)$ . A metric on an open set $U$ is a 2-tensor field $g$ whose components are $C^\infty$ on $U$ and which is symmetric and nondegenerate at each point of $U$ ; $g^{ab}$ denotes the inverse matrix. Partial derivatives $\partial_a$ are coordinate (Fréchet) derivatives. Using the Misner–Thorne–Wheeler $(+\,+\,+)$ convention adopted by the source:

Christoffel symbols $\Gamma^c_{ab}=\tfrac12g^{cs}(\partial_ag_{sb}+\partial_bg_{sa}-\partial_sg_{ab})$ ;
Riemann tensor $R^\mu{}_{\alpha\beta\gamma}=\partial_\beta\Gamma^\mu_{\alpha\gamma}-\partial_\gamma\Gamma^\mu_{\alpha\beta}+\Gamma^\mu_{\sigma\beta}\Gamma^\sigma_{\gamma\alpha}-\Gamma^\mu_{\sigma\gamma}\Gamma^\sigma_{\beta\alpha}$ ;
Ricci tensor $R_{\mu\nu}=R^\alpha{}_{\mu\alpha\nu}$ , scalar curvature $R=g^{\mu\nu}R_{\mu\nu}$ , Einstein tensor $G_{\mu\nu}=R_{\mu\nu}-\tfrac12Rg_{\mu\nu}$ ;
covariant derivative $\nabla_\lambda T_{\mu\nu}=\partial_\lambda T_{\mu\nu}-\Gamma^\sigma_{\lambda\mu}T_{\sigma\nu}-\Gamma^\sigma_{\lambda\nu}T_{\mu\sigma}$ and divergence $(\operatorname{div}T)_\mu=g^{\nu\lambda}\nabla_\lambda T_{\mu\nu}$ , the index-lowered form of $\nabla_\nu T^{\mu\nu}$ ;
the field equations on $U$ : $G_{\mu\nu}(x)+\Lambda g_{\mu\nu}(x)=\kappa T_{\mu\nu}(x)$ for all $x\in U$ .

Formalization targets

Goal: local energy–momentum conservation

For a smooth nondegenerate symmetric metric $g$ on an open $U\subseteq\mathbb{R}^D$ , constants $G,c>0$ , $\kappa=8\pi G/c^4$ , any $\Lambda$ , and any $T$ such that the field equations hold on $U$ :

g^{\beta\lambda}\nabla_\lambda T_{\alpha\beta}=0\quad\text{on }U.

Milestones

Symmetry of the Einstein tensor, $G_{\mu\nu}=G_{\nu\mu}$ .
Metric compatibility, $\nabla_\lambda g_{\mu\nu}=0$ .
The differential Bianchi identity $R^\mu{}_{\alpha[\beta\gamma;\varepsilon]}=0$ .
The contracted Bianchi identity, $G^{\alpha\beta}{}_{;\beta}=0$ .
The trace of the EFE, $R-\tfrac D2R+D\Lambda=\kappa T$ .
Equivalence with the trace-reversed form $R_{\mu\nu}-\tfrac2{D-2}\Lambda g_{\mu\nu}=\kappa(T_{\mu\nu}-\tfrac1{D-2}Tg_{\mu\nu})$ for $D\neq2$ .
The vacuum equations $R_{\mu\nu}=\Lambda g_{\mu\nu}/(\tfrac D2-1)$ when $T=0$ , $D\neq2$ .
The cosmological term as vacuum stress–energy $T^{(\mathrm{vac})}_{\mu\nu}=-\tfrac\Lambda\kappa g_{\mu\nu}$ , with $\rho_{\mathrm{vac}}=-p_{\mathrm{vac}}=\Lambda/\kappa$ .
Minkowski space $\operatorname{diag}(-1,1,1,1)$ is a vacuum solution.

Significance

Conservation of $T_{\mu\nu}$ is a consistency condition that any relativistic field equation for gravity has to satisfy; it is also the starting point for deriving the motion of matter (for dust, the geodesic equation) from the field equations alone. The trace-reversed and vacuum forms are the ones used in practice to study vacuum solutions such as Schwarzschild and Kerr, and Einstein manifolds in geometry.

All of these results are classical and fully proved in the literature. What is not yet available is a machine-checked development of the Levi-Civita curvature calculus in coordinates suitable for these statements: Mathlib currently has no Riemann or Ricci tensor of a pseudo-Riemannian metric. The mission produces that layer and the proofs on top of it.

Difficulty

The algebraic milestones (trace, trace reversal, vacuum form, vacuum energy) only need matrix algebra and the symmetry of $g$ ; without symmetry the identity $g^{\mu\nu}g_{\mu\nu}=D$ fails, so symmetry is essential. The analytic core is the contracted Bianchi identity: it needs the symmetry of mixed second and third partial derivatives (Schwarz's theorem on an open set), derivatives of the matrix inverse $g^{-1}$ , and lengthy index bookkeeping with sums over $\operatorname{Fin} D$ . Since all objects are total functions, every derivative step must be justified by differentiability on the open set $U$ , not taken for granted.

Formalization scope

Coordinates: $\mathbb{R}^D$ is represented as Fin D → ℝ; tensors are Matrix (Fin D) (Fin D) ℝ-valued functions; no manifold structure. $D$ is arbitrary, and no Lorentzian signature is imposed (the results hold for any nondegenerate symmetric metric, which includes the Lorentzian case).
Regularity: the metric components are $C^\infty$ on the open set $U$ ; $T$ carries no assumptions, as the field equations determine it on $U$ .
Total-function conventions: the inverse of a singular matrix is $0$ and the derivative of a non-differentiable function is $0$ ; nondegeneracy on $U$ and openness of $U$ make these junk values irrelevant at points of $U$ .
Divergence is taken on the second index; for symmetric tensors such as $G$ this is the same as the first.
Not formalized: the Newtonian limit (it rests on approximations), the Einstein–Maxwell system, and the polynomial form.
Reusable output: coordinate Christoffel/Riemann/Ricci calculus, metric compatibility, Bianchi identities.

Selected references

Wikipedia, Einstein field equations, revision 1374672993. https://en.wikipedia.org/w/index.php?title=Einstein_field_equations&oldid=1374672993
C. W. Misner, K. S. Thorne, J. A. Wheeler, Gravitation, W. H. Freeman, 1973.
S. Carroll, Spacetime and Geometry: An Introduction to General Relativity, Addison Wesley, 2004.

12 thms3 active usersReviewed

Mathematical Physics Quantum Error Correction Quantum Gravity+1·Captain: Lucas

Harlow TASI 2017: Entanglement Wedge Reconstruction, Quantum RT and JLMS are EquivalentResearch Paper

Motivation

In the AdS/CFT correspondence a quantum theory of gravity in an asymptotically anti-de Sitter spacetime is equivalent to a conformal field theory on its boundary. A central question is how local bulk physics is encoded in the boundary theory, and in particular which bulk region is described by a given boundary subregion $R$ . Harlow's TASI 2017 lectures (arXiv:1802.01040) review the answer that emerged from quantum error correction: the boundary Hilbert space is a code, bulk effective field theory lives in a code subspace, and the boundary subregion $R$ can reconstruct every bulk operator in its entanglement wedge. The lectures state as their main technical target the theorem that this entanglement wedge reconstruction, the quantum Ryu–Takayanagi (RT) formula with a central area operator, and the JLMS formula (equality of boundary and bulk relative entropies) are mathematically equivalent. All of these statements are finite-dimensional linear algebra, which makes them formalizable now.

Timeline. Almheiri, Dong and Harlow proposed the quantum-error-correction interpretation of AdS/CFT in 2014 (arXiv:1411.7041). Jafferis, Lewkowycz, Maldacena and Suh derived the JLMS relation in 2015 (arXiv:1512.06431), and Dong, Harlow and Wall established the implications between JLMS and reconstruction for factors in 2016 (arXiv:1601.05416). Harlow proved the general three-way equivalence for arbitrary finite-dimensional von Neumann algebras in 2016 (arXiv:1607.03901, Comm. Math. Phys. 2017). The TASI lectures (2017, published 2018) present this theorem as Theorem 5.2.

Setting

All Hilbert spaces are finite-dimensional. The boundary space factorizes as $\mathcal H=\mathcal H_R\otimes\mathcal H_{\overline R}$ . A code subspace $\mathcal H_{code}\subseteq\mathcal H$ is described by an isometry $V$ whose columns $|\tilde i\rangle$ are an orthonormal basis of $\mathcal H_{code}$ . An operator $O_R$ on $\mathcal H_R$ represents a logical operator $\tilde O$ if $O_R|\tilde\psi\rangle=\tilde O|\tilde\psi\rangle$ and $O_R^\dagger|\tilde\psi\rangle=\tilde O^\dagger|\tilde\psi\rangle$ for every code state.

A von Neumann algebra $M$ on $\mathcal H_{code}$ is a set of operators closed under sums, products and adjoints and containing all multiples of the identity; $M'$ is its commutant and $Z_M=M\cap M'$ its center. Every such $M$ is block diagonal, $\mathcal H_{code}=\bigoplus_\alpha\mathcal H_{r_\alpha}\otimes\mathcal H_{\overline r_\alpha}$ with $M=\bigoplus_\alpha\mathcal L(\mathcal H_{r_\alpha})\otimes I_{\overline r_\alpha}$ . For a state $\tilde\rho$ with diagonal blocks $p_\alpha\tilde\rho_{r_\alpha\overline r_\alpha}$ , the algebraic entropy is $S(\tilde\rho,M)=-\sum_\alpha p_\alpha\log p_\alpha+\sum_\alpha p_\alpha S(\tilde\rho_{r_\alpha})$ , and the algebraic relative entropy $S(\tilde\rho|\tilde\sigma,M)$ is defined analogously (eqs. (5.16), (5.18)).

Formalization targets

Goal: Theorem 5.2 (entanglement wedge reconstruction theorem)

For $\mathcal H_{code}\subseteq\mathcal H_R\otimes\mathcal H_{\overline R}$ and a von Neumann algebra $M$ on $\mathcal H_{code}$ , the following are equivalent:

\text{(1) every } \tilde O\in M \text{ is represented on } R \text{ and every } \tilde O'\in M' \text{ on } \overline R;

\text{(2) } \exists\,\mathcal L_R\in Z_M:\ S(\tilde\rho_R)=\mathrm{Tr}(\tilde\rho\mathcal L_R)+S(\tilde\rho,M),\ \ S(\tilde\rho_{\overline R})=\mathrm{Tr}(\tilde\rho\mathcal L_R)+S(\tilde\rho,M')\ \ \forall\tilde\rho;

\text{(3) } S(\tilde\rho_R|\tilde\sigma_R)=S(\tilde\rho|\tilde\sigma,M),\ \ S(\tilde\rho_{\overline R}|\tilde\sigma_{\overline R})=S(\tilde\rho|\tilde\sigma,M')\ \ \forall\tilde\rho,\tilde\sigma.

Milestones

Theorem 4.1: four equivalent characterizations of a correctable erasure of $\overline R$ (operator reconstruction on $R$ ; $PX_{\overline R}P=\lambda P$ ; decoupling of a reference system from $\overline R$ ; the explicit encoding $|\tilde i\rangle=U_R(|i\rangle_{R_1}|\chi\rangle_{R_2\overline R})$ ).
Eq. (4.25): the quantum Singleton bound $m\ge\frac{n+k}{2}$ for codes whose accessibility depends only on the number of qudits.
Theorem 5.1: every von Neumann algebra on a finite-dimensional Hilbert space is a block-diagonal direct sum of factors, with the matching descriptions of $M'$ and $Z_M$ .

Significance

Theorem 5.2 turns three separately motivated features of holography into a single mathematical statement. Since the RT formula is independently derived from the gravitational path integral, the theorem implies subregion duality in the entanglement wedge; it also shows that a non-trivial area operator requires an algebra with non-trivial center. Theorem 4.1 is the subsystem-code special case, and Theorem 5.1 is the structure result that gives the algebraic entropies their meaning.

The results are proved in the literature (Harlow 2017 for Theorem 5.2; Theorems 4.1 and 5.1 are standard), but the lectures state Theorem 5.2 without proof, and none of these statements has a machine-checked proof that this mission is aware of. The mission produces formal statements and, eventually, formal proofs of the finite-dimensional structure theory of operator-algebra quantum error correction.

Difficulty

The three conditions live at different levels: (1) is a statement about operators, (2) about von Neumann entropies of single states, and (3) about relative entropies of pairs of states. Passing between them requires control of the full block structure of $M$ relative to the bipartition $R\overline R$ , not only of a single factor, and the classical term $\sum_\alpha p_\alpha\log(p_\alpha/q_\alpha)$ of (5.18) couples different blocks, so the general case does not reduce to the factor case treated earlier in the literature. Relative entropies can be infinite (when supports are not nested), so the equalities in (3) are equalities of extended reals and every argument must remain valid at $+\infty$ .

Formalization scope

Hilbert spaces are coordinate spaces $\mathbb C^{\iota}$ for finite index types, operators are complex matrices, tensor products are Kronecker products, and $\mathcal H_{code}$ is the image of an isometry $V$ (an operator $O_R$ acts on code states as $O_R\otimes I_{\overline R}$ applied to $V$ ). States are density matrices (positive semidefinite, trace one). Von Neumann entropy and relative entropy are defined from eigen-decompositions; relative entropy takes values in the extended reals. A von Neumann algebra is a $*$ -subalgebra of matrices; the algebraic entropies are computed in a block decomposition $U$ of $M$ , which every statement takes as an arbitrary decomposition realizing $M$ (the value does not depend on the choice). The RT identity is stated as an equality of complex numbers. Theorem 4.1 assumes a nonzero code subspace; the Singleton bound assumes $d\ge2$ and $k\ge1$ ; both conditions are implicit in the lectures and are needed for the statements to be true.

A trivializing reading is excluded: the hypotheses of every statement are satisfiable, and the goal is a full equivalence of three non-trivial conditions rather than any single implication.

Useful reusable infrastructure: partial traces and their interaction with Kronecker products, entropies of block-diagonal states, relative entropy (Klein's inequality and its equality case), and the structure theory of finite-dimensional $*$ -algebras of matrices. Contributions of proofs of the individual implications (1)⇒(2), (2)⇒(3), (3)⇒(1) as sketches are welcome.

Selected references

D. Harlow, TASI Lectures on the Emergence of Bulk Physics in AdS/CFT, PoS(TASI2017)002, 2018. https://arxiv.org/abs/1802.01040
D. Harlow, The Ryu–Takayanagi Formula from Quantum Error Correction, Comm. Math. Phys. 354 (2017) 865–912. https://arxiv.org/abs/1607.03901
A. Almheiri, X. Dong, D. Harlow, Bulk Locality and Quantum Error Correction in AdS/CFT, JHEP 04 (2015) 163. https://arxiv.org/abs/1411.7041
D. Jafferis, A. Lewkowycz, J. Maldacena, S. J. Suh, Relative entropy equals bulk relative entropy, JHEP 06 (2016) 004. https://arxiv.org/abs/1512.06431
X. Dong, D. Harlow, A. C. Wall, Reconstruction of Bulk Operators within the Entanglement Wedge in Gauge-Gravity Duality, Phys. Rev. Lett. 117 (2016) 021601. https://arxiv.org/abs/1601.05416

23 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Strict Constraint Qualifications and Sequential Optimality Conditions for Constrained Optimization III: SAKKT-Regularity Is the Weakest Strict Constraint Qualification for SAKKTResearch Paper

Motivation

Algorithms for smooth constrained optimization stop when an approximate optimality test passes. The tests used in practice are sequential optimality conditions: properties of a sequence of iterates $x^k\to x^*$ rather than of the limit point alone. Every local minimizer satisfies them, with or without a constraint qualification. The price is that a point passing such a test need not satisfy the Karush–Kuhn–Tucker (KKT) conditions. A strict constraint qualification for a sequential condition $S$ is a property of the constraints at $x^*$ under which $S$ implies KKT for every objective function. The weaker this property, the larger the class of problems on which the condition certifies KKT points.

The Strong Approximate KKT (SAKKT) condition of Haeser and Schuverdt (J. Optim. Theory Appl. 149(3), 2011) asks for approximate Lagrange multipliers whose inequality part vanishes on every constraint that is strictly satisfied at the current iterate. It strictly implies the Approximate KKT condition (AKKT). Haeser and Schuverdt also showed that SAKKT is equivalent to the Approximate Gradient Projection condition AGP(0) of Martínez and Svaiter (2003). Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) determined the weakest strict constraint qualification associated with each of AGP, CAKKT, LAGP and SAKKT. For AKKT the answer, the Cone Continuity Property, had been found earlier (Andreani et al. 2016). This mission formalizes the SAKKT case, Theorem 4.5 of the preprint.

Setting

Consider the nonlinear program

\min f(x)\quad\text{subject to}\quad h(x)=0,\ g(x)\le0, \tag{1.1}

with $h=(h_1,\dots,h_m)$ and $g=(g_1,\dots,g_p)$ continuously differentiable on $\mathbb R^n$ . The feasible set is $\Omega=\{x:h(x)=0,\ g(x)\le0\}$ , and $J(x^*)=\{j:g_j(x^*)=0\}$ is the set of active inequalities. The KKT condition holds at $x^*$ for $f$ if there are $\lambda\in\mathbb R^m$ and $\mu\in\mathbb R^p_+$ , with $\mu_j=0$ for $j\notin J(x^*)$ , such that $\nabla f(x^*)+\sum_i\lambda_i\nabla h_i(x^*)+\sum_j\mu_j\nabla g_j(x^*)=0$ .

The linearized cone is $L_\Omega(x^*)=\{d:\langle\nabla h_i(x^*),d\rangle=0\ \forall i,\ \langle\nabla g_j(x^*),d\rangle\le0\ \forall j\in J(x^*)\}$ , and $K^\circ=\{v:\langle v,k\rangle\le0\ \forall k\in K\}$ is the polar of a set $K$ . For a convex set $S$ , the normal cone $N_S(y)=\{w:\langle w,z-y\rangle\le0\ \forall z\in S\}$ is defined for $y\in S$ and is empty for $y\notin S$ . $P_S$ is the Euclidean projection onto a nonempty closed convex set $S$ .

For a point $x$ , the linearized set $\Omega(x,0)$ consists of the $z$ with

$\langle\nabla h_i(x),z-x\rangle=0$ for all $i$ ;
$\langle\nabla g_j(x),z-x\rangle\le0$ for every $j$ with $g_j(x)\ge0$ .

It keeps the inequalities that are active or violated at $x$ and drops those strictly satisfied at $x$ .

A feasible $x^*$ satisfies SAKKT for $f$ if there are $x^k\to x^*$ , $\lambda^k\in\mathbb R^m$ and $\mu^k\in\mathbb R^p_+$ , with $\mu^k_j=0$ whenever $g_j(x^k)<0$ , such that

\nabla f(x^k)+\sum_{i=1}^m\lambda_i^k\nabla h_i(x^k)+\sum_{j=1}^p\mu_j^k\nabla g_j(x^k)\to0. \tag{1.2}

It satisfies AGP(0) for $f$ if there is $x^k\to x^*$ with $P_{\Omega(x^k,0)}(x^k-\nabla f(x^k))-x^k\to0$ . The outer limit $\limsup_{z\to z^*}F(z)$ of a set-valued map is the set of limits of sequences $w^k\in F(z^k)$ with $z^k\to z^*$ (1.6). The point $x^*$ is SAKKT-regular (Definition 4.3) if

\limsup_{x\to x^*}N_{\Omega(x,0)}(x)\subset N_{\Omega(x^*,0)}(x^*).

Formalization targets

Goal: Theorem 4.5

For continuously differentiable constraints and a feasible $x^*$ ,

x^*\ \text{SAKKT-regular}\iff\big(\forall f\in C^1:\ \text{SAKKT at }x^*\Rightarrow\text{KKT at }x^*\big).

The forward implication says SAKKT-regularity is a strict constraint qualification for SAKKT; the backward one says it is implied by every such qualification.

Milestones

Proposition 3.1: for nonempty closed convex $C$ and $x\in C$ , $\omega\in N_C(x)\iff P_C(x+\omega)=x$ .
Proposition 4.4: if $x+\varepsilon\in\Omega(x,0)$ , every element of $N_{\Omega(x,0)}(x+\varepsilon)$ is $\sum_i\lambda_i\nabla h_i(x)+\sum_{g_j(x)\ge0}\mu_j\nabla g_j(x)$ with $\mu\ge0$ and $\mu_j\langle\nabla g_j(x),\varepsilon\rangle=0$ ; and $N_{\Omega(x,0)}(x+\varepsilon)\subset N_{\Omega(x,0)}(x)$ .
AGP(0) $\iff$ SAKKT, for every $C^1$ objective (p. 6, from Haeser–Schuverdt).
$-\nabla f(x^*)\in L_\Omega(x^*)^\circ\iff$ KKT at $x^*$ .
(4.22): $N_{\Omega(x^*,0)}(x^*)=L_\Omega(x^*)^\circ$ at a feasible $x^*$ .
(4.23)–(4.24): an AGP(0) sequence for $f$ puts $-\nabla f(x^*)$ in $\limsup_{x\to x^*}N_{\Omega(x,0)}(x)$ .
(4.26): every $\omega^*$ in that outer limit makes AGP(0) hold for $f(x)=-\langle\omega^*,x\rangle$ .

Significance

Theorem 4.5 describes exactly the constraint systems on which a SAKKT sequence converging to $x^*$ certifies a KKT point, for every objective. Any constraint qualification already known to make SAKKT imply KKT implies SAKKT-regularity; at a point that is not SAKKT-regular, some linear objective has a SAKKT sequence converging to a non-KKT point. Because SAKKT is stronger than AKKT and AGP, its regularity condition is weaker than theirs, and Section 5 of the paper places it in the hierarchy of constraint qualifications next to AGP-regularity and CAKKT-regularity. By Proposition 4.4, SAKKT-regularity reads geometrically: the cone generated by the gradients of the equality constraints and of the inequalities that are active or violated at $x$ varies outer semicontinuously as $x\to x^*$ .

The paper's result is proved, and no part of it is formalized on the platform. The mission adds machine-checked statements of the characterization and of the polyhedral convex-analysis facts behind it: the projection characterization of normal cones, the description of normal cones of $\Omega(x,0)$ at perturbed points, and the identification of $N_{\Omega(x^*,0)}(x^*)$ with $L_\Omega(x^*)^\circ$ .

Difficulty

The forward direction passes to the limit in normal cones of sets $\Omega(x^k,0)$ that change with $k$ : the set of rows kept depends on the sign of $g_j(x^k)$ at the moving point, not on the active set at $x^*$ . Projections land at $y^k=x^k+\varepsilon^k$ , while SAKKT-regularity speaks of normal cones at $x^k$ , so the normal vectors must be transported from $y^k$ to $x^k$ ; this is Proposition 4.4, a Farkas-type statement for the cone of active rows. Moving between SAKKT and AGP(0) requires the Haeser–Schuverdt equivalence, which the paper cites rather than proves. The backward direction must build an objective function and a sequential certificate from an arbitrary element of an outer limit, which needs existence and nonexpansiveness of projections onto every $\Omega(x^k,0)$ . Finally, $L_\Omega(x^*)^\circ$ and the KKT multipliers are linked by Farkas' lemma for a finitely generated cone.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); indices are Fin m and Fin p; gradients are Mathlib's gradient.
The standing hypothesis is that every $h_i$ and $g_j$ is $C^1$ . "Smooth objective" in Theorem 4.5 is read as $C^1$ , which is all the argument uses. The objective is quantified inside the equivalence, for fixed constraints and a fixed feasible $x^*$ .
KKT is the multiplier form with sign and complementarity. The paper's reading $-\nabla f(x^*)\in L_\Omega(x^*)^\circ$ is a milestone.
SAKKT imposes $\mu^k_j=0$ when $g_j(x^k)<0$ , at the iterate and not at $x^*$ , and adds no complementarity limit. The page's " $x^k\to x$ " is read as $x^k\to x^*$ .
The normal cone is empty outside the set, and the projection is a predicate (a nearest point), not a choice function. The outer limit is the sequential one of (1.6), with $x$ ranging over all of $\mathbb R^n$ .
Definition 4.3 is the inclusion; its trailing identity with $L_\Omega(x^*)^\circ$ is milestone 5. Proposition 4.4's "elements in $\mathbb R^m$ " is read as $\mathbb R^n$ .
Junk gradients (no $C^1$ hypothesis where continuity is used), a normal cone that is nonempty at points outside the set, an objective quantified outside the equivalence, a support condition placed at $x^*$ , or KKT without sign or complementarity would each trivialize or change the statement; the definitions above rule them out.

All objects are defined in the namespace StrictCQ.SAKKT. Proofs of milestones 1, 2, 4 and 5 are reusable convex analysis beyond this mission; contributions toward a proof of the Haeser–Schuverdt equivalence (milestone 3) are welcome independently of the goal.

Selected references

R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, Strict constraint qualifications and sequential optimality conditions for constrained optimization, Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018. https://doi.org/10.1287/moor.2017.0879
G. Haeser, M. L. Schuverdt, On approximate KKT condition and its extension to continuous variational inequalities, J. Optim. Theory Appl. 149(3):528–539, 2011. https://link.springer.com/journal/10957/volumes-and-issues/149-3
J. M. Martínez, B. F. Svaiter, A practical optimality condition without constraint qualifications for nonlinear programming, J. Optim. Theory Appl. 118:117–133, 2003. https://doi.org/10.1023/A:1023617925436
R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, A cone-continuity constraint qualification and algorithmic consequences, SIAM J. Optim. 26(1):96–110, 2016. https://doi.org/10.1137/15M1008488
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

11 thms3 active usersReviewed

Control Theory Dynamic Programming Markov Chain+1·Captain: mikedeng1

Strong and Weak Equilibria for Time-Inconsistent Stochastic Control in Continuous Time 4: Limits of Equilibria of the Time-Discretized Problems Are Weak Equilibria in Continuous TimeResearch Paper

Motivation

A decision maker is time-inconsistent when the plan that is optimal today stops being optimal tomorrow. The standard source is non-exponential discounting: a reward $t$ units of time ahead is weighted by $\delta(t)$ , and unless $\delta$ is exponential the relative weight of two future dates changes as time passes. Hyperbolic and pseudo-exponential discount functions, which fit experimental and group-decision data better than exponential ones, all have this property. For such an agent "optimal control" is not a meaningful target, and the literature instead looks for equilibrium policies: plans that no current self wants to deviate from, given that all future selves follow the plan.

In discrete time the definition is unambiguous: a policy is an equilibrium if deviating at the current step alone does not help. In continuous time there is no "current step", and the usual definition, due to Ekeland and Lazrak (2006), compares the payoff of the plan with that of a deviation on a short interval $[0,\varepsilon]$ through a first-order condition as $\varepsilon\downarrow0$ . Huang and Zhou (arXiv:1809.09243, Math. Oper. Res. 2021) call this a weak equilibrium, introduce a strong equilibrium that requires the deviation to be unprofitable for every small $\varepsilon$ , and study both for a controlled finite-state Markov chain.

A natural question is whether continuous-time equilibria are the limits of the discrete-time ones as the time step shrinks. This mission formalizes the paper's answer (§5.1): limits of discrete equilibria are always weak equilibria. The paper's Example 5.1 shows they need not be strong.

Setting

The state space is $S=\{1,\dots,N\}$ . A continuous-time Markov chain on $S$ is controlled through its generator $Q=(q_{ij})$ : in state $i$ the row $Q_i$ is chosen from an admissible set $D_i\subseteq E_i=\{q: q_j\ge0\ (j\ne i),\ q_i=-\sum_{j\ne i}q_j\}$ , and the control space is $\mathcal Q=\{Q: Q_i\in D_i\ \forall i\}$ . A payoff function $f(t,i,q)$ gives the reward at time-distance $t$ from now, in state $i$ , under row $q$ . The standing assumptions are continuity of $t\mapsto f(t,i,q)$ on $[0,\infty)$ and, for each $c>0$ , integrability over $[0,\infty)$ of $\sup_{i,\,q\in D_i,\,\|q\|\le c}|f(t,i,q)|$ (condition (2.3)). The expected payoff from state $i$ is

F(i,Q)=\mathbb E_{i,Q}\Big[\int_0^\infty f(t,X_t,Q_{X_t})\,dt\Big]=\int_0^\infty\sum_j(e^{tQ})_{ij}f(t,j,Q_j)\,dt,

and $F(Q)=(F(1,Q),\dots,F(N,Q))$ . With $Q\otimes_\varepsilon Q^*$ the generator that uses $Q$ on $[0,\varepsilon]$ and $Q^*$ afterwards, $Q^*\in\mathcal Q$ is a weak equilibrium if $\liminf_{\varepsilon\downarrow0}\big(F(i,Q^*)-F(i,Q\otimes_\varepsilon Q^*)\big)/\varepsilon\ge0$ for all $i$ and $Q\in\mathcal Q$ . The first-order quantity is $\Gamma^{Q^*}(q)=f(0,i,q)+q\cdot F(Q^*)$ .

Discretization. Fix a mesh $\delta_n>0$ . A transition matrix $u$ (rows in the probability simplex $\mathfrak P$ ) has generator $Q^{u,n}=(u-I)/\delta_n$ , the admissible matrices are $\mathcal A^n=\{u: Q^{u,n}\in\mathcal Q\}$ , and the discrete payoff is $\kappa^n(k,i,\alpha)=f\big(k\delta_n,i,(\alpha-e_i)/\delta_n\big)\,\delta_n$ . The discrete value is $V^n(i,u)=\mathbb E_{i,u}\big[\sum_{k\ge0}\kappa^n(k,X_k,u_{X_k})\big]$ , and $u^n\in\mathcal A^n$ is a discrete equilibrium if $V^n(i,u^n)\ge V^n(i,u\otimes_1u^n)$ for all $i$ and $u\in\mathcal A^n$ , where $u\otimes_1u^n$ uses $u$ at time $0$ and $u^n$ afterwards. The continuation values are $H^n_i(u^n)=\mathbb E_{i,u^n}\big[\sum_{k\ge0}\kappa^n(k+1,X_k,u^n_{X_k})\big]$ . Theorem 5.2 additionally assumes (5.8): for some $T>0$ , $t\mapsto|f(t,i,q)|$ is nonincreasing on $[T,\infty)$ .

Formalization targets

Goal: Theorem 5.2

Let $\delta_n\downarrow0$ , let $u^n$ be an equilibrium of the problem with mesh $\delta_n$ , $Q^n=Q^{u^n,n}$ , and suppose $f(\cdot,i,\cdot)$ is continuous on $[0,\infty)\times D_i$ . If $Q^{n_k}\to Q^*\in\mathcal Q$ along a subsequence, then

\Gamma^{Q^*}(Q^*_i)\ge\Gamma^{Q^*}(Q_i)\quad\text{for all }(i,Q)\in S\times\mathcal Q,\qquad\text{and } Q^* \text{ is a weak equilibrium.}

Milestones

(5.12): an equilibrium $u^n$ satisfies $\kappa^n(0,i,u^n_i)+H^n(u^n)\cdot u^n_i\ge\kappa^n(0,i,u_i)+H^n(u^n)\cdot u_i$ for all $u\in\mathcal A^n$ .
Generator form (proof of Theorem 5.2): dividing by $\delta_n$ , the same inequality reads $f(0,i,Q^n_i)+H\cdot Q^n_i\ge f(0,i,Q^{u,n}_i)+H\cdot Q^{u,n}_i$ .
Continuity of $Q\mapsto F(Q)$ on $\mathcal Q$ (proof of Theorem 3.3).
Lemma 5.1: $H^{n_k}_i(u^{n_k})\to F(i,Q^*)$ along the subsequence.

Significance

The theorem justifies the weak-equilibrium notion from discrete time: whatever a time-inconsistent agent does on a fine time grid, the continuous-time limit satisfies the first-order condition (3.10). Combined with the paper's discrete existence result (Theorem 5.1) and compactness of $\mathcal Q$ , it yields weak equilibria by approximation (Remark 5.3). It also locates the gap between the two notions: the limit is weak but in general not strong.

The result is proved in the paper; nothing about it is open. No part of it has a machine-checked proof. A formal development adds a checked Euler-scheme comparison between $(I+\delta Q)^k$ and $e^{k\delta Q}$ for generator matrices, a dominated passage to the limit for Riemann sums of the payoff, and continuity of the payoff in the generator, each reusable for other finite-state continuous-time control problems.

Difficulty

The obvious argument is to divide the discrete one-step inequality (5.12) by $\delta_n$ and let $n\to\infty$ . Its algebraic part is immediate. The difficulty is the convergence of the discrete continuation values $H^n(u^n)$ , which are infinite sums along a discrete chain with transition matrix $u^n$ , to the continuous payoff $F(Q^*)$ , an integral along the continuous chain with generator $Q^*$ . Three errors must be controlled at once: the discrete chain against the chain sampled from $e^{tQ^n}$ (the difference of $k$ -th powers grows with $k\approx M/\delta_n$ ), the Riemann sum against the integral (needs uniform continuity of $f$ jointly in $t$ and $q$ ), and $F(Q^n)$ against $F(Q^*)$ . The tail of the infinite sums is not controlled by (2.3) alone: integrability of a majorant does not make its samples on a grid summable, which is why (5.8) is assumed. A second subtlety concerns the last step: the paper passes from (3.10) to the weak-equilibrium property through Theorem 3.1, which assumes a condition (3.3) that Theorem 5.2 does not. The conclusion is still true without (3.3), but no numbered statement of the paper provides that step.

Formalization scope

States are Fin N; rows are Fin N → ℝ with the sup norm, generators and transition matrices are Matrix (Fin N) (Fin N) ℝ with the product topology.
Expectations are written through marginals: $F(i,Q)=\int_0^\infty\sum_j(e^{tQ})_{ij}f(t,j,Q_j)\,dt$ (Bochner integral) and $H^n_i(u)=\sum_k\sum_j(u^k)_{ij}\kappa^n(k+1,j,u_j)$ (tsum). No Markov process is constructed.
The weak-equilibrium liminf is encoded as "for every $\eta>0$ , eventually as $\varepsilon\downarrow0$ the quotient is $\ge-\eta$ ".
" $f(\cdot,i,\cdot)$ is continuous" is joint continuity on $[0,\infty)\times D_i$ ; (5.8) is required for $q\in D_i$ ; $\delta_n\downarrow0$ is positivity, monotonicity and convergence to $0$ ; the subsequence is a strictly increasing $\varphi:\mathbb N\to\mathbb N$ .
Not assumed: integrability of $F$ , summability of $H^n$ or (5.2) for $\kappa^n$ (they follow from (2.3) and (5.8)), compactness of $D_i$ , and condition (3.3).
The equilibria $u^n$ , the generators $Q^n=(u^n-I)/\delta_n$ and the subsequence are part of the goal's data. A version that only assumes " $Q^n\to Q^*$ " for arbitrary $Q^n\in\mathcal Q$ would be false and is ruled out.
The continuity milestone is proved in the paper for compact $D_i$ ; it is stated here without compactness, since only convergent sequences in $\mathcal Q$ matter.
Needed infrastructure: bounds on $\|(I+\delta Q)^k-e^{k\delta Q}\|$ for generator matrices, stochasticity of $e^{tQ}$ for generator $Q$ , dominated convergence for the payoff integral and for the discrete series. Contributions of these general lemmas are welcome.

Selected references

Y.-J. Huang and Z. Zhou, Strong and Weak Equilibria for Time-Inconsistent Stochastic Control in Continuous Time, Math. Oper. Res. 46(2), 2021; read as arXiv:1809.09243v3. https://arxiv.org/abs/1809.09243 , https://doi.org/10.1287/moor.2020.1066
I. Ekeland and A. Lazrak, Being serious about non-commitment: subgame perfect equilibrium in continuous time, tech. rep., University of British Columbia, 2006. http://arxiv.org/abs/math/0604264
S. N. Ethier and T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658

8 thms3 active usersReviewed

Bandit Algorithms Operations Research Probability+1·Captain: mikedeng1

Learning Unknown Service Rates in Queues 3: In Heavy Traffic Every α-Consistent Scheduling Policy Has Average Queue-Regret at Least D(μ)(K−1) log t / (4 log log t) Up to Time (K−1)D(μ)/(4ε)Research Paper

Motivation

A switch network is a set of $U$ queues served by $K\ge U$ servers. In every time slot each server can serve at most one queue, so a scheduler must pick a matching of queues to servers. Such systems model input-queued packet switches, crowdsourcing platforms that route job types to worker types, and wireless links with unknown channel quality. When the success probability of each queue–server link is unknown, the scheduler has to learn it from the services it observes while the queues are building up. This makes switch scheduling a multi-armed bandit problem in which the cost is not cumulative reward but queue length.

Krishnasamy, Sen, Johari and Shakkottai (arXiv:1604.06377, Operations Research 2021) measure a scheduler by its queue-regret: the expected difference between its queue lengths and those of a genie that knows the best matching. They show that the queue-regret has two regimes. In the late stage, once the queues regularly empty, it decays like $1/t$ (their Theorem 3, the subject of a sibling mission). In the early stage it grows like $\log t/\log\log t$ , as the regret of a classical bandit does, and the system is then effectively unstable. This mission is about the early stage, made precise in the paper's Theorem 8: in heavy traffic, where the arrival rates are close to the best service rates, every reasonable policy pays logarithmic queue-regret for a long time.

The lower-bound technique descends from Lai and Robbins (1985): a policy that does well on every instance must explore each sub-optimal link about $\log t/\mathrm{KL}$ times, a count obtained by a change of measure and the Bretagnolle–Huber inequality.

Setting

Queues are indexed by $u\in[U]$ and servers by $k\in[K]$ . In every slot $t\ge1$ , queue $u$ receives an arrival $A_u(t)\sim\mathrm{Bernoulli}(\lambda_u)$ , and link $(u,k)$ offers a service $R_{uk}(t)\sim\mathrm{Bernoulli}(\mu_{uk})$ . All of these are independent and i.i.d. over slots. Notation:

$\mu^*_u=\max_k\mu_{uk}$ , attained at $k^*_u$ ;
$\epsilon_u=\mu^*_u-\lambda_u$ and $\Delta_{uk}=\mu^*_u-\mu_{uk}$ ;
$\Delta=\min_{u,k\ne k^*_u}\Delta_{uk}$ , $\mu_{\min}=\min\mu_{uk}$ and $\mu^*=\max\mu_{uk}$ ;
$\bar\epsilon=\frac1U\sum_u\epsilon_u$ .

Assumption 1 asks that every queue have a unique best server and that the best servers of distinct queues be distinct. Assumption 2 is $\epsilon_u>0$ for every $u$ . Assumption 3 draws the initial queue vector from the stationary law of the genie queues.

A scheduler picks a matching $\kappa(t)$ , so queue $u$ is served by server $\kappa_u(t)$ . Its decision may use the past schedules, the services observed on the scheduled links, and private randomness. The queues evolve as $Q_u(t)=(Q_u(t-1)+A_u(t)-R_{u\kappa_u(t)}(t))^+$ . The genie always schedules $k^*$ and has queues $Q^*_u(t)$ . The queue-regret is $\Psi_u(t)=\mathbb E[Q_u(t)-Q^*_u(t)]$ . The schedule counts are $T_{uk}(t+1)=\sum_{s=1}^t\mathbb 1\{\kappa_u(s)=k\}$ .

A policy is $\alpha$ -consistent ( $\alpha\in(0,1)$ ) if on every instance $\mathbb E[T_{uk}(t+1)]\le C\,t^{\alpha}$ for all $u$ and all $k\ne k^*_u$ , with a constant $C$ that may depend on the instance. The key constant is

D(\mu)=\frac{\Delta}{\mathrm{KL}\big(\mu_{\min},\frac{\mu^*+1}{2}\big)},

where $\mathrm{KL}$ is the Bernoulli Kullback–Leibler divergence.

Formalization targets

Goal: Theorem 8 (p. 18)

Fix $\mu$ , an $\alpha$ -consistent policy and $\gamma>1/(1-\alpha)$ . There exist constants $\tau$ and $C_1$ , the same for every arrival vector $\lambda$ , such that, with $T_0=\max\{C_1K^\gamma,\tau\}$ and $\eta=(K-1)D(\mu)/(2T_0)$ :

\bar\epsilon<\tfrac\eta2\ \Longrightarrow\ \frac1U\sum_u\Psi_u(t)\ge\frac{D(\mu)}4(K-1)\frac{\log t}{\log\log t}\quad\text{for } t\in\Big[T_0,\ \tfrac{(K-1)D(\mu)}{4\bar\epsilon}\Big],

\epsilon_u<\eta\ \Longrightarrow\ \Psi_u(t)\ge\frac{D(\mu)}4\max\{U-1,2(K-U)\}\frac{\log t}{\log\log t}\quad\text{for } t\in\Big[T_0,\ \tfrac{(K-1)D(\mu)}{2\epsilon_u}\Big].

Milestones

Lemma 18 (Bretagnolle–Huber, p. 37), referenced from the platform.
Lemma 19 (p. 37): for $t>\tau$ , $\mathbb E[T_{uk}(t+1)]+\sum_{u'\ne u}\mathbb 1\{k^*_{u'}=k\}\mathbb E[T_{u'k^*_u}(t+1)]\ge\frac{(1-\alpha)\log t-\log(4KC)}{\mathrm{KL}(\mu_{\min},(\mu^*+1)/2)}$ .
Corollary 20 (p. 39): the summed forms of Lemma 19, with factors $U(K-1)D(\mu)$ , $(U-1)D(\mu)$ and $(K-U)D(\mu)$ .
Lemma 22 (p. 42): $\Psi_u(t)\ge\sum_{k\ne k^*_u}\Delta_{uk}\mathbb E[T_{uk}(t+1)]-\epsilon_u t$ for any policy.

Significance

Theorem 8 complements the late-stage $1/t$ lower bound. Together they show that queue-regret goes through a phase transition. Up to time of order $K/\epsilon$ , the queue-regret of any consistent policy grows like $\log t/\log\log t$ . Since the left end of the window does not move as $\epsilon\to0$ while the right end grows like $1/\epsilon$ , the heavily loaded regime is exactly where learning costs are visible in queue lengths. The theorem also explains why algorithms designed for the late stage (Q-UCB, Q-ThS in the same paper) cannot avoid this early cost.

The formalization adds a machine-checked statement of a lower bound whose constants are pinned down precisely. In particular it states which quantities $\tau$ and $C_1$ may depend on (see below). Along the way it builds a reusable model of a learning switch scheduler: randomized, history-dependent policies, the coupled genie system and the stationary initial law. It also provides a Lai–Robbins-type count bound (Lemma 19) for matching bandits. The results are proved on paper in the held preprint (§9.2). To the best of the platform's records none of them has been formalized.

Difficulty

The obvious route to Theorem 8 is to bound the queue-regret below by the regret of the corresponding bandit. That fails, because queue-regret is not cumulative: an empty queue forgives past mistakes. The proof therefore needs the stationary start (Assumption 3), so that $\mathbb E[Q^*_u(t)]=\mathbb E[Q_u(0)]$ and the sub-optimal schedules show up as a drift (Lemma 22). This holds only up to a load term $\epsilon_u t$ , which limits the window.

The count bound (Lemma 19) requires a change of measure between two instances that swap the best servers of two queues. It needs a chain rule for the KL divergence of adaptively collected observations, where the policy's own randomness must cancel. Neither the swapped instances nor the trajectory law are standard Mathlib objects.

Formalization scope

Queues are Fin U and servers are Fin K, with $1\le U\le K$ and $K\ge2$ . $K=1$ is trivial, and for it $\Delta$ is an empty minimum.
Slots are 1-based. Matchings are embeddings Fin U ↪ Fin K.
Probability space. The randomness is a product of independent uniforms on $[0,1]$ per slot (arrivals, link services, one private scheduler seed), i.i.d. over slots. Bernoulli variables arise by thresholding. The initial state is drawn independently.
Policies see only past schedules and the services on scheduled links (p. 6), plus a private uniform. This covers every randomized, history-dependent policy, and each choice is required to be measurable in the seed.
The genie shares the initial state, arrivals and services of the policy's system. Queue-regret is a Lebesgue integral of $Q_u(t)-Q^*_u(t)$ , a difference bounded by $t$ .
Assumption 3 is the product of the geometric laws $(1-\rho_u)\rho_u^n$ , $\rho_u=\lambda_u(1-\mu^*_u)/((1-\lambda_u)\mu^*_u)$ . This is the stationary law of the printed recursion.
α-consistency quantifies over every instance with entries in $[0,1]$ satisfying Assumption 1. The constant is chosen after the instance, and the definition does not mention $\lambda$ , because the schedule does not depend on it.
$D(\mu)$ and $1/\mathrm{KL}$ are set to $0$ when $\mu^*=1$ , where the divergence is infinite.
Lemma 19 and Corollary 20 carry $C>0$ , which is without loss of generality. Corollary 20(c)'s sum $\sum_{k>U}$ is the sum over servers that are optimal for no queue.
Constants of Theorem 8. The paper says $\tau,C_1$ are "independent of $(\lambda,\mu)$ ". Its proof supports independence of $\lambda$ only, so the formal statement chooses $\tau,C_1$ after $\mu$ and the policy but before $\lambda$ . Choosing them after $\lambda$ would trivialize the theorem, since a huge $C_1$ makes the hypothesis $\bar\epsilon<\eta/2$ unsatisfiable. The formal $\tau$ also exceeds $e$ , so that $\log\log t>0$ on the window, and $t$ ranges over integers.
Assumptions. Assumptions 1–3 appear exactly where the paper uses them: Lemma 22 and Theorem 8 assume all three, Lemma 19 and Corollary 20 only Assumption 1.

The source is the arXiv v4 preprint; the paper's proofs are in its §§8–9. Welcome contributions include the KL chain rule for adaptively scheduled Bernoulli observations, stationarity of the geometric law for the genie chain, and measurability of the trajectory.

Selected references

S. Krishnasamy, R. Sen, R. Johari, S. Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach, Operations Research 69(1), 2021; preprint arXiv:1604.06377v4. https://arxiv.org/abs/1604.06377
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794
S. Bubeck, V. Perchet, P. Rigollet, Bounded regret in stochastic multi-armed bandits, COLT 2013. https://arxiv.org/abs/1302.1611

9 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Strict Constraint Qualifications and Sequential Optimality Conditions for Constrained Optimization II: AGP-Regularity Is the Weakest Strict Constraint Qualification for AGPResearch Paper

Motivation

Algorithms for smooth constrained optimization stop when an approximate optimality test passes. The tests used in practice are sequential optimality conditions: properties of a sequence of iterates $x^k\to x^*$ rather than of the limit alone. Every local minimizer satisfies them, with or without a constraint qualification, which makes them natural stopping criteria. The price is that a point passing such a test need not satisfy the Karush–Kuhn–Tucker (KKT) conditions. A strict constraint qualification for a sequential condition $S$ is a property of the constraints at $x^*$ under which $S$ implies KKT for every objective function. The weaker this property, the more problems on which the stopping test is guaranteed to certify a KKT point.

The Approximate Gradient Projection (AGP) condition was introduced by Martínez and Svaiter (2003) and is the natural stopping criterion of inexact restoration methods. It is strictly stronger than the Approximate KKT condition (AKKT), and it does not require Lagrange multiplier estimates. Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) determined the weakest strict constraint qualification associated with AGP and with several other sequential conditions. For AKKT the answer had been found earlier: the Cone Continuity Property of Andreani, Martínez, Ramos and Silva (2016). This mission formalizes the AGP case, Theorem 4.2 of the preprint, together with its linear-constraint variant, Theorem 4.6.

Setting

Consider the nonlinear program

\min f(x)\quad\text{subject to}\quad h(x)=0,\ g(x)\le0, \tag{1.1}

with $h=(h_1,\dots,h_m)$ and $g=(g_1,\dots,g_p)$ continuously differentiable on $\mathbb R^n$ . The feasible set is $\Omega=\{x:h(x)=0,\ g(x)\le0\}$ , and $J(x^*)=\{j:g_j(x^*)=0\}$ is the set of active inequalities. The KKT condition holds at $x^*$ for $f$ if there are $\lambda\in\mathbb R^m$ and $\mu\in\mathbb R^p_+$ , with $\mu_j=0$ for $j\notin J(x^*)$ , such that $\nabla f(x^*)+\sum_i\lambda_i\nabla h_i(x^*)+\sum_j\mu_j\nabla g_j(x^*)=0$ .

The linearized cone is $L_\Omega(x^*)=\{d:\langle\nabla h_i(x^*),d\rangle=0\ \forall i,\ \langle\nabla g_j(x^*),d\rangle\le0\ \forall j\in J(x^*)\}$ , and $K^\circ=\{v:\langle v,k\rangle\le0\ \forall k\in K\}$ is the polar of a set $K$ . For a convex set $S$ , the normal cone $N_S(y)=\{w:\langle w,z-y\rangle\le0\ \forall z\in S\}$ is defined for $y\in S$ and is empty for $y\notin S$ . $P_S$ denotes the Euclidean projection onto a closed convex set $S$ .

For $\gamma\in[-\infty,0]$ and a point $x$ , the linearized set $\Omega(x,\gamma)$ of (4.2) consists of the $z$ with

$\langle\nabla h_i(x),z-x\rangle=0$ for all $i$ ;
$\langle\nabla g_j(x),z-x\rangle\le0$ if $g_j(x)\ge0$ ;
$g_j(x)+\langle\nabla g_j(x),z-x\rangle\le0$ if $\gamma<g_j(x)<0$ .

A feasible $x^*$ satisfies AGP( $\gamma$ ) for $f$ if there is a sequence $x^k\to x^*$ with

P_{\Omega(x^k,\gamma)}\big(x^k-\nabla f(x^k)\big)-x^k\to0. \tag{4.1}

The outer limit $\limsup_{z\to z^*}F(z)$ of a set-valued map is the set of limits of sequences $w^k\in F(z^k)$ with $z^k\to z^*$ (1.6). The point $x^*$ is AGP-regular (Definition 4.1) if

\limsup_{(x,\varepsilon)\to(x^*,0)}N_{\Omega(x,-\infty)}(x+\varepsilon)\subset N_{\Omega(x^*,-\infty)}(x^*).

Formalization targets

Goal: Theorem 4.2

For continuously differentiable constraints and a feasible $x^*$ ,

x^*\ \text{AGP-regular}\iff\big(\forall f\in C^1:\ \mathrm{AGP}(-\infty)\text{ at }x^*\Rightarrow\text{KKT at }x^*\big).

The forward implication says AGP-regularity is a strict constraint qualification for AGP; the backward one says it is implied by every such qualification.

Milestones

Proposition 3.1: for nonempty closed convex $C$ and $x\in C$ , $\omega\in N_C(x)\iff P_C(x+\omega)=x$ .
Nonexpansiveness of $P_C$ , used in (4.10).
(4.6): $N_{\Omega(x^*,-\infty)}(x^*)=L_\Omega(x^*)^\circ$ at a feasible $x^*$ .
$-\nabla f(x^*)\in L_\Omega(x^*)^\circ\iff$ KKT at $x^*$ .
(4.8): $N_{\Omega(x^k,\gamma)}(x^k+\varepsilon^k)\subset N_{\Omega(x^k,-\infty)}(x^k+\varepsilon^k)$ for $k$ large.
(4.7)–(4.9): under AGP-regularity, AGP( $\gamma$ ) implies KKT for every $\gamma\in[-\infty,0)$ .
(4.10)–(4.11): every $\omega^*$ in the outer limit makes AGP( $-\infty$ ) hold for $f(x)=-\langle\omega^*,x\rangle$ .

Companion: Theorem 4.6

The same characterization for the Linear AGP condition (LAGP), in which the linear constraints are kept exact and the iterates stay in the set $\Omega_L$ they define. LAGP-regularity (Definition 4.4) is outer semicontinuity of $(x,\varepsilon)\mapsto N_{\Omega_{NL}(x,-\infty)\cap\Omega_L}(x+\varepsilon)$ relative to $x\in\Omega_L$ . Two further items accompany it: Proposition 4.1, the explicit form of $N_{\Omega(x,-\infty)}(x+\varepsilon)$ , and the equality $N_{\Omega_{NL}(x^*,-\infty)\cap\Omega_L}(x^*)=L_\Omega(x^*)^\circ$ appended to Definition 4.4.

Significance

Theorem 4.2 gives the exact boundary of the problems on which an AGP-based stopping test certifies KKT points. Any constraint qualification already known to make AGP imply KKT, for instance the Cone Continuity Property, implies AGP-regularity. Conversely, at a point that is not AGP-regular some objective function has an AGP sequence converging to a non-KKT point. In Section 5 of the paper the theorem places AGP-regularity in the hierarchy of constraint qualifications, with the regularity notions for CAKKT and SAKKT next to it.

The paper's result is proved, and no part of it is formalized on the platform. The mission adds machine-checked statements of the characterization and of the convex-analysis facts it rests on: the projection characterization of normal cones, nonexpansiveness, and the polyhedral normal cone of $\Omega(x^*,-\infty)$ as the polar of the linearized cone. These facts are reusable for any sequential optimality condition built on projections.

Difficulty

The forward direction passes to the limit in normal cones of sets $\Omega(x^k,\gamma)$ that vary with $k$ and are evaluated at perturbed points $x^k+\varepsilon^k$ , which may lie outside $\Omega(x^k,-\infty)$ . For finite $\gamma$ the inclusion of $N_{\Omega(x^k,\gamma)}$ in $N_{\Omega(x^k,-\infty)}$ fails at such points. It holds only for $k$ large, through a continuity argument on the inactive constraints. The backward direction must manufacture an objective function and an AGP sequence from an arbitrary element of an outer limit, which requires existence of projections onto every $\Omega(x^k,-\infty)$ . The identification of $N_{\Omega(x^*,-\infty)}(x^*)$ with $L_\Omega(x^*)^\circ$ needs the localization of a polyhedral normal cone, and the link between $L_\Omega(x^*)^\circ$ and KKT multipliers is Farkas' lemma for a finitely generated cone.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); indices are Fin m and Fin p; gradients are Mathlib's gradient.
The standing hypothesis is that every $h_i$ and $g_j$ is $C^1$ . Objectives in the characterizations are $C^1$ and are quantified inside the equivalence, for fixed constraints and fixed feasible $x^*$ .
KKT is the multiplier form with sign and complementarity. The paper's reading $-\nabla f(x^*)\in L_\Omega(x^*)^\circ$ is a milestone.
$\gamma$ is an extended real and $-\infty$ is its bottom element. The goal states AGP as AGP( $-\infty$ ). The paper's AGP is the $\gamma$ -independent condition of Martínez–Svaiter, which this paper does not prove; milestone 6 gives the forward direction for every $\gamma<0$ .
The normal cone is empty outside the set. A normal cone that is nonempty at infeasible points makes AGP-regularity a different, stronger condition. The projection is a predicate (a nearest point), not a choice function.
The outer limit is sequential, as in (1.6).
The paper says the inclusion (4.8) "always holds"; it is stated for $k$ large, which is what the proof uses. Definition 4.4's " $\Omega_L\times\mathbb R^m$ " is read as $\Omega_L\times\mathbb R^n$ .
A formalization with junk gradients (no $C^1$ hypothesis where the proof needs continuity), an objective quantified outside the equivalence, or KKT without sign or complementarity is ruled out by the statements above.

All objects are defined in the namespace StrictCQ.AGP. Proofs of the convex-analysis milestones are reusable beyond this mission.

Selected references

R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, Strict constraint qualifications and sequential optimality conditions for constrained optimization, Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018. https://doi.org/10.1287/moor.2017.0879
J. M. Martínez, B. F. Svaiter, A practical optimality condition without constraint qualifications for nonlinear programming, J. Optim. Theory Appl. 118:117–133, 2003. https://doi.org/10.1023/A:1023617925436
R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, A cone-continuity constraint qualification and algorithmic consequences, SIAM J. Optim. 26(1):96–110, 2016. https://doi.org/10.1137/15M1008488
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

11 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Shortest Paths in Graphs of Convex Sets II: For Compact 𝒳 the Set-Based Relaxation 𝒮′ of Z = xyᵀ Is Exact at Every Extreme Point of a Polytope 𝒴Research Paper

Motivation

The shortest-path problem in a graph of convex sets (SPP in GCS), introduced by Marcucci, Umenberger, Parrilo and Tedrake (arXiv:2101.11565, SIAM J. Optim. 2024), asks for a path through a directed graph whose vertices carry convex sets, together with a point in each visited set, minimizing a sum of convex edge lengths. It models motion planning around obstacles, hybrid-system control and other problems that mix a discrete choice with continuous positions. The paper formulates it as a mixed-integer convex program whose only nonconvexity, before relaxation, is a family of bilinear equalities $Z = xy^\top$ that couple the continuous positions $x$ with the flow variables $y$ .

Section 7 of the paper studies the convex relaxation used for these bilinear equalities in isolation. Products of valid inequalities linearized by $Z = xy^\top$ are the idea behind the McCormick envelope (McCormick 1976) and the Reformulation-Linearization Technique of Sherali and Adams. This mission formalizes the paper's result that the relaxation is exact at every extreme point of the polytope $\mathcal Y$ , which is the property that makes the mixed-integer formulation exact at binary flows.

Setting

Fix $\mathcal X \subseteq \mathbb R^n$ and $\mathcal Y \subseteq \mathbb R^m$ . Points of $\mathbb R^n\times\mathbb R^m\times\mathbb R^{n\times m}$ are written $(x, y, Z)$ .

The perspective of $\mathcal X$ (Definition 4.1) is $\tilde{\mathcal X} := \operatorname{cl}\{(x, \lambda) : \lambda \ge 0,\ x \in \lambda\mathcal X\} \subseteq \mathbb R^n \times \mathbb R$ .
The cone of valid inequalities (Definition 4.8) is $\mathcal X^\circ := \{(a, b) : a^\top x + b \ge 0 \text{ for all } x \in \mathcal X\}$ .
The dual cone of $\mathcal K \subseteq \mathbb R^n\times\mathbb R$ is $\mathcal K^* := \{(a, b) : a^\top x + b\lambda \ge 0 \text{ for all } (x, \lambda) \in \mathcal K\}$ .
The bilinear set (7.1) is $\mathcal S := \{(x, y, Z) : x \in \mathcal X,\ y \in \mathcal Y,\ Z = xy^\top\}$ .
The set-based relaxation (7.2) multiplies every valid inequality of $\mathcal X$ by every valid inequality of $\mathcal Y$ and replaces $xy^\top$ by $Z$ :

\mathcal S' := \{(x, y, Z) : a^\top Zc + d\,a^\top x + b\,c^\top y + bd \ge 0 \text{ for all } (a, b) \in \mathcal X^\circ,\ (c, d) \in \mathcal Y^\circ\}.

A polytope is a bounded set $\mathcal Y = \{y : c_i^\top y + d_i \ge 0 \text{ for all } i \in \mathcal I\}$ with $\mathcal I$ finite. Its asymmetric relaxation (7.3) is $\{(x, y, Z) : (Zc_i + d_i x,\ c_i^\top y + d_i) \in \tilde{\mathcal X} \text{ for all } i \in \mathcal I\}$ .

Always $\mathcal S \subseteq \mathcal S'$ , and $\mathcal S'$ is convex.

Formalization targets

Goal: Lemma 7.4 (p. 13)

Let $\mathcal X$ be compact and convex, let $\mathcal Y$ be a polytope and let $\hat y$ be an extreme point of $\mathcal Y$ . Then for all $x$ and $Z$ ,

(x, \hat y, Z) \in \mathcal S \iff (x, \hat y, Z) \in \mathcal S'.

Milestones

(7.2), p. 12: $\mathcal S \subseteq \mathcal S'$ for arbitrary sets.
The sentence after (7.2), p. 12: for closed convex $\mathcal X, \mathcal Y$ , every point of $\mathcal S'$ has $x \in \mathcal X$ and $y \in \mathcal Y$ .
Lemma 4.9, p. 6: for nonempty closed convex $\mathcal X$ , $(\tilde{\mathcal X})^* = \mathcal X^\circ$ and $(\mathcal X^\circ)^* = \tilde{\mathcal X}$ .
Proposition 7.1, inclusion $\subseteq$ , p. 12: $\mathcal S'$ is contained in the asymmetric relaxation (7.3), for every family of halfspaces.
Remark 4.2, p. 5: for compact convex $\mathcal X$ , $\tilde{\mathcal X} = \{(x, \lambda) : \lambda \ge 0,\ x \in \lambda\mathcal X\}$ , without closure.
Proof of Lemma 7.4, p. 13: at an extreme point of a polyhedron with finitely many inequalities, $m$ linearly independent inequalities are active.
Proposition 7.1, p. 12: $\mathcal S'$ equals (7.3), when the trivial inequality $1 \ge 0$ is a nonnegative combination of the defining inequalities.
Remark 7.5, p. 14: if $\mathcal Y \subseteq [0,1]^m$ , every point of $\mathcal Y \cap \{0,1\}^m$ is an extreme point of $\mathcal Y$ .
(7.4), p. 13: for compact convex $\mathcal X$ and $\mathcal Y = \operatorname{conv}\{\hat y_j\}_{j\in\mathcal J}$ , $\operatorname{conv}\mathcal S = \{\sum_j (x_j, \lambda_j\hat y_j, x_j\hat y_j^\top) : \sum_j \lambda_j = 1,\ (x_j, \lambda_j) \in \tilde{\mathcal X}\}$ .

Significance

The result. In the paper's mixed-integer program each vertex $v$ contributes a bilinear set $\mathcal S_v$ in which $\mathcal X$ is the convex set at $v$ and $\mathcal Y$ is the polytope of flows on the edges at $v$ . Binary flows corresponding to a path are extreme points of these polytopes, so Lemma 7.4 says that replacing $\mathcal S_v$ by $\mathcal S'_v$ loses nothing at the integer points of the program. This gives the paper's second, geometric proof that its mixed-integer convex formulation is exact (Theorem 5.7). By Remark 7.5 the lemma also extends a known property of the first-level Reformulation-Linearization Technique for bilinear programs with binary variables from polytopes $\mathcal X$ to compact convex sets $\mathcal X$ . Proposition 7.1 is what makes the relaxation finite: it replaces the infinitely many inequalities of $\mathcal S'$ by one perspective-cone constraint per facet of $\mathcal Y$ .

Formalizing it. The results are proved on paper; none of them has a machine-checked proof. The formalization also settles the exact hypotheses. Three statements of this section are false as printed (see Formalization scope), and the corrected versions are posed here with the counterexamples recorded. The perspective cone, the cone of valid inequalities and their duality (Lemma 4.9) are general convex-analysis facts that recur across conic and disjunctive programming.

Difficulty

The direction $\mathcal S \subseteq \mathcal S'$ is one line, since $(a^\top x + b)(c^\top y + d) \ge 0$ . The converse at $\hat y$ needs three ingredients that are each standard and none of which is in Mathlib in this form.

The duality between $\tilde{\mathcal X}$ and $\mathcal X^\circ$ is a bipolar theorem for the closed cone generated by $\mathcal X \times \{1\}$ , in the product $\mathbb R^n \times \mathbb R$ with the pairing $a^\top x + b\lambda$ . The cone needs care at $\lambda = 0$ .
The active-constraint characterization of extreme points of a polyhedron in halfspace form has to be proved directly.
The step " $(u, 0) \in \tilde{\mathcal X}$ implies $u = 0$ " is where boundedness enters. For unbounded $\mathcal X$ the slice $\lambda = 0$ of $\tilde{\mathcal X}$ is the recession cone, and the argument, and the lemma, fail.

Proposition 7.1 as an equality needs an affine Farkas lemma, and its printed proof skips the case of the valid inequality $(0, 1)$ .

Formalization scope

$\mathbb R^n$ is Fin n → ℝ, inner products are dotProduct, $Zc$ is Z *ᵥ c and $xy^\top$ is Matrix.vecMulVec x y. Triples are (x, y, Z) in (Fin n → ℝ) × (Fin m → ℝ) × Matrix (Fin n) (Fin m) ℝ. A polytope is given by a finite family (c i, d i) over a Fintype index and the hypothesis Bornology.IsBounded; extreme points are Mathlib's Set.extremePoints ℝ, never a predicate defined through active constraints. The dual cone uses the pairing $a^\top x + b\lambda$ on the product, not an inner product.

Hypotheses added relative to the page, each with a counterexample to the printed form:

Lemma 7.4 and (7.4): $\mathcal X$ compact. Section 7.1 only asks $\mathcal X$ to be closed and convex. For $\mathcal X = [0, \infty)$ , $\mathcal Y = [0, 1]$ and $\hat y = 0$ , the point $(1, 0, \tfrac12)$ is in $\mathcal S'$ but not in $\mathcal S$ . Compactness is the standing assumption of Section 2 on the sets $\mathcal X_v$ that $\mathcal X$ stands for.
Lemma 4.9: $\mathcal X$ nonempty. For $\mathcal X = \emptyset$ , $\tilde{\mathcal X} = \emptyset$ but $(\mathcal X^\circ)^* = \{0\}$ .
Proposition 7.1 (equality): $1 \ge 0$ is a nonnegative combination of the rows. For $\mathcal Y = \{0\}$ written as $\{y \ge 0, -y \ge 0\}$ and $\mathcal X = [0, 1]$ , the point $(5, 0, 0)$ satisfies (7.3) but not (7.2). The hypothesis holds for every polytope with an interior point and for the flow polytopes of the paper.

Several hypotheses are dropped where they are not needed, which strengthens the statements: nonemptiness of $\mathcal X$ throughout, and boundedness and finiteness in the inclusion of Proposition 7.1 and in the active-constraint milestone.

Trivializing formalizations ruled out: $\mathcal S'$ quantifies over all of $\mathcal X^\circ \times \mathcal Y^\circ$ and is not replaced by (7.3) in the goal; $\mathcal X$ is never allowed to be merely closed in the goal; the hypotheses of the goal are satisfiable ( $\mathcal X = \mathcal Y = [0,1]$ , $\hat y = 0$ is checked in Lean).

A complete development needs the bipolar theorem for closed convex cones in $\mathbb R^{n}\times\mathbb R$ , the closedness of the cone over a compact convex set, the active-constraint characterization of extreme points, and a finite affine Farkas lemma. All of these are reusable well beyond this mission and are welcome as separate contributions.

Selected references

T. Marcucci, J. Umenberger, P. A. Parrilo, R. Tedrake, Shortest Paths in Graphs of Convex Sets, SIAM J. Optim. 34(1), 2024. arXiv:2101.11565v5 (the version cited). https://arxiv.org/abs/2101.11565 , https://doi.org/10.1137/22M1523790
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Corollary 11.7.2, Theorem 14.1). https://doi.org/10.1515/9781400873173
G. P. McCormick, Computability of global solutions to factorable nonconvex programs: Part I — Convex underestimating problems, Math. Program. 10, 1976. https://doi.org/10.1007/BF01580665
H. D. Sherali, W. P. Adams, A Reformulation-Linearization Technique for Solving Discrete and Continuous Nonconvex Problems, Kluwer, 1999. https://doi.org/10.1007/978-1-4757-4388-3

12 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Strict Constraint Qualifications and Sequential Optimality Conditions for Constrained Optimization I: MFCQ or a Full Active-Gradient Cone Is the Weakest Strict CQ for Scaled-AKKTResearch Paper

Motivation

Practical algorithms for nonlinear programming do not stop at an exact Karush–Kuhn–Tucker (KKT) point; they stop when an approximate stationarity test passes. Sequential optimality conditions formalize what such tests certify: they are properties of a feasible point $x^*$ phrased through sequences $x^k \to x^*$ and multiplier estimates, and every local minimizer satisfies them without any constraint qualification. The question that links them back to classical theory is which conditions on the constraints guarantee that a point satisfying a sequential condition is in fact a KKT point. Andreani, Martínez, Ramos and Silva call these strict constraint qualifications and ask, for each sequential condition, for the weakest one.

For the Approximate KKT condition (AKKT) the answer, the Cone Continuity Property, was given by Andreani, Martínez, Ramos and Silva in 2016 (SIAM J. Optim. 26(1)). Section 2 of the present paper treats the Scaled-AKKT condition, which divides the stationarity residual by the size of the multipliers. This scaling appears in the stopping criteria of practical codes and in complexity analyses of nonlinear programming methods. Scaled-AKKT is weaker than AKKT, and the paper uses it as the first, self-contained example of the analysis it then carries out for AGP, CAKKT and SAKKT.

Setting

Fix $n, m, p \ge 0$ and continuously differentiable functions $h_1,\dots,h_m$ , $g_1,\dots,g_p : \mathbb R^n \to \mathbb R$ , where $\mathbb R^n$ carries the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . The feasible set is $\Omega = \{x : h_i(x) = 0,\ g_j(x) \le 0 \text{ for all } i, j\}$ , and $x^* \in \Omega$ is fixed. An index $j$ is active when $g_j(x^*) = 0$ .

For an objective $f$ , the point $x^*$ satisfies KKT if there are $\lambda \in \mathbb R^m$ and $\mu \in \mathbb R^p$ with $\mu \ge 0$ , $\mu_j = 0$ for inactive $j$ , and $\nabla f(x^*) + \sum_i \lambda_i \nabla h_i(x^*) + \sum_j \mu_j \nabla g_j(x^*) = 0$ .

Scaled-AKKT holds at $x^*$ for $f$ if there are sequences $x^k \to x^*$ , $\lambda^k \in \mathbb R^m$ and $\mu^k \in \mathbb R^p$ with $\mu^k \ge 0$ , such that $\min\{\mu^k_j, -g_j(x^k)\} \to 0$ for every $j$ , and

\lim_{k\to\infty} \max\{1, \|\lambda^k\|_\infty, \|\mu^k\|_\infty\}^{-1}\, \Big\|\nabla f(x^k) + \sum_{i=1}^m \lambda^k_i \nabla h_i(x^k) + \sum_{j=1}^p \mu^k_j \nabla g_j(x^k)\Big\| = 0,

where $\|\cdot\|_\infty$ is the supremum norm of a multiplier vector.

The Mangasarian–Fromovitz constraint qualification (MFCQ) holds at $x^*$ if $\nabla h_1(x^*),\dots,\nabla h_m(x^*)$ are linearly independent and some $d$ satisfies $\langle \nabla h_i(x^*), d\rangle = 0$ for all $i$ and $\langle \nabla g_j(x^*), d\rangle < 0$ for all active $j$ . The cone of active gradients is

K(x^*) = \Big\{\sum_{i=1}^m \lambda_i \nabla h_i(x^*) + \sum_{j:\,g_j(x^*)=0} \mu_j \nabla g_j(x^*) : \lambda \in \mathbb R^m,\ \mu_j \ge 0\Big\}.

Formalization targets

Goal: the weakest strict constraint qualification for Scaled-AKKT

For a $C^1$ constraint system and a feasible $x^*$ ,

\big(\text{MFCQ at } x^* \ \text{ or } \ K(x^*) = \mathbb R^n\big) \iff \forall f \in C^1:\ \big(\text{Scaled-AKKT at } x^* \text{ for } f\big) \Rightarrow \big(\text{KKT at } x^* \text{ for } f\big). \qquad (2.3)

The forward implication says that (2.3) is a strict constraint qualification for Scaled-AKKT; the backward implication says that every strict constraint qualification for Scaled-AKKT implies (2.3).

Milestones

If $K(x^*) = \mathbb R^n$ , then $x^*$ is a KKT point for every objective (p. 3).
Scaled-AKKT with a bounded multiplier set $\{\lambda^k, \mu^k\}$ implies KKT (p. 3).
Scaled-AKKT with an unbounded multiplier set yields $\lambda$ , $\mu \ge 0$ supported on the active set, with $\max\{\|\lambda\|_\infty, \|\mu\|_\infty\} = 1$ , solving $\sum_i \lambda_i \nabla h_i(x^*) + \sum_{j \text{ active}} \mu_j \nabla g_j(x^*) = 0$ , display (2.4) (pp. 3–4).
Such a normalized solution of (2.4) excludes MFCQ (p. 4).
Conversely, failure of MFCQ yields a normalized solution of (2.4) (p. 4).
Given a normalized solution of (2.4), Scaled-AKKT holds at $x^*$ for every linear objective $f(x) = \langle x, c\rangle$ (p. 4).

Significance

The result separates Scaled-AKKT sharply from AKKT. For AKKT the weakest strict constraint qualification (the Cone Continuity Property) is implied by many classical conditions, including CPLD and RCPLD. For Scaled-AKKT it is essentially MFCQ, a much stronger requirement. A stopping test of the Scaled-AKKT type therefore certifies a KKT point only under MFCQ, apart from the degenerate case of a full active cone. The other sections of the paper characterize the weakest strict constraint qualifications for AGP, CAKKT and SAKKT, using the same "iff over all objectives" template that this mission formalizes in its simplest form.

The paper's argument is a half-page sketch. A formalization makes explicit several points it leaves implicit: the role of the $1$ in the scaling factor, the vanishing of inactive multipliers forced by the complementarity limit, and the theorem of the alternative that converts failure of MFCQ into a nonzero solution of (2.4). None of these results is formalized on Prove2Me or, to our knowledge, in Mathlib.

Difficulty

The forward direction splits on whether the multipliers stay bounded, and the unbounded case requires normalizing by $\max\{1, \|\lambda^k\|_\infty, \|\mu^k\|_\infty\}$ and extracting a convergent subsequence. Along that subsequence one must check that the normalized multipliers have supremum norm exactly one, that the normalized objective gradient tends to zero, and that inactive multipliers tend to zero; only then does the limit contradict MFCQ. The backward direction needs a theorem of the alternative (Motzkin or Gordan type) for the active gradients, together with linear dependence of the equality gradients. The paper uses it without stating it. It also needs a vector $c$ with $-c \notin K(x^*)$ . The printed text chooses $c \notin K(x^*)$ , which has the wrong sign for the objective $\langle x, c\rangle$ ; milestone 6 is stated for every $c$ , so the sign issue does not propagate.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); the constraints are index families Fin m → E → ℝ and Fin p → E → ℝ; gradients are Mathlib's gradient. Multiplier vectors live in Fin m → ℝ and Fin p → ℝ, whose Mathlib norm is the supremum norm, while residuals use the Euclidean norm. Standing hypotheses: every $h_i$ , $g_j$ is $C^1$ (the paper's "continuous first-order derivatives"), every objective in the goal is $C^1$ , and $x^*$ is feasible. The objective is quantified inside the equivalence, so the left side of the goal depends on $h$ , $g$ , $x^*$ alone. "or" is inclusive. The cone condition is equality of the cone with all of $\mathbb R^n$ , not with its linear span. KKT carries both the sign condition $\mu \ge 0$ and complementarity. MFCQ is defined in its primal (direction) form; defining it as "no nonzero nonnegative null combination" would make milestones 4 and 5 hold by definition, and that reading is excluded. Milestone 2 omits the MFCQ hypothesis present in the paper's sentence because the bounded case does not use it.

A complete development needs subsequence extraction in finite-dimensional spaces, continuity of gradients of $C^1$ functions, and a theorem of the alternative for finitely many vectors. The last two are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, Strict constraint qualifications and sequential optimality conditions for constrained optimization, Optimization Online 5197 (2015); Mathematics of Operations Research 43(3), 2018. https://doi.org/10.1287/moor.2017.0879
R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, A cone-continuity constraint qualification and algorithmic consequences, SIAM Journal on Optimization 26(1), 2016. https://doi.org/10.1137/15M1008488
O. L. Mangasarian, S. Fromovitz, The Fritz John necessary optimality conditions in the presence of equality and inequality constraints, Journal of Mathematical Analysis and Applications 17, 1967. https://doi.org/10.1016/0022-247X(67)90163-1
R. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60(5), 2011. https://doi.org/10.1080/02331930903578700

9 thms3 active usersReviewed

Completed

Dynamic Programming Linear Optimization Operations Research+1·Captain: mikedeng1

On Solving Multistage Stochastic Programs with Coherent Risk Measures: The Inner-Approximation Policy's Nested Risk-Adjusted Cost Is at Most the Upper Bound yResearch Paper

Motivation

Multistage stochastic linear programs model decisions taken over time under uncertainty: reservoir releases in hydro-thermal scheduling, production and inventory plans, capacity expansion. Their standard solution method, stochastic dual dynamic programming (SDDP, Pereira and Pinto 1991), approximates each stage's cost-to-go function from below by cutting planes. This gives a lower bound on the optimal value and a candidate policy, but no guaranteed upper bound: in the risk-neutral case the policy's expected cost is estimated by Monte Carlo simulation.

Planners who are averse to risk replace the expectation in each stage by a coherent risk measure (Artzner, Delbaen, Eber and Heath 1999), nested stage by stage so that the resulting dynamic risk measure is time consistent (Ruszczyński and Shapiro 2006). Under such a nested objective, simulation no longer estimates the cost of a policy: the nested risk of a policy is not an average over sampled scenarios. Philpott, de Matos and Finardi (2013) address this by an inner approximation of the cost-to-go functions from above, built from convex combinations of finitely many points with known upper bounds. Their Proposition 5 shows that the optimal value $y$ of the resulting first-stage problem bounds the nested risk-adjusted cost of the policy defined by the inner approximation. This gives a deterministic upper bound that complements the SDDP lower bound, and they apply it to the Brazilian hydro-thermal system.

Setting

There are $T\ge2$ stages. The decision at stage $t$ is $x_t\in\mathbb R^n$ ; $A_t,E_t$ are $m\times n$ matrices and $c_t\in\mathbb R^n$ . Stage 1 is deterministic: $A_1x_1=b_1$ . For $t\ge2$ a random outcome $\omega_t$ ranges over a finite set $\Omega_t$ , independently of earlier stages, and enters through the right-hand side $b_t(\omega_t)$ . The feasible set of stage $t$ given the previous decision $x_{t-1}$ is

\mathcal X_t(\omega_t)=\{x_t\ge0:\ A_tx_t=b_t(\omega_t)-E_tx_{t-1}\}.

A coherent risk measure $\rho$ maps random costs $Z:\Omega\to\mathbb R$ to $\mathbb R$ and is subadditive, monotone ( $Z_1\le Z_2\Rightarrow\rho(Z_1)\le\rho(Z_2)$ ), positively homogeneous and translation equivariant ( $\rho(\lambda+Z)=\lambda+\rho(Z)$ ). Larger is worse: these are costs. Each stage $t\ge2$ carries a one-step coherent risk measure $\rho_t$ on random costs over $\Omega_t$ . It is extended to costs in $\mathbb R\cup\{+\infty\}$ by $\bar\rho_t(Z)=+\infty$ whenever some outcome has infinite cost.

For $s=2,\dots,T$ fix points $x^1_{s-1},\dots,x^{J_{s-1}}_{s-1}$ and numbers $q^1_s,\dots,q^{J_{s-1}}_s$ . The inner approximation is the lower boundary of the convex hull of the pairs $(x^j_{s-1},q^j_s)$ :

\hat{\mathcal Q}_s(x)=\min\Big\{\sum_j\lambda^jq^j_s:\ \sum_j\lambda^jx^j_{s-1}=x,\ \lambda\ge0,\ \sum_j\lambda^j=1\Big\},

which is $+\infty$ off the convex hull of the points, with $\hat{\mathcal Q}_{T+1}\equiv0$ . The policy's stage problem (13) and the first-stage problem (8) are

q_t(x_{t-1},\omega_t)=\min_{x_t\in\mathcal X_t(\omega_t)}c_t^\top x_t+\hat{\mathcal Q}_{t+1}(x_t),\qquad y=\min_{A_1x_1=b_1}c_1^\top x_1+\hat{\mathcal Q}_2(x_1).

The numbers $q^j_s$ are upper bounds when $q^j_s\ge\bar\rho_s\big(q_s(x^j_{s-1},\omega_s)\big)$ for all $s$ and $j$ . A policy defined by the inner approximation, $\hat\pi$ , takes at each state $x_{t-1}$ and outcome $\omega_t$ an action $\hat x_t(x_{t-1},\omega_t)$ solving (13), and a first-stage action $\hat x_1$ solving (8). The actual risk-adjusted cost of $\hat\pi$ over stages $t,\dots,T$ is

\hat v_t(x_{t-1},\omega_t)=c_t^\top\hat x_t+\bar\rho_{t+1}\big(\hat v_{t+1}(\hat x_t,\omega_{t+1})\big),

with no future term at $t=T$ . The nested risk-adjusted cost of the policy is $v(\hat\pi)=c_1^\top\hat x_1+\bar\rho_2(\hat v_2(\hat x_1,\omega_2))$ .

Formalization targets

Goal: Proposition 5

v(\hat\pi)\ \le\ y.

The bound holds for every $T\ge2$ , every family of coherent $\rho_t$ , every choice of points satisfying the upper-bound property, and every minimizing selection $\hat\pi$ .

Milestones

The convexity display of §2: subadditivity and positive homogeneity imply $\rho(\alpha Z_1+(1-\alpha)Z_2)\le\alpha\rho(Z_1)+(1-\alpha)\rho(Z_2)$ .
$\hat{\mathcal Q}_s$ is the lower boundary of the convex hull $\mathcal H$ of the pairs $(x^j_{s-1},q^j_s)$ (its epigraph is $\mathcal H$ plus the vertical half-line), hence convex with $\hat{\mathcal Q}_s(x^j_{s-1})\le q^j_s$ , and every convex function bounded by the $q^j_s$ at the points lies below $\hat{\mathcal Q}_s$ .
$q_t(\cdot,\omega_t)$ is convex in $x_{t-1}$ .
The interpolation bound $\bar\rho_t\big(q_t(x_{t-1},\omega_t)\big)\le\hat{\mathcal Q}_t(x_{t-1})$ .
The induction claim $\bar\rho_t\big(\hat v_t(x_{t-1},\omega_t)\big)\le\hat{\mathcal Q}_t(x_{t-1})$ for $t=2,\dots,T$ and every $x_{t-1}$ .

Companions

Proposition 3, the risk-neutral case $\rho_t=\mathbb E$ . Proposition 4, the subgradient rule $\sum_mp_m\tilde\zeta_mg(\tilde x,\omega_m)\in\partial_x\rho(Z(x,\omega))$ for $\rho$ given by its dual representation. The existence of a policy $\hat\pi$ , which shows that the hypotheses of the goal can be met.

Significance

Proposition 5 makes the inner approximation a certificate. Any policy computed by minimizing against $\hat{\mathcal Q}_{t+1}$ has nested risk-adjusted cost at most $y$ , a number obtained by solving one linear program. Together with the lower bound $z$ from outer approximation it brackets the risk-adjusted optimal value. The gap $y-z$ then measures the quality of a risk-averse SDDP policy without simulation, which the nested objective does not allow. The bound covers every coherent nesting used in practice, such as mixtures of expectation and CVaR.

The results are proved in the paper. None of them is machine-checked. A formalization adds a precise account of the infinite values the paper does not discuss: infeasible stages, points outside the convex hull, and the extension of $\rho_t$ to $+\infty$ . It also pins down the exact form of the upper-bound hypothesis the induction needs.

Difficulty

The obvious reading of the hypothesis on p. 16, " $q^j_{t+1}$ is an upper bound on $\rho_{t+1}(Q_{t+1}(x^j_t,\omega_{t+1}))$ " with the true value function $Q_{t+1}$ , does not support the induction. The policy $\hat\pi$ does not act optimally, so its cost can exceed the true value, and the inductive step compares $\hat v_t$ with the policy's own stage value $q_t$ , not with $Q_t$ . The hypothesis that works bounds the risk-adjusted optimal value of the policy's stage problem (13) at the points, which is what the paper's Upper Bound Computation actually computes.

The second difficulty is infinite values, which the paper never discusses. A risk measure is defined on real random costs, yet stage problems can be infeasible, $\hat{\mathcal Q}_s$ is $+\infty$ off a convex hull, and a convex combination may put zero weight on a point whose bound is $+\infty$ . Every inequality of the paper has to be re-read in $\mathbb R\cup\{+\infty\}$ , and the extended-real arithmetic must not silently produce a value the paper does not intend.

Formalization scope

Vectors are Fin n → ℝ, all stages share $n$ and $m$ , and costs that may be infinite are EReal. Minima are EReal infima, $+\infty$ on an empty set. Attainment of a minimum is never built into a definition: the policy is a selection with a minimizing property, required at every state where the stage problem is feasible. Stages are natural numbers. Points and bounds are indexed by the stage $s$ of the function $\hat{\mathcal Q}_s$ they define, so pts s j is $x^j_{s-1}$ and qv s j is $q^j_s$ . Stagewise independence is built in: $\omega_t$ ranges over $\Omega_t$ whatever happened before.

Standing assumptions made explicit in the statements:

$T\ge2$ ;
$\rho_t$ coherent for $t=2,\dots,T$ (all four axioms, though the proof uses only monotonicity and convexity);
the terminal convention $\rho_{T+1}(Q_{T+1})=0$ , so $\hat{\mathcal Q}_{T+1}\equiv0$ ;
(8) without the constraint $x_1\ge0$ , as printed;
the upper-bound hypothesis in the form above.

The risk measures $\rho_t$ act on real random costs and are extended by $\bar\rho_t(Z)=+\infty$ when some outcome has infinite cost. In Proposition 4, $\rho$ is given by its dual representation (10); the representation theorem itself is not part of the mission. The existence statement adds solvability of $A_1x_1=b_1$ and boundedness below of the last-stage program, without which (8) or the last stage has no solution.

The goal is not to be trivialized. Its hypotheses mention neither $\hat v_t$ nor the induction claim; the policy must minimize at every feasible state, not only along visited states; and the statement is for general $T$ and general coherent $\rho_t$ , not the expectation. The bound is trivially true when $y=+\infty$ and is informative when $\hat x_1$ lies in the convex hull of the stage-1 points.

A complete development needs:

convexity of extended-real linear-programming value functions in their right-hand side;
convexity of the convex-hull function $\hat{\mathcal Q}$ ;
finite Jensen-type inequalities for monotone convex risk measures;
linear-programming attainment, for the existence companion.

The first two are reusable for any SDDP-type development. Proofs of the milestones in any order are welcome.

Selected references

A. B. Philpott, V. L. de Matos, E. Finardi, On Solving Multistage Stochastic Programs with Coherent Risk Measures, Operations Research 61(4), 2013. https://doi.org/10.1287/opre.2013.1175
P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk, Mathematical Finance 9(3), 1999. https://doi.org/10.1111/1467-9965.00068
A. Ruszczyński, A. Shapiro, Conditional Risk Mappings, Mathematics of Operations Research 31(3), 2006. https://doi.org/10.1287/moor.1060.0204
M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52, 1991. https://doi.org/10.1007/BF01582895
A. Shapiro, Analysis of stochastic dual dynamic programming method, European Journal of Operational Research 209(1), 2011. https://doi.org/10.1016/j.ejor.2010.08.007

8 thms3 active usersReviewed

Completed

Convex Optimization Dynamic Programming Operations Research+1·Captain: mikedeng1

On the Convergence of Decomposition Methods for Multistage Stochastic Convex Programs 1: Deterministic Cutting-Plane Bellman Approximations Become Exact Along the Generated TrajectoriesResearch Paper

Motivation

Multistage stochastic programs model sequential decisions under uncertainty: hydro-thermal scheduling, inventory and capacity planning, portfolio management. The dominant solution methods, Stochastic Dual Dynamic Programming (SDDP, Pereira and Pinto 1991) and its relatives CUPPS and DOASA, never compute the Bellman (future-cost) functions of the problem. Instead they build outer approximations of them by cutting planes: affine minorants obtained from the optimal values and Lagrange multipliers of one-stage subproblems. Practitioners run these methods on very large problems, so the question of whether, and in what sense, the approximations converge is of direct practical relevance.

Earlier convergence proofs (Philpott and Guan 2008; Shapiro 2011) rely on linear stage problems, where only finitely many distinct cuts can be generated and convergence is finite. Girardeau, Leclère and Philpott (Math. Oper. Res. 2015) prove convergence for convex stage problems, where infinitely many distinct cuts may appear and finite termination is lost. This mission covers the first half of that paper: the deterministic multistage problem (§2), whose proof contains the whole scheme of the argument. The stochastic scenario-tree version is the companion mission of this series.

Setting

Fix a horizon $T\ge1$ . States lie in $\mathbb R^d$ and controls in $\mathbb R^p$ ; values are in $\overline{\mathbb R}=\mathbb R\cup\{\pm\infty\}$ . The data are state sets $\mathcal X_t\subseteq\mathbb R^d$ , control multifunctions $\mathcal U_t:\mathbb R^d\rightrightarrows\mathbb R^p$ , stage costs $C_t(x,u)\in\mathbb R\cup\{+\infty\}$ , linear dynamics $f_t(x,u)$ , a final cost $V_T$ and an initial state $x_0$ . The problem (1) is

\min_{x,u}\ \sum_{t=0}^{T-1}C_t(x_t,u_t)+V_T(x_T)\quad\text{s.t. } x_{t+1}=f_t(x_t,u_t),\ x_t\in\mathcal X_t,\ u_t\in\mathcal U_t(x_t).

The Bellman functions are $V_t(x)=\inf_{u\in\mathcal U_t(x)}W_t(x,u)$ on $\mathcal X_t$ and $+\infty$ elsewhere, with $W_t(x,u)=C_t(x,u)+V_{t+1}(f_t(x,u))$ .

Assumptions (H₁) require $\mathcal U_t$ to be a convex multifunction with convex compact values; $C_t$ and $V_T$ to be convex, lower semicontinuous and proper; and $V_T$ to be finite and Lipschitz on $\mathcal X_T$ . They also require extended relatively complete recourse (ERCR): for some $\delta_t>0$ , on the enlarged set $\mathcal X'_t=\mathcal X_t+B_t(\delta_t)$ (a $\delta_t$ -neighbourhood inside the affine hull of $\mathcal X_t$ ) the cost $C_t$ is finite and some admissible control leads into $\mathcal X_{t+1}$ .

The cutting-plane method keeps approximations $V^k_t$ , starting from $V^0_t\equiv-\infty$ and with $V^k_T=V_T$ . At iteration $k$ it runs forward from $x^k_0=x_0$ . At each stage it solves the one-stage problem with $V^{k-1}_{t+1}$ in place of $V_{t+1}$ , which gives a minimizer $u^k_t$ , the optimal value $\theta^k_t$ and a Lagrange multiplier $\beta^k_t$ of the constraint $x=x^k_t$ . It then adds the cut

V^k_t(x)=\max\big(V^{k-1}_t(x),\ \theta^k_t+\langle\beta^k_t,x-x^k_t\rangle\big)

and moves to $x^k_{t+1}=f_t(x^k_t,u^k_t)$ . The approximate cost-to-go is $W^k_t(x,u)=C_t(x,u)+V^k_{t+1}(f_t(x,u))$ .

Formalization targets

Goal: Theorem 2.1

For every run of the method and every $t=0,\dots,T-1$ ,

\lim_{k\to\infty}W_t(x^k_t,u^k_t)-V_t(x^k_t)=0\qquad\text{and}\qquad\lim_{k\to\infty}V_t(x^k_t)-V^k_t(x^k_t)=0.

The first limit says the computed decisions become optimal for the true Bellman functions; the second says the cuts become exact at the visited states. Nothing is claimed away from the generated trajectories.

Milestones

In the order the proof uses them:

Lemma 5.1 (marginal functions of convex problems over convex multifunctions are convex, and attained);
the tightness identity (10), $V^k_t(x^k_t)=\theta^k_t=W^{k-1}_t(x^k_t,u^k_t)$ ;
Lemma 2.2 (i)–(iii): $V_t$ convex and Lipschitz on $\mathcal X_t$ ; validity $V^k_t\le\tilde V_t\le V_t$ ; bounded multipliers;
Corollary 2.1 (one Lipschitz constant for all cuts);
Lemma 5.2 (monotone Lipschitz minorants on a compact set);
the two halves of the backward induction step of the proof of Theorem 2.1.

Companion items state that runs exist under (H₁) and give Kelley's cutting-plane lemma (Lemma 2.1), the warm-up result of §2.

Significance

Theorem 2.1 is a convergence guarantee for cutting-plane decomposition of nonlinear convex multistage problems. It does not depend on finitely many dual extreme points, so it covers problems with nonlinear convex costs and convex control constraints. The result is the template for the stochastic Theorem 3.1, which covers SDDP, CUPPS and DOASA as special cases of a general node-selection scheme. Along the way the paper isolates ERCR, a constraint qualification that is exactly what bounds the Lagrange multipliers and makes the cuts uniformly Lipschitz.

The result is proved in the paper; as far as is known it has no machine-checked proof. This mission produces a Lean statement of the deterministic algorithm, with extended-real Bellman functions, cut validity, and multiplier selection as a predicate on runs. It also supplies the statements of the reusable lemmas: marginal-function convexity, the monotone-minorant lemma, Kelley's method. Formal proofs of the milestones, alternative arguments, and explicit Lipschitz constants are all open.

Difficulty

The naive argument, "the approximations increase and are bounded by $V_t$ , so they converge", only gives pointwise convergence of $V^k_t$ to some limit below $V_t$ . It does not show that the limit equals $V_t$ at the states actually visited, and the visited states change from iteration to iteration. The proof must control cuts computed at one state when they are evaluated at another. This needs a uniform bound on the multipliers $\beta^k_t$ . That bound comes from ERCR (moving a distance $\delta_t/2$ in every direction of the affine hull stays where the cost is finite), together with Lipschitz continuity of $V_t$ on a compact set lying inside the relative interior of its domain. Without ERCR the multipliers can be unbounded and the argument breaks. A second difficulty is the backward induction itself: the conclusion at stage $t$ uses both limits at stage $t+1$ , and passing from $V^k_{t+1}$ to $V^{k-1}_{t+1}$ needs a compactness argument (Lemma 5.2).

Formalization scope

States are EuclideanSpace ℝ (Fin d) and controls EuclideanSpace ℝ (Fin p); costs and value functions are EReal-valued. Convexity of an extended-real function means convexity of its epigraph. Minima are EReal infima ( $+\infty$ over an empty set), with attainment stated separately. $V_T$ is extended by $+\infty$ outside $\mathcal X_T$ .

The Lagrange multiplier condition is encoded by (12): $\beta^k_t$ lies in the direction space of $\operatorname{Aff}(\mathcal X_t)$ and is a subgradient, on $\operatorname{Aff}(\mathcal X_t)$ , of the stage optimal value at $x^k_t$ . A run is a predicate on $(x,u,\theta,\beta)$ : any minimizer and any multiplier are allowed. The paper's iteration $k\ge1$ is Lean's k + 1.

Standing assumptions added to (H₁), all used by the paper's proofs:

$T>0$ ;
every $\mathcal X_t$ ( $t\le T$ ) is convex and compact (the paper uses this on pp. 5, 8 and 11 and states it as (H₂)(1) in §3);
$x_0\in\mathcal X_0$ .

Deviations from the page:

Lemma 5.1 is stated for a jointly convex $J(x,u)$ , the form its proof and its use need.
Lemma 2.2 (ii) states $V^k_t\le\tilde V_t$ on $\operatorname{Aff}(\mathcal X_t)$ . The printed "everywhere" fails outside the affine hull when that hull is a proper subspace.
Corollary 2.1 is stated wherever $V^k_t$ is finite, because $V^k_t\equiv-\infty$ during the first $T-1-t$ iterations.

Limits are Tendsto … (𝓝 0) in EReal. There, convergence to $0$ forces the differences to be eventually finite, so a value of $\pm\infty$ cannot make a limit hold for free. The goal's hypotheses are exactly (H₁) and the run predicate. Statements that only assert the existence of a good run, or bound $\theta^k_t$ instead of the cuts, are not formalizations of Theorem 2.1.

A complete development needs:

Lipschitz continuity of a convex function on a compact subset of the relative interior of its domain;
the existence of subgradients relative to an affine subspace;
marginal-function convexity for extended-real functions.

All three are reusable well beyond this mission. Proofs of any milestone are welcome, as are proofs of the companion items.

Selected references

P. Girardeau, V. Leclère, A. B. Philpott, On the Convergence of Decomposition Methods for Multistage Stochastic Convex Programs, Mathematics of Operations Research 40(1), 2015; author's version hal-01208295v1. https://doi.org/10.1287/moor.2014.0664, https://hal.science/hal-01208295
M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52, 1991. https://doi.org/10.1007/BF01582895
A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Operations Research Letters 36(4), 2008. https://doi.org/10.1016/j.orl.2008.01.013
A. Shapiro, Analysis of stochastic dual dynamic programming method, European Journal of Operational Research 209(1), 2011. https://doi.org/10.1016/j.ejor.2010.08.007
J. E. Kelley, The cutting-plane method for solving convex programs, Journal of the SIAM 8(4), 1960. https://doi.org/10.1137/0108053

12 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Product Price, Quality and Service Decisions under Consumer Choice Models VI: Consumer Surplus Rises as the Firm Also Controls Service Duration, and Again as It Also Controls QualityResearch Paper

Who gains when a firm controls more decisions

A firm that sells differentiated products sets more than prices. It chooses quality levels (features, materials, reliability) and the ancillary services that come free with a product, such as a factory warranty or free maintenance for a fixed period. Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study the joint choice of price, quality and service duration when consumers choose according to the multinomial logit (MNL) model.

A firm allowed to make more decisions can never earn less: it may always ignore the extra instruments. The question this mission formalizes is what happens to consumers. A natural guess is that every new instrument lets the firm extract more of the consumers' surplus. Section 2.3 of the paper (Proposition 5) shows that under MNL demand this guess is wrong: consumer surplus also rises, so more control is a "win–win". The welfare measure is the logit consumer surplus of Anderson, de Palma and Thisse (Discrete Choice Theory of Product Differentiation, MIT Press, 1992).

The mission is the sixth of a series on the paper; each mission defines its own copy of the model in its own namespace.

Setting

There are $N$ products $i\in\mathcal N=\{1,\dots,N\}$ . Product $i$ has a price $p_i$ , a quality level $q_i$ and a service duration $t_i$ , which must lie in a fixed interval $[t_s,t_l]$ . The parameters are: $\alpha_i$ , the consumers' sensitivity to quality; $s_i$ , the utility of one unit of service time; $c_i>0$ , so that producing one unit at quality $q_i$ costs $c_iq_i^2$ ; and $a_i,b_i$ , so that service costs $a_i-b_iq_i$ per unit of time. The sign of $b_i$ is free: higher quality may make service cheaper ( $b_i>0$ ), dearer ( $b_i<0$ ), or leave it unchanged ( $b_i=0$ ).

A consumer buys product $i$ with the MNL choice probability

d_i(\mathbf p,\mathbf q,\mathbf t;\mathcal N)=\frac{\exp(\alpha_iq_i-p_i+t_is_i)}{1+\sum_{j\in\mathcal N}\exp(\alpha_jq_j-p_j+t_js_j)},

where the $1$ is the outside option of buying nothing. With market size one, the firm's profit is

\Pi(\mathbf p,\mathbf q,\mathbf t;\mathcal N)=\sum_{i\in\mathcal N}\big[p_i-c_iq_i^2-t_i(a_i-b_iq_i)\big]\,d_i(\mathbf p,\mathbf q,\mathbf t;\mathcal N),

and the bracket is the markup of product $i$ . Consumer surplus is

\mathrm{CS}(\mathbf p,\mathbf q,\mathbf t)=\log\Big(1+\sum_{i\in\mathcal N}\exp(\alpha_iq_i-p_i+t_is_i)\Big).

Three problems are compared, at the same pre-determined qualities $\mathbf q$ and durations $\mathbf t\in[t_s,t_l]^N$ :

price only: maximize $\Pi(\cdot,\mathbf q,\mathbf t)$ over $\mathbf p\in\mathbb R^N$ , with a maximizer $\mathbf p^\dagger$ ;
price and service: maximize $\Pi(\cdot,\mathbf q,\cdot)$ over $\mathbf p\in\mathbb R^N$ and $\mathbf t'\in[t_s,t_l]^N$ , with a maximizer $(\mathbf p^\ddagger,\mathbf t^\ddagger)$ ;
price, quality and service, problem (4): maximize $\Pi$ over all three, with a maximizer $(\mathbf p^*,\mathbf q^*,\mathbf t^*)$ .

Section 5.1 adds the manufacturer's short-term problem (10): qualities are fixed, and the firm also chooses which products $S\subseteq\mathcal N$ to offer.

Formalization targets

Goal: Proposition 5 (p. 13)

For every maximizer of each of the three problems,

\mathrm{CS}(\mathbf p^\dagger,\mathbf q,\mathbf t)\;\le\;\mathrm{CS}(\mathbf p^\ddagger,\mathbf q,\mathbf t^\ddagger)\;\le\;\mathrm{CS}(\mathbf p^*,\mathbf q^*,\mathbf t^*).

The inequalities are weak; equality holds, for instance, when the pre-determined $\mathbf q,\mathbf t$ are already optimal.

Milestones

Equation (17) (p. 26). For fixed $\mathbf q,\mathbf t$ , the equation $r=\sum_i\exp(\alpha_iq_i-c_iq_i^2+t_i(s_i-(a_i-b_iq_i))-r-1)$ has a unique root $r^\dagger$ ; a price vector is optimal if and only if every markup equals $1+r^\dagger$ ; the optimal profit is $r^\dagger$ .
Proposition 8 (p. 21). In problem (10) all products should be offered, an optimum uses durations $t_s$ or $t_l$ according to the sign of $b_i$ and the position of $q_i$ , every optimal markup is $1+r^*$ , and $r^*$ is the unique root of the corresponding equation.
Consumer surplus at an optimum (Online Supplement p. 1). If every markup is $1+r$ and the profit is $r$ , then $\mathrm{CS}=\log(1+r)$ .
Ordering of profits (Online Supplement p. 2): $r^\dagger\le r^\ddagger\le r^*$ .

Significance

The result separates two effects that are usually conflated. More instruments raise profit; Proposition 5 says that under MNL demand the extra profit comes from serving more consumers (fewer choose the outside option), not from extracting more surplus from each. Proposition 8 states the corresponding structure for a firm whose product designs are already fixed: offer everything, use extreme service durations, and keep markups equal across products.

The paper proves these results; none is formalized. A machine-checked development produces the welfare comparison together with the price step of the MNL multi-product pricing problem (equal markups at every optimum, uniqueness of the optimal profit as a fixed point) as reusable statements, and pins down the boundary cases of Proposition 8 that the printed statement leaves implicit.

Difficulty

The ordering of profits is immediate from the nesting of feasible sets. The obstacle is translating it into consumer surplus: consumer surplus is not monotone in profit along arbitrary price vectors, and the argument needs that at every maximizer of each problem all markups are equal to $1+r$ , with $r$ the optimal profit. That requires a global optimality analysis of the multi-product MNL pricing problem: the profit is not concave in prices, and both the uniqueness of the fixed point and the characterization of all maximizers (not only a stationary point) must be established. Comparing values $\log(1+r)$ with $r$ defined as the optimal profit, without linking them to the maximizers, proves nothing about consumer surplus.

Formalization scope

Products are Fin N (0-based); $N$ is arbitrary and $N=0$ is allowed. The outside option is the $1$ in the denominator, not a product.
Parameters $\alpha,a,b,c,s:\mathrm{Fin}\,N\to\mathbb R$ ; only $c_i>0$ and $t_s\le t_l$ are assumed throughout. No sign is imposed on $b_i$ , $\alpha_i$ , $a_i$ or $s_i$ , and products are not assumed identical.
Qualities range over $\mathbb R$ , not the model's normalized range $[0,a_i/b_i)$ , because the paper's joint optimum is computed over unconstrained qualities. Proposition 8(b) adds the model's bound $q_i\le a_i/b_i$ for $b_i>0$ , without which the printed rule can fail.
"Optimal" means a global maximizer over the stated feasible set. The goal quantifies over all maximizers of the three problems; their existence is not part of Proposition 5.
The MNL formula and the log-sum consumer surplus are definitions; their derivation from Gumbel random utilities is cited, not formalized.
Problem (10) is printed with $\Pi(\mathbf p,\mathbf q,\mathbf t;\mathcal N)$ ; the profit of the offer set $S$ is meant and is what is formalized.

A formalization in which the maximizers are given by the paper's closed-form prices, in which $r^\dagger,r^\ddagger,r^*$ are defined as optimal values and only $\log(1+r)$ is compared, or in which there is a single product, would make the goal trivial or different and is ruled out.

Contributions are welcome on the MNL price step (equation (17)), which is reusable for any multi-product logit pricing model, and on the per-product separation of the duration choice in Proposition 8.

Selected references

R. Wang, C. Ke, S. Cui, Product Price, Quality and Service Decisions under Consumer Choice Models, Manufacturing & Service Operations Management, 2022; accepted manuscript SSRN 3766191. https://ssrn.com/abstract=3766191, https://doi.org/10.1287/msom.2020.0947
S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992, ISBN 978-0-262-01128-0.
D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, 1974, 105–142. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf

9 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Product Price, Quality and Service Decisions under Consumer Choice Models II: The Oligopoly Has a Unique Nash Equilibrium, with Monopoly Qualities and Service Durations and Lower PricesResearch Paper

Motivation

Firms that sell durable goods set three things at once: a price, a quality level, and the length of an ancillary service that comes free with the product, such as a warranty. Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study these joint decisions under multinomial logit (MNL) demand. For a monopolist offering several products they show (their Theorem 1) that each service duration is extreme (the shortest or the longest allowed), each quality is set product by product, and all markups are equal.

A natural question is whether that structure survives competition. In practice, quality and warranty terms are long-term strategic choices while prices react to rivals; if competition changed the optimal qualities and durations, the monopoly analysis would say little about real markets. Section 2.4 of the paper answers the question for an oligopoly of $N$ single-product firms. This mission formalizes that answer, Theorem 2.

Setting

There are $N$ firms; firm $i \in \mathcal N = \{1, \dots, N\}$ sells product $i$ . Product $i$ has a quality sensitivity $\alpha_i$ , a base service cost per unit time $a_i$ , a marginal effect $b_i$ of quality on service cost (of either sign, or zero), a production-cost coefficient $c_i > 0$ (cost $c_i q_i^2$ ), and a service utility per unit time $s_i$ . Firm $i$ chooses a price $p_i$ , a quality $q_i$ and a service duration $t_i \in [t_s, t_l]$ .

A consumer buys product $i$ with the MNL choice probability

d_i(\mathbf p, \mathbf q, \mathbf t; \mathcal N) = \frac{\exp(\alpha_i q_i - p_i + t_i s_i)}{1 + \sum_{j \in \mathcal N} \exp(\alpha_j q_j - p_j + t_j s_j)},

where the $1$ is the outside (no-purchase) option. The payoff of firm $i$ is its markup times its market share:

\Pi_i(\mathbf p, \mathbf q, \mathbf t; \mathcal N) = \big[p_i - c_i q_i^2 - t_i(a_i - b_i q_i)\big]\, d_i(\mathbf p, \mathbf q, \mathbf t; \mathcal N).

A Nash equilibrium is a profile $(\mathbf p, \mathbf q, \mathbf t)$ with every $t_i \in [t_s, t_l]$ such that no firm can raise $\Pi_i$ by changing its own triple $(p_i, q_i, t_i)$ , jointly, to any other triple with duration in $[t_s, t_l]$ . The monopolistic case is problem (4): one firm maximizes $\sum_i \Pi_i$ over all prices and qualities in $\mathbb R^N$ and durations in $[t_s, t_l]^N$ . Finally, the duration index of product $i$ is

\varphi_i(t) = \frac{b_i^2 t^2}{4 c_i} + \Big(s_i - a_i + \frac{\alpha_i b_i}{2 c_i}\Big) t .

Formalization targets

Goal: Theorem 2

Assume $c_i > 0$ for all $i$ , $t_s < t_l$ , and $\varphi_i(t_s) \ne \varphi_i(t_l)$ for all $i$ . Then

\exists!\, (\mathbf p^o, \mathbf q^o, \mathbf t^o) \text{ Nash equilibrium}, \qquad \mathbf t^o = \mathbf t^*,\quad \mathbf q^o = \mathbf q^*,\quad p_i^o \le p_i^* \ (i \in \mathcal N)

for every optimal solution $(\mathbf p^*, \mathbf q^*, \mathbf t^*)$ of the monopolist's problem, which exists. The goal compares with any monopoly optimum and does not presuppose the monopoly formulas of Theorem 1.

Milestones

The proof in the Online Supplement (pp. 2–3) passes through the following statements, which are the mission's milestones:

(EC.1): a firm's profit is the unique root $r_i$ of $r_i(1 + \sum_{j \ne i} e^{\cdot}) = [\text{markup}_i - r_i]\, e^{\alpha_i q_i - p_i + t_i s_i}$ ;
(EC.2): $p_i \mapsto [\text{markup}_i - r_i]\, e^{\alpha_i q_i - p_i + t_i s_i}$ is unimodal with peak at markup $r_i + 1$ ;
(EC.3): in every equilibrium $q_i = (\alpha_i + t_i b_i)/(2c_i)$ and $t_i$ maximizes $\varphi_i$ on $[t_s, t_l]$ ;
the price root $\varphi_i(A)$ of the first-order condition exists, is unique, and decreases in the aggregate $A$ ;
the aggregate equation has a unique root $A^o$ , and the price competition has the unique equilibrium $p_i^o = \varphi_i(A^o)$ ;
$\varphi_i(A) \le A + k_i$ when $A$ exceeds firm $i$ 's attraction by at least one;
$A^o \ge m^*$ , the root of $m = 1 + \sum_i \exp(\alpha_i q_i - c_i q_i^2 - t_i(a_i - b_i q_i - s_i) - m)$ ;
$p_i^o = \varphi_i(A^o) \le m^* + c_i q_i^2 + t_i(a_i - b_i q_i)$ .

Significance

The result. Theorem 2 says that the quality and service rules of the monopoly are robust to competition: each firm sets quality where marginal consumer utility equals marginal cost, and offers the shortest or the longest service, regardless of what its rivals do. Only prices respond to competition, and they fall. The proof also shows that the competitive aggregate $A^o$ exceeds the monopolist's, so more consumers buy and consumer surplus $\log A^o$ is higher than under monopoly. Uniqueness makes comparative statics well defined.

Formalizing it. The theorem is proved in the paper and, to our knowledge, not formalized anywhere. A formal proof requires the MNL price-competition equilibrium argument (existence and uniqueness through a one-dimensional aggregate), which is a standard tool in operations management and industrial organization (Anderson, de Palma and Thisse 1992) and has independent reuse value. Making the argument precise also exposes two points the paper leaves implicit: the tie case in the duration choice, and the domain on which the bound $\varphi_i(A) \le A + k_i$ holds.

Difficulty

The game is not concave: $\Pi_i$ is not concave in firm $i$ 's own strategy $(p_i, q_i, t_i)$ (its best attainable value is convex in the duration $t_i$ , which is why durations end up extreme), and strategies are unbounded in price and quality, so the standard existence theorems for concave games with compact strategy sets do not apply. Writing down the first-order conditions and solving them produces candidates, but it shows neither that a candidate is a global best response nor that no other equilibrium exists. Uniqueness also fails without the no-indifference condition (see below).

Formalization scope

Products are indexed by Fin N (0-based); $N$ is arbitrary. The outside option is the 1 + in the denominator, not an element of Fin N.
Prices and qualities are unconstrained reals. The paper's normalization $q_i \in [0, a_i/b_i)$ (p. 8) is not imposed, because Theorem 1's quality formula and the proof ignore it. Durations lie in $[t_s, t_l]$ for equilibrium profiles, deviations and the monopoly problem alike.
A Nash equilibrium is defined through the published general pure-strategy Nash equilibrium notion (CarbonDoubleCount.Planner.IsPureNash) with Function.update: deviations are unilateral and joint in $(p_i, q_i, t_i)$ , not coordinate by coordinate.
Optimality in the monopoly problem means global maximality over the feasible set, never a first-order condition.
Added hypothesis. $\varphi_i(t_s) \ne \varphi_i(t_l)$ for every $i$ . If $\varphi_i(t_s) = \varphi_i(t_l)$ , firm $i$ has two best responses giving it the same profit and the same attraction, hence the same payoffs to all rivals; both are equilibria and "unique" is false. The paper's proof picks one endpoint "depending on the comparison" and does not treat ties.
"Lower prices" is stated as $p_i^o \le p_i^*$ , as the paper's proof concludes; for $N = 1$ the two problems coincide.
The price root $\varphi_i(A)$ is defined on the region $p > k_i$ , $\exp(w_i - p) < A$ where the first-order condition is increasing in $p$ ; it takes Lean's junk value only for $A \le 0$ , where no statement uses it.

Formalizations that do not count: a price-only game with qualities and durations fixed at the monopoly values (that is the paper's reduction, not the theorem); a two-firm version; an equilibrium notion checked one coordinate at a time; or an equilibrium assumed rather than proved to exist.

A complete development needs real analysis of one-variable functions (monotonicity, the intermediate value theorem, maximization of $x e^{-x}$ -type functions) and finite sums. The pure-Nash definition and the MNL price-competition milestones (4–8) are reusable beyond this paper. Proofs of any milestone, and alternative arguments for the price-equilibrium uniqueness, are welcome.

Selected references

Y. Wang, J. Ke, Y. Cui, Product Price, Quality and Service Decisions under Consumer Choice Models, Manufacturing & Service Operations Management, 2022; accepted manuscript SSRN 3766191. https://ssrn.com/abstract=3766191, https://doi.org/10.1287/msom.2020.0947
S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992. https://doi.org/10.7551/mitpress/2450.001.0001
D. McFadden, Conditional logit analysis of qualitative choice behavior, in Frontiers in Econometrics, Academic Press, 1974.

13 thms3 active usersReviewed

All missions

A Soft Robust Model for Optimization Under Ambiguity: For Every δ > 0, Soft Robust Feasibility Is a Convex Risk Measure Constraint, and Every Normalized Convex Risk Measure Arises This WayResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.1 for δ>0\delta>0δ>0

Milestones: the steps of the proof (p. 1224)

Significance

Difficulty

Formalization scope

Selected references

Continuum Hypothesis: Independence from ZFCTextbook

Motivation

Setting

Formalization targets

Goal: independence of CH from ZFC

Milestones

Significance

Difficulty

Formalization scope

Selected references

Class Number Formula: Continuation of the Dedekind Zeta Function and Dirichlet's FormulaTextbook

Motivation

Setting

Formalization targets

Goal: the class number formula

Milestones

Significance

Difficulty

Formalization scope

Selected references

Ramanujan–Petersson Conjecture (Wikipedia): Coefficient Bounds for Holomorphic Cusp FormsTextbook

Motivation

Setting

Formalization targets

Goal: the Ramanujan–Petersson conjecture for holomorphic cusp forms

The tau function

The Ramanujan LLL-function

Significance

Difficulty

Formalization scope

Selected references

Actuarial Mathematics XC: Structural Corporate Default and Rating-Migration Credit ValuationTextbook

Motivation

Setting

Formalization targets

Merton limited liability and terminal default payoffs

Finite default risk premiums and risk-neutral debt pricing

Three-state rating migration and recoverable default claims

Capstone theorem

Significance

Difficulty

Formalization scope

Selected references

Actuarial Mathematics LXXXIX: Expected Utility, Certainty Equivalents and Stochastic Risk OrdersTextbook

Motivation

Setting

Formalization targets

Expected exponential utility and absolute risk aversion

Actuarial insurance certainty equivalents and premium indifference

Genuine pathwise coupling and finite first-order stochastic dominance

Capstone theorem

Significance

Difficulty

Formalization scope

Selected references

Actuarial Mathematics XCI: Joint-Life Mortality Profit and Contingent Survivor BenefitsTextbook

Motivation

Setting

Formalization targets

Independent joint-life outcomes and probabilities

Outcome-dependent reserves, benefits and death strain

Joint mortality profit and limited-contingent survivor benefits

Capstone theorem

Significance

Difficulty

Formalization scope

Selected references

Actuarial Mathematics LXXVII: Compound Aggregate Masses and the Full Finite Panjer RecursionTextbook

Motivation

Goal: Theorem 2.1 for $\delta>0$

The Ramanujan $L$ -function