Analysis

Partial Differential Equations Probability·Captain: Lucas

Hairer: A Theory of Regularity Structures I — The Reconstruction TheoremResearch Paper

Motivation

Several equations of mathematical physics are written down formally but have no classical meaning as stated. The dynamical $\Phi^4_3$ model $\partial_t u = \Delta u - u^3 + \xi$ on the three-dimensional torus, the KPZ equation $\partial_t h = \partial_x^2 h + (\partial_x h)^2 - \infty + \xi$ , and the parabolic Anderson model $\partial_t u = \Delta u + u\,\xi$ all require multiplying a distribution of negative regularity by itself, an operation that Schwartz distribution theory does not provide. Martin Hairer's A theory of regularity structures (Invent. Math. 198 (2014) 269–504, arXiv:1303.5113) develops a calculus in which such products, and the resulting fixed-point problems, become well posed.

The line of work leading to it is short and well documented: rough path theory (Lyons, 1998) solved the analogous problem for controlled ordinary differential equations driven by irregular signals; Gubinelli's controlled paths (2004) and branched rough paths (2010) reorganised it around local expansions; Hairer's theory extends that idea from paths to fields on $\mathbb{R}^d$ with anisotropic (e.g. parabolic) scaling. Paracontrolled distributions (Gubinelli–Imkeller–Perkowski, 2015) give an alternative route to some of the same equations. The algebraic and probabilistic infrastructure around regularity structures has since been systematised (Bruned–Hairer–Zambotti, 2019; Chandra–Hairer, 2016), but the analytic core is still the 2014 paper.

Setting

Fix a dimension $d$ and a scaling $s = (s_1,\dots,s_d)$ of positive integers, with $|s| = \sum_i s_i$ , and put $\|x\|_s = \max_i |x_i|^{1/s_i}$ . For $\delta > 0$ , a point $x \in \mathbb{R}^d$ and a test function $\varphi$ , the rescaled test function is

(S^{\delta}_{s,x}\varphi)(y) = \delta^{-|s|}\,\varphi\!\left(\frac{y_1-x_1}{\delta^{s_1}},\dots,\frac{y_d-x_d}{\delta^{s_d}}\right).

Write $\mathcal{B}^r_{s,0}$ for the set of test functions supported in $\{\|y\|_s \le 1\}$ whose derivatives up to order $r$ are bounded by $1$ . For $\alpha<0$ , a distribution $\xi$ belongs to the Hölder–Besov space $\mathcal{C}^\alpha_s$ if, on every compact set $K$ , $|\langle \xi, S^{\delta}_{s,x}\eta\rangle| \le C\delta^{\alpha}$ uniformly over $x\in K$ , $\delta \in (0,1]$ and $\eta \in \mathcal{B}^r_{s,0}$ with $r=-\lfloor\alpha\rfloor$ .

A regularity structure $(A,T,G)$ consists of an index set $A \subseteq \mathbb{R}$ containing $0$ , bounded below and locally finite; a graded vector space $T = \bigoplus_{\alpha\in A} T_\alpha$ with $T_0 \cong \mathbb{R}$ spanned by a unit $\mathbf{1}$ ; and a group $G$ of linear operators on $T$ with $\Gamma a - a \in \bigoplus_{\beta<\alpha}T_\beta$ for $a \in T_\alpha$ , and $\Gamma\mathbf{1} = \mathbf{1}$ . Elements of $T_\alpha$ are "homogeneous of order $\alpha$ ": they are placeholders for objects whose size at scale $\varepsilon$ is $\varepsilon^{\alpha}$ .

A model $(\Pi,\Gamma)$ assigns to each point $x$ a linear map $\Pi_x : T \to \mathcal{D}'(\mathbb{R}^d)$ and to each pair $(x,y)$ an element $\Gamma_{xy}\in G$ , subject to $\Gamma_{xx}=\mathrm{id}$ , $\Gamma_{xy}\Gamma_{yz}=\Gamma_{xz}$ , $\Pi_y = \Pi_x\circ\Gamma_{xy}$ and, locally uniformly, the analytic bounds

|(\Pi_x a)(S^{\delta}_{s,x}\varphi)| \lesssim \|a\|_\ell\,\delta^{\ell}, \qquad \|\Gamma_{xy}a\|_m \lesssim \|a\|_\ell\,\|x-y\|_s^{\ell-m}, \qquad a \in T_\ell,\; m<\ell.

A modelled distribution of order $\gamma$ is a function $f : \mathbb{R}^d \to T_{<\gamma}$ such that on every compact $K$

|||f|||_{\gamma;K} = \sup_{x\in K,\ \beta<\gamma}\|f(x)\|_\beta + \sup_{\substack{x,y \in K,\ \|x-y\|_s\le 1 \\ \beta<\gamma}} \frac{\|f(x)-\Gamma_{xy}f(y)\|_\beta}{\|x-y\|_s^{\gamma-\beta}} < \infty;

the space of these is $\mathcal{D}^\gamma$ , and $\mathcal{D}^\gamma(V)$ if $f$ takes values in a sector $V$ , that is, a graded $G$ -invariant subspace vanishing in degrees below its regularity.

Formalization targets

Goal — reconstruction theorem, Theorem 3.10 for $\gamma>0$

With $\alpha = \min A < 0$ and $r$ the order attached to $A$ , for every $f \in \mathcal{D}^\gamma$ with $\gamma>0$ there is a unique distribution $\mathcal{R}f \in \mathcal{C}^\alpha_s$ with

\big|(\mathcal{R}f - \Pi_x f(x))(S^{\delta}_{s,x}\eta)\big| \lesssim \delta^{\gamma} \qquad (x \in K,\ \delta\in(0,1],\ \eta\in\mathcal{B}^r_{s,0}).

The statement asserts only the shape of the estimate — a constant per compact set — and so is insensitive to any later sharpening of constants.

Milestone level — the calculus around the reconstruction operator

The uniqueness clause of Theorem 3.10 in isolation; the existence of a linear reconstruction operator for arbitrary $\gamma \in \mathbb{R}$ (for $\gamma\le 0$ the bound no longer pins it down); Corollary 3.16, improving the regularity of $\mathcal{R}f$ to $\mathcal{C}^\beta_s$ when $f$ takes values in a sector of regularity $\beta$ ; Proposition 3.31, that for $\nu>0$ the action of $\Pi$ on $T_\nu$ is determined by $\Gamma$ and by $\Pi$ in lower homogeneities; and Theorem 4.7, that the truncated pointwise product of $f_1 \in \mathcal{D}^{\gamma_1}(V)$ and $f_2\in\mathcal{D}^{\gamma_2}(W)$ lies in $\mathcal{D}^{\gamma}$ with $\gamma = (\gamma_1+\alpha_2)\wedge(\gamma_2+\alpha_1)$ .

Significance

The reconstruction theorem is what turns a book-keeping device into analysis: it says that a coherent family of local expansions, indexed by base point, glues to a single genuine distribution, with an error controlled by the order of the expansion. Every subsequent operation in the theory — multiplication (Theorem 4.7), composition with smooth functions (Theorem 4.16), the multi-level Schauder estimate (Theorem 5.12), and the fixed-point theorem for singular SPDEs (Theorem 7.8) — is stated and used through it. Without it, the abstract spaces $\mathcal{D}^\gamma$ carry no information about actual distributions.

Regularity structures are not currently available in Mathlib, and neither are the anisotropic Hölder–Besov spaces $\mathcal{C}^\alpha_s$ that the theory is phrased in. The result itself is proved in the literature; the work this mission asks for is a machine-checked proof of the known argument, together with the reusable definitions it needs. The formal development is a prerequisite for anything downstream — Schauder estimates, the fixed-point theory, or the $\Phi^4_3$ and PAM convergence results of §10 — which are natural follow-on missions rather than part of this one.

Difficulty

The naive construction fails: setting $\mathcal{R}f := \Pi_x f(x)$ for a fixed $x$ is wrong away from $x$ , and the pointwise limit $\lim_{\delta\to0}$ of localisations of $\Pi_x f(x)$ around each $x$ does not obviously exist, because the objects being glued are distributions of negative order, not functions, so there is no value to take and no partition-of-unity argument that respects the scaling. Hairer's proof goes through a wavelet multiresolution analysis adapted to the scaling $s$ : one defines the candidate on each dyadic level by pairing with wavelets centred at grid points, and shows the resulting sequence is Cauchy using the $\mathcal{D}^\gamma$ bound level by level. A formalization therefore needs either a scaled wavelet basis with Daubechies-type regularity (Theorem 3.17 in the paper) or a substitute for it; this, and the uniform-in-scale bookkeeping, is where the effort lies. Uniqueness for $\gamma>0$ is by contrast short, and is listed as a separate milestone.

Formalization scope

The development commits to the following conventions, fixed in the mission's definition files. Points of $\mathbb{R}^d$ are Fin d → ℝ. Test functions are smooth and compactly supported, forming a submodule of all real-valued functions, and a distribution is a linear functional on that submodule; the pairing is extended by $0$ to non-test functions, and a lemma in the definition file certifies that rescaling maps test functions to test functions, so no statement is vacuous for that reason. Hairer's $\mathcal{B}^r_{s,0}$ consists of $C^r$ functions; here it consists of smooth ones, which defines the same spaces $\mathcal{C}^\alpha_s$ . The model space is the algebraic direct sum $\bigoplus_{a\in A} T_a$ over the index set, each $T_a$ a real normed space, with $Q_a$ the corresponding projection; the structure group is a subgroup of the linear automorphisms of that direct sum. Sectors are families of subspaces $V_a \subseteq T_a$ ; Hairer's requirement that each $V_a$ admit a complement is automatic in this algebraic setting. The integer $r$ appearing in the model bounds is the smallest one with $\ell > -r$ for all $\ell \in A$ , which is part of the definition of a model rather than a free parameter. All statements quantify over an arbitrary regularity structure, an arbitrary model, and an arbitrary compact set, so they are not satisfiable by a degenerate choice; the goal in particular claims existence, membership in $\mathcal{C}^\alpha_s$ , and uniqueness simultaneously.

Infrastructure that a complete proof will need, and which is reusable beyond this mission: scaled wavelet bases on $\mathbb{R}^d$ , the elementary theory of $\mathcal{C}^\alpha_s$ (including the positive-regularity case), and basic operations on compactly supported test functions under anisotropic rescaling. Contributions of any of these as separate lemmas are welcome, as are reductions that decompose the goal into wavelet-level estimates.

Selected references

M. Hairer, A theory of regularity structures, Inventiones Mathematicae 198 (2014) 269–504. arXiv:1303.5113, DOI:10.1007/s00222-014-0505-4
T. Lyons, Differential equations driven by rough signals, Revista Matemática Iberoamericana 14 (1998) 215–310. DOI:10.4171/RMI/240
M. Gubinelli, Controlling rough paths, Journal of Functional Analysis 216 (2004) 86–140. arXiv:math/0306433
M. Gubinelli, P. Imkeller, N. Perkowski, Paracontrolled distributions and singular PDEs, Forum of Mathematics Pi 3 (2015) e6. arXiv:1210.2684
Y. Bruned, M. Hairer, L. Zambotti, Algebraic renormalisation of regularity structures, Inventiones Mathematicae 215 (2019) 1039–1156. arXiv:1610.08468

13 thms2 active usersReviewed

Completed

Captain: Lucas

Rudin PMA III: Numerical Sequences and SeriesTextbook

Motivation

Chapter 3 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) develops the theory of convergence for sequences and series of numbers: subsequential limits and upper limits, the Cauchy criterion, the comparison, root and ratio tests, power series, summation by parts, and products of series. Its final section answers a question that distinguishes analysis from algebra: an infinite sum is not a sum. For a series that converges only conditionally, the value of the sum depends on the order of the terms, and Riemann's rearrangement theorem (Theorem 3.54) makes the dependence total — by reordering the terms one can prescribe any pair of limit inferior and limit superior for the partial sums, including divergence to $\pm\infty$ .

This mission is the third in a series formalizing Rudin Chapters 1–11. It uses the real and complex number systems of Mission I and the compactness results of Mission II, and it supplies the convergence machinery used by Missions VII and VIII.

Setting

A series $\sum a_n$ is the sequence of partial sums $s_n = a_0 + a_1 + \dots + a_{n-1}$ ; the series converges to $s$ when $s_n \to s$ , and converges absolutely when $\sum \|a_n\|$ converges. The upper limit of a real sequence is $s^{*} = \limsup_{n} s_n$ , taken in the extended real number system $[-\infty, +\infty]$ , and a subsequential limit is a limit of a subsequence there. A rearrangement of $\sum a_n$ is a series $\sum a_{\sigma(n)}$ with $\sigma$ a bijection of the index set onto itself.

The distinction that drives the chapter: for real or complex terms, absolute convergence is equivalent to convergence of $\sum a_{\sigma(n)}$ for every $\sigma$ , to the same sum (Theorem 3.55), whereas mere convergence is not.

Formalization targets

Goal — Riemann's rearrangement theorem (Theorem 3.54)

Let $\sum a_n$ be a series of real numbers which converges but not absolutely, and let $-\infty \le \alpha \le \beta \le +\infty$ . Then there is a rearrangement $\sum a_{\sigma(n)}$ with partial sums $s_n'$ such that

\liminf_{n \to \infty} s_n' = \alpha, \qquad \limsup_{n \to \infty} s_n' = \beta .

Milestones

s^{*} \text{ is a subsequential limit, and } x > s^{*} \Rightarrow s_n < x \text{ eventually; } s^{*} \text{ is unique with these properties} \qquad (3.17)

\textstyle\sum a_n \text{ converges} \iff \forall \varepsilon>0\ \exists N\ \forall m \ge n \ge N,\ \big|\sum_{k=n}^{m} a_k\big| \le \varepsilon \qquad (3.22)

\textstyle\sum_{n\ge 0} x^n = \tfrac{1}{1-x}\ (0 \le x < 1), \text{ divergence for } x \ge 1 \qquad (3.26)

\textstyle\sum n^{-p} \text{ converges} \iff p > 1 \qquad (3.28)

e = \textstyle\sum 1/n! = \lim_n (1 + 1/n)^n \qquad (3.30,\ 3.31)

\alpha = \limsup \|a_n\|^{1/n} < 1 \Rightarrow \text{convergence}, \ \alpha > 1 \Rightarrow \text{divergence} \qquad (3.33)

\text{ratio test} \qquad (3.34)

\text{radius of convergence of } \textstyle\sum c_n z^n \qquad (3.39)

\text{bounded partial sums} + b_n \downarrow 0 \Rightarrow \textstyle\sum a_n b_n \text{ converges} \qquad (3.42)

\text{absolute convergence} \Rightarrow \text{convergence} \qquad (3.45)

\text{Cauchy product: } \textstyle\sum c_n = AB \text{ when } \sum a_n \text{ converges absolutely} \qquad (3.50)

Significance

The rearrangement theorem is the precise statement of why conditional convergence must be handled with care, and it is the reason later chapters insist on uniform or absolute hypotheses before interchanging limit operations: Theorem 3.50 (Mertens) needs absolute convergence of one factor, and the Fourier and Lebesgue theories of Chapters 8 and 11 are built on $L^2$ and $L^1$ convergence rather than pointwise summation. The supporting milestones are the standard convergence tests, which are used constantly in the rest of the book, and the characterization of $\limsup$ , which is the tool that makes the root test and the radius of convergence formula precise.

Mathlib's Summable/HasSum express unconditional summability, which over $\mathbb{R}$ and $\mathbb{C}$ is equivalent to absolute convergence. The conditionally convergent series that this chapter is about are therefore invisible to that API, and the mission works with partial sums directly. Some of the classical tests exist in Mathlib in Summable form and will need restating; the rearrangement theorem itself has to be built.

Difficulty

The goal theorem is a construction, not an estimate: one splits $a_n$ into its positive and negative parts $p_n, q_n$ , observes that $\sum p_n$ and $\sum q_n$ both diverge while $p_n, q_n \to 0$ , and then alternately draws blocks of positive and negative terms to overshoot targets $\beta_m \to \beta$ and undershoot targets $\alpha_m \to \alpha$ . Formalizing the alternating greedy construction requires defining the permutation recursively together with the invariant that every index is eventually used — the bookkeeping, not the analysis, is the hard part. The endpoint cases $\alpha = -\infty$ or $\beta = +\infty$ must be carried through the same construction rather than treated separately.

Formalization scope

Conventions fixed by this mission:

Series convergence is Rudin.SeriesConvergesTo / Rudin.SeriesConverges, defined through Rudin.partialSum a n = ∑_{i<n} a i. Absolute convergence is Rudin.SeriesConvergesAbsolutely. Mathlib's Summable is deliberately not used, since it would collapse the distinction the chapter is about.
Upper and lower limits are taken in EReal via Filter.limsup/Filter.liminf, so $\pm\infty$ are allowed as values of $\alpha$ and $\beta$ in the goal.
Rearrangements are Equiv.Perm ℕ, and the rearranged series is fun k => a (σ k).
Series with complex terms are used where Rudin allows complex terms (3.22, 3.33, 3.34, 3.39, 3.42, 3.45, 3.50); the goal is about real series, as in the book.
The radius-of-convergence milestone is stated as α‖z‖ < 1 and α‖z‖ > 1 rather than ‖z‖ < 1/α, to avoid inversion in EReal.

The goal is not vacuous: conditionally convergent series exist (the alternating harmonic series), so the hypotheses are satisfiable, and the conclusion fixes both limit points exactly rather than merely bounding them.

Selected references

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 3 (pp. 47–78).
Bernhard Riemann, Über die Darstellbarkeit einer Function durch eine trigonometrische Reihe, Abhandlungen der Königlichen Gesellschaft der Wissenschaften zu Göttingen 13 (1867), Section 3.

13 thms2 active usersReviewed

Completed

Topology·Captain: Lucas

Rudin PMA II: Basic TopologyTextbook

Motivation

Convergence, continuity and integration are all statements about nearness, and Chapter 2 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) isolates the amount of structure needed to talk about nearness: a metric. The chapter's payoff is a single theorem, Heine–Borel (Theorem 2.41), which says that in $\mathbb{R}^k$ — and, as the chapter's examples show, only in spaces resembling it — three very different-looking finiteness conditions coincide: being closed and bounded, admitting finite subcovers, and forcing every infinite subset to accumulate. Nearly every existence theorem in the rest of the book (a continuous function on $[a,b]$ attains its maximum, is uniformly continuous, is Riemann-integrable) is an application of that equivalence.

This mission is the second in a series formalizing Rudin Chapters 1–11. It builds on the number systems of Mission I and supplies the topological input for Missions III–VII.

Setting

A metric space is a set $X$ with a distance $d : X \times X \to \mathbb{R}$ that is positive for distinct points, symmetric, and satisfies the triangle inequality. The neighbourhood $N_r(p)$ is the set of $q$ with $d(p,q) < r$ . A point $p$ is a limit point of $E \subseteq X$ if every neighbourhood of $p$ contains a point of $E$ different from $p$ ; $E$ is closed if it contains all its limit points, open if each of its points has a neighbourhood inside $E$ , and its closure $\bar E$ is $E$ together with its limit points. $E$ is perfect if it is closed and every point of $E$ is a limit point of $E$ , and bounded if it is contained in some neighbourhood.

An open cover of $E$ is a family of open sets whose union contains $E$ ; $K$ is compact if every open cover of $K$ has a finite subcover. A $k$ -cell is a product $\{x \in \mathbb{R}^k : a_j \le x_j \le b_j \text{ for all } j\}$ . Two sets $A, B$ are separated if $\bar A \cap B = A \cap \bar B = \varnothing$ , and $E$ is connected if it is not the union of two nonempty separated sets.

Formalization targets

Goal — Heine–Borel (Theorem 2.41)

For $E \subseteq \mathbb{R}^k$ , the following are equivalent:

\text{(a) } E \text{ closed and bounded} \quad\Longleftrightarrow\quad \text{(b) } E \text{ compact} \quad\Longleftrightarrow\quad \text{(c) every infinite } S \subseteq E \text{ has a limit point in } E .

Milestones

\textstyle\bigcup_n E_n \text{ countable when each } E_n \text{ is} \qquad (2.12)

\{0,1\}^{\mathbb{N}} \text{ is uncountable} \qquad (2.14)

\text{arbitrary unions of open sets, finite intersections of open sets, and the closed duals} \qquad (2.24)

\bar E = E \cup E', \quad \bar E \text{ closed}, \quad \bar E = E \Leftrightarrow E \text{ closed}, \quad E \subseteq F \text{ closed} \Rightarrow \bar E \subseteq F \qquad (2.27)

\sup E \in \bar E \qquad (2.28)

\text{open-cover compactness} \Leftrightarrow \text{compactness} \qquad (2.32)

F \subseteq K,\ F \text{ closed},\ K \text{ compact} \Rightarrow F \text{ compact} \qquad (2.35)

\text{finite intersection property for compact sets} \qquad (2.36)

\text{infinite } E \subseteq K \text{ compact} \Rightarrow E \text{ has a limit point in } K \qquad (2.37)

\text{nested } k\text{-cells have a common point} \qquad (2.39)

\text{every } k\text{-cell is compact} \qquad (2.40)

\text{nonempty perfect } P \subseteq \mathbb{R}^k \text{ is uncountable} \qquad (2.43)

E \subseteq \mathbb{R} \text{ connected} \Leftrightarrow (x,y \in E,\ x<z<y \Rightarrow z \in E) \qquad (2.47)

Significance

Heine–Borel is the bridge between the order completeness of $\mathbb{R}$ established in Chapter 1 and the analytic theorems of Chapters 3–7: the bisection argument that proves $k$ -cells compact is the same argument that produces convergent subsequences (Bolzano–Weierstrass, Theorem 2.42), and compactness is what converts local information into global statements. Theorem 2.43 supplies the standard source of uncountable sets of measure zero — the Cantor set is the running example — which matters again in Chapter 11. Theorem 2.47, characterizing the connected subsets of the line as the order-convex ones, is the topological content of the intermediate value theorem proved in Chapter 4.

Mathlib has an extensive metric-space and compactness library, so much of this chapter exists there in some form. What this mission adds is the explicit correspondence with Rudin's formulations: his open-cover definition of compactness against the library's filter-based IsCompact (a milestone in its own right), his $\varepsilon$ -style limit points against closure, and his $k$ -cells against the library's boxes. The resulting dictionary is what the remaining missions in the series use when they need a compactness argument.

Difficulty

The mathematics is standard, and the difficulty is almost entirely in the translation layer. Two places bite. First, Rudin's compactness quantifies over arbitrary open covers, so the statement is a $\Pi$ -type over families of sets, while Mathlib's IsCompact is a statement about filters; the equivalence is available in the library but only after the cover is presented in the right indexed form. Second, "limit point" in Rudin's sense is not p ∈ closure E: the point must be approached by points of $E$ other than $p$ , so isolated points of $E$ are excluded, and statements such as 2.27(a) and 2.41(c) are false if the two notions are conflated.

Formalization scope

Conventions fixed by this mission:

Metric spaces are Mathlib's [MetricSpace X]; IsOpen, IsClosed, closure, Perfect, IsCompact, Bornology.IsBounded and IsPreconnected are used for Rudin's corresponding notions.
Rudin's limit points are Rudin.IsLimitPoint p E, defined with the explicit $\varepsilon$ and the condition $q \ne p$ , and his open-cover compactness is Rudin.IsCoverCompact.
$k$ -cells are Rudin.kCell k a b inside EuclideanSpace ℝ (Fin k); the case where some $a_j > b_j$ gives the empty set, which is why the nested-cell milestone assumes each cell is nonempty, exactly as Rudin's construction does.
Connectedness is IsPreconnected, which admits the empty set, matching Rudin's convention that a set is connected unless it splits into two nonempty separated pieces.
The Heine–Borel goal is stated as a TFAE list in Rudin's order (a), (b), (c).

The equivalence is not vacuous: all three conditions are satisfied by any $k$ -cell and all three fail for $\mathbb{R}^k$ itself when $k \ge 1$ .

Selected references

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 2 (pp. 24–55).
The mathlib Community, The Lean Mathematical Library, CPP 2020. https://doi.org/10.1145/3372885.3373824

15 thms2 active usersReviewed

Completed

Captain: Lucas

Rudin PMA I: The Real and Complex Number SystemsTextbook

Motivation

Every course in analysis begins by fixing what a real number is, because the theorems that follow — the intermediate value theorem, the convergence of monotone bounded sequences, the compactness of closed bounded intervals — are false over the rationals and true over the reals for exactly one reason: the least-upper-bound property. Walter Rudin opens Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) with this point. His Example 1.1 exhibits the gap concretely: the set of rationals $p$ with $p^2 < 2$ has no least upper bound in $\mathbb{Q}$ . Chapter 1 then constructs an ordered field in which no such gap occurs, and derives from that single axiom the archimedean property, the density of $\mathbb{Q}$ , and the existence of $n$ -th roots.

This mission is the first in a series formalizing Rudin Chapters 1–11. It covers the chapter's number-system foundations: the ordering axioms, the real field, the complex field, and euclidean space $\mathbb{R}^k$ .

Setting

An ordered set is a set $S$ with a transitive relation $<$ such that for $x, y \in S$ exactly one of $x < y$ , $x = y$ , $y < x$ holds. If $E \subseteq S$ and there is $\beta \in S$ with $x \le \beta$ for all $x \in E$ , then $E$ is bounded above and $\beta$ is an upper bound. A least upper bound (supremum) of $E$ is an upper bound $\alpha$ such that no $\gamma < \alpha$ is an upper bound. The ordered set $S$ has the least-upper-bound property if every nonempty $E \subseteq S$ that is bounded above has a least upper bound in $S$ .

An ordered field is a field $F$ carrying an order such that $x + y < x + z$ whenever $y < z$ , and $xy > 0$ whenever $x > 0$ and $y > 0$ . Rudin's Theorem 1.19 asserts that an ordered field $\mathbb{R}$ with the least-upper-bound property exists and contains $\mathbb{Q}$ as a subfield; the members of $\mathbb{R}$ are the real numbers. The complex field $\mathbb{C}$ is the set of ordered pairs $(a,b)$ of reals with the usual operations, written $a + bi$ , with $|z| = (z\bar z)^{1/2}$ ; euclidean $k$ -space $\mathbb{R}^k$ is the set of $k$ -tuples with the inner product $x \cdot y = \sum_{j} x_j y_j$ and norm $|x| = (x\cdot x)^{1/2}$ .

Formalization targets

Goal — the real field is the unique complete ordered field (Theorem 1.19)

\text{$K$ an ordered field with the least-upper-bound property} \;\Longrightarrow\; \exists!\, e : K \xrightarrow{\ \sim\ } \mathbb{R} \text{ an order-preserving field isomorphism.}

Existence of such a field is witnessed in Lean by $\mathbb{R}$ itself; what carries the content of Rudin's theorem, and what the goal asks for, is that the least-upper-bound property pins the field down up to a unique isomorphism of ordered fields. Uniqueness of $e$ also gives Rudin's second assertion for free: any embedding of $\mathbb{Q}$ is the canonical one, so $K$ contains $\mathbb{Q}$ as an ordered subfield.

Milestones

\neg\,\exists p \in \mathbb{Q},\ p^2 = 2 \qquad (\text{Example } 1.1)

\text{LUB property} \Rightarrow \text{GLB property, with } \inf B = \sup(\text{lower bounds of } B) \qquad (1.11)

x>0 \Rightarrow \exists n \in \mathbb{N},\ nx > y; \qquad x<y \Rightarrow \exists p \in \mathbb{Q},\ x<p<y \qquad (1.20)

x>0,\ n>0 \Rightarrow \exists!\, y>0,\ y^n = x \qquad (1.21)

|\bar z| = |z|,\quad |zw| = |z||w|,\quad |\operatorname{Re} z| \le |z|,\quad |z+w| \le |z|+|w| \qquad (1.33)

\Big|\sum_{j} a_j \overline{b_j}\Big|^2 \le \sum_j |a_j|^2 \sum_j |b_j|^2 \qquad (1.35)

|x \cdot y| \le |x|\,|y|, \quad |x+y| \le |x|+|y|, \quad |x-z| \le |x-y|+|y-z| \qquad (1.37)

Significance

The least-upper-bound property is the only non-algebraic input to the whole of single-variable analysis, and the chapter shows how much follows from it alone: the archimedean property, which rules out infinitesimals; the density of $\mathbb{Q}$ , which makes approximation arguments possible; and the existence of $n$ -th roots, which repairs precisely the defect exhibited by $\sqrt{2}$ . The uniqueness statement is what licenses the common practice of treating "the" real numbers as a single object regardless of the construction used (Dedekind cuts, as in Rudin's appendix, or Cauchy sequences).

Mathlib already contains $\mathbb{R}$ , $\mathbb{C}$ , and a uniqueness theorem for conditionally complete linearly ordered fields, and several of the milestones are available there in some form. The work this mission asks for is therefore bridging work: stating Rudin's hypotheses in his own terms — an order with the least-upper-bound property as a hypothesis on a set, not as a typeclass whose data includes a chosen supremum operator — and deriving the standard library form from them. That bridge is what later missions in the series reuse.

Difficulty

The individual statements are elementary, and the mathematical difficulty is genuinely low; what makes the chapter non-mechanical in a proof assistant is the mismatch between hypothesis and structure. Mathlib's completeness is packaged as ConditionallyCompleteLinearOrder, a structure carrying sSup and sInf as data; Rudin's is a proposition about an arbitrary ordered field. Turning the proposition into the structure (in order to invoke the library's uniqueness theorem) is the one step where the obvious "just apply the Mathlib lemma" move does not typecheck.

Formalization scope

Conventions fixed by this mission:

Rudin's least-upper-bound property is the predicate Rudin.HasLeastUpperBoundProperty, using Mathlib's IsLUB, BddAbove, lowerBounds; no completeness typeclass is assumed of K.
Ordered fields are [Field K] [LinearOrder K] [IsStrictOrderedRing K], which is exactly Rudin's Definition 1.17.
Order-field isomorphisms are Mathlib's ≃+*o (OrderRingIso), so "unique isomorphism" is stated as ∃ e, ∀ e', e' = e.
$\mathbb{C}$ is Mathlib's ℂ and $|z|$ is the norm ‖z‖; euclidean $k$ -space is EuclideanSpace ℝ (Fin k) with the inner product inner ℝ x y, so Rudin's $\mathbb{R}^k$ facts are norm and inner-product inequalities.
Statements bundling several of Rudin's conclusions (1.33, 1.37) are stated as a single conjunction, in the order the book lists them.

Nothing here is vacuous: the goal quantifies over an arbitrary ordered field satisfying the property, and ℝ itself is such a field, so the hypothesis is satisfiable and the conclusion is not automatic.

Selected references

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 1 (pp. 1–21) and its Appendix.
The mathlib Community, The Lean Mathematical Library, CPP 2020. https://doi.org/10.1145/3372885.3373824

10 thms2 active usersReviewed

Dynamical Systems Optimization·Captain: mikedeng1

Examples of Pathological Dynamics of the Subgradient Method for Lipschitz Path-Differentiable Functions: A Bounded Subgradient Sequence That Does Not Converge for a Whitney-Stratifiable KŁ FunctionResearch Paper

Motivation

The small-step subgradient method is the basic algorithm for minimizing a nonsmooth, nonconvex, locally Lipschitz function $f:\mathbb R^n\to\mathbb R$ . It is also the scheme behind stochastic gradient training of neural networks with nonsmooth activations. From a starting point $x_0$ it iterates

x_{i+1}=x_i-\varepsilon_i v_i,\qquad v_i\in\partial^c f(x_i),

with step sizes $\varepsilon_i\to0$ and $\sum_i\varepsilon_i=+\infty$ . The basic question is whether a bounded run converges. For smooth $f$ , and for continuous-time subgradient flows, convergence follows from a Kurdyka–Łojasiewicz (KŁ) inequality together with tame geometry such as Whitney stratifiability (Bolte, Daniilidis, Lewis, Shiota 2007; Absil, Mahony, Andrews 2005). Whether the same hypotheses suffice for the discrete nonsmooth method was open.

R. Ríos-Zertuche (arXiv:2007.11699, published in Math. Oper. Res. 2022) is a companion to the work of Bolte, Pauwels and Ríos-Zertuche on the long-term dynamics of the subgradient method for path-differentiable functions (arXiv:2006.00098). That work proves positive results, such as slowdown near limit points and convergence of the values under the weak Sard condition. The examples paper shows that these results cannot be improved to convergence of the iterates. Its first example (Section 2) lives on $\mathbb R^2$ and is the subject of this mission.

Setting

For a locally Lipschitz $f:\mathbb R^n\to\mathbb R$ , the Clarke subdifferential $\partial^c f(x)$ is the convex envelope of all limits $\lim\nabla f(y_k)$ along sequences $y_k\to x$ of points where $f$ is differentiable. The critical set is $\operatorname{crit}f=\{x:0\in\partial^c f(x)\}$ .

A subgradient sequence (Definition 1) is a sequence obeying the recursion above with positive steps $\varepsilon_i\to0$ , $\sum\varepsilon_i=+\infty$ . The function $f$ is path-differentiable (Definition 2) if for every Lipschitz curve $\gamma$ and almost every $t$ , $(f\circ\gamma)'(t)=v\cdot\gamma'(t)$ for all $v\in\partial^c f(\gamma(t))$ . It satisfies the weak Sard condition (Definition 3) if it is constant on each connected component of $\operatorname{crit}f$ . It is Whitney $C^\infty$ -stratifiable (Definition 5) if its graph in $\mathbb R^{n+1}$ is a locally finite union of disjoint connected $C^\infty$ submanifolds. These pieces must satisfy the frontier condition and Whitney's condition A: limits of tangent spaces of a stratum contain the tangent spaces of the strata in its boundary.

The example works on $\mathbb R^2$ . For $i\ge2$ let

\vartheta_i=\sum_{k=2}^{i}\frac1{k\log k},\qquad x_i=\Bigl[1+\frac{(-1)^i}{i}\Bigr](\cos\vartheta_i,\sin\vartheta_i),

$\varepsilon_i=\|x_{i+1}-x_i\|$ and $v_i=-(x_{i+1}-x_i)/\varepsilon_i$ . Let $\varphi(x)=|1-\|x\||$ be the distance to the unit circle $S^1$ . Let $\psi$ be a smooth radial bump with values in $[0,1]$ , equal to $1$ on $B_1(0)$ , vanishing for $\|x\|\ge2$ and non-increasing along rays. Set $\psi_i(x)=\psi(2^i(x-x_i))$ and $V_i(x)=(x-x_i)\cdot v_i+1/i$ . For $i_0\ge2$ ,

f(x)=\Bigl(1-\sum_{i\ge i_0}\psi_i(x)\Bigr)\varphi(x)+\sum_{i\ge i_0}\psi_i(x)V_i(x).\tag{4}

Formalization targets

Goal

There are $f:\mathbb R^2\to\mathbb R$ , steps $(\varepsilon_i)$ and a sequence $(x_i)$ such that $(x_i)$ is a bounded, non-convergent subgradient sequence of $f$ , and $f$ has all of the following properties:

it is Lipschitz and path-differentiable;
it satisfies the weak Sard condition;
it is Whitney $C^\infty$ -stratifiable;
it is $C^\infty$ on a ball around every $x_i$ ;
it satisfies

\|\nabla f(x)\|\ge\tfrac12\qquad\text{for all }x\notin\operatorname{crit}f.

This is the paper's negative answer to its question Q9, combined with its remarks in Q1 and Q12. The witness is left existential.

Milestones

The milestones are the properties of the explicit witness (4):

the step-size estimates ( $\varepsilon_i\to0$ , $\sum\varepsilon_i=\infty$ , $\sum\varepsilon_i^2<\infty$ );
Lemma 7: $v_i$ is close to $\pm x_i/\|x_i\|$ , and radial projection is Lipschitz near $x_i$ ;
Proposition 6 (i)–(vii): smoothness off $S^1\cup\{0\}$ ; $\nabla f=v_i$ on $B_{1/2^i}(x_i)$ , so that $(x_i)$ is a subgradient sequence; $\partial^c f(p)=\{ap:a\in[-1,1]\}$ on $S^1$ ; $\operatorname{crit}f=S^1\cup\{0\}$ ; Lipschitz path-differentiability; Whitney stratifiability; and $\|\nabla f\|>1/2$ off the critical set;
the weak Sard condition;
$\operatorname{acc}\{x_i\}=S^1$ , with boundedness and non-convergence.

Significance

The example is a counterexample: the standard toolbox of tame geometry plus a KŁ inequality does not give convergence of the discrete small-step subgradient method, even with a uniform gradient lower bound away from the critical set and the weak Sard condition. In continuous time the same hypotheses give convergence. The gap therefore comes from discretization. Any convergence proof for nonsmooth subgradient methods needs further structure, such as definability in an o-minimal structure or a stronger KŁ inequality near the critical set. Q12 adds that requiring the iterates to stay in the full-measure set of differentiability points does not help.

The result is proved in the paper; to our knowledge none of it is formalized. Formalizing it gives the first machine-checked Clarke-subdifferential, path-differentiability and Whitney-stratification counterexample. It also gives reusable estimates for an explicit sequence spiralling onto a circle.

Difficulty

Most of the steps are explicit estimates, but three of them are delicate.

The Clarke subdifferential on $S^1$ . It must be computed although infinitely many bumps accumulate there. Near each $x_i$ the gradient of $f$ contains the term $\nabla\psi_i\,(V_i-\varphi)$ , where $\nabla\psi_i$ is of size $2^i$ . Showing that the limiting gradients are still only $\pm p$ requires the second-order agreement of $V_i$ and $\varphi$ on $B_{1/2^{i-1}}(x_i)$ , and that rests on the estimate of Lemma 7.
Path differentiability. It does not follow from local Lipschitz continuity. A Lipschitz curve may cross the circle at uncountably many times, so the chain rule has to be checked for every element of $\partial^c f(\gamma(t))$ at almost every such time.
Whitney's condition A. It must hold where the two-dimensional strata of the graph meet the circle stratum. That requires control of the tangent planes of the graph along sequences entering the bump regions.

Formalization scope

Everything lives in EuclideanSpace ℝ (Fin n). The definitions follow these conventions:

$\partial^c f(x)$ is the convex hull of the published ShorNonsmooth.AlmostDiff.almostGradients, which uses cluster points of the gradients rather than limits; the two sets are the same.
Path differentiability quantifies over every Lipschitz curve and every element of $\partial^c f(\gamma(t))$ , and also asserts that $\gamma$ is differentiable at $t$ , which holds almost everywhere by Rademacher's theorem.
Strata are connected, pairwise disjoint and locally finite at the points of the graph. Each is a $C^k$ coordinate-slice submanifold (the published ProjLikeRetr.Retractor.IsSubmanifold) for every $k$ . Tangent spaces are spans of tangent cones, and Grassmannian convergence is convergence of the subspace gap to $0$ .
The bump is an arbitrary BumpProfile with exactly the properties listed on p. 6, and the series in (4) are tsums. The indices $i<2$ , where $1/0=0$ and $\log 1=0$ in Lean, are never used.

Four statements are adjusted, and each adjustment is disclosed in its item:

Proposition 6 (i) is stated on $\mathbb R^2\setminus(S^1\cup\{0\})$ , as in the paper's proof, because $f$ has a cone point at $0$ .
The last link " $<2/i$ " of the step-size chain is false and is dropped.
Proposition 6 (ii), (iv), (vii) and the weak Sard claim hold for $i_0$ beyond a threshold depending on the bump. For small $i_0$ the bump supports overlap.
The KŁ clauses also assert differentiability, since Lean's gradient is $0$ at non-differentiable points.

The goal cannot be met trivially. Boundedness of the sequence and the conditions $\varepsilon_i\to0$ , $\sum\varepsilon_i=\infty$ are part of it, and they rule out an affine $f$ . Every regularity property is a separate conjunct. Contributions that develop the geometry of Whitney stratifications and path differentiability in Lean are reusable well beyond this example.

Selected references

R. Ríos-Zertuche, Examples of pathological dynamics of the subgradient method for Lipschitz path-differentiable functions, arXiv:2007.11699v1, 2020; Math. Oper. Res., 2022. https://arxiv.org/abs/2007.11699
J. Bolte, E. Pauwels, R. Ríos-Zertuche, Long term dynamics of the subgradient method for Lipschitz path differentiable functions, arXiv:2006.00098, 2020. https://arxiv.org/abs/2006.00098
J. Bolte, A. Daniilidis, A. Lewis, M. Shiota, Clarke subgradients of stratifiable functions, SIAM J. Optim. 18 (2007). https://doi.org/10.1137/060670080
D. Davis, D. Drusvyatskiy, S. Kakade, J. D. Lee, Stochastic subgradient method converges on tame functions, Found. Comput. Math. 20 (2020). https://arxiv.org/abs/1804.07795
P.-A. Absil, R. Mahony, B. Andrews, Convergence of the iterates of descent methods for analytic cost functions, SIAM J. Optim. 16 (2005). https://doi.org/10.1137/040605266

18 thms1 active userReviewed

Control Theory Operations Research·Captain: mikedeng1

Optimal Dynamic Momentum Strategies: For Horizons Within the Look-Back Period, the Optimal Weight Is the Mean-Variance Weight Plus a Hedging Term Weighted Toward Recent ReturnsResearch Paper

Motivation

Time-series momentum is the empirical regularity that an asset's recent excess return predicts its future excess return. It has been documented across equity indices, currencies, commodities and bonds (Moskowitz, Ooi & Pedersen 2012), and momentum portfolios are among the most widely traded systematic strategies. Most of that literature builds portfolios from a single signal: the average return over a look-back window. Li and Liu (Operations Research 2022) ask what a long-horizon investor who rebalances should do when expected returns really are driven by such a moving average. Their answer has a structural feature that a Markovian model such as Merton's (Merton 1971) cannot produce. The optimal weight depends on the whole recent price path, not only on the current momentum.

Setting

A risky asset has price $S_t$ and log price $s_t=\ln S_t$ , with

\frac{dS_t}{S_t} = [\alpha m_t + (1-\alpha)\mu + r]\,dt + \sigma\,dB_t,\qquad m_t = \frac1\tau\int_{t-\tau}^{t}\Big(\frac{dS_u}{S_u} - r\,du\Big),

where $B$ is a Brownian motion. Momentum $m_t$ is the equally weighted moving average of excess returns over a look-back window of length $\tau>0$ . The parameter $0<\alpha<1$ measures how strongly momentum enters the expected return, $\mu$ is the unconditional risk premium, $r$ is the constant short rate and $\sigma>0$ is the volatility. Because the drift depends on $s_t - s_{t-\tau}$ , the price is not Markov: the state at time $t$ is the whole path on $[t-\tau,t]$ .

An investor with constant relative risk aversion $\gamma>0$ maximizes expected utility of terminal wealth at a horizon $T$ by trading the asset and a riskless bond. The mission works in the paper's short-horizon regime $0\le T\le\tau$ , with the investor standing at time $0$ , so the realized path $s$ on $[-\tau,0]$ is known.

The paper's analysis (Appendix A.2) produces the following objects:

the market price of risk at time $0$ , $\theta_0 = [(1-\alpha)\mu - \alpha(r-\sigma^2/2) + \frac\alpha\tau(s_0-s_{-\tau})]/\sigma$ ;
functions $A_1, A_2$ on $[0,T]$ that solve a Riccati equation and a linear equation, the system (A.9), with $A_1(T)=A_2(T)=0$ and forcing term $s_{u-\tau}$ ;
the optimal weight $\phi^*_0 = \theta_0/(\gamma\sigma) + A_{1,0}s_0 + A_{2,0}$ of (A.11);
explicit functions $C_0$ , $\hat\omega$ , the weight $\omega$ on $[-\tau,0]$ and a constant $C_1$ , all of (A.14).

The Lean development names them theta0, SolvesA9, phiStar, C0, omegaHat, omega and C1 in the namespace DynMomentum.ShortHorizon.

Formalization targets

Goal: Proposition 3.3

For every solution $(A_1,A_2)$ of (A.9),

\phi^*_0 = \underbrace{\frac{\alpha}{\gamma\sigma^2}\int_{-\tau}^{0}\frac1\tau\Big(\frac{dS_v}{S_v}-r\,dv\Big) + \frac{(1-\alpha)\mu}{\gamma\sigma^2}}_{\phi^M_0} + \underbrace{\frac{(1-\gamma)\alpha}{\gamma\sigma^2}\int_{-\tau}^{0}\omega_v\Big(\frac{dS_v}{S_v}-r\,dv\Big) + C_1}_{\phi^H_0}. \tag{3.8}

Moreover, $\omega$ is positive on $(-\tau,0]$ when $T>0$ , strictly increasing on $[-\tau,T-\tau]$ , and constant on $[T-\tau,0]$ . The first summand $\phi^M$ is the myopic mean-variance weight; the second, $\phi^H$ , is the hedging demand.

Milestones

(A.9) solves (A.8). The ansatz $f(x,t)=\exp\{A_{1,t}x^2/2+A_{2,t}x+A_{3,t}\}$ solves the Feynman–Kac PDE (A.8) whenever $(A_1,A_2,A_3)$ solve (A.9).
(A.13), $A_1$ . The closed form $A_{1,t}=\alpha(\gamma-1)(1-e^{2\alpha(T-t)/(\sqrt\gamma\tau)})/(\gamma\sigma^2\tau D(T,t))$ solves the Riccati equation with $A_{1,T}=0$ .
(A.13), $A_2$ . For any solution $A_1$ , the variation-of-constants integral for $A_2$ solves the linear equation with $A_{2,T}=0$ .
(A.14). $\hat\omega_u>0$ for $u\in[-\tau,-\tau+T]$ .
Proposition 3.3, last sentence. The positivity and shape of $\omega$ , stated on its own.

Significance

The result. Proposition 3.3 shows that a momentum investor who rebalances should not trade on momentum alone. The hedging demand weights past returns unequally, with more weight on recent ones, so two price paths with identical momentum lead to different optimal positions. This is the paper's explanation of why path dependence is intrinsic to optimal momentum trading. It underlies the paper's later comparisons with momentum-only strategies, the horizon extension of Proposition 6.3, and the closed-form expansions of Online Appendix III.

Formalizing it. The proof's analytic half, from (A.9) to (3.8), is summarized in the paper by the phrase "after some manipulations". Writing that step out yields a checked identity between an ODE-defined weight and an explicit integral formula. Doing so has already caught an error. The constant $C_1$ printed in (A.14) is wrong: it differs from the true value by a path-independent amount, and it becomes correct after deleting both occurrences of $-\sigma^2/2$ (a numerical solution of (A.9) agrees with the corrected formula to $10^{-10}$ ). The proposition is proved in the paper. As far as is known, no part of it has been machine-checked.

Difficulty

Each milestone is a direct calculus statement; the goal is not. The obvious approach is to substitute the closed forms (A.13) into (A.11) and simplify. That leaves $A_{2,0}$ as a double integral of the past path $s$ against two nested exponential kernels written in the ODE's own parameterization, while (3.8) is a single integral of returns $dS/S$ against the weight $\omega$ of (A.14), which is written in a different parameterization. The paper gives no derivation of the match. The path is only continuous, so no step may differentiate $s$ . Separately, the Riccati closed form divides by a quantity that vanishes for small $\gamma<1$ , so every step has to track where that denominator is positive.

Formalization scope

What is formalized. Everything from (A.9) to (3.8). The stochastic layer is not formalized: Lemmas 3.1–3.2 (martingale method), the measure change, the Feynman–Kac representation and the volatility matching (A.10)–(A.12) need stochastic integration, Itô's formula and martingale representation, which Mathlib does not have at this revision. Equation (A.11) is therefore taken as the definition of the optimal weight: $\phi^*_0 := \theta_0/(\gamma\sigma) + A_{1,0}s_0 + A_{2,0}$ .
Time. The statement is at $t=0$ with horizon $0\le T\le\tau$ and the path on $[-\tau,0]$ , as in Appendix A.2. The model is time-homogeneous, so a general $t$ is a shift.
ODEs. "Solves (A.9)" means a derivative within $[0,T]$ at every point of $[0,T]$ , plus the terminal conditions. At $T=0$ the derivative clause is vacuous; that is the paper's zero-horizon case.
Admissibility. The hypothesis $D(T,0)=(\sqrt\gamma-1)e^{2\alpha T/(\sqrt\gamma\tau)}+(\sqrt\gamma+1)>0$ is added. It holds automatically for $\gamma\ge1$ . Without it, the Riccati solution blows up for small $\gamma<1$ and the goal would be vacuous.
Pathwise returns. The return integral $\int_{-\tau}^0 w_v(dS_v/S_v - r\,dv)$ , for a deterministic absolutely continuous weight $w$ with derivative $w'$ , is read as $w_0s_0 - w_{-\tau}s_{-\tau} - \int_{-\tau}^0 w'_vs_v\,dv + (\sigma^2/2-r)\int_{-\tau}^0 w_v\,dv$ . This is its value by Itô's formula and the product rule. With $w\equiv1/\tau$ it gives back $m_0$ of (2.3).
Corrections. $C_1$ is the corrected constant described above. The positivity of $\omega$ is stated on $(-\tau,0]$ under $T>0$ , because $\omega_{-\tau}=0$ and $\omega\equiv0$ when $T=0$ .
What a correct formalization rules out. The goal is not obtained by definition. $\phi^*$ is (A.11), never $\phi^M+\phi^H$ . The functions $\omega$ , $\hat\omega$ , $C_0$ and $C_1$ are the explicit formulas of (A.14), never derived from the ODE solution. The goal quantifies over every solution of (A.9), not over the closed forms.
Infrastructure. The development uses Mathlib's HasDerivWithinAt, interval integrals, Real.exp and Real.sqrt. Two lemmas are reusable well beyond this mission: the closed form of a constant-coefficient scalar Riccati equation, and variation of constants for a scalar linear ODE with merely continuous forcing. Contributions of those lemmas, of uniqueness for (A.9), and of the integration-by-parts step are welcome.

Selected references

K. Li and J. Liu, Optimal Dynamic Momentum Strategies, Operations Research, 2022. https://doi.org/10.1287/opre.2021.2254
R. C. Merton, Optimum consumption and portfolio rules in a continuous-time model, Journal of Economic Theory 3(4), 1971. https://doi.org/10.1016/0022-0531(71)90038-X
T. J. Moskowitz, Y. H. Ooi and L. H. Pedersen, Time series momentum, Journal of Financial Economics 104(2), 2012. https://doi.org/10.1016/j.jfineco.2011.11.003

7 thms1 active userReviewed

Numerical Analysis Operations Research Probability·Captain: mikedeng1

Fast Hybrid Schemes for Fractional Riccati Equations (Rough Is Not So Tough): Explicit Lower and Upper Bounds on the Convergence Radius of the Fractional Power-Series SolutionResearch Paper

Motivation

In the rough Heston model of El Euch and Rosenbaum, the variance of an asset is driven by a fractional kernel with Hurst exponent $H<\tfrac12$ , which matches the roughness observed in realized volatility. The model keeps one feature of the classical Heston model: the characteristic function of the log-price is explicit up to the solution of a deterministic equation, here a fractional Riccati equation

D^\alpha\psi=\lambda\psi^2+\mu\psi+\nu,\qquad \alpha=H+\tfrac12,

with complex coefficients $\lambda,\mu,\nu$ that depend on the Fourier variable (El Euch–Rosenbaum 2019). Pricing a vanilla option by Fourier inversion requires this solution for many complex parameters, and the equation has no closed form. The standard numerical method, the fractional Adams scheme, is slow because of the memory of the fractional derivative.

Callegaro, Grasselli and Pagès (arXiv:1805.12587v4) observe that with zero initial condition the solution is a fractional power series $\psi(t)=\sum_{k\ge0}a_kt^{k\alpha}$ whose coefficients obey an explicit convolution recursion. The series can be summed very fast, but only on its interval of convergence; beyond it they switch to a hybrid numerical scheme. Where the switch happens is governed by the convergence radius, and their Theorem 3.3 bounds it explicitly from below and, for parameters of equal sign, from above.

Setting

Fix $\alpha\in(0,2]$ and $\lambda,\mu,\nu\in\mathbb C$ . Identifying the coefficients of the series in the Riccati equation yields the coefficient recursion $(A_{\lambda,\mu,\nu})$ (3.19)–(3.20):

a_0=0,\qquad a_1=\frac{\nu}{\Gamma(\alpha+1)},\qquad a_{k+1}=\big(\lambda\,a^{*2}_k+\mu\,a_k\big)\frac{\Gamma(\alpha k+1)}{\Gamma(\alpha k+\alpha+1)}\quad(k\ge1),

where $a^{*2}_k=\sum_{\ell=1}^{k-1}a_\ell a_{k-\ell}$ is the discrete convolution (so $a^{*2}_1=0$ ). Each $a_{k+1}$ depends on $a_1,\dots,a_k$ only, so the sequence is uniquely determined; in Lean it is coeff α lam mu nu : ℕ → ℂ.

The convergence radius of $\sum_ka_kt^{k\alpha}$ is given by Hadamard's formula (3.21):

R_{\psi_{\lambda,\mu,\nu}}=\liminf_k|a_k|^{-\frac1{\alpha k}}\in[0,+\infty],

in Lean radius α (coeff α lam mu nu). With $x_+=\max(x,0)$ , $a\wedge b=\min(a,b)$ and the Beta function $B(a,b)=\Gamma(a)\Gamma(b)/\Gamma(a+b)$ , the paper introduces the constants

c_\alpha=2^{2-(1-2\alpha)_+-2(\alpha-1)_+}\alpha^{\alpha-1}B(\alpha\wedge1,\alpha\wedge1),\qquad \widetilde B(\alpha)=B(\alpha,\alpha)-2^{1-2\alpha},

\tau_*=\frac{2^{\frac1\alpha-(\frac1\alpha-2)_+}\,\alpha}{\Big(|\mu|+\sqrt{|\mu|^2+c_\alpha\frac{|\lambda||\nu|}{\Gamma(\alpha)}}\Big)^{1/\alpha}},\qquad C_\alpha=\begin{cases}(3\cdot5^{\alpha-1})^{\frac1{2\alpha}}\sqrt\alpha,&\alpha\in(0,1],\\ \sqrt{2\alpha}/\widetilde B(\alpha),&\alpha\in(1,2].\end{cases}

Formalization targets

Goal: Theorem 3.3 (a)–(b)

For $0<\alpha\le2$ :

for all $\lambda,\mu,\nu\in\mathbb C$ with $\lambda\nu\ne0$ ,

0<\tau_*\le R_{\psi_{\lambda,\mu,\nu}};

for real $\lambda,\nu>0,\ \mu\ge0$ (resp. $\lambda,\nu<0,\ \mu\le0$ ),

R_{\psi_{\lambda,\mu,\nu}}\le R_{\psi_{|\lambda|,0,|\nu|}}\le C_\alpha\Big(\frac{\Gamma(\alpha+1)}{\lambda\nu}\Big)^{\frac1{2\alpha}}.

Milestones

In attack order: the Riemann-sum Lemma A.1 (A.39); Kershaw's Gamma-ratio inequalities (A.41); the coefficient upper bounds $|a_k|\le C_*k^{\alpha-1}\rho_*^k$ of (B.49) for $\alpha\le1$ and (B.51) for $\alpha>1$ ; Proposition B.1 (a) (for $\mu=0$ the even coefficients vanish and $b_k=a^0_{2k-1}$ solves (B.50)) and (b) (comparison $a_k\ge a^0_k\ge0$ ); Theorem 3.3 (c) (sign symmetry $a^{(\lambda,\mu,\nu)}_k=(-1)^{k-1}a^{(\lambda,-\mu,\nu)}_k$ ); the lower-bound propagation $b_k\ge c^*\rho^{*k}k^{\alpha-1}$ of §B.1.2 ( $\alpha\le1$ ); the Riemann-sum bound (B.52) with $\widetilde B(\alpha)>0$ ; and the lower-bound propagation of §B.2.2 ( $\alpha>1$ ).

Significance

The lower bound $\tau_*$ is an explicit, parameter-dependent time up to which the series converges absolutely: on $[0,\tau_*)$ the Riccati solution, and with it the rough Heston characteristic function, can be evaluated by summing a series with no discretization error. The upper bound shows that for parameters of equal sign the radius is finite and of order $(\lambda\nu)^{-1/(2\alpha)}$ , which is why the paper's hybrid scheme (series near $0$ , a numerical scheme beyond) is needed for long maturities. The two bounds together fix the scale on which the hybrid scheme switches methods.

The result is proved in the paper (Appendix B). The proof has not been machine-checked. A formal development adds a checked convergence guarantee for a recursion used in option-pricing code, and its auxiliary results (Kershaw's inequality for the Gamma function, which the pinned Mathlib does not contain, and Riemann-sum bounds for symmetric monotone functions) are reusable outside this paper. The paper prints a strict inequality $R>\tau_*$ ; its proof gives $R\ge\tau_*$ , which is what the goal asks. Upgrading to the strict inequality would be a sharpening beyond the paper.

Difficulty

The obvious approach is to bound $|a_k|$ by a geometric sequence $C\rho^k$ and propagate the bound by induction through the recursion. It fails: the convolution $\sum_{\ell=1}^{k-1}\rho^\ell\rho^{k-\ell}$ contributes a factor $k-1$ that the Gamma ratio $\Gamma(\alpha k+1)/\Gamma(\alpha k+\alpha+1)\approx(\alpha k)^{-\alpha}$ absorbs only when $\alpha\ge1$ , and then with constants that are far from sharp. The propagated bound therefore needs a polynomial correction $k^{\alpha-1}$ . That turns the convolution into a Riemann sum of $(x(1-x))^{\alpha-1}$ , which is convex for $\alpha\le1$ and concave for $\alpha\ge1$ , and controlling it takes a non-asymptotic Gamma-ratio inequality valid for every $k\ge1$ rather than Stirling asymptotics. For the upper bound on the radius, the coefficients must be bounded from below, which requires positivity, the vanishing of the even coefficients when $\mu=0$ , and a separate comparison between the cases $\mu\ge0$ , $\mu=0$ and $\mu\le0$ .

Formalization scope

Everything is stated about the coefficient sequence and its Hadamard radius. The fractional derivative, the Riccati equation itself and the function $\psi$ do not appear, as in the paper, which identifies the coefficients formally. Conventions:

Indexing. coeff α lam mu nu : ℕ → ℂ, with $a_0=0$ ; the convolution at index $j$ runs over $\ell\in\{1,\dots,j-1\}$ (Finset.Ico 1 j). Gamma factors are Real.Gamma of real arguments, cast to $\mathbb C$ ; for $\alpha>0$ every argument is at least $1$ .
Radius. radius α a = liminf_{k→∞} ‖a k‖₊^{-1/(α k)} in ℝ≥0∞, with $0^{-x}=+\infty$ for $x>0$ , so vanishing coefficients (all even ones when $\mu=0$ ) do not lower the radius. Real bounds enter through ENNReal.ofReal.
Beta function through Gamma, $B(a,b)=\Gamma(a)\Gamma(b)/\Gamma(a+b)$ .
Real parameters (Proposition B.1, Theorem 3.3 (b)–(c), the lower-bound propagations) are real numbers cast into $\mathbb C$ ; coefficient inequalities are stated on real parts.
Hypotheses relative to the page: $0<\alpha\le2$ for the printed " $\alpha\in[0,2]$ "; $\nu\ne0$ from the standing Assumption 3.1 ( $\lambda\nu\ne0$ ); $|\mu|^2$ for the printed $\mu^2$ under the square roots; $\tau_*\le R$ in place of the printed $R>\tau_*$ ; $(-1)^{k-1}$ for the printed $(-1)^k$ in Theorem 3.3 (c); $\lambda\nu$ in the numerator of the §B.1.2 constant $\rho^*$ . Lemma A.1 uses exactly its stated hypotheses; its printed "hence convex" claim does not follow from them and is not needed for its inequalities.

A trivializing formalization is excluded: the radius is Hadamard's $\liminf$ in $[0,+\infty]$ , not a supremum of convergence points computed in $\mathbb R$ (which would be $0$ on an unbounded set), and the recursion carries the paper's $a_0=0$ and $\ell=1,\dots,k-1$ conventions, so that $a_2=\mu\nu/\Gamma(2\alpha+1)$ and, at $\alpha=1,\lambda=\nu=1,\mu=0$ , the coefficients are those of $\tan$ ( $1,0,\tfrac13,\dots$ ), with $\tau_*=1$ and $R=\pi/2$ .

A complete development needs: real-analytic Gamma-function inequalities (log-convexity is in Mathlib; Kershaw's bounds are not); Riemann-sum estimates for symmetric monotone functions on $(0,1)$ ; the Beta integral $\int_0^1(u(1-u))^{\alpha-1}du=B(\alpha,\alpha)$ (Mathlib has Complex.betaIntegral); and $\liminf$ manipulations of $n$ -th roots in ℝ≥0∞. The Gamma-ratio and Riemann-sum lemmas are reusable beyond this mission. Contributions to any milestone, and alternative proofs of the radius bounds, are welcome.

Not formalized: the "Moreover" sentences of Theorem 3.3 (b) (monotonicity and blow-up of the maximal Riccati solution) and (c) (convergence at the radius), the non-homogeneous Theorem 6.1, and the numerical scheme of §4–§5.

Selected references

G. Callegaro, M. Grasselli, G. Pagès, Fast Hybrid Schemes for Fractional Riccati Equations (Rough is not so Tough), Mathematics of Operations Research 46(1), 2021; arXiv:1805.12587v4. https://arxiv.org/abs/1805.12587
O. El Euch, M. Rosenbaum, The characteristic function of rough Heston models, Mathematical Finance 29(1):3–38, 2019. https://doi.org/10.1111/mafi.12173
D. Kershaw, Some extensions of W. Gautschi's inequalities for the gamma function, Mathematics of Computation 41(164):607–611, 1983. https://doi.org/10.1090/S0025-5718-1983-0717710-7
E. Abi Jaber, M. Larsson, S. Pulido, Affine Volterra processes, Annals of Applied Probability 29(5):3155–3200, 2019; arXiv:1708.08796. https://arxiv.org/abs/1708.08796

13 thms1 active userReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Courier Dispatch in On-Demand Delivery II: In a Crowded Market with Endogenous Demand, Batch Delivery Earns More Exactly Below One Threshold in Wait Cost and in Service RadiusResearch Paper

Why dispatch and pricing interact

A delivery vendor controls both how a courier serves orders and what customers pay. Serving one order per trip avoids waiting for a second order, but serving two together can save travel time when demand is high. If the vendor can change its price, it also changes the rate at which customers join the system. The preferred dispatch rule therefore depends on an economic decision as well as a queueing calculation. Chen and Hu study this interaction for a single courier in a disk-shaped market and compare the vendor's revenue under dedicated and two-order batch delivery in their paper. The present mission concerns their crowded-market results, Propositions 3 and 4, in the authors' SSRN version of 2022-09-21.

The paper first analyzes fixed demand rates, then lets the vendor choose a demand rate by setting a price. The latter decision changes the comparison: customers with a high cost of waiting favor a less crowded, dedicated service, while sufficiently patient customers can make batching more profitable. The service radius has an analogous effect. The paper's threshold is expressed through the product of wait cost and radius, so these two comparative statics describe the same switch Chen and Hu, §5 and Online Appendix A.

Delivery model and limiting revenue

A vendor is located at the center of a disk of radius $r>0$ . Customers arrive at locations uniformly distributed over that disk. The vendor has one courier and chooses between dedicated delivery, one order per round trip, and batch delivery, two orders per trip. The effective demand rate is $\lambda$ . A customer incurs wait cost at rate $c>0$ and has a valuation in $[0,1]$ . The vendor's price induces its chosen demand rate. Chen and Hu give the dedicated service rate $\mu_D=3/(4r)$ and batch service rate $\mu_B=45\pi/[4r(32+15\pi)]$ in equations (4) and (9).

The paper uses the following expected waiting times, with variation coefficients $C_D=9/8$ and $C_B\approx0.583$ :

W_D(\lambda,\mu,C)=\frac{\lambda C}{2\mu(\mu-\lambda)},\qquad W_B(r,\lambda,\mu,C)=\frac{1}{2\lambda}+\frac{\lambda C}{2\mu(2\mu-\lambda)}+\frac r3.

Dedicated delivery is evaluated for $0\le\lambda<\mu_D$ ; batch delivery for $0<\lambda<2\mu_B$ . The first batch term is the wait to form a pair. The final term represents travel while the other order is delivered. The batch in-line wait is the paper's Kingman-based approximation for an $E_2/G/1$ queue, whereas the dedicated in-line wait uses its $M/G/1$ expression equations (5), (11), and (12).

In a finite market, the valuation distribution affects the price needed to induce demand. As the potential arrival rate grows, the paper's crowded-market revenue becomes

V_\infty(\lambda,w)=\lambda(1-cw).

For each dispatch rule, insert its wait into this function and optimize over its stable demand range. The resulting optimal revenues are denoted $\operatorname{Opt}_D(c,r)$ and $\operatorname{Opt}_B(C_B,c,r)$ . The mission uses suprema to express these values. The paper motivates this limiting objective in (14)–(15) and Lemma 1 (16)–(17).

Formalization targets

One threshold for both parameters

The goal is a single $\alpha^*>0$ such that, for every $c,r>0$ ,

\operatorname{Opt}_B(C_B,c,r)>\operatorname{Opt}_D(c,r)\quad\Longleftrightarrow\quad cr<\alpha^*, \qquad \operatorname{Opt}_D(c,r)>\operatorname{Opt}_B(C_B,c,r)\quad\Longleftrightarrow\quad cr>\alpha^*.

Thus the wait-cost threshold at a fixed radius is $c_\infty=\alpha^*/r$ , and the radius threshold at a fixed wait cost is $r_\infty=\alpha^*/c$ . At the threshold the two optimized revenues agree. For the paper's numerical $C_B=0.583$ , it reports $\alpha^*\approx0.1355$ Online Appendix (A.7)–(A.8).

Demand and price at the switch

As either $c$ or $r$ increases through its threshold, the optimal demand rate has a downward jump and the corresponding optimal price has an upward jump. The formal statements require both one-sided limits to exist and the inequalities between them to be strict. They cover every selection of optimal demands, including any ambiguity at the tie. These are parts (ii) of Propositions 3 and 4.

The milestones cover strict concavity of the revenue objectives, their explicit optimizers and values where attained, the single crossing of the revenue gap, the demand comparison at the tie, and the two propositions individually. The goal combines those propositions through the common product $cr$ .

What the result and formalization establish

The threshold tells the vendor which dispatch rule maximizes limiting revenue after the price has been adjusted optimally. It also locates a discontinuous operational change: a small movement in customer impatience or service area across the threshold changes the chosen mode, demand rate, and price. Comparing the waiting-time formulas at one fixed demand would not provide this revenue decision, because each mode can choose a different demand rate Chen and Hu, §5.

Chen and Hu prove the paper result analytically, while the threshold and its supporting claims here are proposed Lean statements awaiting proofs. A completed formalization would connect exact claims about the rational waiting-time expressions, optimization over open stability ranges, the unique revenue crossing, and one-sided limits. It would also record which conclusions use the paper's approximated batch wait and numerically estimated coefficient. These are reusable patterns for queue-based pricing models, even though this mission formalizes this paper's particular geometry and service rules.

Where the argument is delicate

The two dispatch modes have different singular boundaries and different optimizers. The batch wait diverges as demand tends to zero, yet batch revenue can have a finite boundary supremum that is not attained for some parameter values. The dedicated objective has a different service-rate pole. Consequently, replacing either optimization with an unrestricted real supremum, or asserting that every batch supremum has a maximizer, changes the claim. The revenue comparison also needs one crossing for the full positive range of $cr$ , including values beyond the range where the appendix's interior batch optimizer applies. Finally, a strict jump in demand does not by itself supply the existence of both one-sided limits; the formal statements ask for those limits explicitly Online Appendix A.

Formalization scope

Lean uses real-valued $r,c,\lambda$ and the paper's closed-form waits, service rates, and limiting revenue. The name lam denotes $\lambda$ . The batch coefficient is a real parameter satisfying $0.58\le C_B\le0.59$ , an explicit interval around the paper's numerical $0.583$ rather than a claimed exact evaluation of its integral. Every threshold statement assumes $c,r>0$ ; the auxiliary optimum statements use the page's $cr<T_B$ range when they assert an interior maximizer. The domains are $[0,\mu_D)$ and $(0,2\mu_B)$ , with zero excluded for batch because its $1/(2\lambda)$ wait is singular. The optimal revenues are defined as suprema of the actual objective images. The threshold is existential and is never defined from the desired answer.

The formal development does not construct the Poisson arrival process, random trip lengths, $M/G/1$ queue, or $E_2/G/1$ approximation behind the waits. It takes the paper's equations (5) and (12) as definitions. The finite-density function $V_n$ is recorded for context, but Lemma 1's convergence from finite to limiting optimized revenue is outside this mission's milestone list; the goal is explicitly the crowded-market limit. The printed (A.6)–(A.8) contain a coefficient error in the batch value, so the formal batch value uses the corrected expression and defines the revenue gap directly from the suprema. The printed batch optimization interval includes zero, which the stated waiting-time formula does not support. Definitions for objectives, stable domains, optimal demand, and one-sided jumps are reusable within related pricing formalizations. Contributions that establish the stated optimizer, crossing, or limit claims without changing their domains are within scope Chen and Hu, equations (12), (15), (A.3)–(A.8).

Selected references

Mingliu Chen and Ming Hu, Courier Dispatch in On-Demand Delivery, SSRN preprint 3675063, version of 2022-09-21. SSRN record and paper.
Mingliu Chen and Ming Hu, Courier Dispatch in On-Demand Delivery, Management Science, 2023, DOI 10.1287/mnsc.2023.4858. The formal statements use the SSRN version above.

10 thms1 active userReviewed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Mechanism Design under Approximate Incentive Compatibility 4: Randomized Perturbed Delayed Mechanisms Gain Ω(ε^(α/(2α−1))) Revenue Under Local α-Power EnvelopesResearch Paper

Motivation

Classical mechanism design assumes that agents optimize exactly: a buyer facing a menu of lotteries picks the one that maximizes expected utility, and an incentive compatible (IC) mechanism makes truth-telling optimal. Buyers that are only approximately rational, or that face small costs of computing or reporting, need only be made to prefer the truth up to a slack $\varepsilon$ . Approximate incentive compatibility ( $\varepsilon$ -IC) is the corresponding relaxation of the IC constraints. It is also used in computer science as a robustness notion and in learning settings where a mechanism is only approximately optimal for the buyer.

Balseiro, Besbes and Castro (arXiv:2103.03403) ask how much revenue a seller of one item can gain from such a relaxation. For a single buyer, Myerson's theory gives the IC optimum as a posted price. With $\varepsilon$ -IC the feasible set grows, and the paper determines the order of the additional revenue as $\varepsilon\downarrow 0$ .

Timeline. The rounding argument attributed to Noam Nisan, first used by Balcan, Blum, Hartline and Mansour (FOCS 2005), turns an $\varepsilon$ -IC mechanism into an IC one with a small revenue loss; for a single buyer it bounds the gain by $O(\sqrt\varepsilon)$ for every distribution (Proposition 1 of the paper). Balseiro, Besbes and Castro (2021; v2 2022; Operations Research 2024) prove an $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ upper bound (Theorem 1) under a curvature condition on the revenue curve, show that deterministic mechanisms gain only $\Theta(\varepsilon)$ (Theorem 2), and give a matching $\Omega(\varepsilon^{\alpha/(2\alpha-1)})$ lower bound by an explicit randomized construction (Theorem 3). This mission formalizes the lower bound.

Setting

A seller sells one item to one buyer. The buyer's value $v$ has a cumulative distribution function $F$ with density $f$ supported on $S=[0,\bar v]$ , $\bar v>0$ . Assumption 1 requires $f$ to have bounded variation on $S$ . Write $\bar F=1-F$ , the revenue curve $R(v)=v\,\bar F(v)$ (the revenue of a posted price $v$ ), and $\dot R(v)=\bar F(v)-v f(v)$ .

A direct mechanism $m=(x,t)$ gives a buyer who reports $v$ the item with probability $x(v)\in[0,1]$ and charges $t(v)$ . It is individually rational (IR) if $v\,x(v)-t(v)\ge 0$ for all $v\in S$ , and $\varepsilon$ -incentive compatible (IC $_\varepsilon$ ) if

v\,x(v)-t(v)\ \ge\ v\,x(v')-t(v')-\varepsilon\qquad\forall v,v'\in S.

$\mathcal M(\varepsilon)$ is the set of IR and IC $_\varepsilon$ mechanisms, $\Pi(m)=\int_0^{\bar v}t(v)f(v)\,dv$ the expected revenue, and $\Pi^\star(\mathcal M(\varepsilon))=\sup_{m\in\mathcal M(\varepsilon)}\Pi(m)$ . A best reporting mapping $v^\star$ for $m$ picks, for each value $v$ , a report in $\arg\max_{w\in S}\{v\,x(w)-t(w)\}$ .

Local $\alpha$ -power envelopes (Definition 1): $R$ has a unique maximizer $p^\star$ on $S$ , interior, and there are $\alpha>1$ , $\kappa_L,\kappa_U>0$ and $\ell>0$ with $(p^\star-\ell,p^\star+\ell)\subset(0,\bar v)$ and

\kappa_L\alpha|v-p^\star|^\alpha\le(p^\star-v)\,\dot R(v)\le\kappa_U\alpha|v-p^\star|^\alpha\quad\text{on }(p^\star-\ell,p^\star+\ell).

The parameter $\alpha$ measures how flat $R$ is at its peak; $\alpha=2$ is the generic smooth case.

Perturbed delayed mechanisms (§5.1). For $\mu,\delta>0$ the buyer is steered to report $v^\star(v\,|\,\mu,\delta)$ , equal to $0$ below $p^\star-\delta$ , to $v-\mu$ on $[p^\star-\delta,p^\star+\delta+\mu]$ , and to $p^\star+\delta$ above. With $w$ its generalized inverse, the allocation $x_{pd}$ solves on $[0,p^\star+\delta]$ the ordinary and delay differential equations

\dot x(v)=\frac{x(v)}{w(v)-v}\ \ (v\le p^\star-\delta),\qquad x(0)=\frac{\varepsilon}{p^\star-\delta},\qquad \dot x(v)=\frac{x(v)-x(v^\star(v))}{w(v)-v}\ \ (p^\star-\delta\le v\le p^\star+\delta),

is $1$ above $p^\star+\delta$ , and the payment $t_{pd}$ is given explicitly in terms of $x_{pd}$ and $v^\star$ .

Formalization targets

Goal: Theorem 3 (p. 27)

Under Assumption 1 and local $\alpha$ -power envelopes there are $C>0$ and $\varepsilon_0>0$ such that for all $\varepsilon\in(0,\varepsilon_0]$ some $m\in\mathcal M(\varepsilon)$ satisfies

\Pi(m)\ \ge\ \Pi^\star(\mathcal M(0))+C\,\varepsilon^{\alpha/(2\alpha-1)} .

The constants may depend on the distribution, but not on $\varepsilon$ .

Milestones

Lemma 5 (p. 59): solutions of (ODE)-(DDE) are non-decreasing on $[0,p^\star+\delta]$ .
Proposition 3 (p. 31): if $x_{pd}(v)\to 1$ as $v\uparrow p^\star+\delta$ , then $v^\star(\cdot\,|\,\mu,\delta)$ is a best reporting mapping for $m_{pd}$ .
Proposition 4 (p. 33): the system has a unique solution on $[0,p^\star+\delta]$ , which is positive, non-decreasing and given in closed form (eq. (25)).
Lemma 6 (p. 60): with $\Gamma(t)=\sum_{j=0}^{\lfloor t\rfloor+1}\frac{(-1)^je^{-j}}{j!}(t+1-j)^j$ ,

2(t+1)e^{-1}e^{-t}<\Gamma(t)\le2(t+2)e^{-(t+1)}\qquad(t\ge0).

Proposition 5 (p. 34): for $\mu>\varepsilon e$ some $\delta\in[\mu^2/(4\varepsilon)-\mu,\ \mu^2/(4\varepsilon)]$ makes $x_{pd}$ reach $1$ at $p^\star+\delta$ , and then $m_{pd}\in\mathcal M(\varepsilon)$ .
Proposition 6 (p. 35): the revenue identity

\Pi(m_{pd})=\int_0^{p^\star+\delta}x_{pd}(v)\big(vf(v)-\bar F(v+\mu)\dot w(v)\big)dv+R(p^\star+\delta)+\int_{p^\star+\delta}^{p^\star+\delta+\mu}\bar F(v)\,dv .

Significance

The result. Theorem 3 shows that the $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ upper bound of Theorem 1 is tight up to the logarithm. Since $\alpha/(2\alpha-1)<1$ for $\alpha>1$ , the revenue gain from approximate incentive compatibility is supralinear in $\varepsilon$ : a seller who exploits $\varepsilon$ -optimizing buyers gains strictly more than the order- $\varepsilon$ gain available to deterministic mechanisms (Theorem 2). Randomization is therefore what makes the relaxation valuable, and the curvature $\alpha$ of the revenue curve at the optimal price determines the exponent, which ranges from $1$ (as $\alpha\downarrow1$ ) to $1/2$ (as $\alpha\to\infty$ ), the latter matching Nisan's universal bound.

Formalizing it. The result is proved in the paper's online appendix; none of it is formalized. A formal development would supply a machine-checked revenue lower bound for an explicit class of $\varepsilon$ -IC mechanisms, a formal treatment of a linear delay differential equation with a piecewise history (method of steps, closed-form solution), and the two-sided bound on $\Gamma$ , which the paper derives from the renewal function of uniform interarrival times.

Difficulty

The obvious approach, perturbing the optimal posted price or a hard/soft floor mechanism, gains only order $\varepsilon$ (Theorem 2). To gain more, the mechanism must make the buyer misreport downward in a coordinated way, and the allocation that sustains a prescribed misreporting strategy is the solution of a delay differential equation. Three steps are delicate: showing that this solution exists, is unique and is monotone (the delay term couples $x(v)$ to $x(v-\mu)$ ); choosing the delay $\delta$ so that the allocation reaches exactly $1$ at $p^\star+\delta$ , which requires the sharp two-sided bound on $\Gamma$ and an intermediate value argument; and verifying global $\varepsilon$ -IC, since a best-response argument must rule out every deviation, not only local ones. The final bound balances the gain $\bar F(p^\star+\delta+\mu)\,\mu$ against losses of order $\kappa_U(\delta+\mu)^\alpha$ , with $\mu$ of order $\varepsilon^{\alpha/(2\alpha-1)}$ .

Formalization scope

Values are reals, every function is a total function $\mathbb R\to\mathbb R$ whose values matter only on $S=[0,\bar v]$ , and the density is integrable on $S$ with total mass $1$ . Mechanisms are required to be measurable, which the expectation $\mathbb E_v[t(v)]$ presumes. $\Pi^\star$ is a supremum (sSup); the goal is stated with an explicit witness $m\in\mathcal M(\varepsilon)$ , which is equivalent because the revenue image is nonempty and bounded above by $\bar v$ . $\dot R$ is defined as $\bar F-vf$ , not as a derivative. The $\Omega$ constants are quantified after the distribution and before $\varepsilon$ .

The derivatives in (ODE)-(DDE) are one-sided at the endpoints of their closed intervals. At $p^\star-\delta$ the two right-hand sides differ, so a two-sided derivative would make the system unsolvable and every statement about its solutions vacuous; this encoding rules out that trivialization. The goal does not mention perturbed delayed mechanisms: any witness is acceptable.

Disclosed additions relative to the page: $\mu\le p^\star-\delta$ in the §5.1 statements (presumed by the paper's definition of $w$ ); Propositions 3–6 and Lemma 5 are stated for any price $p^\star$ with $0<\delta<p^\star$ and $p^\star+\delta+\mu<\bar v$ , since their proofs never use optimality of $p^\star$ ; in Proposition 6 the integrand $\psi\cdot f$ is written in product form because $\psi$ divides by $f$ .

A complete development needs: absolutely continuous distribution functions and integration by parts on intervals; existence and uniqueness for linear ODEs and for a delay equation by the method of steps; Irwin–Hall distributions or a direct analytic bound for Lemma 6; and the intermediate value theorem. The delay-equation and $\Gamma$ results are reusable outside mechanism design. Contributions to any milestone, and alternative proofs of Lemma 6, are welcome.

Selected references

S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403
M.-F. Balcan, A. Blum, J. D. Hartline, Y. Mansour, Mechanism Design via Machine Learning, FOCS 2005, 605–614. https://doi.org/10.1109/SFCS.2005.50
R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 58–73, 1981. https://doi.org/10.1287/moor.6.1.58
P. Milgrom, I. Segal, Envelope Theorems for Arbitrary Choice Sets, Econometrica 70(2), 583–601, 2002. https://doi.org/10.1111/1468-0262.00296
R. D. Driver, Ordinary and Delay Differential Equations, Springer, 1977 (reprint 2012). https://doi.org/10.1007/978-1-4684-9467-9

10 thms1 active userReviewed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

A Generalized Newton Method for Subgradient Systems 2: Under Metric Regularity and Semismoothness*, the FBE-Based Newton Algorithm Converges Superlinearly in Quadratic Composite OptimizationResearch Paper

Motivation

Many optimization models in statistics, signal processing and machine learning minimize a smooth loss plus a nonsmooth regularizer, $\min_x f(x)+g(x)$ . When $f$ is quadratic this is the quadratic composite problem, which also appears as the subproblem of sequential quadratic programming and of proximal Newton methods. First-order splitting methods (proximal gradient, forward-backward) handle such problems with only the proximal mapping of $g$ , but converge at best linearly. Newton-type methods converge superlinearly but classically need either smoothness or convexity of $g$ , or strong regularity (uniqueness and Lipschitz stability) of the solution.

Khanh, Mordukhovich and Phat (arXiv:2009.10551v2, 2022; Mathematics of Operations Research 2023) designed a Newton-type method for the stationarity inclusion $0\in\partial\varphi(x)$ of a nonconvex composite cost whose steps use only the proximal mapping and the second-order subdifferential (generalized Hessian) of $g$ , and proved local superlinear convergence under metric regularity rather than strong metric regularity. This mission formalizes that result, Theorem 7.8 of the paper, together with the chain of propositions through which it is proved.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product. A function $g:\mathbb R^n\to(-\infty,+\infty]$ is proper if it is finite somewhere, and prox-bounded if it is bounded below by a quadratic $-a\|x\|^2-c$ . The limiting subdifferential $\partial g(x)$ collects limits of Fréchet subgradients at nearby points with nearby values.

For a set-valued map $G:\mathbb R^n\rightrightarrows\mathbb R^m$ the limiting coderivative $D^*G(x,y)(w)$ is the set of $u$ with $(u,-w)$ a limiting normal to $\operatorname{gph}G$ at $(x,y)$ ; the second-order subdifferential is $\partial^2g(x,v)=D^*(\partial g)(x,v)$ . $G$ is metrically regular around $(\bar x,\bar y)$ if $\operatorname{dist}(x;G^{-1}(y))\le\mu\operatorname{dist}(y;G(x))$ near $(\bar x,\bar y)$ , and semismooth* at $(\bar x,\bar y)$ if $\langle u^*,u\rangle=\langle v^*,v\rangle$ for every $u^*$ in the directional coderivative $D^*G((\bar x,\bar y);(u,v))(v^*)$ .

$g$ is prox-regular at $\bar x$ for $\bar v\in\partial g(\bar x)$ with modulus $r>0$ if it is lower semicontinuous near $\bar x$ and, for some $\varepsilon>0$ ,

g(x)\ge g(u)+\langle v,x-u\rangle-\tfrac r2\|x-u\|^2

for $x,u$ within $\varepsilon$ of $\bar x$ , $|g(u)-g(\bar x)|<\varepsilon$ and $v\in\partial g(u)$ within $\varepsilon$ of $\bar v$ ; continuously prox-regular if in addition $g(x_k)\to g(\bar x)$ along subgradient pairs $(x_k,v_k)\to(\bar x,\bar v)$ .

The cost is $\varphi=f+g$ with $f(x)=\tfrac12\langle Ax,x\rangle+\langle b,x\rangle+\alpha$ , $A$ symmetric. The proximal mapping $\operatorname{Prox}_{\gamma g}(u)$ is the argmin set of $y\mapsto g(y)+\frac1{2\gamma}\|y-u\|^2$ , and the forward-backward envelope (FBE) is

\varphi_\gamma(x)=\inf_y\Big\{f(x)+\langle\nabla f(x),y-x\rangle+g(y)+\tfrac1{2\gamma}\|y-x\|^2\Big\}.

Algorithm 7.6 with parameter $\gamma$ : if $0\in\partial\varphi(x^k)$ stop; otherwise set $u^k=x^k-\gamma(Ax^k+b)$ , pick $v^k\in\operatorname{Prox}_{\gamma g}(u^k)$ , choose $d^k$ with

-\tfrac1\gamma(x^k-v^k)-Ad^k\in\partial^2g\big(v^k,\tfrac1\gamma(u^k-v^k)\big)(x^k-v^k+d^k),

and set $x^{k+1}=x^k+d^k$ .

Formalization targets

Goal: Theorem 7.8

Let $g$ be proper, prox-bounded and continuously prox-regular at a stationary point $\bar x$ ( $0\in\partial\varphi(\bar x)$ ) for $-A\bar x-b$ with modulus $r$ , and let $\partial\varphi$ satisfy at $(\bar x,0)$ : (H1) solvability of $-v\in\partial^2\varphi(x,v)(d)$ near $(\bar x,0)$ , (H2) metric regularity, (H3) semismoothness*. Then

\exists\gamma_0\in(0,r^{-1}]\ \forall\gamma\in(0,\gamma_0)\ \text{with }I-\gamma A\text{ nonsingular}\ \exists U\ni\bar x:\ \text{Algorithm 7.6 is well-defined from }U,

and every run from $x^0\in U$ converges Q-superlinearly to $\bar x$ .

Milestones

Theorem 5.7: the same conclusion for the $C^{1,1}$ Newton method $-\nabla\varphi(x^k)\in\partial\langle d^k,\nabla\varphi\rangle(x^k)$ .
Proposition 7.2: near $\bar x$ , the prox-gradient map is single-valued and Lipschitz, $\varphi_\gamma$ is $C^1$ with $\nabla\varphi_\gamma(x)=\gamma^{-1}(I-\gamma\nabla^2f(x))(x-\operatorname{Prox}_{\gamma g}(x-\gamma\nabla f(x)))$ , and $\nabla\varphi_\gamma(x)=0\iff0\in\partial\varphi(x)$ .
Proposition 7.3: the generalized Hessian of $\varphi_\gamma$ in terms of $\partial^2 g$ .
Remark 7.7: a step of Algorithm 7.6 is a step of Algorithm 5.3 for $\varphi_\gamma$ .
Proposition 7.4(i): $\partial\varphi$ is metrically regular iff $\nabla\varphi_\gamma$ is.
Proposition 7.5: semismoothness* of $\partial g$ passes to $\nabla\varphi_\gamma$ .

Significance

The result gives a locally superlinear method for nonconvex composite problems that uses only first- and second-order information of the regularizer, and it replaces strong metric regularity, which forces isolated solutions, by metric regularity. The FBE reduction (Propositions 7.2–7.5) is reusable on its own: it identifies the stationary points, the generalized Hessian, and the regularity of a nonsmooth composite cost with those of a smooth function.

Formalizing it builds the first machine-checked library of coderivative calculus on Prove2Me: normal cones to graphs, limiting and directional coderivatives, second-order subdifferentials, metric regularity and semismoothness*. As far as the platform record shows, none of the paper's results has a machine-checked proof. The paper's proofs lean on second-order sum and chain rules from Mordukhovich's monograph and on Poliquin–Rockafellar's analysis of Moreau envelopes of prox-regular functions; those external results are part of the work.

Difficulty

The FBE of a nonconvex $g$ is not globally smooth; its smoothness near $\bar x$ comes from the local single-valuedness of $\operatorname{Prox}_{\gamma g}$ , which prox-regularity provides only for small $\gamma$ and only near $\bar x-\gamma\nabla f(\bar x)$ . The printed parameter range $\gamma\in(0,r^{-1})$ is too large: a far-away deep well of $g$ can capture the proximal point (see the correction below). Transferring (H1)–(H3) from $\partial\varphi$ to $\nabla\varphi_\gamma$ requires exact second-order calculus (sum and chain rules for coderivatives), not inclusions, and metric regularity is not preserved by the obvious estimates: the paper uses a coderivative characterization. Finally, Theorem 5.7 itself requires an inexact Newton analysis in which the Newton inclusion is solved by an arbitrary element of a coderivative, not by a matrix.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); products carry the sup norm, which does not change any normal cone. A symmetric $A$ is a self-adjoint continuous linear operator.
$g$ and $\varphi$ take values in EReal; $g$ is assumed proper. The envelopes are EReal-valued infima; wherever $\varphi_\gamma$ is differentiated, finiteness on a neighbourhood is asserted and the real-valued function is differentiated. $\nabla^2 f(x)$ is the derivative of gradient f.
$\partial$ is the published analytic limiting subdifferential NonconvexSplitting.Shared.LimitingSubdiff. It agrees with the paper's geometric definition (2.9) for functions lower semicontinuous around the point, which covers every function the statements apply it to.
Metric regularity uses $\operatorname{dist}(\cdot;\emptyset)=+\infty$ . Directional normals read $t_k\downarrow0$ as $t_k>0$ , $t_k\to0$ . For a $C^{1,1}$ or $C^1$ function, $\partial^2\varphi(x)$ is the coderivative of the single-valued gradient map.
The proximal mapping is the argmin set; runs may select any proximal point and any direction solving the Newton inclusion; conclusions hold for every run. The stop rule is a constant tail. "Well-defined from $U$ " means every partial run from $U$ can be continued. Q-superlinear convergence is in $\varepsilon$ -form, which avoids the ratio $0/0$ .
Correction. Propositions 7.2–7.5, Remark 7.7 and Theorem 7.8 are claimed for every $\gamma\in(0,r^{-1})$ ; that is false. For $n=1$ , $A=0$ , $b=0$ and $g(y)=\tfrac12y^2$ on $[-5,5]$ , $g(y)=-1000-|y-10|$ on $[9,11]$ , $+\infty$ elsewhere ( $\bar x=0$ , $r=1$ , $\gamma=\tfrac12$ ), $\operatorname{Prox}_{\gamma g}=\{9\}$ near $0$ and every run jumps to the stationary point $9$ . All these items are posed as "there is $\gamma_0\in(0,r^{-1}]$ such that for every $\gamma\in(0,\gamma_0)$ ", the range the cited Poliquin–Rockafellar theorem supports. Theorem 5.7 is posed as printed.
The goal cannot be trivialized: $\gamma_0>0$ is asserted, the convergence is claimed for every run and every admissible $\gamma$ below $\gamma_0$ , and the hypotheses are satisfied, for instance, by $g=\tfrac12\|\cdot\|^2$ . Specializing $g$ to be convex, $A=0$ , $A$ positive definite, or $\bar x$ a tilt-stable minimizer would change the theorem and is not accepted.
Needed infrastructure: limiting normal cones and coderivatives, their sum and chain rules for a smooth plus a set-valued map, the Mordukhovich criterion, Moreau envelopes of prox-regular functions (Poliquin–Rockafellar). These are reusable well beyond this mission; contributions of any of them as separate theorems are welcome.

Selected references

P. D. Khanh, B. S. Mordukhovich, V. T. Phat, A Generalized Newton Method for Subgradient Systems, arXiv:2009.10551v2, 2022; Mathematics of Operations Research, 2023. https://arxiv.org/abs/2009.10551
B. S. Mordukhovich, Variational Analysis and Generalized Differentiation I: Basic Theory, Springer, 2006. https://doi.org/10.1007/3-540-31247-1
R. A. Poliquin, R. T. Rockafellar, Prox-regular functions in variational analysis, Transactions of the AMS 348 (1996) 1805–1838. https://doi.org/10.1090/S0002-9947-96-01544-9
H. Gfrerer, J. V. Outrata, On a semismooth* Newton method for solving generalized equations, SIAM Journal on Optimization 31 (2021) 489–517. https://doi.org/10.1137/19M1257408
P. Patrinos, A. Bemporad, Proximal Newton methods for convex composite optimization, IEEE CDC 2013. https://doi.org/10.1109/CDC.2013.6760233

13 thms1 active userReviewed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

A Generalized Newton Method for Subgradient Systems 1: Under Metric Regularity and Semismoothness*, the Prox-Based Newton Algorithm Converges Superlinearly for Prox-Regular FunctionsResearch Paper

Motivation

Many problems in optimization reduce to a subgradient inclusion $0\in\partial\varphi(x)$ : for a smooth $\varphi$ this is the gradient equation $\nabla\varphi(x)=0$ , and for an extended-real-valued $\varphi=f+g$ (a smooth loss plus an indicator or a nonsmooth regularizer) it is the first-order optimality condition of a composite problem. Newton's method is the classical way to solve such equations with a superlinear rate, but its textbook form needs $\varphi\in C^2$ and a nonsingular Hessian. Khanh, Mordukhovich and Phat (arXiv:2009.10551v2, 2022; Mathematics of Operations Research, 2023) design a Newton-type method in which the Hessian is replaced by Mordukhovich's second-order subdifferential $\partial^2\varphi$ , and prove local superlinear convergence under two assumptions that are weaker than the usual ones: metric regularity (instead of strong metric regularity or tilt stability) and the semismooth* property of Gfrerer and Outrata.

Timeline of the ingredients:

1996: Poliquin and Rockafellar introduce prox-regular functions and show that, for small parameters, their Moreau envelopes are $C^{1,1}$ near the reference point and their proximal mappings are single-valued and Lipschitz there (Trans. AMS 348).
2002: Klatte and Kummer develop Newton methods for Lipschitzian equations through generalized derivatives (Nonsmooth Equations in Optimization, Kluwer).
2021: Gfrerer and Outrata define semismooth* set-valued maps and a semismooth* Newton method (SIAM J. Optim. 31).
2021: Mordukhovich and Sarabi give a generalized Newton method for tilt-stable minimizers of prox-regular functions (SIAM J. Optim. 31).
2020/2022: Khanh, Mordukhovich and Phat replace tilt stability and strong metric regularity by metric regularity of $\partial\varphi$ .

Setting

Let $\varphi:\mathbb R^n\to(-\infty,\infty]$ be proper. Its limiting subdifferential $\partial\varphi(x)$ collects the limits of Fréchet subgradients at points $x_k\to x$ with $\varphi(x_k)\to\varphi(x)$ . For a set $\Omega$ , the regular normal cone $\widehat N_\Omega(z)$ contains the vectors $a$ with $\langle a,w-z\rangle\le o(\|w-z\|)$ for $w\in\Omega$ ; the limiting normal cone $N_\Omega(z)$ contains the limits of regular normals at nearby points. For a set-valued $G$ , the coderivative is $D^*G(x,y)(w)=\{u:(u,-w)\in N_{\operatorname{gph}G}(x,y)\}$ , and the second-order subdifferential is $\partial^2\varphi(x,v)=D^*\partial\varphi(x,v)$ .

The function $\varphi$ is prox-regular at $\bar x$ for $\bar v\in\partial\varphi(\bar x)$ with modulus $r>0$ if it is l.s.c. around $\bar x$ and, for some $\varepsilon>0$ , $\varphi(x)\ge\varphi(u)+\langle v,x-u\rangle-\tfrac r2\|x-u\|^2$ whenever $x,u$ lie within $\varepsilon$ of $\bar x$ , $|\varphi(u)-\varphi(\bar x)|<\varepsilon$ and $v\in\partial\varphi(u)$ lies within $\varepsilon$ of $\bar v$ . It is continuously prox-regular if, in addition, $\varphi(x_k)\to\varphi(\bar x)$ along every $(x_k,v_k)\to(\bar x,\bar v)$ with $v_k\in\partial\varphi(x_k)$ . It is prox-bounded if it is bounded below by a quadratic function.

For $\lambda>0$ , the Moreau envelope and proximal mapping are

e_\lambda\varphi(x)=\inf_y\Big\{\varphi(y)+\tfrac1{2\lambda}\|y-x\|^2\Big\},\qquad \operatorname{Prox}_\lambda\varphi(x)=\operatorname*{argmin}_y\Big\{\varphi(y)+\tfrac1{2\lambda}\|y-x\|^2\Big\}.

Algorithm 6.2 starts at $x^0\in U_\lambda=\operatorname{rge}(I+\lambda\partial\varphi)$ . While $0\notin\partial\varphi(x^k)$ it sets $v^k=\lambda^{-1}(x^k-\operatorname{Prox}_\lambda\varphi(x^k))$ , picks any $d^k$ with $-v^k\in\partial^2\varphi(x^k-\lambda v^k,v^k)(\lambda v^k+d^k)$ , and moves to $x^{k+1}=x^k+d^k$ .

The standing assumptions at a solution $\bar x$ are:

(H1) the inclusion $-v\in\partial^2\varphi(x,v)(d)$ is solvable for every $(x,v)\in\operatorname{gph}\partial\varphi$ near $(\bar x,0)$ ;
(H2) $\partial\varphi$ is metrically regular around $(\bar x,0)$ ;
(H3) $\partial\varphi$ is semismooth* at $(\bar x,0)$ .

Formalization targets

Goal: Theorem 6.6 (corrected parameter range)

If $\varphi$ is proper, prox-bounded, continuously prox-regular at $\bar x$ for $0\in\partial\varphi(\bar x)$ with constants $r,\varepsilon$ , and (H1)–(H3) hold, then

\exists\,\lambda_0\in(0,r^{-1}]\ \ \forall\lambda\in(0,\lambda_0)\ \ \exists\,U\in\mathcal N(\bar x),\ U\subseteq U_\lambda:\ \text{Algorithm 6.2 is well-defined from }U\text{ and every run from }U\text{ converges Q-superlinearly to }\bar x.

Milestones

Lemma 5.4: for continuous $F$ , metric regularity around $\bar x$ holds iff $\|v\|\ge c\|u\|$ for all $v\in D^*F(x)(u)$ , $x$ near $\bar x$ .
Lemma 5.6: $D^*F(\bar x)(u_1+u_2)\subseteq D^*F(\bar x)(u_1)+D^*F(\bar x)(u_2)$ for locally Lipschitz $F$ .
Lemma 5.5: for $C^{1,1}$ $\varphi$ , $\nabla\varphi$ is semismooth* at $\bar x$ iff $\nabla\varphi(x)-\nabla\varphi(\bar x)-\partial^2\varphi(x)(x-\bar x)\subseteq o(\|x-\bar x\|)$ .
Theorem 5.7: the $C^{1,1}$ Newton method (Algorithm 5.3) converges locally Q-superlinearly under (H1)–(H3) for $\nabla\varphi$ .
Lemma 6.3 (i)–(iii), corrected: near $\bar x+\lambda\bar v$ , and for $\lambda$ small, $e_\lambda\varphi$ is $C^{1,1}$ , $\operatorname{Prox}_\lambda\varphi$ is single-valued, monotone and Lipschitz, and $\nabla e_\lambda\varphi(x)=\lambda^{-1}(x-\operatorname{Prox}_\lambda\varphi(x))$ .
Lemma 6.4, corrected: $x^*\in D^*\nabla e_\lambda\varphi(x,v)(v^*)\iff x^*\in\partial^2\varphi(x-\lambda v,v)(v^*-\lambda x^*)$ .
Remark 6.5, corrected: the steps of Algorithm 6.2 are the steps of Algorithm 5.3 for $e_\lambda\varphi$ .

Significance

The result gives a Newton method for nonsmooth, nonconvex subgradient inclusions whose convergence does not require strong metric regularity. Example 5.2 of the paper exhibits a $C^{1,1}$ function whose gradient is metrically regular and semismooth* but not strongly metrically regular, so the theorem covers solutions that earlier generalized Newton theories exclude. Through the Moreau envelope, the method reduces to a $C^{1,1}$ gradient equation; the same reduction, with the forward–backward envelope, drives the paper's composite algorithm (the companion mission) and its applications to Lasso-type problems.

The paper's results are proved on paper; none of them, nor the underlying theory of coderivatives, second-order subdifferentials or semismooth* maps, is formalized in Mathlib. This mission produces a machine-checked development of that layer and of the convergence theorem. It also fixes a defect: as printed, Lemma 6.3 and Theorem 6.6 claim their conclusions for every $\lambda\in(0,r^{-1})$ , which is false (see Formalization scope); the formal statements are the corrected ones.

Difficulty

The obvious argument says "Algorithm 6.2 is Algorithm 5.3 for $e_\lambda\varphi$ , so apply Theorem 5.7". Each step of that sentence carries the difficulty. Transferring (H1)–(H3) from $\partial\varphi$ to $\nabla e_\lambda\varphi$ requires the coderivative of the inverse $(\lambda I+\partial\varphi^{-1})^{-1}$ , which needs a local graphical calculus for limiting normals that Mathlib does not have. The $C^{1,1}$ property of the envelope and single-valuedness of the proximal map hold only for small $\lambda$ and near $\bar x+\lambda\bar v$ : prox-regularity is local while $\operatorname{Prox}_\lambda\varphi$ minimizes globally, so a far-away deep well can capture the proximal point. Theorem 5.7 itself rests on a uniform coderivative bound from metric regularity (Lemma 5.4, a pointwise-to-uniform form of the Mordukhovich coderivative criterion) and on the semismooth* estimate (Lemma 5.5), which combines directional normal cones with the symmetry of generalized Hessians.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); definitions are stated on real inner product spaces, and $E\times F$ carries the sup norm (the cones are norm-independent).
$\partial$ is the published analytic limiting subdifferential NonconvexSplitting.Shared.LimitingSubdiff. It agrees with the paper's geometric (2.9) for functions l.s.c. around the point, which covers every function $\partial$ is applied to here.
$\varphi$ takes values in EReal and is assumed proper; the envelope is EReal-valued, and finiteness is asserted wherever it is differentiated.
$\operatorname{Prox}_\lambda\varphi(x)$ is the argmin set. A run of an algorithm selects any proximal point and any direction solving the Newton inclusion. The stop of Step 1 is a constant tail. Well-definedness means every partial run from $U$ can be continued.
Metric regularity uses $\operatorname{dist}(\cdot;\emptyset)=+\infty$ . Q-superlinear convergence is stated in $\varepsilon$ -form, avoiding $0/0$ . $C^{1,1}$ is local to a neighbourhood.
Correction. Lemma 6.3, Lemma 6.4, Remark 6.5 and Theorem 6.6 are posed as "there is $\lambda_0\in(0,r^{-1}]$ such that for every $\lambda\in(0,\lambda_0)$ ", on neighbourhoods instead of $U_\lambda$ . As printed they fail for $\varphi(y)=\tfrac12y^2$ on $[-5,5]$ , $-1000-|y-10|$ on $[9,11]$ , $+\infty$ elsewhere, with $\bar x=0$ , $r=1$ , $\lambda=\tfrac12$ : there $\operatorname{Prox}_\lambda\varphi(x)=\{9\}$ near $0$ , and Algorithm 6.2 jumps to the stationary point $9$ . Lemmas 5.4–5.6 and Theorem 5.7 are posed as printed.
Trivializing formalizations are ruled out: $\lambda_0>0$ is part of the conclusion, so the $\forall\lambda$ is never vacuous; conclusions hold for every run rather than for a run chosen by Classical.choose; and $\varphi$ is not specialized (no convexity, which would make $U_\lambda=\mathbb R^n$ ; no $C^2$ ; no strong metric regularity; no assumption that $\bar x$ is a minimizer).
Reusable infrastructure: normal cones to graphs, limiting and directional coderivatives, metric regularity, semismooth*, prox-regularity, Moreau envelopes. Formalizations of Mordukhovich's coderivative criterion, of the scalarization formula $D^*F(\bar x)(u)=\partial\langle u,F\rangle(\bar x)$ for Lipschitz $F$ , and of Poliquin–Rockafellar's Theorem 4.4 are especially welcome.

Selected references

P. D. Khanh, B. S. Mordukhovich, V. T. Phat, A Generalized Newton Method for Subgradient Systems, arXiv:2009.10551v2, 2022; Math. Oper. Res., 2023. https://arxiv.org/abs/2009.10551
R. A. Poliquin, R. T. Rockafellar, Prox-regular functions in variational analysis, Trans. Amer. Math. Soc. 348, 1996. https://doi.org/10.1090/S0002-9947-96-01544-9
H. Gfrerer, J. V. Outrata, On a semismooth Newton method for solving generalized equations*, SIAM J. Optim. 31, 2021. https://doi.org/10.1137/19M1257408
B. S. Mordukhovich, M. E. Sarabi, Generalized Newton algorithms for tilt-stable minimizers in nonsmooth optimization, SIAM J. Optim. 31, 2021. https://doi.org/10.1137/20M1329937
B. S. Mordukhovich, Variational Analysis and Generalized Differentiation I, Springer, 2006. https://doi.org/10.1007/3-540-31247-1
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

15 thms1 active userReviewed

Control Theory Economics Operations Research·Captain: mikedeng1

Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost IV: Low Switching Cost, Control-Band Value Functions Meet the Optimality ConditionsResearch Paper

Motivation

Many service relationships are dynamic contracts in which the principal cannot observe the agent's effort, only its noisy consequences. Cao, Sun and Tian (Management Science, 2024) study such a relationship when the principal can suspend the agent and must pay a fixed switching cost to restart work. Suspension is a punishment that does not end the relationship, and it is used in practice for platform workers, contractors and franchisees. The paper shows that, when the switching cost and the revenue are low, the optimal contract has a control-band structure: the agent's promised utility is kept inside an interval, the agent is suspended when it falls below the lower end, and work resumes at the upper end. Two-threshold policies of this kind are standard in optimal switching problems with switching costs (Duckworth and Zervos, 2001; Vath and Pham, 2007), whose verification arguments the paper compares with its own.

This mission is the fourth of a series formalizing the analytic core of the paper. It covers the low-switching-cost region (Area III of the paper's Figure 2).

Setting

A Poisson process of arrivals brings revenue $R$ each. The base arrival rate is $\underline\mu\ge0$ ; if the agent works, at cost $b>0$ per unit of time, the rate becomes $\mu>\underline\mu$ . Write $\Delta\mu=\mu-\underline\mu$ . The principal's cost rate while the agent works is $c\ge b$ , restarting work costs $K>0$ , and the principal and the agent discount at rates $0<r\le\rho$ . Assumption 1 is $R\Delta\mu>c$ . The constants are

\beta=\frac b{\Delta\mu},\quad \bar w=\frac{\beta\mu}\rho,\quad \underline v=\frac{\underline\mu R}r,\quad \bar V=\frac{R\mu-c-(\rho-r)\bar w}r,\quad \bar V(w)=\frac{R\mu-c-(\rho-r)w}r .

The promised utility $w\ge0$ is the state. For a function $f$ on $\mathbb R_+$ with left derivative $f'$ , the paper's operators are

(\mathcal A_If)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,

(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu,

for the working state $I$ and the suspended state $\emptyset$ . A pair $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) if $\mathcal A_IV_I\ge0$ , $\mathcal A_\emptyset V_\emptyset\ge0$ , $0\le V_I-V_\emptyset\le K$ and $V_I(0),V_\emptyset(0)\ge\underline v$ .

Two families of functions enter. In the suspended state, $V_c(w)=\underline v+w+c\,w^{r/\rho}$ (24) solves $\mathcal A_\emptyset V=0$ with $V(0)=\underline v$ . In the working state, for $\tilde w<\bar w$ , $V_{\tilde w}$ is the $C^1$ solution of the delay differential equation (25), in which $V(w)$ is coupled to the look-ahead value $V((w+\beta)\wedge\tilde w)$ , with $V_{\tilde w}=\bar V(\tilde w)$ beyond $\tilde w$ ; $\mathcal V_{\tilde w}$ is its concavification (Lemma 2), linear below a threshold $\check w(\tilde w)$ . Lemma 3's $\hat{\mathrm w}$ is the unique $\tilde w$ with $\mathcal V_{\tilde w}(0)=\underline v$ under Condition 1.

The parameter regions are Condition 1 ( $\mu\ge\rho-r$ or $R<\hat R$ ), Condition 2 (its negation) and Condition 3: Condition 1 and $K<\bar K_1$ , or Condition 2 and $K<\underline K$ , with $\hat R$ (28), $\bar K_1$ (K1) and $\underline K$ (33) explicit thresholds.

The paper uses three different hats: Definition 1's payment threshold $\hat w$ , Lemma 3's upright $\hat{\mathrm w}$ , and Proposition 6's bold $\hat{\mathbf w}$ , the upper end of the control band.

Formalization targets

Goal: Proposition 7, first claim

Under Condition 3 there are parameters $(\mathsf c,\hat{\mathbf w},\bar\vartheta,\underline\vartheta)$ satisfying Proposition 6 such that

V_I(w)=\begin{cases}V_{\mathsf c}(w),&w<\underline\vartheta\\ \mathcal V_{\hat{\mathbf w}}(w),&w\ge\underline\vartheta\end{cases},\qquad V_\emptyset(w)=\begin{cases}V_{\mathsf c}(w),&w<\bar\vartheta\\ \mathcal V_{\hat{\mathbf w}}(w)-K,&w\ge\bar\vartheta\end{cases}\qquad(46)

satisfy (20)–(22).

Proposition 6

Under Condition 3 there is $(\mathsf c,\hat{\mathbf w},\bar\vartheta,\underline\vartheta)$ with $\mathsf c>0$ , $\underline\vartheta<\bar\vartheta<\hat{\mathbf w}$ and value matching and smooth pasting at both thresholds:

\mathcal V_{\hat{\mathbf w}}(\underline\vartheta)=V_{\mathsf c}(\underline\vartheta),\quad \mathcal V_{\hat{\mathbf w}}'(\underline\vartheta)=V_{\mathsf c}'(\underline\vartheta),\quad \mathcal V_{\hat{\mathbf w}}(\bar\vartheta)=V_{\mathsf c}(\bar\vartheta)+K,\quad \mathcal V_{\hat{\mathbf w}}'(\bar\vartheta)=V_{\mathsf c}'(\bar\vartheta)>1 .

Milestones

Lemma EC.4 (the first step of the EC.3.9 construction), Proposition 6, and the two hardest parts of (20) at the constructed tuple: Lemma EC.12 ( $\mathcal A_\emptyset V_\emptyset\ge0$ on $[\bar\vartheta,\hat{\mathbf w})$ ) and Lemma EC.13 ( $\mathcal A_IV_I\ge0$ below $\underline\vartheta$ ). The other steps of the construction are posed as further statements of the mission without milestone status: Lemma EC.7 (the root of $\psi=K$ under Condition 1), Lemma EC.8 and Lemma EC.11 (the Condition 2 counterparts of EC.4 and EC.7).

Significance

Proposition 7 is the analytic certificate behind the paper's Theorem 5: combined with the verification Theorem 1, it shows that the control-band contract is optimal in the low-cost region, and that the principal's value is $V_\emptyset(w)-w$ . Without it the third case of the paper's main Theorem 2 is unproved. The construction of Proposition 6 also gives a computable description of the band, which the paper uses for its numerical illustrations.

The results are proved in the paper's e-companion; none of them has a machine-checked proof. This mission states the analytic part as Lean targets. The delay-ODE layer (existence, uniqueness and shape of $V_{\tilde w}$ ) is shared with the first mission of the series, and Proposition 7's proof depends on it. The stochastic contract model, the verification theorem and the optimality Theorems 1–5 are not formalized in this series.

Difficulty

Each piece of (20)–(22) is a one-variable inequality, but the functions are not explicit. $\mathcal V_{\hat{\mathbf w}}$ is defined through a delay equation, and the band's endpoints are defined implicitly through four nested steps: matching at $\underline\theta$ , a range bound $\underline\theta^0$ , an upper threshold $\bar\theta(\underline\theta)$ and a root of a gap function $\psi$ . The natural argument, convexity or concavity of $\mathcal A_IV_I$ on the suspension region, fails: on $[0,\underline\vartheta)$ the function $\mathcal A_IV_I$ mixes $V_{\mathsf c}$ with the look-ahead value $V_I(w+\beta)$ and is not convex (p. 28), so the convexity arguments of the switching literature do not apply. The paper's proof of this single inequality occupies EC.3.12, with eight auxiliary lemmas.

Formalization scope

Functions are ℝ → ℝ and every statement quantifies over $w\ge0$ . The standing assumptions are $0\le\underline\mu<\mu$ , $0<b\le c$ , $K>0$ , $0<r\le\rho$ and Assumption 1; $\underline\mu\ge0$ and $b>0$ are disclosed additions. Conventions:

$f'$ in $\mathcal A_I,\mathcal A_\emptyset$ is the left derivative; derivatives of $V_{\tilde w}$ , $\mathcal V_{\tilde w}$ are taken within $\mathbb R_+$ .
(20) is posed for $w>0$ : at $0$ the left derivative does not exist and $V_{\mathsf c}'(0^+)=+\infty$ .
$V_{\tilde w}$ is a solution of (25)–(26) chosen when one exists; $\check w$ , $\hat{\mathrm w}$ , $\bar K_1$ , $\underline\theta^0$ , $\bar\theta$ are infima or suprema of sets the paper describes; $\tilde w(\underline\theta)$ , $C(\underline\theta)$ are chosen matching pairs.
"Increasing/decreasing" is strict.
$\underline K$ (33) uses the corrected bracket $((\rho-\mu)/\rho)\beta$ in place of the printed $(r/\rho)\beta$ ; the printed form contradicts the proof's (EC.69).
Proposition 6's " $\hat{\mathbf w}<\hat{\mathrm w}$ " is read as $\hat{\mathbf w}<\bar w$ in the Condition 2 case, where $\hat{\mathrm w}$ does not exist; $0<\underline\vartheta$ is stated.
The goal is existential over Proposition 6 tuples. Lemmas EC.12 and EC.13 are stated at the tuple constructed in EC.3.9, in both cases of Condition 3; EC.13 is posed on $(0,\underline\vartheta)$ .
Lemma EC.11's second limit is printed at $0$ ; it is stated at $\breve{\underline\theta}$ , as the proof computes it.

The tuple is never defined by the property that (46) satisfies (20)–(22); the construction definitions are Steps 1–4 of EC.3.9 only, and the goal requires all of Proposition 6's conclusions. The second claim of Proposition 7, (48) on the contract's utility, is out of scope.

A complete development needs existence, uniqueness and regularity for the linear delay equation (25) (reusable for other delay problems), implicit-function arguments for $\tilde w(\underline\theta)$ , and the sign analysis of EC.3.12. Proofs of single milestones, and of the delay-ODE lemmas of the series' first mission, are welcome.

Selected references

P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845
K. Duckworth, M. Zervos, A model for investment decisions with switching costs, Annals of Applied Probability 11(1), 2001. https://doi.org/10.1214/aoap/998926992
V. L. Vath, H. Pham, Explicit solution to an optimal switching problem in the two-regime case, SIAM Journal on Control and Optimization 46(2), 2007. https://doi.org/10.1137/050638783

9 thms1 active userReviewed

Control Theory Economics Operations Research·Captain: mikedeng1

Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost I: Condition 1, High Switching Cost, Not-Hiring Value Functions Meet the Optimality ConditionsResearch Paper

Motivation

Many service relationships let a firm pause an agent instead of firing them: a sales representative who brings in no customers for a while is suspended, a contractor is laid off for a season and recalled. Pausing is not free. Every restart carries a switching cost $K$ (re-training, re-establishing a territory, setting up the work environment), so a principal who suspends too readily pays for it. Cao, Sun and Tian (Management Science, 2024) study the optimal dynamic contract for this trade-off in continuous time, building on the Poisson-arrival moral-hazard model of Sun and Tian (2018). Their main result (Theorem 2) splits the parameter space into three regimes: never hire, hire and keep the agent working forever, and a control-band contract with suspension episodes of fixed length. This mission covers the first regime under the paper's Condition 1.

Setting

A principal earns a revenue $R$ per arrival of a Poisson process. Without effort the arrival rate is $\underline\mu\ge0$ ; an agent who works, at private cost $b>0$ per unit time, raises it to $\mu>\underline\mu$ . Write $\Delta\mu=\mu-\underline\mu$ . The principal's cost rate while the agent works is $c\ge b$ , every start of work costs $K>0$ , and the principal and the agent discount at rates $0<r\le\rho$ . Assumption 1 is $R\Delta\mu>c$ . The derived constants are

\beta=\frac{b}{\Delta\mu},\qquad \bar w=\frac{\beta\mu}{\rho},\qquad \underline v=\frac{\underline\mu R}{r},\qquad \bar V(w)=\frac{R\mu-c-(\rho-r)w}{r}.

The state of a contract is the agent's promised utility $w\ge0$ . The paper's verification theorem reduces optimality to a pair of functions: $V_I$ for the working state and $V_\emptyset$ for the suspended state. For a function $f$ on $\mathbb R_+$ , with $f'$ its left derivative, the operators are

(\mathcal A_If)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,

(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu,

and $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) if $\mathcal A_IV_I\ge0$ , $\mathcal A_\emptyset V_\emptyset\ge0$ , $0\le V_I-V_\emptyset\le K$ on $\mathbb R_+$ , and $V_I(0)\ge\underline v$ , $V_\emptyset(0)\ge\underline v$ .

The working-state candidate is built from the delay differential equation (25): for $\tilde w\in[0,\bar w)$ , $V_{\tilde w}$ is the $C^1$ function on $[0,\tilde w]$ with

(\mu+r)V(w)-\mu V\big((w+\beta)\wedge\tilde w\big)+\rho(\bar w-w)V'(w)-(\mu R-c)+(\rho-r)w=0,

and $V(w)=\bar V(\tilde w)$ for $w\ge\tilde w$ . $V_{\tilde w}$ may be convex near $0$ ; $\check w(\tilde w)$ is the point up to which $V_{\tilde w}''>0$ , and the concavification $\mathcal V_{\tilde w}$ replaces $V_{\tilde w}$ on $[0,\check w(\tilde w))$ by its tangent line at $\check w(\tilde w)$ . Condition 1 is " $\mu\ge\rho-r$ or $R<\hat R$ " with

\hat R=\Big[\frac cb+\frac{(\rho-r)\mu}{\Delta\mu(\rho-r-\mu)}\cdot\frac{\rho-\mu}{\rho}\Big]\beta.

Under it there is a unique $\hat{\mathrm w}\in[0,\bar w)$ with $\mathcal V_{\hat{\mathrm w}}(0)=\underline v$ (Lemma 3). Three hats occur in the paper: $\hat w$ of Definition 1 (a payment threshold), $\hat{\mathrm w}$ of Lemma 3 (used here), and $\hat{\mathbf w}$ of Proposition 6 (not used here). For $K<\bar V(\hat{\mathrm w})-\underline v$ , Lemma 4 gives a tangent pair $(\bar\theta^K,m^K)$ : the line $m^Kw+\underline v$ touches $\mathcal V_{\hat{\mathrm w}}-K$ at $\bar\theta^K$ . Finally $\bar K_1=\inf\{K\in(0,\bar V(\hat{\mathrm w})-\underline v]\mid m^K<1\}$ (K1).

Formalization targets

Goal: Proposition 3 (p. 22)

Under Condition 1 and $\bar K_1\le K\le\bar V(\hat{\mathrm w})-\underline v$ , for the pair $(\bar\theta^K,m^K)$ of (29),

V_I=\mathcal V_{\hat{\mathrm w}},\qquad V_\emptyset(w)=\begin{cases}m^Kw+\underline v,&w\le\bar\theta^K,\\ \mathcal V_{\hat{\mathrm w}}(w)-K,&w>\bar\theta^K,\end{cases}

satisfy (20)–(22).

Milestones

Lemma EC.2: existence and uniqueness of $V_{\tilde w}$ , $\tilde w\in[0,\bar w)$ .
Lemma EC.2(iii)–(iv): $V_{\tilde w}$ increasing; $V_{\tilde w}$ decreasing and $V_{\tilde w}'$ increasing in $\tilde w$ .
Lemma 2(i): the sign pattern of $V_{\tilde w}''$ around $\check w(\tilde w)$ , and $\check w(\tilde w)\le(1-r/\rho)\beta$ .
Lemma 2(ii)–(iii): $\mathcal V_{\tilde w}$ increasing and concave; comparison in $\tilde w$ .
Lemma 3: $\hat{\mathrm w}$ exists and is unique; $\mathcal V_{\hat{\mathrm w}}'(0)>1$ when $\check w(\hat{\mathrm w})>0$ .
Proposition 2: for $K\ge\bar V(\hat{\mathrm w})-\underline v$ , $(\mathcal V_{\hat{\mathrm w}},\underline v)$ satisfies (20)–(22).
Lemma 4: tangent pairs exist; $\bar\theta^K$ increases and $m^K$ decreases in $K$ ; $\bar\theta^K\to\check w(\hat{\mathrm w})$ as $K\downarrow0$ .

Significance

Propositions 2 and 3 are the analytic certificates behind Theorem 2(i): combined with the verification theorem (Theorem 1), they show that under Condition 1 and $K\ge\bar K_1$ the principal's utility from any incentive-compatible contract promising $w$ is at most $V_\emptyset(w)-w\le\underline v$ , so never hiring the agent is optimal, and $\bar K_1$ is exactly the switching-cost threshold of that regime. The same objects ( $V_{\tilde w}$ , $\mathcal V_{\hat{\mathrm w}}$ , the tangent pairs) reappear in the low-cost control-band regime (Propositions 6–7), so a formal development of the delay ODE and its concavification is reused there.

The paper proves all these results; none is formalized. The mission formalizes the deterministic half of the guess-and-verify argument. The stochastic contract model (point processes, promise keeping, incentive compatibility), Theorem 1 and the optimality theorems are outside its scope.

Difficulty

The obvious approach, verifying (20)–(22) by direct computation, works for the linear pieces but not for $\mathcal V_{\hat{\mathrm w}}$ , which has no closed form: (25) is a delay equation solved backwards from $\tilde w$ in steps of length $\beta$ , and the closed form (EC.52) of the paper holds only on the last step $[(\tilde w-\beta)^+,\tilde w]$ . Every property of $\mathcal V_{\hat{\mathrm w}}$ used in the goal (monotonicity, the single change of convexity, the comparison in $\tilde w$ that makes $\hat{\mathrm w}$ unique) has to be extracted from the equation itself, across the kinks of $w\mapsto(w+\beta)\wedge\tilde w$ . On the second branch of $V_\emptyset$ , $\mathcal A_\emptyset V_\emptyset\ge0$ is not a pointwise identity either: it requires $m^K\le1$ , which is where $K\ge\bar K_1$ enters.

Formalization scope

Parameters form a structure with real fields; the standing assumptions $0\le\underline\mu<\mu$ , $0<b\le c$ , $K>0$ , $0<r\le\rho$ , $R\Delta\mu>c$ are a hypothesis of every theorem. $\underline\mu\ge0$ and $b>0$ are disclosed additions (a rate and a cost).
Functions are ℝ → ℝ; every statement quantifies over $w\ge0$ only. In $\mathcal A_I,\mathcal A_\emptyset$ , $f'$ is the left derivative (derivWithin f (Set.Iic w) w, the paper's p. 15 convention); in statements about $V_{\tilde w}$ and $\mathcal V_{\tilde w}$ , derivatives are taken within $\mathbb R_+$ ; in (25), within $[0,\tilde w]$ .
(20) is required for $w>0$ : at $w=0$ a left derivative of a function on $\mathbb R_+$ does not exist. (21) and (22) are as printed.
$V_{\tilde w}$ is a chosen solution of (25)–(26) (Lemma EC.2 is the milestone that makes this meaningful); $\check w(\tilde w)$ is a supremum defined through the sign of $V''$ , and $\hat{\mathrm w}$ an infimum; $\bar K_1$ is an infimum. None is defined by the property a theorem asserts about it.
The goal holds for every pair satisfying (29); the pair is unique, and at $K=\bar V(\hat{\mathrm w})-\underline v$ it is $(\hat{\mathrm w},0)$ . The second branch of (30) is extended beyond $\hat{\mathrm w}$ , as the paper's proof uses.
"Increasing/decreasing" mean strictly. The contract-utility claim $U(\underline\Gamma)=\underline v$ of Proposition 2 is not stated.
Ruled out: weakening (20)–(22) (dropping the upper bound $K$ in (21), or (22)), or defining $V_{\tilde w}$ by its closed form (EC.52), which is valid only near $\tilde w$ .

Needed infrastructure: existence and uniqueness for linear ODEs with a terminal condition, extended step by step across a delay; one-sided derivatives of piecewise functions; concavity from sign conditions on second derivatives. Proofs of the milestones, and reusable lemmas about delay equations of this form, are welcome.

Selected references

P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845 (cited from the authors' manuscript with e-companion).
P. Sun, F. Tian, Optimal Contract to Induce Continued Effort, Management Science 64(9), 2018. https://doi.org/10.1287/mnsc.2017.2795

11 thms1 active userReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality I: Feasible Solutions of the Continuous Stopping LP Can Be Improved to Threshold FormResearch Paper

Motivation

Two classical online selection problems sit at opposite ends of an information spectrum. In the secretary problem items arrive in uniformly random order, only their relative ranks are observed, and the best possible probability of stopping on the best item tends to $1/e$ . In the i.i.d. prophet inequality the values are independent draws from a known distribution, and the best guarantee against the expected maximum is the constant $\approx 0.745$ of Hill and Kertz (1982), shown tight by Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (2017).

Correa, Cristi, Epstein and Soto (arXiv:2011.06516) interpolate between the two with the $p$ -sample-driven optimal stopping problem. Each of $N$ items is sampled independently with probability $p$ ; the decision maker observes the relative rankings of the sampled items, then faces the remaining items online, observing relative rankings, and makes irrevocable stop/continue decisions. Stopping on the item of overall rank $i$ earns a reward $Y_i$ , with $Y_1\ge Y_2\ge\cdots$ . At $p=0$ and $Y=(1,0,0,\dots)$ this is the secretary problem; for adversarial $Y$ the optimal guarantee tends to $0.745$ as $p\to1$ , the i.i.d. prophet constant.

For known $Y$ , the paper writes a linear program over the stopping probabilities of rank-based algorithms (after Buchbinder, Jain and Singh, 2014) and takes its limit as $N\to\infty$ . The analysis rests on one structural result, Theorem 2: this limiting program can be restricted, without loss, to solutions of an explicit threshold form, so that the optimal algorithm stops on an item of current rank $i$ after a time $t_i$ . This mission is that theorem.

Setting

Fix $p\in[0,1)$ . Time runs over $[p,1]$ (time $t$ is the fraction of the $N$ items seen so far; the sample accounts for the first fraction $p$ in the limit), and ranks $\ell=1,2,\dots$ refer to the relative rank of the current item among all items seen so far. A candidate solution is a function $q(t,\ell)$ , the density of stopping at time $t$ on an item of relative rank $\ell$ .

The cumulative mass of $q$ is $M_q(t)=\int_p^t\sum_{s\ge1}q(\tau,s)\,d\tau$ . A solution is feasible for the continuous linear program CLP $_p$ when $q(t,\ell)\ge0$ , each $q(\cdot,\ell)$ is integrable on $[p,1]$ , and

t\,q(t,\ell)+M_q(t)\le1\qquad\forall t\in[p,1],\ \forall\ell\ge1 .

For $k\ge1$ the negative-binomial term is $\mathrm{nb}_{k,\ell}(t)=\sum_{j=\ell}^{k}\binom{j-1}{\ell-1}(1-t)^{j-\ell}t^{\ell}$ , the probability that a NegativeBinomial $(\ell,t)$ variable is at most $k$ , and

F_k(q)=\sum_{\ell=1}^{k}\int_p^1 q(t,\ell)\,\mathrm{nb}_{k,\ell}(t)\,dt .

$F_k(q)$ is the limit of the probability that the algorithm stops on an item of overall rank at most $k$ . The objective of CLP $_p$ is $Y_1-\sum_{k\ge1}(Y_k-Y_{k+1})(1-F_k(q))$ for a non-increasing sequence $Y$ , so any solution that increases every $F_k$ is at least as good.

A threshold sequence is a non-decreasing $(t_i)_{i\ge0}\subseteq[p,1]$ with $t_0=p$ ; put $T_i=\prod_{j=1}^{i}t_j$ .

Formalization targets

Goal: Theorem 2 (p. 8)

For every feasible $q$ there are a feasible $q^*$ and a threshold sequence $(t_i)$ with $F_k(q^*)\ge F_k(q)$ for all $k\ge1$ , such that for every $\ell\ge1$ and $t\in[p,1)$

t\,q^*(t,\ell)+\int_p^t\sum_{s\ge1}q^*(\tau,s)\,d\tau=1\ \ (t\ge t_\ell),\qquad q^*(t,\ell)=0\ \ (t<t_\ell),\tag{5–6}

q^*(t,\ell)=\begin{cases}T_i/t^{i+1}&t\in[t_i,t_{i+1}),\ \ell\le i,\\0&\text{else.}\end{cases}\tag{7}

Milestones

Lemma 17 (p. 28): $\mathrm{nb}_{k,\ell}$ is non-decreasing on $[0,1]$ for $1\le\ell\le k$ .
Lemma 18 (p. 29): $\mathrm{nb}_{k,\ell}(t)$ is non-increasing in $\ell\ge1$ for $t\in[0,1]$ .
(8) (p. 9): one mass-moving step $q_{n-1}\mapsto q_n$ , which pushes each component to the right up to the envelope $\frac1t(1-M_{q_{n-1}}(t))$ , keeps each component's mass, satisfies $M_{q_n}\le M_{q_{n-1}}$ in the form (8), and preserves feasibility.
$F_k(q_{n-1})\le F_k(q_n)$ (p. 9) for the same step.
Uniqueness (p. 10): for fixed thresholds, (5)–(6) have at most one feasible solution on $[p,1)$ .
Existence (p. 10): the function (7) satisfies (5)–(6).

Significance

Theorem 2 turns an infinite-dimensional linear program over functions of two variables into the reduced problem RP $_p$ , an optimization over a single non-decreasing sequence of thresholds. Every quantitative result of the paper is read off RP $_p$ : the optimal ratio for each $p$ , its limit as $p\to1$ (Theorem 8, mission II of this series) and the explicit lower bound $\alpha^*p$ (Theorem 9, mission III). It also identifies the optimal rank-based algorithms as threshold rules: accept the current item if it is among the $i$ best seen so far, where $i$ grows at the times $t_i$ .

The result is proved in the paper. It has not been formalized, and neither has any part of the continuous-LP approach to secretary and prophet problems. The formal development produces a reusable layer: continuous stopping LPs with extended-real cumulative constraints, monotonicity of negative-binomial distribution functions in both parameters, and a rearrangement argument for integrals against monotone weights.

Difficulty

The obvious argument is to improve $q$ greedily: push each component's mass as far right as the constraint allows. One step is easy, but the step changes the constraint itself, since the envelope $\frac1t(1-M_q(t))$ depends on all components. The proof iterates, needs the thresholds $t_\ell(n)$ to be monotone in $n$ , and must pass to a limit $q_\infty$ in $L^1$ with a dominating function that exists only because the smallest threshold is bounded away from $0$ . The limit thresholds need not be monotone in $\ell$ , and the components must then be reordered using Lemma 18. Finally, (5)–(6) are an integral equation in which each component depends on the sum of all others; identifying their unique solution with (7) needs both a uniqueness argument for a linear ODE and a telescoping computation.

Formalization scope

A solution is a function q : ℝ → ℕ → ℝ, a representative of an element of $L^1([p,1]\times\mathbb N)$ . Ranks, $k$ , $i$ , $j$ are 1-based; $q(\cdot,0)$ is never used. Constraints are imposed pointwise for all $t$ , as printed.
The cumulative mass $M_q(t)$ is the lower Lebesgue integral of $\sum_{s\ge1}q(\tau,s)$ in $[0,\infty]$ , never a Bochner integral of a real series, which Lean would set to $0$ on divergent data.
Integrability of each $q(\cdot,\ell)$ is part of feasibility, so $F_k$ is never a junk value.
Equations (5)–(7) are imposed on $[p,1)$ , not on $[p,1]$ . At the single point $t=1$ the printed (5) and (7) contradict each other whenever finitely many thresholds are below $1$ (already for $q=0$ ). Feasibility of $q^*$ is required on all of $[p,1]$ .
The threshold intervals $[t_i,t_{i+1})$ are half-open, as in (7); they are pairwise disjoint because $(t_i)$ is non-decreasing.
"Increasing" in Lemma 17 and "decreasing" in Lemma 18 are read as non-decreasing and non-increasing.
The mass-moving step (milestones 3–4) takes the thresholds $t_\ell(n)$ as hypotheses satisfying their defining equation, and requires them to be positive (this only matters at $p=0$ , where the paper's equation already forces it).
Milestone 6 assumes $t_1>0$ , and claims (5) at $t$ when $t<t_i$ for some $i$ or when $T_m/t_m^m\to0$ ; on the page these conditions are implicit, and without them the claim fails.
A statement of Theorem 2 that keeps only "there is a feasible $q^*$ with $F_k(q^*)\ge F_k(q)$ " is trivial ( $q^*=q$ ); equations (5)–(7) are part of the goal and must not be dropped.
Mathlib supplies interval and lower Lebesgue integrals, series in $[0,\infty]$ and binomial coefficients. Contributions welcome: the negative-binomial lemmas, the rearrangement inequality for monotone weights, and a Grönwall-type uniqueness argument for the integral equation.

Selected references

J. Correa, A. Cristi, B. Epstein, J. A. Soto, Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality, arXiv:2011.06516v2, 2021. https://arxiv.org/abs/2011.06516
T. P. Hill, R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, Annals of Probability 10(2), 1982. https://doi.org/10.1214/aop/1176993861
J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted price mechanisms for a random stream of customers, ACM EC 2017. https://doi.org/10.1145/3033274.3085137
N. Buchbinder, K. Jain, M. Singh, Secretary problems via linear programming, Mathematics of Operations Research 39(1), 2014. https://doi.org/10.1287/moor.2013.0604

8 thms1 active userReviewed

Control Theory Economics Operations Research·Captain: mikedeng1

Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost III: Condition 2, Medium Switching Cost, Always-Work Value Functions Meet the Optimality ConditionsResearch Paper

Motivation

Many service relationships pay an agent per unit of output whose arrival is random: a salesperson closing deals, a call-centre worker resolving tickets, a contractor delivering jobs. When effort is unobservable, the classical tool for keeping an agent motivated is the threat of termination after poor performance. In practice firms often use a milder punishment, suspension: the agent is sent home for a while and later called back. Restarting work is not free, and each restart costs the firm a fixed switching cost.

P. Cao, P. Sun and F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost (Management Science, 2024), characterise the optimal dynamic contract in this setting. The optimal contract depends on the size of the switching cost: when it is large the firm should not hire, when it is moderate the firm should keep the agent working forever, and when it is small the firm uses a control-band contract with suspension episodes. Their proof is "guess and verify": a stochastic verification theorem (their Theorem 1) turns any pair of functions satisfying a system of quasi-variational inequalities into an upper bound on the principal's value, and Propositions 2–7 exhibit such pairs in each parameter region.

This mission formalizes the certificate for the medium-switching-cost region under Condition 2 (Area II of the paper's Figure 2), where the agent is never suspended.

Setting

The principal faces a Poisson stream of arrivals, each worth revenue $R$ . Without effort the arrival rate is $\underline\mu\ge0$ ; an agent who exerts effort, at cost $b>0$ per unit time, raises it to $\mu>\underline\mu$ . Write $\Delta\mu=\mu-\underline\mu$ . The principal's total cost rate while the agent works is $c\ge b$ , every start of work costs a switching cost $K>0$ , and the principal and agent discount at rates $0<r\le\rho$ . Assumption 1 is $R\Delta\mu>c$ .

The paper's derived constants are

\beta=\frac{b}{\Delta\mu},\quad \bar w=\frac{\beta\mu}{\rho},\quad \underline v=\frac{\underline\mu R}{r},\quad \bar V=\frac{R\mu-c-(\rho-r)\bar w}{r},\quad \bar K_2=\bar V-\underline v-\bar w,

together with the revenue thresholds $\hat R$ (28) and $\bar R$ (34) and the switching-cost threshold $\underline K$ (33). Condition 2 is $\mu<\rho-r$ and $R\ge\hat R$ : the agent is much more impatient than the principal and revenue is high.

The state variable is the agent's promised utility $w\ge0$ . Two operators act on functions $f$ of $w$ , where $f'$ is the left derivative:

(\mathcal A_I f)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,

(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu.

The first is a delay-differential operator for the working state, the second a first-order operator for the suspended state. A pair $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) when $\mathcal A_IV_I\ge0$ , $\mathcal A_\emptyset V_\emptyset\ge0$ , $0\le V_I-V_\emptyset\le K$ and $V_I(0),V_\emptyset(0)\ge\underline v$ .

The suspended-state equation $\mathcal A_\emptyset V=0$ with $V(0)=\underline v$ is solved by $V_c(w)=\underline v+w+c\,w^{r/\rho}$ (24). In the region of this mission the paper builds

V_\emptyset(w)=\begin{cases}V_{c_K}(w),&w\le\bar w,\\ \bar V-K,&w>\bar w,\end{cases}\qquad V_I(w)=\begin{cases}V_{c_K}(w),&w\le\underline\theta_K,\\ \bar V+m_K(w-\bar w),&\underline\theta_K<w\le\bar w,\\ \bar V,&w>\bar w,\end{cases}

from parameters $(c_K,m_K,\underline\theta_K)$ chosen so that $V_{c_K}$ pastes smoothly onto the line at $\underline\theta_K$ and ends at $\bar V-K$ at $\bar w$ .

Formalization targets

Goal: Proposition 5 (first claim)

Under Condition 2 and $K\in[\underline K,\bar K_2)$ , for every triple $(c_K,m_K,\underline\theta_K)$ with $\underline\theta_K\in(0,\bar w)$ , $c_K>0$ , $m_K\in[\frac{\rho-r}{\rho-r-\mu},\frac{\bar V-\underline v}{\bar w})$ and

V_{c_K}(\underline\theta_K)=\bar V+m_K(\underline\theta_K-\bar w),\qquad V'_{c_K}(\underline\theta_K)=m_K,\qquad V_{c_K}(\bar w)=\bar V-K,

the functions $V_I,V_\emptyset$ above satisfy (20)–(22).

Milestones

(EC.67): explicit $C^1(\underline\theta)$ and $m(\underline\theta)$ solve the value-matching and smooth-pasting equations at any $\underline\theta\in(0,\bar w]$ .
Lemma EC.3: $\psi_1(\underline\theta)=\bar V-\underline v-\bar w-C^1(\underline\theta)\bar w^{r/\rho}$ is continuous and strictly decreasing on $[0,\bar w]$ , so $\psi_1=K$ has a unique root $\underline\theta_K\in(0,\bar w)$ for $K\in(0,\bar K_2)$ ; the root decreases in $K$ and tends to $\bar w$ as $K\downarrow0$ .
Lemma 5: for every $K\in[\underline K,\bar K_2)$ the triple exists, and $c_K$ , $m_K$ , $\underline\theta_K$ are monotone in $K$ .

Lemma 5 guarantees that the goal is not vacuous.

Significance

Proposition 5 is the analytic half of the paper's Theorem 4: combined with the verification theorem, it shows that in Area II the principal's optimal value is attained by a contract that pays the agent $\beta$ per arrival and never suspends. The threshold $\underline K$ separates this region from the control-band region of Proposition 7, so the explicit formula for $\underline K$ is the boundary of the phase diagram.

The result is proved in the paper. No machine-checked version exists. A formal proof checks a delicate sign argument near $w=0$ , where $V_{c_K}$ has infinite slope, and it checks the threshold $\underline K$ , whose printed formula contains an error (see Formalization scope). The paper's companion identity (41), $U(\bar\Gamma)=\bar V-\bar w-K=V_\emptyset(\bar w)-\bar w$ , is about the utility of a contract and is not part of this mission; its deterministic half is immediate from (39).

Difficulty

The cases $w\in[\underline\theta_K,\bar w]$ and $w>\bar w$ are algebraic. The difficulty is $w\in(0,\underline\theta_K)$ : there $V_I$ is the curve $V_{c_K}$ , and $w+\beta$ lands beyond $\bar w$ (Condition 2 gives $\beta>\bar w$ ), so $\mathcal A_IV_I$ couples the curve with the constant $\bar V$ . Positivity there needs more than the sign of the smooth-pasting slope: it uses the lower bound on $m_K$ in (35), which is exactly where the threshold $\underline K$ enters. A direct sign check at $\underline\theta_K$ alone does not cover the interval. The existence lemma requires monotonicity of $\psi_1$ , whose expression mixes powers $\underline\theta^{r/\rho-1}$ with a linear factor.

Formalization scope

All functions are ℝ → ℝ and every quantifier ranges over $w\ge0$ ; powers are Real.rpow. The standing assumptions $0\le\underline\mu<\mu$ , $0<b\le c$ , $K>0$ , $0<r\le\rho$ , $R\Delta\mu>c$ are one hypothesis Standing; $\underline\mu\ge0$ and $b>0$ are read off the model and stated explicitly. The left derivative is derivWithin f (Set.Iic w) w, following the paper's convention on p. 15. Condition (20) is posed for $w>0$ only: at $w=0$ the right derivative of $V_{c_K}$ is $+\infty$ , so the paper's (20) there is an extended-real statement and Lean's junk derivative would make it false. (21) and (22) are posed as printed.

The threshold $\underline K$ of (33) is corrected: the printed bracket contains $\frac r\rho\beta$ , but the paper's own proof identifies $\underline K$ with $\check K_2$ of (EC.69), which gives $\frac{\rho-\mu}{\rho}\beta$ . With the printed term Lemma 5 fails (for $r=0.2,\rho=1.2,b=c=1,R=5,\mu=0.9,\underline\mu=0.1$ , the printed value is $-0.069$ , the corrected one $7.2533$ ). Equation (36) is printed with a free $w$ that should read $\underline\theta_K$ . The range $\underline\theta_K\in(0,\bar w)$ , given by the proof, is stated.

The goal quantifies over all triples satisfying Lemma 5's conclusions; such a triple is unique, so this is the paper's claim, and Lemma 5 rules out a vacuous goal. Dropping the bound $K$ in (21), the condition (22), or the lower bound on $m_K$ would trivialize or change the statement.

The development needs the derivative of $w\mapsto w^{r/\rho}$ , sign analysis of explicit real functions, and the intermediate value theorem. The Setting file is shared with the other missions of this series and will be consolidated. Proofs of the milestones in any order are welcome; (EC.67) is a self-contained calculus exercise.

Selected references

P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845 (cited from the authors' manuscript and e-companion: §4.2 pp. 24–26, EC.3.7–EC.3.8 pp. ec32–ec34).
Y. Sannikov, A Continuous-Time Version of the Principal-Agent Problem, Review of Economic Studies 75(3), 2008. https://doi.org/10.1111/j.1467-937X.2008.00486.x
B. Biais, T. Mariotti, J.-C. Rochet, S. Villeneuve, Large Risks, Limited Liability, and Dynamic Moral Hazard, Econometrica 78(1), 2010. https://doi.org/10.3982/ECTA7261

6 thms1 active userReviewed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Online Stochastic Matching: New Algorithms with Better Bounds 2: The Per-Advertiser Inequality Behind the 0.706 Ratio for General Arrival Rates, in the Limit f − s ≤ 1 − ln 2Research Paper

Motivation

Online stochastic matching models display advertising and similar allocation problems in which requests arrive one at a time and must be served immediately. A bipartite graph links a set $A$ of advertisers to a set $I$ of impression types; $n$ requests arrive, each of a type drawn independently with $\mathbb P(\text{type } i) = r_i/n$ , and each request must be assigned at once and irrevocably to an unmatched interested advertiser, or dropped. Performance is measured by the competitive ratio $\mathbb E[\mathrm{ALG}]/\mathbb E[\mathrm{OPT}]$ , where OPT is the maximum matching of the realized graph.

Without distributional knowledge the best possible ratio is $1 - 1/e$ (Karp, Vazirani and Vazirani, 1990). Knowing the type distribution allows more:

Feldman, Mehta, Mirrokni and Muthukrishnan (2009) first beat $1 - 1/e$ , with $0.670$ , when every arrival rate is integral; Bahmani and Kapralov improved this to $0.699$ .
Manshadi, Oveis Gharan and Saberi (2011) obtained $0.705$ for integral rates and $0.702$ for general arrival rates, using offline statistics drawn by sampling.
Jaillet and Lu (2014) introduced Random Lists Algorithms with modified LPs and obtained $1 - 2e^{-2} \approx 0.729$ for integral rates (Theorem 1), $0.725$ for vertex weights (Theorem 2) and $0.706$ for general rates (Theorem 3).

This mission concerns the analytic core of Theorem 3, the general-rates bound.

Setting

For an advertiser $a$ , let $f = f_a \le 1$ be the LP flow into $a$ . Its neighbours $a_1 \in A^*_a$ , which include a dummy advertiser $a_d$ with $f_{a_d} = 1$ , are indexed by $j = 1, \dots, k$ . For each neighbour, $x_j = m_{a,a_1} = m_{a_1,a} \ge 0$ is the expected number of random lists $\langle a, a_1\rangle$ , and $y_j = f_{a_1} \le 1$ is the neighbour's flow, so that $x_j \le y_j$ . Write $s = \sum_j x_j \le f$ and $\beta = \max_j x_j$ .

Claim 2 of the paper introduces the functions

h(y,x)=\begin{cases}\dfrac{y}{y-x}\bigl(e^{-x}-e^{-y}\bigr), & x\ne y,\\[4pt] y\,e^{-y}, & x=y,\end{cases}\qquad g(y,x)=h(y,0)-h(y,x),

where $g(f_{a_1}, m_{a_1,a})$ is the probability that $a$ is matched through a list headed by $a_1$ . The per-advertiser bracket is

B(f;x,y)=1-e^{-f}+\frac1e\sum_j g(f,x_j)-\frac1{2e}\Bigl(\sum_j g(y_j,x_j)\Bigr)^2+\frac1{2e}\sum_j g(f,x_j)^2,

and the reduced function of three variables is

R(f,\beta,s)=\frac1f\Bigl(1-e^{-f}+\frac1e\frac{s}{\beta}g(f,\beta)-\frac1{2e}\bigl(e^{-1}(s-\beta)+g(1,\beta)\bigr)^2+\frac1{2e}g(f,\beta)^2\Bigr).

In Lean these are h, g, bracket f x y and R f β s in RandomListsMatching.GeneralRates.

Formalization targets

Goal: the per-advertiser bound

For $0 < f \le 1$ , any $k \ge 0$ and reals with $0 \le x_j \le y_j \le 1$ , $s = \sum_j x_j \le f$ and $f - s \le 1 - \ln 2$ ,

\frac{B(f;x,y)}{f} \ge 0.706 .

The paper bounds $\sum_a p_a / \sum_a f_a$ below by $\min_a B(f_a; \cdot)/f_a$ (p. 15), so this inequality is the whole of what Theorem 3's numerical constant rests on.

Milestones

Claim 3 (three clauses, p. 15): for $y \in [0,1]$ , $h(y,\cdot)$ is convex and decreasing on $[0,y]$ and $g(y,\cdot)$ is concave and increasing on $[0,y]$ ; for $x \ge 0$ , $g(\cdot, x)$ is increasing on $[x,\infty)$ .
Inequality (5), analytic part (p. 15): for $0 \le x \le y \le 1$ , $h(y,0)-h(y,x) \le -x\,\partial_2 h(y,0) \le e^{-1}x$ .
Chord bound (p. 15): $\sum_j g(f,x_j) \ge (s/\beta)\, g(f,\beta)$ .
Cross-sum bound (p. 15): $\sum_j g(y_j,x_j) \le e^{-1}(s-\beta) + g(1,\beta)$ .
Reduction (p. 15): $B(f;x,y)/f \ge R(f,\beta,s)$ when $\beta > 0$ .
Claim 4, corrected (p. 16): $R(f,\beta,s) \ge 0.706$ on $1 \ge f \ge s \ge \beta > 0$ , $f - s \le 1 - \ln 2$ .

Significance

The result. Theorem 3 gives $0.706$ for online stochastic matching with general (non-integral) arrival rates, improving the $0.702$ of Manshadi et al. The probabilistic half of its proof reduces matching probabilities to the closed forms $h$ and $g$ ; the paper then states that "in the remaining part of the section, we only use algebraic manipulations and the following properties of functions $g$ and $h$ ". That remaining part, posed here, is an exact real inequality, and it is where the constant $0.706$ is decided.

Formalizing it. The paper proves Claim 3 in one line ("can be easily verified by taking first and second order partial derivatives") and Claim 4 by a grid computation over cubes of side $0.001$ , with no recorded error analysis. A machine-checked proof replaces both. It also settles the regime of the constant: Claim 4 as printed, with the constraint $f - s \le (1 - \ln 2) + 1/n$ "for $n \ge 100$ ", is false, and the bound holds in the limit form stated here. None of these statements has a formal proof anywhere, to the extent of the search made for this mission.

Difficulty

The margin is small. The minimum of $R$ over the feasible region is about $0.706028$ , attained near $(f,\beta,s) = (1, 0.565, \ln 2)$ on the boundary $f - s = 1 - \ln 2$ ; the margin over $0.706$ is under $3 \cdot 10^{-5}$ . Any argument that loses a constant factor in the estimates of $e^{-x}$ , or replaces $\ln 2$ by a rational bound that is not tight to five digits, fails. The bound is a three-variable statement with the minimum on a boundary face, so a one-variable monotonicity argument does not settle it.

The second difficulty is the function $h$ itself. Its two-case definition is continuous but the quotient form has a removable singularity at $x = y$ , which is exactly the end of the interval $[0, y]$ on which Claim 3 asserts convexity and concavity. Derivative computations that are routine away from the diagonal need care there.

The natural first idea for the goal, to apply Claim 4 directly to the bracket, does not type-check: the bracket depends on the whole family $(x_j, y_j)$ , and the reduction to three variables through the chord and cross-sum bounds is a separate step.

Formalization scope

All quantities are real numbers. $e$ is Real.exp 1, $\ln 2$ is Real.log 2, and $0.706$ is the exact rational (0.706 : ℝ).
$h$ keeps the paper's case split at $x = y$ . The neighbour family is indexed by Fin k, and $k = 0$ is allowed.
"Increasing" and "decreasing" are non-strict (MonotoneOn, AntitoneOn); convexity is ConvexOn ℝ (Set.Icc 0 y). The derivative in (5) is deriv (fun t => h y t) 0, the derivative in the second argument; the page's $\partial h/\partial y$ is a slip.
Pinned hypotheses. The goal requires $f > 0$ (an advertiser with $f_a = 0$ contributes $0/0$ in the paper and $0$ in Lean). Claim 4 and the reduction require $\beta > 0$ , because $s/\beta$ is $0$ in Lean at $\beta = 0$ and $R(1,0,1) \approx 0.607$ ; in the paper $\beta = 0$ forces $s = 0$ , a case the goal covers directly. The hypotheses $x_j \le y_j \le 1$ are the paper's $m_{a_1,a} \le s_{a_1} \le f_{a_1} \le 1$ .
Claim 4 is corrected. As printed it is false: at $n = 100$ , $(f,\beta,s) = (1, 0.55886, \ln 2 - 0.01)$ meets the printed constraints and gives $R \approx 0.70521$ . The goal fails at $n = 100$ as well (about $0.70543$ ). Both are stated in the limit $f - s \le 1 - \ln 2$ , the regime in which the paper claims Theorem 3 (" $n$ is large enough so that a factor of $1 + O(1/n)$ is negligible", p. 6). The constant $0.706$ is unchanged.
Out of scope. Theorem 3 itself, LP (4), the list construction of §5.3, Claim 2 and the bound on $p_a$ are not posed. They rest on " $\approx$ " replacements of binomial sums and on an asymptotic independence whose proof "is omitted in the paper", so they have no exact finite- $n$ statement.
No trivializing reading. The goal's hypotheses are met, for example, by $k = 1$ , $f = 1$ , $x_1 = 0.7$ , $y_1 = 1$ , and the conclusion is not vacuous there. Its hypotheses do not exclude the minimizer, and the division by $f$ is guarded.

A complete development needs the derivative calculus of $h$ on $[0,y]$ , including the diagonal, and certified interval bounds for $e^{-x}$ and $\ln 2$ . The latter is reusable well beyond this mission. Proofs of Claim 3 or Claim 4 alone are welcome contributions.

Selected references

P. Jaillet and X. Lu, Online Stochastic Matching: New Algorithms with Better Bounds, Mathematics of Operations Research, 2014; authors' accepted manuscript, rev. June 2013. https://doi.org/10.1287/moor.2013.0621
V. H. Manshadi, S. Oveis Gharan and A. Saberi, Online Stochastic Matching: Online Actions Based on Offline Statistics, Mathematics of Operations Research 37(4):559–573, 2012. https://doi.org/10.1287/moor.1120.0551
J. Feldman, A. Mehta, V. Mirrokni and S. Muthukrishnan, Online Stochastic Matching: Beating 1 − 1/e, FOCS 2009, pp. 117–126. https://arxiv.org/abs/0905.4100
R. M. Karp, U. V. Vazirani and V. V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, STOC 1990, pp. 352–358. https://doi.org/10.1145/100216.100262

10 thms1 active userReviewed

Partial Differential Equations Probability Stochastic Systems·Captain: mikedeng1

Diffusion Approximation for Fully Coupled Stochastic Differential Equations 1: The Parametric Poisson Equation Has a Unique Centered Solution with Optimal Regularity in x and yResearch Paper

Motivation

Poisson equations for the generator of an ergodic diffusion are a standard tool in stochastic averaging, homogenization and diffusion approximation: to show that a fast ergodic component averages out in a slow equation, one writes the fluctuation $f(X_t,Y_t)$ as $\mathscr L_0 u$ and applies Itô's formula to $u$ . This requires a solution $u$ whose regularity is controlled in two variables at once: the fast variable $x$ , in which the operator is elliptic, and the slow variable $y$ , which enters as a parameter.

Pardoux and Veretennikov (Ann. Probab. 2001, 2003, 2005) studied this equation in the whole space $\mathbb R^{d_1}$ and used it for diffusion approximation of slow–fast SDEs. In parts I and III the operator does not depend on the parameter, and the solution's regularity in $x$ is of Sobolev type; regularity in $y$ was obtained by differentiating the associated semigroup in the parameter (Röckner–Xie, Remark 2.2(iii) and p. 1213).
Röckner and Xie (2021) prove optimal Hölder regularity in $x$ and show that regularity in $y$ follows from it, for fully coupled coefficients that depend on both variables and are only Hölder continuous. This mission formalizes that result (their Theorem 2.1) and the steps of its proof.

Setting

Fix $d_1,d_2\ge1$ , a matrix field $a(x,y)=(a^{ij}(x,y))$ and a vector field $b(x,y)\in\mathbb R^{d_1}$ on $\mathbb R^{d_1}\times\mathbb R^{d_2}$ . The frozen operator acts on functions of $x$ with $y$ held fixed:

\mathscr L_0(x,y)=\sum_{i,j=1}^{d_1}a^{ij}(x,y)\frac{\partial^2}{\partial x_i\partial x_j}+\sum_{i=1}^{d_1}b^i(x,y)\frac{\partial}{\partial x_i}.

The Poisson equation (1.1) is $\mathscr L_0(x,y)u(x,y)=f(x,y)$ for all $x\in\mathbb R^{d_1}$ , for each parameter $y\in\mathbb R^{d_2}$ .

The standing assumptions are:

(Aσ): $a=\sigma\sigma^*$ is uniformly nondegenerate, i.e. $\lambda^{-1}|\xi|^2\le|a(x,y)\xi|^2\le\lambda|\xi|^2$ for some $\lambda>1$ ;
(Ab): $\lim_{|x|\to\infty}\sup_y\langle x,b(x,y)\rangle=-\infty$ , a weak recurrence condition.

Under these, for each $y$ the frozen diffusion $dX_t=b(X_t,y)\,dt+\sigma(X_t,y)\,dW_t$ has a unique invariant measure $\mu^y$ . Since constants solve $\mathscr L_0u=0$ , the equation is only solvable for centered right-hand sides, $\int f(x,y)\,\mu^y(dx)=0$ for every $y$ (1.3), and the solution is fixed by requiring it to be centered as well.

Regularity is measured in weighted Hölder classes. $f\in C^{\delta,0}_p$ ( $0<\delta\le1$ ) means $|f(x,y)|\le C(1+|x|^m)$ and $|f(x_1,y)-f(x_2,y)|\le C(|x_1-x_2|^\delta\wedge1)(1+|x_1|^m+|x_2|^m)$ , uniformly in $y$ . $C^{\delta,\eta}_p$ adds $\eta$ derivatives in $y$ , with a $(\eta-[\eta])$ -Hölder top derivative. The subscript $b$ denotes the bounded version, and $C^{2+\delta,\eta}_p$ asks the same of $\nabla^2_xu$ together with growth bounds on $u$ and $\nabla_xu$ .

Formalization targets

Goal: Theorem 2.1

If (Aσ), (Ab) hold and $a,b\in C^{\delta,\eta}_b$ with $0<\delta\le1$ , $\eta\ge0$ , then for every centered $f\in C^{\delta,\eta}_p$ there is a unique centered $u\in C^{2+\delta,\eta}_p$ with $\mathscr L_0u=f$ . For some $C_0,m>0$ ,

|u|+|\nabla_xu|+|\nabla^2_xu|\le C_0(1+|x|^m),\qquad|\nabla^2_xu(x_1,y)-\nabla^2_xu(x_2,y)|\le C_0(|x_1-x_2|^\delta\wedge1)(1+|x_1|^m+|x_2|^m),

and, for $\eta>0$ , $\|u(x,\cdot)\|_{C^\eta_b}\le C_0(1+|x|^m)$ .

Milestones, in the order of the proof

The transfer formula for $\eta=1$ (Remark 3.3(ii), Lemma 3.2(i)): if $u\in C^{2+\delta,0}_p$ solves $\mathscr L_0u=h-\bar h$ , then

\partial_y\int h(x,y)\,\mu^y(dx)=\int\Big[\partial_yh-\frac{\partial\mathscr L_0}{\partial y}u\Big](x,y)\,\mu^y(dx).

The increment formula (3.10) for $\eta\in(0,1)$ (Lemma 3.2(ii)), with $\bar h\in C^\eta_b$ .
Theorem 2.1 for $\eta=0$ : existence, uniqueness and the $x$ -estimates (2.1)–(2.2).
Step 3: the right-hand side $\partial_yf-\partial_y\mathscr L_0\,u$ of the differentiated equation is centered.
Step 3: for $\eta=1$ the solution satisfies $\partial_yu\in C^{2+\delta,0}_p$ and $|\partial_yu|\le C(1+|x|^m)$ .
Step 4: for $\eta\in(0,1)$ , $|u(x,y_1)-u(x,y_2)|\le C(|y_1-y_2|^\eta\wedge1)(1+|x|^m)$ .

Significance

The theorem supplies the corrector used in Theorem 2.3 of the same paper, the weak convergence rate of the slow component of a fully coupled multiscale SDE to its averaged limit. Its form, regularity in $y$ matching that of the data and no derivative of $\mu^y$ in $y$ , is what lets the rates depend only on the regularity of the coefficients in the slow variable. The transfer formulas (3.9)–(3.10) also show that averaged coefficients $\bar h(y)=\int h\,d\mu^y$ inherit the $y$ -regularity of $h$ , a question that comes up in every averaging or homogenization limit.

The result is proved in the paper. None of it is formalized: Lean and Mathlib have no fundamental solutions of non-divergence elliptic operators, no Schauder theory and no invariant measures of diffusions. The mission poses the statements, so that the proof can be built in layers and the parts that do not depend on the Gaussian kernel bounds (the transfer formulas given a solution, the induction in Steps 3–4) can be proved separately.

Difficulty

Existence and the estimates (2.1)–(2.2) rest on the probabilistic representation $u=\int_0^\infty T_tf\,dt$ and on Gaussian bounds and ergodic decay for the fundamental solution $p_t(x,x';y)$ of $\mathscr L_0(\cdot,y)$ (Lemma 3.1, cited from Ladyzhenskaya–Solonnikov–Ural'tseva and Pardoux–Veretennikov II, Proposition 3). The coefficients are only Hölder in $x$ , so the Hessian bound needs the cancellation $\int\nabla^2_xp_t\,dx'$ (3.3), not just a size estimate on $\nabla^2_xp_t$ . The obvious approach to $y$ -regularity, differentiating $T_tf$ or $\mu^y$ in $y$ , needs derivatives of the invariant density in the parameter, which are hard to control. The paper's route, differentiating the equation and using the transfer formula to recenter, only works if the differentiated right-hand side is again centered. That centering is the content of Lemma 3.2.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d); $\nabla_x$ , $\nabla^2_x$ are fderiv and iteratedFDeriv ℝ 2 in $x$ , $\partial^j_y$ is iteratedFDeriv ℝ j in $y$ , with operator norms. $y$ -derivatives in the milestones are directional.
(Aσ) includes symmetric positive semidefiniteness of $a$ (the content of $a=\sigma\sigma^*$ ). (Ab) is the $\forall M\,\exists R$ form.
$\mu^y$ is a hypothesis: a family of probability measures, each infinitesimally invariant for $\mathscr L_0(\cdot,y)$ ( $\int\mathscr L_0g\,d\mu^y=0$ for smooth compactly supported $g$ ). Under the assumptions this is the unique invariant measure of the frozen SDE (1.7); the SDE itself is not formalized. No moment bounds on $\mu^y$ are assumed, since they are consequences.
Centering includes $\mu^y$ -integrability, and every integral formula in a conclusion asserts integrability of its integrand, so no statement can hold through a junk zero integral.
The classes include the polynomial growth bound and all lower $y$ -derivatives; matrix coefficients are in $C^{\delta,\eta}_b$ entrywise; $\eta\ge0$ is real, split as $[\eta]+$ fractional part; a $y$ -derivative is read as continuous ( $C^k$ in $y$ ). The $C^\eta_b$ norm is in max form.
Not posed: the clause that $C_0,m$ depend "only on $d_1,d_2$ , $\|a\|_{C^{\delta,0}_b}$ , $\|b\|_{C^{\delta,0}_b}$ , $[f]_{C^{\delta,0}_p}$ ", which is false as printed ( $[f]_{C^{\delta,0}_p}$ is a supremum over the unit ball, and $\lambda$ and the rate in (Ab) are missing), and the recursive constant $\mathcal K_\eta$ of (2.4)–(2.5). The constants exist for each fixed $(a,b,f)$ . (2.1)–(2.2), printed under "Case η = 0", are asserted for every $\eta$ .
Uniqueness is stated for the whole class $C^{2+\delta,\eta}_p$ , not only among solutions that satisfy the estimates. Without the invariance of $\mu^y$ for the same $a,b$ , or without centering, the statement would be false; both are part of the hypotheses.
Useful contributions beyond this mission: Hölder spaces with polynomial weights, fundamental solutions of non-divergence-form operators, invariant measures of elliptic diffusions, and the identification of infinitesimally invariant measures with invariant measures of the diffusion.

Selected references

M. Röckner, L. Xie, Diffusion approximation for fully coupled stochastic differential equations, Ann. Probab. 49(3), 1205–1236, 2021. https://doi.org/10.1214/20-AOP1475
E. Pardoux, A. Yu. Veretennikov, On the Poisson equation and diffusion approximation. I, Ann. Probab. 29(3), 1061–1085, 2001. https://doi.org/10.1214/aop/1015345596
E. Pardoux, A. Yu. Veretennikov, On Poisson equation and diffusion approximation. II, Ann. Probab. 31(3), 1166–1192, 2003. https://doi.org/10.1214/aop/1055425774
E. Pardoux, A. Yu. Veretennikov, On the Poisson equation and diffusion approximation 3, Ann. Probab. 33(3), 1111–1133, 2005. https://doi.org/10.1214/009117905000000062
O. A. Ladyzhenskaya, V. A. Solonnikov, N. N. Ural'tseva, Linear and Quasi-linear Equations of Parabolic Type, AMS Translations of Mathematical Monographs 23, 1968. https://mathscinet.ams.org/mathscinet-getitem?mr=0241822

8 thms1 active userReviewed

Dynamical Systems Stochastic Systems·Captain: mikedeng1

On Well-Posedness of Forward–Backward SDEs—A Unified Approach 3: With Constant Coefficients, σ₃ ≠ 0, σ₃h ≠ 1 the Dominating ODE Keeps y and (1 − σ₃y)⁻¹ Bounded for Every T Iff One of Four Cases HoldsResearch Paper

Motivation

A forward–backward stochastic differential equation (FBSDE) couples a forward diffusion $X$ with a backward equation for a pair $(Y,Z)$ whose terminal value depends on $X_T$ . Such systems arise from the stochastic maximum principle, from option pricing with large investors, and from stochastic differential games. Whether an FBSDE with Lipschitz coefficients has a unique solution on an arbitrary horizon $[0,T]$ is a classical question: small-time solvability is easy, but global solvability can fail even for linear equations.

J. Ma, Z. Wu, D. Zhang and J. Zhang, On well-posedness of forward–backward SDEs—a unified approach (arXiv:1110.4658v2, Ann. Appl. Probab. 25 (2015)), reduce well-posedness to the existence of bounded solutions of two deterministic dominating ordinary differential equations, obtained from the difference quotients of the coefficients. For linear FBSDEs with constant coefficients the two dominating ODEs coincide, and the authors give sharp criteria for global solvability. This mission formalizes the criterion in the case $\sigma_3\neq0$ , where the dominating ODE has a rational right-hand side with a pole.

Earlier global results for coupled FBSDEs rested on the four-step scheme (Ma–Protter–Yong 1994) or on monotonicity conditions (Hu–Peng 1995); §7.4 of the paper compares the dominating-ODE approach with these methods.

Setting

The linear FBSDE (4.1) with constant coefficients is determined by nine reals $b_1,b_2,b_3,\sigma_1,\sigma_2,\sigma_3,f_1,f_2,f_3$ and a terminal slope $h$ . Its dominating function is (3.9),

F(y)=f_1+f_2y+y(b_1+b_2y)+\frac{(f_3+b_3y)\,y\,(\sigma_1+\sigma_2y)}{1-\sigma_3y},

defined for $y\neq1/\sigma_3$ . When $\sigma_3\neq0$ it can be rewritten as (5.8),

F(y)=\frac{\alpha_0}{1/\sigma_3-y}+\alpha_1+\alpha_2y+\alpha_3y^2,\qquad \alpha_3=b_2-\frac{b_3\sigma_2}{\sigma_3},

for constants $\alpha_0,\alpha_1,\alpha_2$ . The dominating ODE (5.3) is the backward integral equation

y_t=h+\int_t^TF(y_s)\,ds,\qquad t\in[0,T].

The paper needs a solution satisfying (5.9): both $y$ and $(1-\sigma_3y)^{-1}$ are bounded on $[0,T]$ . Since $y_T=h$ , this forces $\sigma_3h\neq1$ (Remark 5.5).

The comparison tool is Lemma 5.1. For measurable $F^0,F^1,F^2$ it gives a unique solution of $y^0_t=h^0+\int_t^TF^0(s,y^0_s)\,ds$ lying between a sub-solution $y^1$ and a super-solution $y^2$ of perturbed equations (5.2).

Formalization targets

Goal: Theorem 5.6 (corrected)

For $\sigma_3\neq0$ and $h\sigma_3\neq1$ , the ODE (5.3) has a solution satisfying (5.9) for every $T>0$ if and only if one of the following holds:

$h<1/\sigma_3$ , $F(h)\le0$ , and $F$ has a zero in $(-\infty,h]$ or $\alpha_3=0$ ;
$h>1/\sigma_3$ , $F(h)\ge0$ , and $F$ has a zero in $[h,\infty)$ or $\alpha_3=0$ ;
$h<1/\sigma_3$ , $F(h)\ge0$ , and $F$ has a zero in $[h,1/\sigma_3)$ or $F(y)\to0$ as $y\uparrow1/\sigma_3$ ;
$h>1/\sigma_3$ , $F(h)\le0$ , and $F$ has a zero in $(1/\sigma_3,h]$ or $F(y)\to0$ as $y\downarrow1/\sigma_3$ .

The limit alternatives in cases 3 and 4 are not printed in the paper. Without them the equivalence is false. Take $\sigma_3=1$ , $f_1=1$ , $f_2=-1$ , all other coefficients $0$ , and $h=0$ . Then $F(y)=1-y$ , and $y_t=1-e^{t-T}$ satisfies (5.9) on every horizon, yet none of the printed cases holds. The gap is in the Appendix (p. 48): it asserts that $F$ is positive on the closed interval $[h,\sigma_3^{-1}]$ when $\alpha_0=0$ , which fails when the polynomial part vanishes at the pole. A companion item records the counterexample.

Milestones

The milestones follow the paper's proof:

the decomposition (5.8);
the comparison Lemma 5.1;
the three sufficiency arguments of p. 23 (case (i) with a zero, case (i) with $\alpha_3=0$ , case (iii));
the necessity bounds of the Appendix:
- in case (i): a zero exists when $\alpha_3>0$ , and $F(y)\le-\varepsilon(h+1-y)^2$ when $\alpha_3<0$ and there is no zero;
- in case (iii): a zero exists when $\alpha_0<0$ , and $F(y)\ge\varepsilon(\sigma_3^{-1}-y)^{-1}$ when $\alpha_0>0$ and there is no zero;
the comparison with the explicit solution $(\sigma_3^{-1}-\tilde y_t)^2=(\sigma_3^{-1}-h)^2-2\varepsilon(T-t)$ ;
the case $\alpha_0=0$ , with the endpoint positivity made a hypothesis.

Significance

In the paper, Theorem 5.6 is the sharp solvability criterion for linear FBSDEs with constant coefficients and $\sigma_3\neq0$ . The paper describes these sharp conditions as setting the "limits" for the solvability of general FBSDEs, and the nonlinear Theorems 5.9–5.11 and the main well-posedness Theorem 7.4 are modelled on them. Because the criterion is an equivalence, it also says when no regular decoupling field can be built from the dominating ODE, whatever the horizon.

The result is proved in the paper, but the printed statement is not correct as an equivalence (see above). The mission states and asks for a corrected version, a machine-checked counterexample to the printed one, and formal versions of each step of the proof. The deterministic parts (comparison for backward integral equations, finite-time blow-up of scalar autonomous ODEs, pole-reaching for rational vector fields) are basic real analysis with no current Lean library. They are reusable well beyond FBSDEs. No part of this paper has a machine-checked proof.

Difficulty

Each sufficiency case is an a priori bound: a comparison with a constant or explicitly solvable equation keeps the solution in a fixed interval away from the pole. The difficulty is on the necessity side, where three kinds of failure must be excluded:

blow-up to $\pm\infty$ when $\alpha_3\neq0$ has the wrong sign;
reaching the pole in finite time when $\alpha_0>0$ ;
reaching the pole when $\alpha_0=0$ .

The obvious argument for the last case, " $F$ is bounded below by a positive constant up to the pole", is exactly what fails when $F$ tends to $0$ at the pole. There the solution approaches the pole only asymptotically, and the right criterion is the corrected one above. A second subtlety is that $F$ is only locally Lipschitz off the pole, so comparison must be carried out on a band in which the solution provably stays.

Formalization scope

Time is real, with $0\le t\le T$ and $T>0$ . The coefficients form a record Coeffs of nine reals, and Coeffs.F is (3.9) verbatim. A solution on $[0,T]$ is a function $y:\mathbb R\to\mathbb R$ such that, for every $t\in[0,T]$ , the integrand $s\mapsto F(y_s)$ is integrable on $[t,T]$ and $y_t=h+\int_t^TF(y_s)\,ds$ ; values outside $[0,T]$ are irrelevant. Condition (5.9) is a uniform bound on $|y|$ together with $|1-\sigma_3y_t|\ge\kappa$ for some $\kappa>0$ . "For arbitrary $T$ " is a universal quantifier over $T>0$ outside the existential.

Lean's conventions are total, so several trivializing formalizations are ruled out explicitly:

Lean's integral of a non-integrable function is $0$ , so integrability is part of the solution predicate.
Lean's $x/0=0$ gives Coeffs.F a junk value at the pole. No statement evaluates $F$ there: every zero point, bound and limit in the statements lives strictly on one side of $1/\sigma_3$ .
(5.9) is never encoded as a bound on the Lean inverse $(1-\sigma_3y)^{-1}$ , which is $0$ at the pole.
$\sigma_3\neq0$ is assumed wherever $\alpha_3$ or $1/\sigma_3$ appears.
Lemma 5.1 adds the hypothesis $y^1\le y^2$ , without which it is false, and asks the $c^i$ to be integrable.

The constants $\alpha_0,\alpha_1,\alpha_2$ of (5.8) enter the necessity milestones only through the decomposition hypothesis, never through a formula.

The development needs a Picard–Lindelöf or comparison argument for backward scalar integral equations with locally Lipschitz right-hand sides, monotonicity of autonomous scalar solutions, and the intermediate value theorem. Contributions of a general comparison lemma for scalar integral equations would serve this mission and both other missions of the series.

Selected references

J. Ma, Z. Wu, D. Zhang, J. Zhang, On well-posedness of forward–backward SDEs—a unified approach, Ann. Appl. Probab. 25(4):2168–2214, 2015. arXiv:1110.4658v2, doi:10.1214/14-AAP1046
J. Ma, P. Protter, J. Yong, Solving forward–backward stochastic differential equations explicitly—a four step scheme, Probab. Theory Related Fields 98:339–359, 1994. doi:10.1007/BF01192258
Y. Hu, S. Peng, Solution of forward–backward stochastic differential equations, Probab. Theory Related Fields 103:273–283, 1995. doi:10.1007/BF01204218
J. Ma, J. Yong, Forward–Backward Stochastic Differential Equations and Their Applications, Lecture Notes in Math. 1702, Springer, 1999. doi:10.1007/978-3-540-48831-6

14 thms1 active userReviewed

Mathematical Physics Probability·Captain: mikedeng1

Conformal Weldings of Random Surfaces: SLE and the Quantum Gravity Zipper 1: Reverse SLE_κ/GFF Coupling — Zipping Up a Free Boundary GFF by a Reverse Loewner Flow Preserves Its LawResearch Paper

Motivation

Liouville quantum gravity describes random surfaces whose area measure is formally $e^{\gamma h(z)}dz$ , where $h$ is a Gaussian free field (GFF). Schramm–Loewner evolution (SLE $_\kappa$ ) describes random fractal curves that arise as scaling limits of interfaces in critical lattice models. Sheffield's paper Conformal weldings of random surfaces: SLE and the quantum gravity zipper (arXiv:1012.4797, Ann. Probab. 44 (2016), DOI 10.1214/15-AOP1055) shows that the two theories fit together: SLE curves are the interfaces obtained by conformally welding independent quantum surfaces along their boundaries.

The starting point of that program is a coupling between the reverse Loewner flow and the free boundary GFF (Theorem 1.2 of the paper): zipping up the upper half-plane by a reverse SLE $_\kappa$ map, and changing coordinates by the rule of Liouville quantum gravity, does not change the law of the field. This mission formalizes that theorem and the calculations of §4.1 that prove it.

Timeline. Couplings of forward SLE with the GFF go back to Schramm–Sheffield for $\kappa=4$ (arXiv:1008.2447) and to Dubédat for general $\kappa$ (arXiv:0712.3018). The reverse coupling with the free boundary GFF and the factor $Q\log|f_T'|$ is Sheffield's (2010 preprint, published 2016); it underlies the later mating-of-trees theory of Duplantier–Miller–Sheffield (arXiv:1409.7055).

Setting

Let $\mathbb H=\{z\in\mathbb C:\operatorname{Im}z>0\}$ . A test function is a smooth, compactly supported real function $\rho$ with support in $\mathbb H$ ; it has mean zero if $\int_{\mathbb H}\rho(z)\,dz=0$ . For a function $F$ write $(F,\rho)=\int F\rho\,dz$ .

The free boundary Green's function is $G(y,z)=-\log|y-z|-\log|y-\bar z|$ , and the energy of two test functions is

E(\rho_1,\rho_2)=\int_{\mathbb H}\int_{\mathbb H}\rho_1(y)\,G(y,z)\,\rho_2(z)\,dy\,dz .

A free boundary GFF $\tilde h$ is a random modulo-additive-constant distribution: for every family of mean-zero test functions $\rho_1,\dots,\rho_n$ , the vector $((\tilde h,\rho_j))_j$ is a centred Gaussian vector with covariance $(E(\rho_i,\rho_j))_{i,j}$ . Pairings with test functions of nonzero mean are not defined.

Fix $\kappa>0$ and a standard Brownian motion $B$ , and put $W_t=\sqrt\kappa B_t$ . The reverse Loewner flow is $f_t(z)=g_t(z)-W_t$ , where for each $z\in\mathbb H$

\partial_t g_t(z)=\frac{-2}{g_t(z)-W_t},\qquad g_0(z)=z ,

the pathwise form of $df_t(z)=\frac{-2}{f_t(z)}dt-\sqrt\kappa\,dB_t$ . Write $f_t'=\partial_zf_t$ and

Q=\frac{2}{\sqrt\kappa}+\frac{\sqrt\kappa}{2},\qquad \mathfrak h_0(z)=\frac{2}{\sqrt\kappa}\log|z|,\qquad \mathfrak h_t(z)=\mathfrak h_0(f_t(z))+Q\log|f_t'(z)| .

The fraktur $\mathfrak h_t$ are deterministic functionals of the flow. Finally $G_t(y,z)=G(f_t(y),f_t(z))$ , $E_t(\rho_1,\rho_2)=\iint\rho_1(y)G_t(y,z)\rho_2(z)\,dy\,dz$ , and $C_t(z)=-\log\operatorname{Im}f_t(z)-\log|f_t'(z)|$ .

Formalization targets

Goal: Theorem 1.2

For every $T>0$ , with $\tilde h$ independent of $B$ ,

\mathfrak h_0+\tilde h\ \overset{d}{=}\ \mathfrak h_T+\tilde h\circ f_T\qquad\text{(modulo additive constants),}

that is, the pairing vectors with every finite family of mean-zero test functions have the same law. Here $(\tilde h\circ f_T,\rho)=(\tilde h,|(f_T^{-1})'|^2\rho\circ f_T^{-1})$ .

Milestones (in the order the proof uses them)

The reverse-flow table on p. 44: $\frac{d}{dt}f_t'(z)=2f_t'(z)/f_t(z)^2$ .
The table on p. 47: $\frac{d}{dt}G_t(y,z)=-\operatorname{Re}\frac{2}{f_t(y)}\operatorname{Re}\frac{2}{f_t(z)}$ .
$\operatorname{Im}f_t(z)$ is strictly increasing in $t$ .
$|\partial_tC_t(z)|$ is bounded uniformly for $z$ in a compact subset of $\mathbb H$ and all $t$ .
For fixed $z$ , $\mathfrak h_t(z)$ is a martingale.
For mean-zero $\rho$ , $(\mathfrak h_t,\rho)$ is a martingale.
For fixed $x\neq y$ , $\mathfrak h_t(x)\mathfrak h_t(y)+G_t(x,y)$ is a martingale.
(4.2): $(\mathfrak h_t,\rho_1)(\mathfrak h_t,\rho_2)+E_t(\rho_1,\rho_2)$ is a martingale.
The one-dimensional law: mixing $\mathcal N((\mathfrak h_T,\rho),E_T(\rho))$ over $B$ gives $\mathcal N((\mathfrak h_0,\rho),E(\rho,\rho))$ .
Proposition 3.1: a random modulo-constant distribution whose mean-zero pairings are $\mathcal N(0,E(\rho,\rho))$ is the free boundary GFF.

Significance

The result. Theorem 1.2 says that the free boundary quantum surface $(\mathbb H,\mathfrak h_0+\tilde h)$ is invariant in law under zipping up by an independent reverse SLE $_\kappa$ for a fixed time. It is the stationarity statement behind the quantum gravity zipper: Theorems 1.3–1.4 and 1.8 of the paper (the welding of boundary arcs of equal quantum length, treated in the companion mission) start from it, and the subsequent theory of quantum wedges, quantum cones and mating of trees uses it as a basic tool. It also gives an alternate way to sample the field: first sample $B$ (hence the curve), then sample an independent GFF, and form $\mathfrak h_T+\tilde h\circ f_T$ .

Formalizing it. The theorem is proved in the literature, and the paper itself regards several steps as standard (Proposition 3.1 is cited to [She07]). No part of it has a machine-checked proof. A complete development would give Lean its first Gaussian free field, its first reverse Loewner flow, and martingale statements for SLE functionals; the deterministic Loewner calculus of milestones 1–4 is useful independently of the probabilistic part.

Difficulty

The time derivatives in milestones 1–3 are routine once the flow is known to be holomorphic in $z$ , and milestone 4 follows from them. The obstacle is upgrading local martingales to martingales and exchanging the stochastic dynamics with integration in $z$ . Itô's formula gives that $\mathfrak h_t(z)$ is a continuous local martingale; that it is a true martingale needs the bound of milestone 4, which shows that it is a Brownian motion run for a time at most a constant times $t$ . Passing from points to $(\mathfrak h_t,\rho)$ and to (4.2) needs integrability of $\mathfrak h_t(z)$ uniformly on the support of $\rho$ and a Fubini argument. Mathlib has neither Itô calculus nor quadratic variation, so these steps need either a stochastic-calculus library or a direct argument. The final step (milestones 9–10) needs the Cramér–Wold device for an infinite-dimensional Gaussian field and the change of variables $E(\rho^{f_T})=E_T(\rho)$ .

Formalization scope

$\mathbb H$ is the open set $\{0<\operatorname{Im}z\}$ of $\mathbb C$ as a real normed space; test functions are Mathlib's 𝓓(ℍ, ℝ); integrals are Bochner integrals for Lebesgue measure on $\mathbb C$ and $\mathbb C\times\mathbb C$ .
The free boundary GFF is a predicate on a map $\Omega\to$ (test functions $\to\mathbb R$ ): measurable pairings, and multivariateGaussian 0 (E(ρ_i,ρ_j)) laws for every mean-zero family. Every statement pairs only with mean-zero test functions.
The Green's function carries no factor $1/(2\pi)$ (the Dirichlet inner product carries $(2\pi)^{-1}$ ).
The reverse Loewner flow is pathwise: an ODE in $t$ for $g_t=f_t+W_t$ , required for every $z\in\mathbb H$ and $t\ge0$ . Time is $\mathbb R_{\ge0}$ . The deterministic milestones are stated for every continuous driving function.
$B$ is Mathlib's IsBrownianReal, taken with every path continuous and every coordinate measurable; martingales are with respect to its natural filtration and hold for all $t\ge0$ .
The goal is stated through the conditional law given $B$ : the $P$ -mixture of $\mathcal N\big(((\mathfrak h_T,\rho_j))_j,(E_T(\rho_i,\rho_j))\big)$ equals the law of $((\mathfrak h_0,\rho_j)+(\tilde h,\rho_j))_j$ , with $\tilde h$ on its own probability space. The mixture is a lower Lebesgue integral of set probabilities.
A trivializing formalization would define $E_t$ with the forward Green's function, mix over a measure other than the law of $B$ , or let the GFF predicate fix only one-dimensional laws; none of these is used, and Proposition 3.1 is stated separately.
Welcome contributions: a Loewner-ODE library (existence, uniqueness, holomorphy in $z$ ), Gaussian free field infrastructure, and martingale arguments without Itô calculus.

Selected references

S. Sheffield, Conformal weldings of random surfaces: SLE and the quantum gravity zipper, Ann. Probab. 44(5) (2016), 3474–3545. arXiv:1012.4797, DOI 10.1214/15-AOP1055
S. Sheffield, Gaussian free fields for mathematicians, Probab. Theory Related Fields 139 (2007), 521–541. arXiv:math/0312099
O. Schramm, S. Sheffield, A contour line of the continuum Gaussian free field, Probab. Theory Related Fields 157 (2013), 47–80. arXiv:1008.2447
J. Dubédat, SLE and the free field: partition functions and couplings, J. Amer. Math. Soc. 22 (2009), 995–1054. arXiv:0712.3018
B. Duplantier, S. Sheffield, Liouville quantum gravity and KPZ, Invent. Math. 185 (2011), 333–393. arXiv:0808.1560
B. Duplantier, J. Miller, S. Sheffield, Liouville quantum gravity as a mating of trees, Astérisque 427 (2021). arXiv:1409.7055

14 thms1 active userReviewed

Probability Stochastic Systems·Captain: mikedeng1

On Well-Posedness of Forward–Backward SDEs—A Unified Approach 1: Under Cases I–III the FBSDE Has a Decoupling Field with Bounded Difference Quotients and a Unique L² Solution on [0, T]Research Paper

Motivation

A forward–backward stochastic differential equation (FBSDE) couples a forward SDE, solved from an initial state, with a backward SDE, solved from a terminal condition that depends on the forward state. Such systems arise from the stochastic maximum principle, from quasilinear parabolic PDEs through Feynman–Kac formulas, and in mathematical finance. Whenever a control problem or a market model is solved through its first-order conditions, a fully coupled FBSDE appears, and the question is whether it has a unique solution.

The history has a recurring gap: each method covers a different regime, and none handles coefficients that are random, fully coupled, and have a forward diffusion depending on the martingale integrand $Z$ , over an arbitrary horizon.

1993: F. Antonelli proved well-posedness over a small time interval by contraction, under a smallness condition on the coupling.
1994: J. Ma, P. Protter and J. Yong introduced the four-step scheme, solving Markovian FBSDEs with deterministic coefficients over arbitrary horizons through a quasilinear PDE; the forward diffusion may not depend on $z$ in a degenerate way.
1995–1999: Y. Hu, S. Peng and Z. Wu developed the method of continuation, which allows random coefficients over arbitrary horizons under a monotonicity condition on the coefficients.
1999–2002: E. Pardoux and S. Tang, and F. Delarue, extended the PDE and fixed-point approaches under weak-coupling or strong-monotonicity conditions, in the Markovian setting.
2015: J. Ma, Z. Wu, D. Zhang and J. Zhang (the source of this mission) gave a unified approach through the decoupling field and a scalar ordinary differential equation that dominates its spatial derivative.

Setting

Fix a horizon $T>0$ and a probability space carrying a one-dimensional Brownian motion $B$ , with $\mathbb F$ its natural filtration augmented by the null sets. All processes are real valued. The FBSDE (1.1) is

X_t=x+\int_0^t b(s,\Theta_s)\,ds+\int_0^t\sigma(s,\Theta_s)\,dB_s,\qquad Y_t=g(X_T)+\int_t^T f(s,\Theta_s)\,ds-\int_t^T Z_s\,dB_s ,

for $t\in[0,T]$ , with $\Theta=(X,Y,Z)$ . The coefficients $b,\sigma,f$ depend on $(t,\omega,x,y,z)$ and $g$ on $(x,\omega)$ . Assumption 2.1 asks that they be progressively measurable for fixed $(x,y,z)$ , that $I_0^2=\mathbb E\{(\int_0^T[|b|+|f|](t,0,0,0)dt)^2+\int_0^T|\sigma|^2(t,0,0,0)dt+|g(0)|^2\}$ be finite, and that they be Lipschitz in $(x,y,z)$ with a common constant $K_0$ , uniformly in $\omega$ . Solutions are sought in the space $\mathbb L^2$ of progressively measurable $\Theta$ with $\|\Theta\|^2_{\mathbb L^2}=\mathbb E\{\sup_t(|X_t|^2+|Y_t|^2)+\int_0^T|Z_t|^2dt\}<\infty$ .

A decoupling field (Definition 2.2) is a random field $u(t,x)$ with $u(T,\cdot)=g$ such that, on every short interval $[t_1,t_2]$ and from every square-integrable initial state, the FBSDE with terminal map $u(t_2,\cdot)$ is uniquely solvable and its solution satisfies $Y_t=u(t,X_t)$ .

The difference quotients (3.1) of the coefficients — $\tilde b_i,\tilde\sigma_i,\tilde f_i$ in the variables $x,y,z$ ( $i=1,2,3$ ) and $\tilde h$ for $g$ — enter the scalar function

F=f_1+f_2y+y(b_1+b_2y)+\frac{(f_3+b_3y)\,y\,(\sigma_1+\sigma_2y)}{1-\sigma_3y},

and its essential supremum $\overline F(t,y)$ and infimum $\underline F(t,y)$ over all quotients give the dominating ODEs (3.13): $\overline y_t=\overline h+\int_t^T\overline F(s,\overline y_s)ds$ and $\underline y_t=\underline h+\int_t^T\underline F(s,\underline y_s)ds$ , with $\overline h,\underline h$ the bounds of $\tilde h$ .

Formalization targets

Goal: Theorem 7.4

Fix $c_1,c_2,c_3$ with $c_1>0$ , $0<c_2<c_3$ , $c_1c_3<1$ (5.13). There are $\varepsilon>0$ and $C>0$ , depending only on $T$ , $K_0$ and $c_1,c_2,c_3$ , such that whenever Assumption 2.1 holds and the quotients satisfy one of the nine conditions of Cases I–III ((5.14); (5.15)–(5.18); (5.19)–(5.22)), uniformly in the quotient arguments, then (i) the FBSDE has a decoupling field $u$ whose quotient $(u(t,x_1)-u(t,x_2))/(x_1-x_2)$ obeys the bound assumed of $\tilde h$ with $c_2$ replaced by $c_3$ , and (ii) for every $x$ there is a unique solution in $\mathbb L^2$ , with

\|\Theta\|^2_{\mathbb L^2}\le C\,\big[\,|x|^2+I_0^2\,\big].

Milestones

Lemma 5.1: comparison for scalar backward ODEs between a sub- and a super-solution.
Theorems 5.9, 5.10, 5.11: under each case, the dominating ODEs have bounded solutions with the bound of $h$ transported to $c_3$ , and $1-\sigma_3y$ stays away from $0$ .
Theorems 6.1, 6.2, 6.3: over a short horizon $T\le\delta$ , unique solvability, solutions of (3.13) in a band, and a random field $u$ whose quotients lie between $\underline y$ and $\overline y$ .
Theorem 2.3: a decoupling field gives a unique global solution with $Y_t=u(t,X_t)$ .

A companion statement, Corollary 7.5, gives well-posedness over $[0,T]$ under the sign conditions (7.5) or (7.6), with no smallness constant.

Significance

The theorem replaces structural assumptions (small horizon, monotonicity, deterministic coefficients, $\sigma$ independent of $z$ ) by conditions that can be read off the coefficients through a scalar ODE. It covers random coefficients and a forward diffusion that depends on $z$ , the case in which the classical Riccati-type obstruction $\sigma_3h=1$ appears, and it recovers the earlier sufficient conditions as special cases (§7.4 of the paper). The decoupling field produced in (i) is uniformly Lipschitz, which is the input to the comparison and stability results of §8 and to numerical schemes based on $Y_t=u(t,X_t)$ .

The result is proved in the paper; nothing here is open mathematically. None of it is formalized: there is no machine-checked existence theory for coupled FBSDEs in any proof assistant this mission is aware of. A complete development would be the first formal well-posedness theorem for a fully coupled FBSDE, and the milestones — the ODE comparison lemma, the small-time theory, and the patching argument of Theorem 2.3 — are each self-contained.

Difficulty

The obvious approach is a contraction argument on $[0,T]$ . It works only when $T$ is small, because the Lipschitz constant of the solution map grows with the coupling; iterating it over a partition requires a terminal condition $u(t_i,\cdot)$ whose Lipschitz constant does not deteriorate from one subinterval to the next. Controlling that constant is the whole problem. Its spatial derivative satisfies a backward stochastic Riccati equation with quadratic growth in both $y$ and $z$ and a singularity where $1-\sigma_3y=0$ ; such equations need not have bounded solutions, and the standard comparison theory for quadratic BSDEs does not apply off the region where the generator is Lipschitz. A second difficulty is the small-time theory itself: when $\sigma$ depends on $z$ , even a linear FBSDE with constant coefficients is well posed on short intervals only if $\sigma_3h\ne1$ (Theorem 7.1 of the paper), so in Cases II and III, where $\sigma_3$ and $h$ are large, the contraction argument does not apply even for small $T$ .

Formalization scope

The development reuses the platform's Peng1990.SMP.Stochastic (standard Brownian motion, $L^2_{\mathcal F}$ , the $L^2$ Itô integral IsItoIntegral) and the augmented Brownian filtration of ReflectedBSDE.Existence.Setting. Time is $\mathbb R_{\ge0}$ , time integrals are over real intervals, and the stochastic integral $\int_{t_1}^t\sigma\,dB$ is $J_t-J_{t_1}$ for an Itô integral process $J$ of $\mathbf 1_{(t_1,t_2]}\sigma(s,\Theta_s)$ .

Committed conventions:

Lipschitz bounds use the $\ell^1$ norm on $\mathbb R^3$ and hold for every $\omega$ ; $I_0^2$ and $\|\Theta\|^2_{\mathbb L^2}$ are lower Lebesgue integrals in $[0,\infty]$ .
Uniqueness is uniqueness in $\mathbb L^2$ : $X,Y$ agree a.s. at each time and $Z$ agrees $dt\otimes d\mathbb P$ -a.e.
Solutions are unique only up to modification, so (7.2) is asserted for one solution in $\mathbb L^2$ .
Definition 2.2's " $0=t_1<t_2\le T$ " is read as $0\le t_1$ , as the proof of Theorem 2.3 uses it.
Every condition on the quotients holds for every $t\in[0,T]$ , almost surely, for all arguments with distinct coordinates. $\overline F(t,c)\le\varepsilon$ is stated in exactly that form. $\overline F,\underline F,\overline h,\underline h$ as functions are $\mathrm{EReal}$ -valued, and solutions of (3.13) keep them finite.
" $(1-\sigma_3y)^{-1}$ is bounded" is $|1-\tilde\sigma_3y_t|\ge\kappa>0$ . Every use of $\alpha_3=b_2-b_3\sigma_2/\sigma_3$ carries $\tilde\sigma_3\ne0$ , and (5.19), (5.21) carry the heading $\sigma_3\ne0$ of Table 3 in the goal.
The quotient bounds on $u$ hold for each $t$ and each pair $x_1\ne x_2$ almost surely.
Lemma 5.1 additionally assumes $y^1\le y^2$ and $L\ge0$ , both implicit on the page.

The constants $\varepsilon$ , $\delta$ and $C$ are chosen before the probability space and the coefficients. A formalization that places them after the coefficients, integrates without integrability, divides at the pole $1-\sigma_3y=0$ , uses a real-valued essential supremum of an unbounded family, or states uniqueness without a solution class would make the statements vacuous or false; none of these is used.

Contributions are welcome on every milestone. The ODE layer (Lemma 5.1 and the a priori bounds of Theorems 5.9–5.11) needs only real analysis and is a natural first target. The stochastic layer needs Itô-integral facts (linearity, restriction to subintervals, the Burkholder–Davis–Gundy and Doob inequalities in $L^2$ ) and the Lipschitz BSDE theory; these are reusable well beyond this mission.

Selected references

J. Ma, Z. Wu, D. Zhang, J. Zhang, On well-posedness of forward–backward SDEs—a unified approach, Ann. Appl. Probab. 25(4):2168–2214, 2015. https://arxiv.org/abs/1110.4658
F. Antonelli, Backward–forward stochastic differential equations, Ann. Appl. Probab. 3(3):777–793, 1993. https://doi.org/10.1214/aoap/1177005363
J. Ma, P. Protter, J. Yong, Solving forward–backward stochastic differential equations explicitly — a four step scheme, Probab. Theory Related Fields 98:339–359, 1994. https://doi.org/10.1007/BF01192258
Y. Hu, S. Peng, Solution of forward–backward stochastic differential equations, Probab. Theory Related Fields 103:273–283, 1995. https://doi.org/10.1007/BF01204218
S. Peng, Z. Wu, Fully coupled forward–backward stochastic differential equations and applications to optimal control, SIAM J. Control Optim. 37(3):825–843, 1999. https://doi.org/10.1137/S0363012996313549
F. Delarue, On the existence and uniqueness of solutions to FBSDEs in a non-degenerate case, Stochastic Process. Appl. 99:209–286, 2002. https://doi.org/10.1016/S0304-4149(02)00085-6
J. Ma, J. Yong, Forward–Backward Stochastic Differential Equations and their Applications, Lecture Notes in Math. 1702, Springer, 1999. https://doi.org/10.1007/978-3-540-48831-6

14 thms1 active userReviewed

Algebraic Geometry Optimization·Captain: mikedeng1

Exploiting Symmetries in SDP-Relaxations for Polynomial Optimization 1: A G-Linear Functional Is Integration Against a G-Invariant Measure on K iff Its Symmetrized Localizing Forms Are PSDResearch Paper

Motivation

Polynomial optimization asks for the minimum $f^*$ of a polynomial $f$ over a set $K\subseteq\mathbb R^n$ cut out by polynomial inequalities. Lasserre's moment relaxation (Lasserre 2001) replaces the minimization over points by a minimization over probability measures on $K$ , and then over linear functionals on polynomials that satisfy semidefinite constraints. The bridge between measures and semidefinite constraints is Putinar's theorem (Putinar 1993): on a compact basic semialgebraic set with an Archimedean description, a linear functional comes from a measure exactly when it is nonnegative on the quadratic module of the constraints.

Many problems of practical size are invariant under a group of linear transformations: permutations of variables, sign changes, rotations of a polygon. Gatermann and Parrilo (2004) showed how such symmetry block-diagonalizes sums-of-squares programs. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 2013) carry the reduction to the moment side. Their first step, Theorem 3.2, is a symmetric version of Putinar's theorem: for invariant data it suffices to consider functionals that are themselves invariant, and these are characterized by positivity of symmetrized localizing forms. This mission formalizes that theorem.

Setting

Write $\mathbb R[X]=\mathbb R[X_1,\dots,X_n]$ . Let $G$ be a finite subgroup of $\mathrm{GL}_n(\mathbb R)$ . A matrix $\sigma\in G$ acts on points by $x\mapsto\sigma x$ and on polynomials by

p^\sigma(x):=p(\sigma^{-1}x),

the linear substitution $X_i\mapsto\sum_j(\sigma^{-1})_{ij}X_j$ . A polynomial is $G$ -invariant if $p^\sigma=p$ for every $\sigma\in G$ .

Fix $g_1,\dots,g_m\in\mathbb R[X]$ and the feasible set

K=\{x\in\mathbb R^n:\ g_j(x)\ge0,\ j=1,\dots,m\}.

Assumption 2.1 requires $K$ to be compact and some polynomial $u=u_0+\sum_j u_jg_j$ , with sums of squares $u_0,\dots,u_m$ , to have a compact superlevel set $\{u\ge0\}$ . Put $g_0:=1$ .

A linear map $L^G:\mathbb R[X]\to\mathbb R$ is $G$ -linear if $L^G(f)=L^G(f^\sigma)$ for all $f$ and all $\sigma\in G$ . Its symmetrized localizing forms are

\mathcal L^G_{g_j}(p,q)=L^G\Big(\frac1{|G|}\sum_{\sigma\in G}(p\cdot q)^\sigma\cdot g_j\Big),\qquad 0\le j\le m.

For a Borel measure $\mu$ on $\mathbb R^n$ , $\mu^\sigma(B)=\mu(\sigma^{-1}(B))$ is its image under $x\mapsto\sigma x$ , and $\mu$ is $G$ -invariant if $\mu^\sigma=\mu$ for all $\sigma\in G$ . A measure on $K$ is one with $\mu(\mathbb R^n\setminus K)=0$ .

Formalization targets

Goal: Theorem 3.2

If the $g_j$ are $G$ -invariant and Assumption 2.1 holds, then for a $G$ -linear $L^G$ : $\exists\,\mu\ \text{finite, $G$-invariant, on }K:\ \ L^G(p)=\int p\,d\mu\ \ \forall p \quad\Longleftrightarrow\quad \mathcal L^G_{g_j}(p,p)\ge0\ \ \forall p\in\mathbb R[X],\ \forall\, 0\le j\le m.$

Milestones

Theorem 2.2 (Putinar). Under Assumption 2.1, a linear $L$ is integration against a probability measure on $K$ iff $L(1)=1$ and $L(s_0+\sum_js_jg_j)\ge0$ for all sums of squares $s_0,\dots,s_m$ .
Averaging identity (p. 10). For $G$ -linear $L^G$ : $L^G(p)=\frac1{|G|}\sum_\sigma L^G(p^\sigma)=L^G\big(\frac1{|G|}\sum_\sigma p^\sigma\big)$ .
Only-if computation (p. 11). For a finite $G$ -invariant $\mu$ on compact $K$ and invariant $g_j$ : $\int\frac1{|G|}\sum_\sigma(f^2)^\sigma g_j\,d\mu=\int f^2g_j\,d\mu\ge0$ .
If computation (p. 11). For $G$ -linear $L^G$ and invariant $g$ : $\mathcal L^G_g(h,h)=L^G(h^2g)$ .
Invariance from moments (p. 11). A finite measure on compact $K$ with $\int h\,d\mu=\int h^\sigma d\mu$ for every polynomial $h$ and every $\sigma\in G$ is $G$ -invariant.

Significance

The result. Theorem 3.2 turns the moment relaxation of a $G$ -invariant problem into one over $G$ -linear functionals. Such a functional is determined by its values on the invariant ring $\mathbb R[X]^G$ , so its moment variables are indexed by a basis of invariants instead of all monomials (Example 3.3 of the paper: five variables instead of fifteen for $C_4$ on $\mathbb R^4$ in degree 2). The block-diagonalized relaxations and the convergence result of §3 (Theorems 3.4–3.7) rest on it.

Formalizing it. The theorem is proved in the paper, modulo Putinar's theorem, which is cited. Neither Putinar's theorem nor any Archimedean Positivstellensatz is in Mathlib or on the platform. A complete formalization therefore needs (i) Putinar's theorem itself, in its dual moment form, and (ii) the determinacy of compactly supported finite measures by polynomial moments in several variables. Both are reusable well beyond this paper: every moment-SOS hierarchy result in the literature cites them.

Difficulty

The group-theoretic steps (milestones 2–4) are finite averaging and change of variables. The weight of the theorem sits in two analytic facts. The first is Putinar's theorem: nonnegativity on the quadratic module is an algebraic condition, and producing a measure from it requires the Archimedean hypothesis of Assumption 2.1 in an essential way; without that hypothesis the statement is false in general. The second is that the measure Putinar's theorem returns has to be shown $G$ -invariant. Equality of the polynomial moments of $\mu$ and $\mu^\sigma$ does not by itself identify two measures; it does so here because both are finite and carried by a compact set, where polynomials are dense in the continuous functions. A further detail: Putinar's theorem is stated for normalized functionals, and Theorem 3.2 is not normalized, so the degenerate case $L^G(1)=0$ must be shown to force $L^G=0$ .

Formalization scope

Polynomials are MvPolynomial (Fin n) ℝ, points Fin n → ℝ, and $G$ a Subgroup (GL (Fin n) ℝ) with a Fintype instance. The action on polynomials is the linear substitution aeval, so $G$ is an arbitrary finite matrix group, not only a permutation group. Sums of squares are Mathlib's IsSumSq. "psd" for the symmetric form $\mathcal L^G_{g_j}$ means $\mathcal L^G_{g_j}(p,p)\ge0$ for every polynomial $p$ , with no degree truncation; $j=0$ ( $g_0=1$ ) is included. Measures live on the Borel σ-algebra of $\mathbb R^n$ , $\mu^\sigma$ is Measure.map along the continuous (hence measurable) map $x\mapsto\sigma x$ , and "measure on $K$ " is $\mu(\mathbb R^n\setminus K)=0$ .

Committed conventions and disclosed readings:

Finite measure. The paper writes "a $G$ -invariant measure on $K$ ". It is formalized as a finite Borel measure; this is the reading that makes $\int p\,d\mu$ meaningful for every polynomial, and finite measures on a compact set make every polynomial integrable.
No normalization. As on the page, Theorem 3.2 has neither $L^G(1)=1$ nor a probability measure; Theorem 2.2 has both.
Direction of $\mu^\sigma$ . With $\mu^\sigma$ the image of $\mu$ under $\sigma$ , one has $\int h^\sigma d\mu=\int h\,d\mu^{\sigma^{-1}}$ , where the paper writes $\int h\,d\mu^\sigma$ . Statements quantify over all $\sigma\in G$ , so the difference does not change their content.

Trivializing formalizations are ruled out: integrals are taken only against finite measures carried by a compact set, so no statement holds because a Bochner integral of a non-integrable function is $0$ ; positivity is through the forms on all of $\mathbb R[X]$ , not replaced by pointwise nonnegativity; and the invariance of $\mu$ is a conclusion of milestone 5, never a hypothesis.

Contributions welcome: Putinar's theorem (milestone 1) and multivariate moment determinacy on compact sets are the reusable infrastructure; the averaging milestones are a natural first entry point.

Selected references

C. Riener, T. Theobald, L. Jansson Andrén, J. B. Lasserre, Exploiting symmetries in SDP-relaxations for polynomial optimization, Math. Oper. Res. 38(1):122–141, 2013. arXiv:1103.0486v3, doi:10.1287/moor.1120.0558
M. Putinar, Positive polynomials on compact semi-algebraic sets, Indiana Univ. Math. J. 42(3):969–984, 1993. doi:10.1512/iumj.1993.42.42045
J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11(3):796–817, 2001. doi:10.1137/S1052623400366802
K. Gatermann, P. A. Parrilo, Symmetry groups, semidefinite programs, and sums of squares, J. Pure Appl. Algebra 192:95–128, 2004. doi:10.1016/j.jpaa.2003.12.011

7 thms1 active userReviewed

Probability Stochastic Systems·Captain: mikedeng1

Affine Volterra Processes 3: Global Solutions with Nonpositive Real Part of the Square-Root Riccati–Volterra EquationResearch Paper

Motivation

The Volterra square-root model describes a nonnegative, time-dependent state whose present value depends on a weighted history. Ordinary square-root diffusions use a constant kernel and have a Markov state; replacing that kernel by a function of elapsed time allows persistent or singular memory. This matters for the transform formulas used to characterize distributions of such processes. Those formulas depend on a deterministic nonlinear integral equation, and require a solution that exists at every finite time. Abi Jaber, Larsson and Pulido isolate that requirement in Lemma 6.3 of Affine Volterra processes, arXiv:1708.08796v3 (2019).

The paper's Section 6 treats processes in the nonnegative orthant and its Section 7 specializes the framework to a Volterra Heston model. The present mission concerns the deterministic equation behind the Section 6 transform. The stochastic existence theorem and the transform identity are separate results in the same paper. Keeping this mission on the integral equation makes its analytic content usable independently of a chosen probability space.

Setting

Fix a finite coordinate set of size $d$ . A diagonal kernel consists of real functions $K_i(t)$ for $t\ge0$ , with the $i$ -th entry of the matrix kernel equal to $K_i$ and all off-diagonal entries zero. A resolvent of the first kind for $K_i$ is a nonnegative measure $L_i$ for which the convolution $K_i*L_i$ equals one at positive times. The relevant regularity condition, labeled (2.5), requires local square integrability and positive-time translation bounds of order $h^{\gamma_i}$ for some $\gamma_i\in(0,2]$ . Condition (3.4) requires a kernel to be nonnegative, nonzero, nonincreasing and continuous at positive times. It also requires its resolvent measure to have decreasing interval masses $L_i([s,s+t])$ as $s$ increases. Each shifted function $\Delta_hK_i(t)=K_i(t+h)$ must satisfy (3.4) for $0\le h\le1$ , with its own resolvent. These are the assumptions of Theorem 6.1 and hence of its Lemma 6.3 (pp. 6, 14, 28–29).

Let $u=(u_i)$ be a complex row vector and let $f(t)=(f_i(t))$ be a locally integrable complex row function. Let $B$ be a real matrix whose off-diagonal entries are nonnegative, and let $\sigma_i>0$ . The $i$ -th square-root Riccati–Volterra equation is

\psi_i(t)=u_iK_i(t)+\int_0^t K_i(t-s)\left(f_i(s)+\sum_j\psi_j(s)B_{ji}+\frac{\sigma_i^2}{2}\psi_i(s)^2\right)\,ds.

The index $B_{ji}$ selects column $i$ : in the paper's notation $B=(b^1\;\cdots\;b^d)$ and the coupling is $\psi(s)b^i$ . The kernel acts only on the $i$ -th equation, while $B$ couples the coordinates. The coefficient $b^0$ from the stochastic process does not enter this equation (equation (6.3), p. 27).

Formalization targets

The goal is the global existence, uniqueness and sign statement of Lemma 6.3. If $\operatorname{Re}u_i\le0$ and $\operatorname{Re}f_i\le0$ , then

\exists!\,\psi\in L^2_{\mathrm{loc}}(\mathbb R_+,\mathbb C^d) \quad\text{solving (6.3) globally, with}\quad \operatorname{Re}\psi_i\le0\quad\text{for every }i.

For functions defined only up to null sets, the equation, uniqueness and sign conclusion are understood almost everywhere. The goal has no fixed time horizon and no hard-coded kernel: it covers every diagonal kernel satisfying the paper's conditions. The five milestones record the source's analytic support: the shifted resolvent bounds (3.9)–(3.10), the $L^2$ stability lemma C.1, maximal-solution Theorem B.1, global-solution Corollary B.3 and nonnegative-orthant invariance Theorem C.2. Their statements and locations are recorded in the milestone list.

Significance

Global solvability makes the square-root transform equation meaningful at any finite horizon. Uniqueness fixes the transform parameter determined by a kernel and forcing function. The nonpositive real part is the sign property needed in the paper's subsequent exponential-affine transform argument for nonnegative states (Theorem 6.1(ii), pp. 28–29). Without a global solution, that argument would only address a time interval before a possible blow-up.

The result is proved in the cited paper; this mission asks for a machine-checked development of that known theorem and its supporting integral-equation results. Its reusable output includes an $L^2$ notion of Volterra solution, the first-kind resolvent hypotheses, maximal lifetime, stability under changes of forcing and kernel, and a comparison statement for diagonal systems. The goal and milestones are presently proof obligations, not claims of existing machine-checked proofs.

Difficulty

Local solvability alone does not control the quadratic term $\psi_i^2$ for arbitrarily large time. In particular, a generic local fixed-point theorem can yield a maximal solution whose $L^2$ norm diverges at a finite horizon. Sign information for the real part is also coupled to the imaginary part through that quadratic term; checking each coordinate independently does not establish invariance of the nonpositive half-plane. The analysis has to preserve the kernel's first-kind resolvent conditions and the off-diagonal sign pattern of $B$ across the coupled system. Singular kernels allowed by (2.5) prevent replacing the problem with a standard ordinary differential equation.

Formalization scope

Time is represented by real numbers and every local $L^p$ condition is restricted to positive bounded intervals. Vectors are functions on Fin d; matrix $L^p$ membership is componentwise. These finite-dimensional norms are equivalent to the Euclidean and operator norms used in the paper. The kernel regularity estimates are Big-O statements as $h$ tends to zero through positive values. A first-kind resolvent is a nonnegative measure supported on nonnegative times, with the convolution identity and interval-mass monotonicity stated directly. The convolution at positive time is an interval integral; the bound at zero in (3.10) uses the integral on $[0,0]$ , while the source describes a right-continuous extension when available.

Solutions are locally square integrable and satisfy their equations almost everywhere. The integrability of each asserted convolution is part of the solution predicate, so the default zero value of a nonintegrable Lean integral cannot create a spurious solution. A maximal lifetime is extended-nonnegative-real valued, allowing infinity, and a finite lifetime requires an infinite extended $L^2$ norm. Sign conditions on locally integrable forcing and on the solution are almost everywhere. Measurable time dependence of the nonlinear drift is made explicit for Theorem B.1 and Corollary B.3, where it is necessary to interpret their integrals. The condition $b^0\ge0$ of the square-root process is omitted from the goal because $b^0$ is absent from (6.3).

The development needs Mathlib's Bochner integrals, local $L^p$ predicates, measures, complex arithmetic and asymptotic filters. Proof contributions to the five source milestones and the goal are welcome, including infrastructure for nonconvolution Volterra resolvents where the paper cites earlier literature. The formalization must keep the coefficient $\sigma_i^2/2$ , the column index $B_{ji}$ , and every shift $h\in[0,1]$ .

Selected references

E. Abi Jaber, M. Larsson and S. Pulido, Affine Volterra processes, arXiv:1708.08796v3, 2019. Preprint.
G. Gripenberg, S.-O. Londen and O. Staffans, Volterra Integral and Functional Equations, Cambridge University Press, 1990. DOI.

8 thms1 active userReviewed

Probability Stochastic Systems·Captain: mikedeng1

Affine Volterra Processes 2: The Exponential-Affine Transform Formula via the Riccati–Volterra EquationResearch Paper

Motivation

Many stochastic models have a present state that depends on a weighted history of past drift and noise. A stochastic Volterra equation captures this dependence through a kernel $K$ : a recent increment and an older increment can enter the current state with different weights. Classical affine diffusions arise from the special constant kernel $K=I$ . For those diffusions, conditional Fourier–Laplace transforms can often be found from finite-dimensional Riccati ordinary differential equations. The paper by Abi Jaber, Larsson and Pulido asks for an analogous transform when the kernel retains memory. Its Theorem 4.3 gives a formula for a continuous affine Volterra process under a stated Riccati–Volterra solution assumption.

The result matters for models in which the history cannot be replaced by the current state alone. The transform characterizes conditional distributions and integrated path functionals in the form used by the paper's later results. The present mission isolates Theorem 4.3 and four of its stated supporting claims. The paper proves these results; the mission seeks machine-checked proofs of their Lean statements.

Setting

Fix a positive integer $d$ and a deterministic, matrix-valued kernel $K:[0,\infty)\to\mathbb R^{d\times d}$ whose entries are locally square integrable. The Volterra convolution of $K$ with a vector function $v$ is $(K*v)(t)=\int_0^t K(t-s)v(s)\,ds$ . Matrix convolutions retain the order of multiplication: $(K*R)(t)=\int_0^t K(t-s)R(s)\,ds$ .

Let $A^0,\ldots,A^d$ be real symmetric matrices and $b^0,\ldots,b^d$ real column vectors. Their affine covariance and drift are $a(x)=A^0+\sum_i x_iA^i$ and $b(x)=b^0+\sum_i x_i b^i$ . The matrix $B=(b^1\ \cdots\ b^d)$ has the $b^i$ as columns. For a complex row $u$ , write $A(u)=(uA^1u^\top,\ldots,uA^du^\top)$ ; the transpose is ordinary, with no complex conjugation.

An affine Volterra process $X$ is a continuous solution of

X_t=x_0+\int_0^t K(t-s)b(X_s)\,ds+\int_0^t K(t-s)\sigma(X_s)\,dW_s.

Here $W$ is a $d$ -dimensional Brownian motion on a usual stochastic basis, $x_0$ is deterministic, and $X$ stays in a state space $E$ . The continuous coefficient $\sigma$ obeys $\sigma(x)\sigma(x)^\top=a(x)$ on $E$ , where $a(x)$ is positive semidefinite. This is Definition 4.1 and the standing setting of Section 4 of the paper.

Formalization targets

The main target is Theorem 4.3. Fix a finite horizon $T$ , a complex row $u$ , and an integrable complex-row function $f$ . Suppose a square-integrable function $\psi$ solves the Riccati–Volterra equation

\psi=uK+\bigl(f+\psi B+\tfrac12A(\psi)\bigr)*K.

Define $Y$ by the stochastic integral and drift in equations (4.4)–(4.5). The theorem identifies $Y_t$ with a conditional mean plus a quadratic correction:

Y_t=\mathbb E[uX_T+(f*X)_T\mid\mathcal F_t] +\tfrac12\int_t^T\psi(T-s)a(\mathbb E[X_s\mid\mathcal F_t])\psi(T-s)^\top\,ds, \qquad 0\le t\le T.

It also states that $e^{Y}$ is a local martingale on $[0,T]$ . If it is a true martingale, then the exponential-affine transform formula is

\mathbb E\!\left[e^{uX_T+(f*X)_T}\mid\mathcal F_t\right]=e^{Y_t},\qquad t\le T.

The milestone list records Lemma 4.2's conditional and unconditional means, the mean Volterra equation stated in the proof of Theorem 4.3, the resolvent commutation claim in the proof of Lemma 4.4, and Lemma 4.4's equivalent Riccati equation. A second-kind resolvent $R_B$ of $-KB$ uses the paper's sign convention $H*R_B=R_B*H=H-R_B$ for $H=-KB$ ; the equivalent equation uses $E_B=K-R_B*K$ .

Significance

The conditional transform links a path-dependent stochastic equation to a deterministic nonlinear Volterra equation. It supplies a way to describe the law of a future state together with a linear functional of its past. The conditional-mean milestone separately gives a usable formula for $\mathbb E[X_T\mid\mathcal F_t]$ , while the resolvent milestones identify the deterministic kernel relations needed by the transform.

The source provides proofs of these claims. The formalization task is to check their assumptions and equalities against a precise model of Brownian Itô integration, conditional expectation, and matrix convolution. Published Lean definitions for Brownian motion and an Itô integral relation are reused. The affine Volterra process, its Riccati equation, and these theorem statements are drafted here; their proofs remain open.

Difficulty

The conditional payoff involves the entire path before $T$ , while $X$ generally has no finite-dimensional Markov state. Consequently, the familiar affine-diffusion formula in terms of $X_t$ alone is not the target of Theorem 4.3. Deterministic matrix convolutions are order-sensitive, and the two resolvents of $-KB$ and $-BK$ have different kernels. Stochastic convolutions also have integrands that depend on the terminal time. The passage from fixed-time integral equalities to a continuous local-martingale process requires care about versions and filtration adaptation.

Formalization scope

Processes use nonnegative real time, while deterministic kernels and interval integrals use real time. Finite-dimensional $L^p$ conditions are checked componentwise. Kernel and resolvent identities between locally integrable functions hold almost everywhere on positive time. Riccati equations hold almost everywhere on $[0,T]$ ; stochastic and conditional identities hold almost surely at each fixed time. The local-martingale claim uses the real and imaginary parts of the complex exponential, stopped at $T$ .

The process definition includes the Section 4 assumptions on symmetry, covariance positivity, continuity of $\sigma$ , deterministic $x_0$ , and the usual stochastic basis. Brownian Itô terms are constrained by the published integral relation. Deterministic drift convolutions require integrable integrands. The theorem asserts integrability of the payoff and of $X_s$ as conclusions, preventing conditional expectation from defaulting to zero. In (4.6) the conditional means $\mathbb E[X_s\mid\mathcal F_t]$ enter the $ds$ -integral through a jointly measurable version in $(s,\omega)$ , so that integral cannot default to zero. The dimension is positive, and the theorem does not specialize the kernel to $I$ or insert a resolvent assumption into its goal.

A complete development will need reusable results on locally integrable matrix kernels and their resolvents, stochastic Fubini interchange, moment bounds for Volterra solutions, and conditional expectation of the resulting integrals. The moment bound is posed as Lemma 3.1 in the companion existence mission. This draft includes the four listed milestones; Lemmas 2.1 and 2.5 from the source are left for a fuller stochastic Fubini and semimartingale encoding. Contributions that preserve their general hypotheses and conclusions are welcome.

Selected references

E. Abi Jaber, M. Larsson, and S. Pulido, Affine Volterra processes, arXiv:1708.08796v3, 2019. Preprint

14 thms1 active userReviewed

Probability Stochastic Systems·Captain: mikedeng1

Affine Volterra Processes 1: Nonnegative Weak Solutions of Stochastic Volterra Equations with Resolvent-Monotone KernelsResearch Paper

Motivation

Many stochastic models use a process whose response to a disturbance depends on the time elapsed since that disturbance. An ordinary stochastic differential equation uses only the current state and instantaneous coefficients. A stochastic Volterra equation instead weights its past drift and noise through a convolution kernel. Such equations include the constant kernel as a familiar limiting case, while singular or decaying kernels allow different memory patterns. The paper Affine Volterra processes studies this class to obtain non-Markovian models that retain tractable affine transform formulas. Before any transform can be used for a nonnegative state variable, the underlying equation must actually admit a solution that stays nonnegative. Abi Jaber, Larsson and Pulido, §§1–3.

The mission focuses on the paper's existence and invariance theorem, Theorem 3.6 of the pinned preprint. It is a separate question from uniqueness or explicit transforms: the coefficients are only continuous with linear growth, so classical contraction arguments for Lipschitz coefficients do not directly settle it. The proof also has to preserve the boundary of the nonnegative orthant despite a drift and noise term that depend on the entire past. Abi Jaber, Larsson and Pulido, Theorems 3.3–3.6.

Setting

Fix dimensions $d,m\ge0$ . The kernel $K$ is a deterministic function from nonnegative time to real $d\times d$ matrices. The drift $b$ maps $\mathbb R^d$ to $\mathbb R^d$ , and the diffusion coefficient $\sigma$ maps $\mathbb R^d$ to real $d\times m$ matrices. Given a deterministic initial state $x_0$ and an $m$ -dimensional Brownian motion $W$ , a continuous adapted process $X$ solves

X_t=x_0+\int_0^t K(t-s)b(X_s)\,ds+ \int_0^t K(t-s)\sigma(X_s)\,dW_s,\qquad t\ge0.

The deterministic and stochastic terms are matrix-vector convolutions: an event at time $s$ has an effect at time $t$ weighted by $K(t-s)$ . A weak solution is allowed to choose its stochastic basis and Brownian motion. A strong solution is adapted to the completed filtration generated by its prescribed Brownian motion. All bases satisfy the usual completeness and right-continuity conditions. The equation is read at each fixed time almost surely, with $X$ having continuous sample paths. Abi Jaber, Larsson and Pulido, (1.1), §3.

The paper's condition (2.5) asks each scalar kernel entry to be locally square-integrable and to satisfy two estimates of order $h^\gamma$ as $h\downarrow0$ : the integral of its square over $[0,h]$ , and the squared $L^2$ difference between its time shift by $h$ and itself over each finite interval. The exponent satisfies $0<\gamma\le2$ and may differ by entry. For the goal, $K$ is diagonal. Each diagonal entry $K_i$ is nonnegative, nonzero, nonincreasing and continuous on positive time. Its resolvent of the first kind $L_i$ is a nonnegative measure whose convolution with $K_i$ is the constant one; condition (3.4) also requires the interval mass $L_i([s,s+t])$ to be nonincreasing in $s$ for every $t\ge0$ . Abi Jaber, Larsson and Pulido, (2.5), (2.13), (3.4).

Formalization targets

Nonnegative weak existence

The goal is Theorem 3.6. Write $\mathbb R^d_+=\{x\in\mathbb R^d:x_i\ge0\text{ for all }i\}$ . Suppose $K$ is diagonal and satisfies (2.5) and (3.4) componentwise. Suppose $b$ and $\sigma$ are continuous, satisfy $\max\{|b(x)|,\|\sigma(x)\|\}\le c_{\mathrm{LG}}(1+|x|)$ , and obey the boundary condition for every $x\in\mathbb R^d$ :

x_i=0\quad\Longrightarrow\quad b_i(x)\ge0\ \text{and}\ \sigma_{ik}(x)=0\quad\text{for every }k.

Then the target is

\forall x_0\in\mathbb R^d_+,\quad \exists\text{ a continuous weak solution }X\text{ of (1.1) with }X_t\in\mathbb R^d_+.

The milestone list records the paper's moment bound, strong existence for Lipschitz coefficients, and general weak existence with a first-kind resolvent. They are numbered results from the same preprint and establish distinct parts of the existence framework. Abi Jaber, Larsson and Pulido, Lemma 3.1 and Theorems 3.3, 3.4, 3.6.

Significance

The conclusion says more than finite-time nonnegativity of a proposed process: it asserts that a stochastic basis, Brownian motion and continuous solution actually exist for every nonnegative initial condition under the stated kernel and boundary assumptions. This supports later use of the affine transform results on state spaces with nonnegative coordinates. The paper treats this existence theorem as one of the main inputs to its square-root and rough-volatility examples. Abi Jaber, Larsson and Pulido, §§3, 6.

The theorem is already proved in the source paper. The formalization task is to state and eventually verify that known result in Lean, including the exact memory-kernel condition and the stochastic basis chosen by weak existence. The published Brownian and Itô-integral definitions are reused. A verified solution would leave reusable definitions for Volterra kernels, first-kind resolvents, and weak convolution equations, as well as machine-checked statements for the supporting existence theorems.

Difficulty

For Lipschitz coefficients, the paper obtains a unique strong solution. The goal permits only continuous coefficients of linear growth. Approximating them by better-behaved coefficients does not by itself guarantee that a limit solves the original convolution equation or remains in the nonnegative orthant. The stochastic convolution depends on the full history through $K(t-s)$ , and the boundary condition must be propagated through that memory. A direct appeal to an ordinary SDE invariance theorem therefore does not cover the claim. The first-kind resolvent and the monotonicity in (3.4) are central to the stated assumptions. Abi Jaber, Larsson and Pulido, proofs of Theorems 3.4 and 3.6.

Formalization scope

Lean uses EthierKurtz.SDEState d, a Euclidean $d$ -vector, for states; real matrices for $K$ and $\sigma$ ; nonnegative real process time; and real arguments for deterministic kernels and interval integrals. Local $L^2$ membership is componentwise, which is equivalent to membership under any norm on the finite-dimensional matrix space. The matrix norm in linear growth is the Euclidean operator norm. The big- $O$ bounds in (2.5) are taken as $h$ tends to zero from the right. Each diagonal kernel has its own exponent and its own positive resolvent measure. A general matrix first-kind resolvent is encoded entrywise as the difference of two measures finite on compact positive-time intervals, so it may have infinite total mass.

The weak-solution predicate existentially quantifies the stochastic basis, Brownian motion and continuous process. Each stochastic convolution has a witness satisfying the published Brownian Itô relation; an unconstrained process cannot witness the equation. Drift terms carry interval integrability, avoiding a default-zero value for a nonintegrable integral. The stochastic basis is complete at time zero and right-continuous. The goal asserts orthant membership at every fixed time almost surely; continuous paths yield an orthant-valued version. The zero-time equation and empty-index cases are included. Contributions that formalize stochastic-convolution continuity, compactness of path laws, first-kind resolvent calculus, or invariance of the orthant are in scope.

Selected references

E. Abi Jaber, M. Larsson and S. Pulido, Affine Volterra processes, arXiv:1708.08796v3, 2019. Preprint

12 thms1 active userReviewed

Dynamical Systems Probability Stochastic Systems·Captain: mikedeng1

Averaging Dynamics Driven by Fractional Brownian Motion: Young Solutions of dxⁿ = fₙ(t, xⁿ)dB Converge in Probability in C^α to the Solution of dx = f̄(x)dB When |fₙ − f̄|_{−κ,γ} → 0Research Paper

Why oscillating coefficients matter

An equation driven by fractional Brownian motion can respond to a rapidly varying coefficient even when that coefficient has no useful pointwise limit. Hairer and Li study this issue for fractional Brownian motion with Hurst index above one half. Their Section 3 isolates a deterministic averaging statement: if the time antiderivatives of the coefficients approach those of a limiting coefficient in a suitable negative Hölder norm, the solutions approach the limiting solution in probability. This statement supplies a common target for averaging models whose fast variables have very different origins. The authors use it later with mixing fast processes, and also present a quasi-periodic example. The result and its role in the paper are stated in Hairer and Li, Section 3.

The problem sits at the boundary of two familiar views of differential equations. A pathwise Young equation is defined from individual sufficiently regular paths, whereas the available estimates for the oscillating coefficient and the fractional Brownian driver involve probability and conditional expectation. The mission records the precise point where these descriptions meet. It treats the published article, rather than a preprint, and targets its Theorem 3.13.

Driver, coefficients, and solutions

An $m$ -dimensional fractional Brownian motion $B=(B^1,\ldots,B^m)$ with index $H$ is a centered Gaussian process with independent coordinates and covariance

\mathbb E[B_s^iB_t^j]=\mathbf1_{i=j}\frac{|s|^{2H}+|t|^{2H}-|t-s|^{2H}}2.

The paper works with a two-sided process and $1/2<H<1$ . It uses a version whose sample paths are locally $\beta$ -Hölder for every $\beta<H$ . The mission names that version condition separately, because the covariance law alone does not select particular sample paths. The relevant past sigma algebra at time $s$ is generated by increments $B_u-B_v$ with $u,v\le s$ . These conventions come from pp. 1826 and 1831–1832 of the article.

For a path $x$ on $[0,T]$ , write $|x|_\alpha$ for its homogeneous Hölder seminorm and $|x|_\infty$ for its supremum norm. The norm on $C^\alpha[0,T]$ is $|x|_\infty+|x|_\alpha$ . A Young integral $\int_s^t f_r\,db_r$ is the limit of left-point sums over partitions of $[s,t]$ as the largest cell shrinks to zero. A Young solution from $x_0$ is an $\alpha$ -Hölder path satisfying its integral equation at every time, with value $x_0$ at time zero. Here $BC^2$ means bounded, twice continuously differentiable maps with bounded derivatives through order two; $C^{\zeta,2}$ means $\zeta$ -Hölder in time with values in $BC^2$ . These are the paper's conventions on pp. 1829 and 1835–1838.

The negative Hölder bound $|f|_{-\kappa,\gamma}\le K$ means that the time antiderivative of $f$ has increments bounded by $K|t-s|^{1-\kappa}$ , and that the difference of those increments at spatial points $x,y$ is bounded by $K|t-s|^{1-\kappa}|x-y|^\gamma$ . Both bounds apply on the time window in question when $|t-s|\le1$ . This is equation (3.12) in the article. It measures cancellation over time; it does not require $f(t,x)$ itself to be small.

Formalization targets

The goal is the $dB$ part of Theorem 3.13. Let $f_n$ be $C^{\zeta,2}$ , let the limiting $\bar f$ be autonomous and in $BC^2$ , and suppose $|f_n-\bar f|_{-\kappa,\gamma}\to0$ . The exponents satisfy $1/2<\alpha<H-\kappa$ , $H-\kappa>1/2$ , $H-\kappa+\gamma\alpha>1$ , and $\alpha<\zeta\le1$ . For Young solutions with the same starting point,

dx_t^n=f_n(t,x_t^n)\,dB_t,\qquad dx_t=\bar f(x_t)\,dB_t,

the target is

\forall\varepsilon>0,\qquad P\bigl(\|x^n-x\|_{C^\alpha[0,T]}>\varepsilon\bigr)\longrightarrow0.

The milestone list follows the statements used around this target: the Hölder composition estimate of Lemma 2.1, the RKHS estimate of Lemma 3.3, the fractional Brownian integral estimate of Lemma 3.4, the stochastic sewing lemma of Lemma 3.5, the Young case of (3.18) from Lemmas 3.10 and 3.12, the Kolmogorov inclusions (3.24), and the deterministic stability estimate of Lemma 2.2. Each is a separate formal theorem. The authors' proofs follow their statements in Sections 2 and 3 and the Appendix; Lemma 3.5 is quoted from Lê, Theorem 2.1 without proof in the article.

What the result provides

The target gives convergence of entire solution paths in a Hölder topology, in probability. In the paper, this lets a model-specific estimate of the negative Hölder distance be used to conclude convergence of the corresponding dynamical system. Theorem A is obtained by adding such an estimate for a stationary mixing fast process; the deterministic statement here isolates the part independent of that model. These uses are described in Sections 1 and 3.

The published paper proves the result. This mission asks for machine-checked proofs of the stated Lean theorems. Its reusable work would include a pathwise Young integral over arbitrary partitions, Hölder norms that retain the value $+\infty$ , a two-sided vector fractional Brownian motion interface, and stochastic estimates for time-dependent integrands. The goal and milestones in this proposal are statements with proof placeholders; the local build checks their types, not their proofs.

Main obstruction

Pointwise control of $f_n-\bar f$ is unavailable: a rapidly oscillating function can be large at most times and still have small time antiderivatives. Applying a pathwise Young stability estimate directly to $f_n-\bar f$ therefore leaves a coefficient norm that need not tend to zero. The integral estimate must connect cancellation measured by $|\cdot|_{-\kappa,\gamma}$ with $L^p$ bounds on the driven equation. The dependence on the past of the fractional Brownian motion makes this step more delicate than an estimate for a deterministic integrand. The required estimates and their domains appear in Lemmas 3.4–3.12.

Formalization scope

Time is $\mathbb R$ for the two-sided driver; coefficient and solution assertions use $[0,T]$ with $T>0$ . State spaces are finite-dimensional real Euclidean spaces. The goal takes $H\in(1/2,1)$ from the standing setting of Section 3.1, and it assumes the locally Hölder version of $B$ described on p. 1826. The solutions are required almost surely to satisfy the Young equation from the same $x_0$ . This requirement fixes the processes to the equations; the convergence claim cannot be obtained by choosing arbitrary paths. Probability of the norm event uses the measure of that set, and the conclusion is convergence in probability in the full $C^\alpha$ norm.

The Lean definitions use $[0,\infty]$ for path and process seminorms, so unbounded suprema are not replaced by a default real value. The negative Hölder hypothesis uses real bounds $K_n\to0$ instead of an infimum that could be meaningless on an empty class. The Young integral quantifies over every monotone partition and the mesh limit of its left-point sums. The fBm definition includes Gaussianity, means, and every cross-coordinate covariance; its path version is explicit. Interval integrals in the coefficient bound are applied to time-continuous coefficients in the goal. Lemmas 3.4 and 3.10 use the increment filtration, the case needed for this theorem.

The paper's Lemma 2.2 needs a common initial value for its homogeneous-seminorm estimate; the formal statement includes it and records the printed issue. The paper writes the limiting coefficient with a time argument but uses an autonomous coefficient in (3.23), which the goal adopts. This proposal covers the $dB$ equation. The final $dt$ extension in Theorem 3.13 and the conditional-expectation estimate (3.19) remain outside its current items. Contributions that close these gaps, or supply a general conditional Wiener integral matching the article's notation, would extend the development.

Selected references

M. Hairer and X.-M. Li, Averaging dynamics driven by fractional Brownian motion, Annals of Probability 48(4), 2020, 1826–1860. DOI.
K. Lê, A stochastic sewing lemma and applications, 2018, arXiv:1810.10500, cited as [23] in Hairer and Li. arXiv.

9 thms1 active userReviewed

Missions

Hairer: A Theory of Regularity Structures I — The Reconstruction TheoremResearch Paper

Motivation

Setting

Formalization targets

Goal — reconstruction theorem, Theorem 3.10 for γ>0\gamma>0γ>0

Milestone level — the calculus around the reconstruction operator

Significance

Difficulty

Formalization scope

Selected references

Rudin PMA III: Numerical Sequences and SeriesTextbook

Motivation

Setting

Formalization targets

Goal — Riemann's rearrangement theorem (Theorem 3.54)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Rudin PMA II: Basic TopologyTextbook

Motivation

Setting

Formalization targets

Goal — Heine–Borel (Theorem 2.41)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Rudin PMA I: The Real and Complex Number SystemsTextbook

Motivation

Setting

Formalization targets

Goal — the real field is the unique complete ordered field (Theorem 1.19)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Examples of Pathological Dynamics of the Subgradient Method for Lipschitz Path-Differentiable Functions: A Bounded Subgradient Sequence That Does Not Converge for a Whitney-Stratifiable KŁ FunctionResearch Paper

Motivation

Setting

Formalization targets

Goal

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Dynamic Momentum Strategies: For Horizons Within the Look-Back Period, the Optimal Weight Is the Mean-Variance Weight Plus a Hedging Term Weighted Toward Recent ReturnsResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Fast Hybrid Schemes for Fractional Riccati Equations (Rough Is Not So Tough): Explicit Lower and Upper Bounds on the Convergence Radius of the Fractional Power-Series SolutionResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.3 (a)–(b)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Courier Dispatch in On-Demand Delivery II: In a Crowded Market with Endogenous Demand, Batch Delivery Earns More Exactly Below One Threshold in Wait Cost and in Service RadiusResearch Paper

Why dispatch and pricing interact

Delivery model and limiting revenue

Formalization targets

One threshold for both parameters

Demand and price at the switch

What the result and formalization establish

Where the argument is delicate

Goal — reconstruction theorem, Theorem 3.10 for $\gamma>0$