Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record≤ 2Open frontier

8 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record

3 provers on it7 of 7 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record≤ 2Open frontier

8 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record

3 provers on it7 of 7 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Analysis Functional Analysis Partial Differential Equations·Captain: mikedeng1

Notes on Partial Differential Equations VIII: Strongly Continuous Semigroups and the Lumer–Phillips TheoremTextbook

Motivation

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

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

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

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: the Lumer–Phillips theorem (Theorem 5.38)

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

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

9 thms2 active usersReviewed

Analysis Harmonic Analysis Partial Differential Equations·Captain: mikedeng1

Notes on Partial Differential Equations VII: The Heat Kernel and the Linear Heat and Schrödinger EquationsTextbook

Motivation

The heat equation $u_t = \Delta u$ and the free Schrödinger equation $i u_t = -\Delta u$ are the two model evolution equations of linear PDE on $\mathbb{R}^n$ . The first describes diffusion and is the prototype of every parabolic equation; the second describes a free quantum particle and is the prototype of dispersive wave equations. Both are solved explicitly by the Fourier transform and by convolution with a Gaussian-type kernel, and the estimates obtained from these formulas (smoothing, $L^2$ and $H^s$ energy bounds, $L^1 \to L^\infty$ decay) are the tools later used for nonlinear problems: semilinear heat equations, nonlinear Schrödinger equations, Galerkin constructions for general parabolic PDE, and Strichartz estimates.

This mission formalizes Chapter 5, §§5.1–5.3, of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014, author's copy), which follows the presentation of Taylor's Partial Differential Equations (Taylor, vol. I, Ch. 3). The classical material goes back to Fourier (1822) for the heat kernel and to the analysis of dispersion for the Schrödinger group in the twentieth century; the goal and milestones are textbook results with complete proofs in the literature.

Setting

Write $\mathbb{R}^n$ for Euclidean space with Lebesgue measure, $|x|$ for the Euclidean norm and $\Delta = \sum_i \partial_i^2$ for the Laplacian. The heat kernel is

\Gamma(x,t) = \frac{1}{(4\pi t)^{n/2}}\, e^{-|x|^2/4t}, \qquad x \in \mathbb{R}^n,\ t > 0,

and for data $f$ the heat convolution is $u(x,t) = \int_{\mathbb{R}^n} \Gamma(x-y,t) f(y)\,dy$ .

The Schwartz space $\mathcal S(\mathbb{R}^n)$ consists of smooth functions all of whose derivatives decay faster than every power of $|x|$ , with the Fréchet topology of the seminorms $\sup |x^\alpha \partial^\beta f|$ . A curve $u : I \to \mathcal S$ on a time interval $I$ has a strong derivative $v$ at $t$ if the difference quotients $(u(t+h)-u(t))/h$ converge to $v$ in $\mathcal S$ ; $C^k(I;\mathcal S)$ and $C^\infty(I;\mathcal S)$ are defined with continuous strong derivatives. A Schwartz solution of the heat problem with data $f \in \mathcal S$ is a curve $u \in C([0,\infty);\mathcal S) \cap C^1(0,\infty;\mathcal S)$ with $u(0) = f$ and $u_t(t) = \Delta u(t)$ for $t > 0$ ; a Schwartz solution of the Schrödinger problem is $u \in C^1(\mathbb{R};\mathcal S)$ with $u(0) = f$ and $i u_t = -\Delta u$ for all $t$ .

The Fourier transform is used in the book's normalization,

\hat f(k) = \frac{1}{(2\pi)^n}\int_{\mathbb{R}^n} f(x)\, e^{-ik\cdot x}\,dx,

and, with $\langle k\rangle = (1+|k|^2)^{1/2}$ , the Sobolev norm is $\|f\|_{H^s} = \big((2\pi)^n\int \langle k\rangle^{2s}|\hat f(k)|^2\,dk\big)^{1/2}$ for $s \in \mathbb{R}$ .

Formalization targets

Goal: smoothing by the heat kernel (Theorem 5.5)

Let $1 \le p \le \infty$ and $f \in L^p(\mathbb{R}^n)$ . Then the heat convolution converges absolutely for $t>0$ , $u$ is $C^\infty$ on $\mathbb{R}^n \times (0,\infty)$ , and

u_t = \Delta u \quad (t > 0).

If $p < \infty$ , every derivative of $u$ tends to zero as $|x| \to \infty$ at each fixed $t > 0$ , and

u(\cdot,t) \to f \ \text{ in } L^p \text{ as } t \to 0^+.

This is the chapter's statement that rough data are instantly smoothed while the initial condition is attained in the $L^p$ sense; it involves no Fourier transform.

Milestones

Eq. (5.9): $\Gamma$ is $C^\infty$ on $\mathbb{R}^n \times (0,\infty)$ and $\Gamma_t = \Delta\Gamma$ .
Theorem 5.4: for $f \in \mathcal S$ the heat problem has a unique Schwartz solution; it lies in $C^\infty([0,\infty);\mathcal S)$ , satisfies $\hat u(k,t) = \hat f(k) e^{-t|k|^2}$ , and equals the heat convolution for $t > 0$ .
Theorem 5.8: $\|u(t)\|_{L^2} \le \|f\|_{L^2}$ and $\|u(t)\|_{L^\infty} \le (4\pi t)^{-n/2}\|f\|_{L^1}$ .
Theorem 5.9: $\|u(t)\|_{H^s} \le \|f\|_{H^s}$ for all $s \in \mathbb{R}$ , $t \ge 0$ .
Theorem 5.10: on $[0,T]$ , $\max_t \|u(t)\|_{H^s} \le \|f\|_{H^s}$ and $\|Du\|_{L^2([0,T];H^s)} \le \tfrac{1}{\sqrt 2}\|f\|_{H^s}$ .
Theorem 5.15: for $f \in \mathcal S$ the Schrödinger problem has a unique solution in $C^\infty(\mathbb{R};\mathcal S)$ , with $\hat u(k,t) = e^{-it|k|^2}\hat f(k)$ and $u(\cdot,t) = \Gamma_S(\cdot,t) * f$ for $t \ne 0$ , $\Gamma_S(x,t) = (4\pi i t)^{-n/2} e^{i|x|^2/4t}$ .
Theorem 5.16: $\|u(t)\|_{L^2} \le \|f\|_{L^2}$ , $\|u(t)\|_{L^\infty} \le (4\pi|t|)^{-n/2}\|f\|_{L^1}$ and, for $2<p<\infty$ , $\|u(t)\|_{L^p} \le (4\pi|t|)^{-n(1/2-1/p)}\|f\|_{L^{p'}}$ .
Theorem 5.17: $\|u(t)\|_{H^s} = \|f\|_{H^s}$ for all $s$ and $t$ .

A further item, not a milestone, records that $\int \Gamma(x,t)\,dx = 1$ for $t > 0$ (p. 131).

Significance

The result itself. Theorem 5.5 is the statement that the heat semigroup maps $L^p$ into smooth functions decaying with all derivatives, and that it is strongly continuous on $L^p$ for $p < \infty$ . It is used whenever a parabolic problem with rough data is solved by the Duhamel formula, in particular for the semilinear heat equation in the next part of the chapter. Theorem 5.4 and the energy estimates 5.9–5.10 are the input for generalized $H^s$ solutions (Theorem 5.12) and for Galerkin existence for parabolic PDE in Chapter 6. The Schrödinger estimates 5.16–5.17 are the linear input of the local theory of nonlinear Schrödinger equations and of Strichartz estimates.

Formalizing it. All results are classical and fully proved on paper. Mathlib has Schwartz functions, its own Fourier transform on $\mathcal S$ with Plancherel, Gaussian integrals and Fourier transforms of Gaussians, convolution and approximate identities for compactly supported kernels, and the Laplacian on inner-product spaces. It does not have the heat kernel on $\mathbb{R}^n$ as a solution operator, the differentiation of Schwartz-valued curves, the $H^s$ energy estimates, or the dispersive estimates for the Schrödinger group. A platform development of the heat kernel exists only on $\mathbb{R}^3$ with a viscosity parameter (the Navier–Stokes mission), and the platform's Plancherel theorem is in Mathlib's normalization. The remaining work is to formalize the known proofs in the book's normalization and dimension.

Difficulty

For the goal, the obvious argument is "differentiate under the integral sign and apply the mollifier theorem". Both steps need care in Lean. Differentiation in $(x,t)$ requires domination of every derivative of $\Gamma$ uniformly on neighbourhoods of $(x,t)$ , paired by Hölder's inequality with an arbitrary $f \in L^p$ . The approximation-of-identity result in Mathlib and in the book (Theorem 1.28) is stated for compactly supported mollifiers, whereas $\Gamma(\cdot,t)$ has full support, so the $L^p$ convergence needs the Gaussian version with a tail estimate. The decay of all derivatives as $|x| \to \infty$ relies on $p < \infty$ . For the Schwartz-space results the difficulty is the calculus of $\mathcal S$ -valued curves: strong differentiability is convergence of difference quotients in every Schwartz seminorm, and uniqueness requires passing from the strong equation to the pointwise ODE for $\hat u(k,t)$ . The $L^{p'} \to L^p$ bound (5.16) rests on Riesz–Thorin interpolation, which Mathlib does not have.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with volume; coordinates are 0-based (i : Fin n). $\Delta$ is Mathlib's Laplacian: on functions for the goal and (5.9), and $\Delta : \mathcal S \to \mathcal S$ for the Schwartz solutions. Smoothness is ContDiff/ContDiffOn ℝ ∞.
$\mathcal S$ is Mathlib's SchwartzMap with its Fréchet topology, the same as the book's. Real-valued for the heat equation, complex-valued for Schrödinger. Strong derivatives, $C^\infty(I;\mathcal S)$ and the two solution predicates are defined in HunterPDE.HeatFourier.SchwartzCurve. Uniqueness in Theorem 5.4 is agreement for $t \ge 0$ .
The Fourier transform is the book's $(2\pi)^{-n}\int f e^{-ik\cdot x}$ , defined explicitly; Mathlib's 𝓕 is not used. The $H^s$ norm is $[0,\infty]$ -valued and is the norm of the book's $H^s$ inner product, $\big((2\pi)^n\int\langle k\rangle^{2s}|\hat f|^2\big)^{1/2}$ ; the norm formula printed with Definition 5.74 places $(2\pi)^n$ outside the square root, which differs by the constant $(2\pi)^{n/2}$ and does not affect any statement here, since every $H^s$ inequality and identity has an $H^s$ norm on both sides. $L^p$ norms are eLpNorm in $[0,\infty]$ , and the factors $1/(4\pi|t|)^{\dots}$ in Theorem 5.16 are divisions in $[0,\infty]$ , so $t = 0$ gives the trivial bound $\infty$ .
Corrections of the page. (i) The book states $u \in C_0^\infty(\mathbb{R}^n \times (0,\infty))$ in Theorem 5.5 for every $p \le \infty$ . For $p = \infty$ this fails ( $f \equiv 1$ ), so the decay of derivatives is stated for $p < \infty$ , which is the case its proof covers. " $C_0^\infty$ " is read as the proof explains it: every derivative tends to zero as $|x| \to \infty$ at fixed $t > 0$ . (ii) The Schrödinger kernel is printed as $(4\pi i t)^{-n/2}e^{-i|x|^2/4t}$ . The sign of the exponent contradicts the book's (5.15), so the corrected $e^{+i|x|^2/4t}$ is used, with the principal-branch power.
Theorems 5.9 and 5.10 assume the solution property of Theorem 5.4 rather than $C^\infty$ regularity in time. By Theorem 5.4 this is the same solution. The absolute convergence of (5.5) is part of the goal's conclusion.
Ruling out trivializations. The goal is not the statement " $u$ is smooth": the heat equation, the decay of every derivative and the $L^p$ convergence are all required. No hypothesis restricts $f$ beyond $f \in L^p$ . The solution predicates are satisfiable (the zero curve solves the problem with zero data), and existence in Theorems 5.4 and 5.15 is asserted, not assumed.
Not included: generalized $H^s$ solutions (Definition 5.11, Theorem 5.12), the heat $L^{p'}\to L^p$ bound (5.10), and the Fourier-transform background of Appendix 5.B (Theorems 5.66–5.73). Contributions welcome: a Gaussian approximate-identity theorem in $L^p$ , the $\mathcal S$ -valued calculus of Proposition 5.3, and a conversion lemma between the book's and Mathlib's Fourier normalizations. All three are reusable across this series (semigroups, the semilinear heat equation, NLS).

Selected references

J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, Chapter 5. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
M. E. Taylor, Partial Differential Equations I: Basic Theory, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4419-7055-8
L. C. Evans, Partial Differential Equations, 2nd ed., AMS Graduate Studies in Mathematics 19, 2010, §2.3 and §4.3. https://doi.org/10.1090/gsm/019
T. Cazenave, Semilinear Schrödinger Equations, Courant Lecture Notes 10, AMS, 2003, Ch. 2. https://doi.org/10.1090/cln/010

12 thms2 active usersReviewed

Control Theory Dynamical Systems Linear algebra·Captain: mikedeng1

Stabilization for a Perturbed Chain of Integrators in Prescribed Time I: Prescribed-Time Estimates for the Linear Time-Varying FeedbackResearch Paper

Motivation

Many control tasks have to settle at a given deadline, not merely eventually. Examples are missile guidance, where the interception time is fixed in advance, and rendezvous or consensus manoeuvres that must finish by a scheduled instant. Prescribed-time stabilization asks for a feedback that brings the state of a system to the origin at a time $T>0$ chosen by the designer, independently of the initial condition, and keeps this property under disturbances. It is stronger than finite-time stabilization, where the settling time depends on the initial state, and stronger than fixed-time stabilization, where it is only bounded uniformly.

Song, Wang, Holloway and Krstić (Automatica 2017) obtained prescribed-time regulation of normal-form systems with feedback gains that grow without bound as $t\to T$ . The computations required explicit time derivatives of the gain function. Chitour, Ushirobira and Bouhemou (SIAM J. Control Optim. 2020) recast this construction as time-varying homogeneity: a time-dependent dilation of the state combined with a change of time turns the prescribed-time problem into a standard exponential-stabilization problem on an infinite horizon. The analysis then reduces to linear matrix inequalities. This mission formalizes the linear-feedback part of that paper (§3.1, pp. 1026–1030).

Timeline:

2010: Chitour and Sigalotti (SIAM J. Control Optim. 48) prove a Lyapunov LMI for $J_n - b e_n K^T$ , uniform over a bounded range $\underline b\le b\le\bar b$ .
2017: Song, Wang, Holloway and Krstić give prescribed-time regulation with a time-varying feedback.
2020: Chitour, Ushirobira and Bouhemou remove the upper bound $\bar b$ (Proposition 10) and derive the prescribed-time estimate by time-varying homogeneity (Corollary 14).

Setting

Fix a positive integer $n$ and a prescribed time $T>0$ . Let $(e_i)_{1\le i\le n}$ be the canonical basis of $\mathbb R^n$ , and let $J_n$ be the $n$ -th Jordan block, $J_n e_i = e_{i-1}$ with $e_0=0$ . The perturbed chain of integrators is

\dot x(t) = J_n x(t) + \big(d(t) + b(t)u(t)\big) e_n, \qquad t\in[0,T),

with state $x(t)\in\mathbb R^n$ and control $u(t)\in\mathbb R$ . Here $d$ is a measurable matched disturbance, and $b$ is an uncertain control gain with $b(t)\ge\underline b>0$ and no upper bound.

With weights $r_i = n-i+1$ , the dilation is $D^{\mathbf r}_\mu = \operatorname{diag}(\mu^{r_1},\dots,\mu^{r_n})$ and $D_{\mathbf r} = \operatorname{diag}(r_1,\dots,r_n)$ . An admissible weight is a continuous function $a\ge0$ on $[0,T]$ with $\int_t^T a>0$ for $t<T$ . It defines

\lambda(t) = \frac{1}{\int_t^T a(\xi)\,d\xi},\qquad s(t) = \int_0^t\lambda(\xi)\,d\xi,\qquad 0\le t<T.

The parameter $\lambda$ blows up at $T$ , and $s$ maps $[0,T)$ onto $[0,\infty)$ . In the coordinates $y = D^{\mathbf r}_{\lambda(t)}x$ and the time $s$ , the system becomes

y' = \big(a D_{\mathbf r} + J_n\big)y + (b u + d)e_n .

The feedback studied is $u = -K^T D^{\mathbf r}_\eta y$ , that is $u(t) = -K^T D^{\mathbf r}_{\eta\lambda(t)}x(t)$ in the original variables, where $K\in\mathbb R^n$ and $\eta\ge1$ .

Formalization targets

Goal: Corollary 14 (corrected)

There is a rate $\mu>0$ depending only on $n$ and $\underline b$ such that, for every $T$ and admissible $a$ , there are $K$ and $C>0$ with

|x_i(t)| \le \frac{1}{(\eta\lambda(t))^{n-i+1}}\Big(C\eta\max(1,\eta^{n-1})e^{-\mu\eta s(t)}\|x(0)\| + C\max_{r\in[0,t]}|d(r)|\Big)

for every $\eta\ge1$ , every $b\ge\underline b$ , every disturbance $d$ , every closed-loop solution, every $t\in[0,T)$ and every $1\le i\le n$ . Since $\lambda(t)\to\infty$ , every coordinate reaches $0$ at the prescribed time $T$ .

Milestones

§3 (10): $\dot\lambda = a\lambda^2$ , $\lambda$ is nondecreasing and tends to $\infty$ at $T$ , and $s$ is an increasing $C^1$ bijection $[0,T)\to[0,\infty)$ .
§3 (7)–(11): the transformed dynamics.
Proposition 10: $\exists\rho,S,K$ such that $(J_n - be_nK^T)^TS + S(J_n-be_nK^T)\preceq-\rho\,\mathrm{Id}$ for all $b\ge\underline b$ .
Proposition 11: the same LMI with $aD_{\mathbf r}$ added, uniformly in $|a|\le C_0$ .
Proposition 12 (corrected): the ISS estimate (17) in the time $s$ .
Proposition 13: the $\eta$ -scaled LMI (20).

Significance

Corollary 14 says that a linear feedback with a time-varying gain drives the chain of integrators to the origin at the designer's deadline $T$ . The guarantee holds for every control gain $b\ge\underline b$ , however large, and gives an explicit input-to-state bound for the matched disturbance. The weight $a$ is free, so the blow-up profile of the gain can be chosen, for example to converge faster than polynomially. Proposition 10 removes the upper bound on $b$ from the classical LMI, and is of independent use for high-gain and persistently excited systems.

On formalization: the results are proved on paper; no formalization of them is known. The mission produces checked statements of the LMIs, the time change, and the prescribed-time estimate. Two printed estimates are false as stated, (17) and (23), and the mission states corrected versions (see Formalization scope). Formal proofs would certify the corrected constants.

Difficulty

The obvious approach is to take a Lyapunov function for the constant-coefficient closed loop and differentiate it along trajectories. This fails for two reasons. First, $b$ ranges over an unbounded interval, so no compactness argument yields a common Lyapunov matrix, and a single $S$ and $K$ must work for all $b\ge\underline b$ at once. Second, the transformed system carries the time-varying term $a(s)D_{\mathbf r}$ , and in the original time the feedback gain $\lambda(t)$ is unbounded. Estimates must survive both the rescaling by $D^{\mathbf r}_{\eta\lambda(t)}$ and the change of time. Constants that look harmless in the new time, such as the condition number of $S$ and the value $\lambda(0)$ , reappear in the original variables, and dropping them makes the printed estimates false.

Formalization scope

Lean representation: vectors of $\mathbb R^n$ are Fin n → ℝ, and coordinate i : Fin n is the paper's index i.val + 1, so $r_i$ = n - i.val. Matrices are Matrix (Fin n) (Fin n) ℝ, and $e_nK^T$ is vecMulVec (eN n) K. Matrix inequalities use the Loewner order (open scoped MatrixOrder), and "real symmetric positive definite" is PosDef. The norm $\|\cdot\|$ is Euclidean, written out as eucNorm. Solutions are Carathéodory solutions in integral form: for every $t$ in the interval, the right-hand side is integrable on $[0,t]$ and the integral identity holds. This matches the paper's measurable $b$ and $d$ . The standing assumptions are $n\ge1$ (§3), $T>0$ , $a$ continuous and nonnegative on $[0,T]$ with $\int_t^Ta>0$ on $[0,T)$ , and $b\ge\underline b>0$ . No upper bound on $b$ is assumed anywhere. $\max|d|$ is replaced by an arbitrary bound $D$ of $|d|$ on the interval.

Corrected statements, with milestone texts kept verbatim:

(17) as printed has no constant on the transient term and fails for $n\ge2$ : with $a\equiv1$ and $y(0)=e_1$ , $|y_1|$ first increases. Proposition 12 is stated with $C_S$ on that term.
(23) as printed fails at $t=0$ whenever $\int_0^Ta<1$ . The goal is stated with a constant $C$ on the transient term, and $K$ and $C$ may depend on $T$ and $a$ . The rate $\mu$ and the disturbance gain $C_S$ depend only on $n$ and $\underline b$ , as on the page.
Proposition 13's undefined $\mu_*$ is the $\rho$ of its statement.
" $\lambda$ increasing" is read as nondecreasing.
Corollary 14's " $t\ge0$ " is read as $t\in[0,T)$ .

Trivializing encodings are ruled out as follows. The integrability clause of IsIntegralSolution prevents a non-integrable right-hand side from integrating to $0$ . Every constant is quantified before the objects it must not depend on: the rate $\mu$ before $T$ and $a$ , $K$ before $\eta$ , and $\rho,S,K$ before $b$ . No statement weakens the estimates to mere convergence.

Needed infrastructure: Lyapunov estimates for absolutely continuous solutions, Loewner-order congruence, and interval-integral calculus for the time change. The LMI lemmas and the integral-form solution predicate are reusable in other control missions. Proofs of any milestone are welcome, and so are sharper constants.

Selected references

Y. Chitour, R. Ushirobira, H. Bouhemou, Stabilization for a Perturbed Chain of Integrators in Prescribed Time, SIAM J. Control Optim. 58(2):1022–1048, 2020. https://doi.org/10.1137/19M1285937
Y. Song, Y. Wang, J. Holloway, M. Krstić, Time-varying feedback for regulation of normal-form nonlinear systems in prescribed finite time, Automatica 83:243–251, 2017. https://doi.org/10.1016/j.automatica.2017.06.008
Y. Chitour, M. Sigalotti, On the stabilization of persistently excited linear systems, SIAM J. Control Optim. 48:4032–4055, 2010. https://doi.org/10.1137/080737812

10 thms2 active usersReviewed

Completed

Combinatorics Convex Optimization Discrete Geometry+2·Captain: Shuze Chen

Discrete Convex Analysis XXIII: Directional Derivatives and Subdifferentials of M-Convex FunctionsTextbook

Motivation

An M-convex function is defined on the integer lattice, but chapter 6's earlier results (companion missions 06-mconvex-functions-i, 22-ch06b-mconvexfunctions, 23-ch06c-mconvexfunctions) show it always extends to a genuine convex function on real space. Once that extension exists, every tool of classical convex analysis — directional derivatives, subdifferentials, positive homogeneity — becomes available, and the natural question is whether these classical objects remain combinatorially special when applied to an M-convex function's extension. This mission answers that question at its sharpest: the directional derivative of an M-convex function at any point is again a positively homogeneous M-convex function, its subdifferential is exactly the admissible-potential set of a distance function satisfying the triangle inequality, and this correspondence between positively homogeneous M-convex functions and triangle-inequality distance functions is itself a clean one-to-one correspondence. This closes the loop between chapters 4-5 (M-convex and L-convex sets, distance functions) and the continuous convex-analytic machinery chapter 8 needs for its duality theory.

Companion missions 06-mconvex-functions-i, 22-ch06b-mconvexfunctions, and 23-ch06c-mconvexfunctions cover this chapter's optimality theory, algebraic toolkit, and convex-extensibility characterization. This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the chapter's real-variable capstones: the transfer of M-convexity's basic operations, optimality criterion, and supermodularity to the polyhedral (real-variable) setting, the identification of positively homogeneous M-convex functions with distance functions satisfying the triangle inequality, and — this mission's goal — the full directional-derivative/subdifferential correspondence.

Setting

Fix a finite ground set $V$ . A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (polyhedral) M-convex if it satisfies the real-variable exchange axiom (M-EXC[R]): for $x,y \in \operatorname{dom}_{\mathbb R} g$ and $u \in \operatorname{supp}^+(x-y)$ , some $v \in \operatorname{supp}^-(x-y)$ and $\alpha_0 > 0$ make the exchange inequality hold on $\alpha \in [0,\alpha_0]$ ; M♮-convex if its lift to one extra coordinate is M-convex. The directional derivative of $g$ at $x \in \operatorname{dom}_{\mathbb R} g$ in direction $d$ is $g'(x;d) = \inf_{t>0} (g(x+td) - g(x))/t$ . A function is positively homogeneous if $g(tx) = t \cdot g(x)$ for all $t > 0$ ; write $0M[\mathbb R \to \mathbb R]$ for the positively homogeneous polyhedral M-convex functions. A distance function $\gamma$ satisfying the triangle inequality and its set of admissible potentials $D(\gamma)$ were introduced in chapter 5; the subdifferential $\partial_{\mathbb R} f(x) = \{p : f(y) - f(x) \ge \langle p, y-x \rangle\ \forall y\}$ generalizes this to any function $f$ at a point $x$ in its domain.

Formalization targets

Goal: the directional-derivative/subdifferential correspondence

For $f \in M[\mathbb R \to \mathbb R]$ and $x \in \operatorname{dom}_{\mathbb R} f$ , setting $\gamma_{f,x}(u,v) = f'(x;-\chi_u+\chi_v)$ :

\gamma_{f,x} \text{ satisfies the triangle inequality}, \quad \partial_{\mathbb R} f(x) = D(\gamma_{f,x}) \ne \emptyset, \quad f'(x;\cdot) = \widehat{\gamma_{f,x}}(\cdot),

with the analogous statement for $f \in M[\mathbb Z \to \mathbb R]$ at an integer point $x$ , using $\gamma_{f,x}(u,v) = f(x-\chi_u+\chi_v)-f(x)$ (Theorem 6.61). This is the weakest stable form: it identifies the subdifferential exactly, as a set, rather than bounding its size or complexity, and holds at every point of the domain uniformly.

Supporting structural targets

Ten further results build the real-variable toolkit and the positive-homogeneity correspondence this goal completes: the transfer of M♮-convexity, the basic operations, the optimality criterion, supermodularity, and weighted-minimizer polyhedrality to the real-variable setting (Theorems 6.48-6.52, Proposition 6.53), the identification of the classes $0M[\mathbb Z|\mathbb R \to \mathbb R]$ and $0M[\mathbb R \to \mathbb R]$ and the compatibility of convex extension with positive homogeneity (Proposition 6.56), the two directions of the correspondence between positively homogeneous M-convex functions and triangle-inequality distance functions (Propositions 6.57-6.58, Theorem 6.59), and the fact that a directional derivative of an M-convex function is itself positively homogeneous and M-convex (Proposition 6.60).

Significance

Theorem 6.61 is the technical bridge that lets discrete convex analysis borrow the entire apparatus of classical convex duality: because the subdifferential of an M-convex function is always the admissible-potential set of a chapter-5 distance function, every fact already proved about $D(\gamma)$ (its polyhedral structure, its own L-convexity, its relationship to shortest paths) transfers immediately to subdifferentials of M-convex functions. This is exactly the mechanism the book calls out as essential for Chapter 8's separation theorem for M♮-convex functions. The $0M \leftrightarrow T$ correspondence (Theorem 6.59) is independently significant: it says the positively homogeneous special case of M-convex function theory — which is what directional derivatives of any M-convex function reduce to, by Proposition 6.60 — is exactly as rich as ordinary shortest-path distance function theory, no more and no less, so nothing new needs to be built to understand local behavior at a point.

None of these results are open — they are Murota's account of how the discrete exchange axiom interacts with directional differentiation and subgradients, a bridge chapter between the purely combinatorial theory of chapters 4-6 and the duality theory of chapter 8. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (MExchangeAxiomR, DirDeriv, GammaHat) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to Theorem 6.61 would try to compute $\partial_{\mathbb R} f(x)$ directly from the definition of subgradient and separately verify it happens to equal some $D(\gamma)$ ; the book's actual proof instead derives the equality of sets from the M-optimality criterion (Theorem 6.52) applied pointwise: $p \in \partial_{\mathbb R} f(x)$ is shown, via a chain of logical equivalences, to be exactly the condition defining $D(\gamma_{f,x})$ , so no separate verification of polyhedrality or nonemptiness is needed beyond what Theorem 6.52 and Proposition 6.60 already supply. The genuine difficulty is upstream, in Proposition 6.60 itself: showing a directional derivative is M-convex requires exploiting the local validity of the identity $f(x+d)-f(x) = f'(x;d)$ for small $\|d\|_1$ (Eq. (6.85)) and then extending the exchange property from that neighborhood to all of $\mathbb R^V$ using positive homogeneity — a two-step argument with no single-step shortcut, since the exchange axiom's defining inequality is not obviously homogeneous-invariant on its own.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; real-domain functions are (V→ℝ)→WithTop ℝ. The directional derivative is built directly as an infimum of difference quotients over $t>0$ , matching the book's own local characterization (Eq. (6.85)) without a separate limit construction. Positive homogeneity and the classes 0M[R→R]/0M[Z→R] are stated exactly as the book defines them (the latter via positive homogeneity of the convex extension, not of f itself, since f is undefined off Zⱽ). Theorems 6.49-6.50 restate 4 of their 8 operations (matching the identical scope decision for chunk 22-ch06b-mconvexfunctions's Theorem 6.13); Theorem 6.61 omits the dual-integral refinement clauses for the M[R→R|Z]/ M[Z→Z] sub-classes. Both reductions are documented, not trivializing omissions — see Difficulty above and HARD.md/MODERATION_NOTES.md. No numeric constants are hard-coded anywhere in this mission. This mission's definitions are redeclared from chunks 06-mconvex-functions-i, 21-ch05b-lconvexsets (for the distance-function/admissible-potential vocabulary), 22-ch06b-mconvexfunctions, and 23-ch06c-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the twelve sorrys are welcome; the goal and Proposition 6.60 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
K. Murota and A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research, 24 (1999), pp. 95-105 (the polyhedral M-convex function theory this mission's real-variable results are drawn from).

56 thms2 active usersReviewed

Completed

Convex Optimization Numerical Analysis Optimization·Captain: mikedeng1

The Relaxation Method for Linear Inequalities III: Reflexion in a Closed Bounded Convex Set Terminates or Ends in OscillationResearch Paper

Motivation

The relaxation method for a system of linear inequalities, introduced by Agmon and by Motzkin and Schoenberg in back-to-back papers of the Canadian Journal of Mathematics (1954), solves $\sum_j a_{ij}x_j + b_i \ge 0$ by repeatedly moving a point towards, or across, the most violated half-space. It is the ancestor of the perceptron algorithm, of Kaczmarz-type projection methods, and of the method of alternating projections, all of which are still used in feasibility problems, tomography and machine learning.

Motzkin and Schoenberg's paper ends (Part IV, §§9–10) by asking whether the behaviour of the reflexion process — the relaxation step with factor $\lambda = 2$ — survives when the finite family of half-spaces is replaced by an infinite one. They answer this for one natural infinite family: all supporting half-spaces of a closed bounded convex set. This mission formalizes that answer, Theorem 3 of the paper.

Timeline of the thread this mission belongs to:

1922 — Fejér observes that a sequence approaching every point of a set monotonically has useful convergence properties (Fejér, Math. Annalen 85, 1922).
1954 — Agmon proves convergence of the relaxation method for $0 < \lambda < 2$ (Agmon, Canad. J. Math. 6, 1954, pp. 382–392); Motzkin and Schoenberg prove finite termination of the reflexion method ( $\lambda = 2$ ) for full-dimensional solution polytopes (Theorem 1), the oscillation behaviour in lower dimension (Theorem 2), and the convex-body version (Theorem 3) (Motzkin–Schoenberg 1954).

Setting

Let $E_n$ be $n$ -dimensional Euclidean space and let $A \subseteq E_n$ be a nonempty, closed, bounded, convex set. Its dimension $r$ is the dimension of its affine span $L_r$ , the smallest flat containing $A$ .

For $p \notin A$ let $q$ be the point of $A$ nearest to $p$ ; it exists and is unique. The image of $p$ with respect to $A$ is

p_1 = F(p) = p + 2(q - p), \qquad (3.1)

the reflexion of $p$ through $q$ . The reflexion process starts at $p_0 \notin A$ and sets $p_{\nu+1} = F(p_\nu)$ as long as $p_\nu \notin A$ (3.2). Either the process terminates with some $p_N \in A$ , or it produces an infinite sequence of points outside $A$ .

The family $F$ of supporting half-spaces of $A$ consists of the closed half-spaces $H \supseteq A$ whose bounding hyperplane touches $A$ . The paper observes that the half-space $H_0$ through $q$ normal to $pq$ is the member of $F$ farthest from $p$ , so (3.1) is exactly the reflexion step of the relaxation method applied to the infinite family $F$ .

A sequence $\{q_\nu\}$ of points outside $A$ is Fejér-monotone with respect to $A$ if $q_\nu \ne q_{\nu+1}$ and $|q_{\nu+1} - a| \le |q_\nu - a|$ for all $a \in A$ . Two points $u, v$ are symmetric with respect to a flat $L$ if their midpoint lies in $L$ and $u - v$ is orthogonal to $L$ .

Formalization targets

Goal: Theorem 3 (p. 402)

For every nonempty closed bounded convex $A \subseteq E_n$ with affine span $L_r$ , every $p_0 \notin A$ and every run $\{p_\nu\}$ of the reflexion process:

\textbf{Case 1: } r = n \implies \exists N,\ p_N \in A.

\textbf{Case 2: } r < n \implies \begin{cases} p_0 \in L_r \implies \exists N,\ p_N \in A,\\[2pt] p_0 \notin L_r \implies p_\nu \notin A\ \forall \nu, \text{ and } \exists \nu_0, u \ne v \text{ symmetric w.r.t. } L_r:\ \{p_\nu, p_{\nu+1}\} = \{u, v\}\ \forall \nu > \nu_0. \end{cases}

No number of steps is fixed: termination is finite but not uniformly bounded.

Milestones (attack order)

§9 — the half-space $H_0$ belongs to $F$ , maximizes $\operatorname{dist}(p, H)$ over $F$ , and every farthest member of $F$ yields the step (3.1).
§10 — an infinite run of the reflexion process is Fejér-monotone with respect to $A$ .
Lemma 1, Case 1 — a sequence Fejér-monotone with respect to a set of dimension $n$ converges to a point.
§10 — the limit of an infinite run lies in $A$ and on its boundary.
Theorem 3, Case 1 — if $r = n$ the process always terminates.
§10 — orthogonal projection on a flat $L \supseteq A$ commutes with the image map, and each step keeps the distance to $L$ while switching sides.

Significance

The result. Theorem 3 shows that the dichotomy proved in the paper for finitely many half-spaces — finite termination when the target is full-dimensional, eventual oscillation otherwise — holds for the infinite family of all supporting half-spaces of a convex body. Case 1 says that reflecting through the nearest point, a method that uses no information about $A$ beyond metric projection, reaches a full-dimensional convex body in finitely many steps from any start. Case 2 says that for a lower-dimensional body the process detects this: the iterates settle into a two-cycle whose midpoint is a point of $A$ , so a solution can be read off.

Formalizing it. The theorem is proved in the paper (1954), with a short proof of Case 1 that relies on geometric intuition about normal cones near a boundary point. To our knowledge no machine-checked proof exists. A complete development produces a verified finite-termination theorem for a projection method on general convex bodies, together with reusable facts about Fejér-monotone sequences and metric projections that recur throughout the analysis of projection algorithms.

Difficulty

The obvious argument for Case 1 is: the run is Fejér-monotone, hence converges (Lemma 1), and its limit $a$ lies on the boundary of $A$ ; then derive a contradiction. For a polytope (Theorem 1) the contradiction comes from finiteness: eventually every reflexion is in one of finitely many hyperplanes through $a$ , which keeps the iterates on a sphere around $a$ . For a convex body there are infinitely many supporting hyperplanes near $a$ , and the iterates are reflected in a different one at every step; no finiteness argument is available. What replaces finiteness is an argument about how the supporting hyperplanes of $A$ at boundary points near $a$ are oriented, and the paper gives it only as an informal geometric sketch. Making this step rigorous is the main work of the mission.

Numerical experiments show that termination can take tens of thousands of steps near sharp corners of a polygon, so no bound on the number of steps in terms of the distance of $p_0$ to $A$ alone can be expected.

Formalization scope

Space. $E_n$ is EuclideanSpace ℝ (Fin n). $A$ is a Set with four explicit hypotheses: A.Nonempty, IsClosed A, Convex ℝ A, Bornology.IsBounded A. Nonemptiness is implicit in the paper ("of dimension $r$ ", "the point of $A$ nearest to $p$ ").
The image as a relation. IsImage A p p₁ holds when $p_1 = p + 2(q - p)$ for a nearest point $q$ of $A$ ; the nearest point is not chosen by a function. For closed convex nonempty $A$ this relation is a function on $E_n$ . A run is any sequence with IsImage A (p ν) (p (ν+1)) whenever p ν ∉ A; values after entering $A$ are unconstrained. Every statement quantifies over every run from every $p_0 \notin A$ ; a formalization that only asserts the existence of some terminating run is ruled out.
Dimension. $L_r$ is affineSpan ℝ A; $r = n$ is affineSpan ℝ A = ⊤, $r < n$ is affineSpan ℝ A ≠ ⊤. No separate natural number $r$ is introduced.
Symmetry. IsSymmetricWrt L u v: midpoint ℝ u v ∈ L and u - v orthogonal to L.direction. For $r < n - 1$ this is a point reflection through the foot of the perpendicular, not a reflection in a hyperplane. The goal also requires $u \ne v$ and strict alternation $p_\nu \leftrightarrow p_{\nu+1}$ for $\nu > \nu_0$ (strict inequality, as printed).
Boundary is frontier A; distances to sets are Metric.infDist.
Generalizations recorded. Lemma 1, Case 1 is stated for an arbitrary set $A \subseteq E_n$ with full affine span (the paper states it for the polytope of (1.4) and applies it in §10 to a convex body). The projection milestone is stated for any flat $L \supseteq A$ , not only after the paper's reduction to $r = n - 1$ . The §9 milestone expresses "the reflexion process with respect to $F$ amounts to (3.1)" as: every farthest member of $F$ , with any nearest point on it, gives the same step.
Duplication. Case 1 appears both as a milestone and inside the goal, because the paper's proof of Case 2 cites Case 1. Solvers will need to transfer Case 1 from $E_n$ to the flat $L_r$ (an isometric copy of $E_r$ ).
Infrastructure. Mathlib's metric projection onto complete convex sets (exists_norm_eq_iInf_of_complete_convex, norm_eq_iInf_iff_real_inner_le_zero) and EuclideanGeometry.orthogonalProjection cover the basic geometry. Normal cones of convex sets and their upper semicontinuity are not in Mathlib; a contribution there is reusable well beyond this mission. Proofs of any milestone, and alternative proofs of Case 1, are welcome.

Selected references

T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 393–404. https://doi.org/10.4153/CJM-1954-038-x
S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 382–392 (the companion paper in the same issue).
L. Fejér, Über die Lage der Nullstellen von Polynomen, die aus Minimumforderungen gewisser Art entspringen, Mathematische Annalen 85 (1922), 41–48.

11 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XX: Perpetual American Options and Credit GrantingTextbook

Motivation

An American option may be exercised at any moment up to maturity, so pricing one is not an integration problem but a stopping problem: the holder must decide, at each date and in each state of the market, whether the payoff available now beats the option value of waiting. A perpetual American put pushes this to its limit — there is no maturity at all, so the horizon is unbounded and the problem has no terminal condition to induct backwards from. What replaces the terminal condition is a fixed point characterization, and the classical answer, going back to McKean (1965) and Merton (1973) in continuous time and to Cox, Ross and Rubinstein (1979) in the binomial model, is that the price is the smallest superharmonic majorant of the payoff.

Bäuerle and Rieder's Chapter 11 (Markov Decision Processes with Applications to Finance, Springer, 2011) derives this from their own general unbounded-horizon stopping theory rather than from stochastic analysis, and in the same chapter applies the bounded-horizon version to a problem from banking rather than trading: when should a bank cancel a credit line? The two halves share one mathematical shape — a stopping problem whose optimal policy turns out to be of threshold type — and this mission formalizes both, with the perpetual put as the goal.

Setting

The binomial model (§11.1). A stock moves from price $x$ to $xu$ with risk-neutral probability $q$ and to $xd$ with $1-q$ , where $0 < d < u$ , and the discount factor is $\beta \in (0,1]$ . The defining relation of the risk-neutral measure,

\beta q u + \beta(1-q)d = 1,

is carried as a hypothesis of the model: it is what makes the discounted stock price a martingale, and the proofs use it directly.

The American put with strike $K$ pays $(K-x)^+$ when exercised. With $n$ periods to maturity its price satisfies the recursion $J_0(x) = (K-x)^+$ and

J_n(x) = \max\Big\{(K-x)^+,\ \beta\big(q J_{n-1}(xu) + (1-q)J_{n-1}(xd)\big)\Big\} =: \mathcal{T}J_{n-1}(x),

the maximum being "exercise now" against "hold". Proposition 11.1.2 describes the price $\pi_n(x) := J_{N-n}(x)$ at time $n$ of an option maturing at $N$ : it is continuous in $x$ , decreasing in $n$ , and — the part that carries the argument — $x \mapsto \pi_n(x) + x$ is increasing, even though $\pi_n$ itself decreases in $x$ . That single reformulation, obtained by adding $x$ to both sides of the recursion and using the risk-neutral relation, is what yields the threshold structure: there are exercise boundaries $K =: x_N^* \ge x_{N-1}^* \ge \dots \ge x_0^* \ge 0$ with $\tau^* = \inf\{n \le N \mid X_n \le x_n^*\}$ optimal. Exercise when the stock falls far enough, and the boundary rises as maturity approaches.

The perpetual put (Theorem 11.1.3, the goal). With no expiration date the price at time zero is a supremum over all stopping times, $\tau \le \infty$ included:

P(x) := \sup_{\tau \le \infty} \mathbb{E}^{\mathbb{Q}}_x\big[\beta^\tau (K - S_\tau)\big],

with the stopping reward set to zero on $\{\tau = \infty\}$ . The theorem says four things: $P$ is the limit of the finite-maturity prices $J_n$ ; $P$ solves $\mathcal{T}P = P$ and satisfies $0 \le P \le K$ ; $P$ is the smallest superharmonic function majorizing $(K-x)^+$ ; and, if the value $J_{f^*}$ of the exercise-region policy dominates $\mathcal{T}J_{f^*}$ , then $P$ equals that value and $\tau^* = \inf\{n \mid X_n \in E^*\}$ , the hitting time of $E^* = \{x \mid P(x) = (K-x)^+\}$ , is optimal.

The conditional in part d) is the book's own and is not decoration: without it the exercise region need not deliver an optimal stopping time, and the unconditional version is a different, false statement. The boundedness $0 \le P \le K$ in b) is likewise a genuine claim rather than a side remark — the fixed point equation alone admits other solutions, and it is boundedness together with minimality that pins $P$ down among them.

Credit granting (§11.2). A bank holds a credit contract of maximal duration $N$ . Each period it observes a rating class $x_n$ evolving as a Markov process $Q^X$ , and chooses to extend — earning $c(x)$ — or to cancel, ending the contract. The value iteration is $J_n(x) = \max\{0,\ c(x) + \beta\int J_{n-1}\,dQ^X(\cdot|x)\}$ . Under two structural assumptions — $c$ increasing, and $Q^X$ stochastically monotone, so that a better-rated borrower stays better-rated — Theorem 11.2.1 gives the same shape of answer as the option: cancel exactly when the rating falls below a threshold $x_n^*$ , and those thresholds rise as the remaining duration shortens, since a marginal borrower is no longer worth keeping when there is little time left to recover.

Theorem 11.2.2 repeats this when the borrower is not rated at all. The bank has only a prior $\mu_0$ on the repayment probability and one signal per period; the state $(s,n)$ records $s$ positive signals out of $n$ , and the expected repayment probability is the posterior mean $q(s,n)$ . Monotonicity here is for the order of p. 342 — more positive signals and fewer negative ones — and not the coordinatewise order, under which the claim would be false: an extra signal that is negative makes the state worse.

What is being asked

Formalize Theorem 11.1.3 in full, all four parts: the limit identification, the fixed point equation with its bounds, the minimality among superharmonic majorants, and the conditional optimality of the exercise-region stopping time. The three milestones are Proposition 11.1.2, the finite-horizon put whose threshold structure the perpetual case specializes, and the two credit granting theorems, which run the same bounded-horizon argument on a different model.

The stopping-time apparatus is built rather than assumed: the stock path, the law $\mathbb{Q}$ pinned by its finite-dimensional distributions, stopping times valued in $\mathbb{N}\cup\{\infty\}$ , and the reward vanishing at $\infty$ . Part a) of the goal is the identification of the supremum with $\lim_n J_n$ , so carrying $P$ as an abstract function would make the theorem vacuous.

6 thms2 active usersReviewed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XIX: Theory of Optimal Stopping ProblemsTextbook

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

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

What is being asked

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

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

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

16 thms2 active usersReviewed

Analysis Operations Research Stochastic Systems·Captain: mikedeng1

Diffusion approximations for open queueing networks with service interruptions 1: explicit Lipschitz bounds for the oblique reflection mapResearch Paper

Motivation

Heavy-traffic and fluid approximations for open queueing networks are obtained by writing the queue-content process as a deterministic function of a simpler netput process (arrivals minus potential service, corrected for routing) and then transferring a functional limit theorem for the netput through that function. The function is the multidimensional reflection map of Harrison and Reiman (Harrison and Reiman 1981), extended from continuous paths to paths with jumps by Reiman (Reiman 1984). The transfer works only if the map is continuous, and quantitative bounds on the approximation error require it to be Lipschitz with a known modulus.

Chen and Whitt (Chen and Whitt 1993) use this map to derive diffusion approximations for networks whose servers are subject to interruptions. Before doing so, Section 2 of the paper supplies "explicit Lipschitz bounds" for the map in the uniform topology: a bound in the Harrison–Reiman scaling (Proposition 2.1) and a new bound that depends on the routing matrix only through its powers (Proposition 2.3).

Timeline. Harrison and Reiman (1981) proved existence, uniqueness and continuity of the map on continuous paths for a routing matrix of spectral radius less than one. Reiman (1984) extended it to paths with jumps. Chen and Mandelbaum (Leontief systems, RBV's and RBM's, 1991, cited in the paper as [4]) noted that a minor extension of the argument makes the map Lipschitz on $D([0,T],\mathbb R^n)$ with the uniform topology. Chen and Whitt (1993, Section 2) made the Lipschitz constants explicit.

Setting

Fix a dimension $n$ and an $n\times n$ matrix $Q$ whose transpose $Q^{\mathsf t}$ is substochastic: all entries of $Q$ are nonnegative and every column sum of $Q$ is at most $1$ . Assume also $Q^k \to 0$ as $k\to\infty$ . With Markovian routing, $Q^{\mathsf t}$ is the routing matrix of an open network of $n$ queues.

Vectors $c\in\mathbb R^n$ carry the norm $\|c\| = \sum_j |c_j|$ , and matrices carry the maximum absolute column sum $\|P\| = \max_j \sum_i |P_{ij}|$ (Eq. (2.5)). $D([0,T],\mathbb R^n)$ is the space of paths that are right-continuous with left limits on $[0,T]$ . For a path $x$ , $|x|\in\mathbb R^n$ is the vector of coordinatewise sup norms, $|x|_j = \sup_{0\le t\le T}|x_j(t)|$ , and $\|x\| = \big\||x|\big\| = \sum_j \sup_{t}|x_j(t)|$ .

The reflection of $x \in D$ is the pair $(y,z) = (\psi(x),\phi(x))$ with $y \in D$ and

z = x + (I-Q)\,y \ge 0, \qquad y_j \text{ nondecreasing},\ y_j(0) = 0, \qquad \int_0^T z_j(t)\,dy_j(t) = 0 \quad (1\le j\le n).

The last condition says that $y_j$ increases only when $z_j = 0$ . In queueing terms, $z$ is the vector of queue contents and $y$ the cumulative idleness. The operator $\pi_x(y) = (Qy - x)^{\uparrow}\vee 0$ , where $f^{\uparrow}(t) = \sup_{0\le s\le t} f(s)$ coordinatewise, has the reflection as its fixed point (Eq. (2.4)). Write $\gamma = \|Q^n\|$ .

Formalization targets

Goal: Proposition 2.3

For all $x_1,x_2\in D$ with reflections $(\psi(x_i),\phi(x_i))$ ,

|\psi(x_1)-\psi(x_2)| \le (I-Q)^{-1}|x_1-x_2| \quad\text{componentwise},\tag{2.9}

\|\psi(x_1)-\psi(x_2)\| \le \|(I-Q)^{-1}\|\,\|x_1-x_2\| \le \sum_{k=0}^\infty \|Q^k\|\,\|x_1-x_2\| \le \frac{n}{1-\gamma}\|x_1-x_2\|,\tag{2.10}

\|\phi(x_1)-\phi(x_2)\| \le \big(1+\|I-Q\|\,\|(I-Q)^{-1}\|\big)\|x_1-x_2\| \le \Big(1+\frac{2n}{1-\gamma}\Big)\|x_1-x_2\|.\tag{2.11}

The constants are those of the paper. The goal fixes nothing beyond the standing assumptions on $Q$ .

Milestones

Existence and uniqueness of the reflection for $x\in D$ with $x(0)\ge0$ (Section 2, p. 337).
Eq. (2.4): given (2.1)–(2.2), the complementarity condition (2.3) is equivalent to $y = \pi_x(y)$ .
$\gamma = \|Q^n\| < 1$ (p. 338).
Proposition 2.2: $\|\pi_x^k(y_1)-\pi_x^k(y_2)\| \le \|Q^k|y_1-y_2|\| \le \|y_1-y_2\|$ for $k\ge1$ , the factor $\gamma$ for $k\ge n$ , and $\pi_x^k(y_1)\to\psi(x)$ .
Proposition 2.1: for $Q^* = \Lambda^{-1}Q\Lambda$ with $\Lambda$ diagonal and $\|Q^*\| = \alpha<1$ , the moduli $\|\Lambda\|\|\Lambda^{-1}\|/(1-\alpha)$ for $\psi$ and $1 + \|I-Q\|\|\Lambda\|\|\Lambda^{-1}\|/(1-\alpha)$ for $\phi$ .
Remark (2.1): for $n=1$ , $Q=0$ the bounds are attained.
Remark (2.2): for two queues in series, (2.10) gives modulus $2$ , while (2.7) gives at best $4$ (every modulus $\ge 4$ is attained, $4$ at $z = 1/2$ ).

Significance

Proposition 2.3 makes the queue-content and idleness processes of an open network Lipschitz functions of the netput, in the uniform norm, with a modulus computed from the routing matrix alone. Combined with the fact that Lipschitz continuity in the uniform topology passes to the Skorohod $J_1$ and $M_1$ topologies (Section 2 of the paper), it is what turns a functional central limit theorem for arrival and service processes into a heavy-traffic limit for the network. The paper uses it in exactly this way in Sections 3–4. Explicit moduli also yield rates: an error of order $\varepsilon$ in the netput produces an error of at most $n\varepsilon/(1-\gamma)$ in the idleness process.

On the formal side, the results are proved in the paper, but neither the reflection map nor $D([0,T],\mathbb R^n)$ has a machine-checked development in Mathlib or on this platform. The mission would provide a reusable definition of the oblique reflection map with a Lebesgue–Stieltjes complementarity condition, its fixed-point characterization, and certified Lipschitz constants, as a foundation for any later formal heavy-traffic limit.

Difficulty

The componentwise bound (2.9) is short once the fixed-point form of the map is available. The difficulty lies in the infrastructure beneath it. The fixed-point characterization (2.4) is a one-dimensional Skorokhod-problem argument carried out coordinatewise for paths with jumps, where the complementarity condition must be handled through Lebesgue–Stieltjes measures. A jump of $y_j$ is allowed at a time where $z_j = 0$ even if $z_j$ was positive just before. Existence needs the iterates $\pi_x^k(0)$ to converge in $D$ and the limit to satisfy (2.1)–(2.3). The explicit constants involve $(I-Q)^{-1}$ , $\sum_k\|Q^k\|$ and $\gamma = \|Q^n\|<1$ . The last inequality is a combinatorial fact about transient substochastic matrices. It does not follow from $\|Q\|\le1$ .

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and $\|P\|$ is the maximum absolute column sum. Paths are functions ℝ → Fin n → ℝ, of which only the restriction to $[0,T]$ matters. Membership in $D([0,T],\mathbb R^n)$ is the predicate IsCadlagOn T x: right-continuous on $[0,T)$ , left limits on $(0,T]$ , and (redundantly) bounded on $[0,T]$ . The reflection is the predicate IsReflection Q T x y z. Every theorem is stated for all pairs satisfying it, so no choice function and no junk value are involved. Condition (2.3) is encoded as "the Lebesgue–Stieltjes measure $dy_j$ of $\{t\in[0,T]: z_j(t)>0\}$ is zero". For $z\ge0$ this is equivalent to $\int_0^T z_j\,dy_j=0$ . $\pi_x^k$ is Nat.iterate, $(I-Q)^{-1}$ is Mathlib's matrix inverse (invertible under the standing assumptions), and $\sum_k\|Q^k\|$ is a tsum stated together with its summability.

Corrections and conventions, each disclosed in the item concerned:

The norm (2.6). The page prints $\|x\| = \sup_t\sum_j|x_j(t)|$ . Under that norm Propositions 2.1 and 2.3 are false for $n\ge2$ . With $Q=0$ , $n=2$ , $T=1$ , $x_1\equiv0$ and $x_2 = (-\mathbf 1_{[0.1,0.2)}, -\mathbf 1_{[0.3,0.4)})$ , one gets $\|x_1-x_2\|=1$ but $\psi(x_2) = (\mathbf 1_{[0.1,1]},\mathbf 1_{[0.3,1]})$ has norm $2$ . The paper's proofs are valid for $\|x\| = \sum_j\sup_t|x_j(t)|$ , which is used throughout. In dimension one the two norms coincide.
(2.8) prints $\phi(x_1)-\phi(x_1)$ . The formalization states $\phi(x_1)-\phi(x_2)$ .
(2.2)–(2.3) print the index range $1\le j\le J$ . The dimension is $n$ .
$x(0)\ge0$ is added to the existence item. Conditions (2.1)–(2.2) force $z(0)=x(0)$ , so no reflection exists otherwise. The Lipschitz bounds are stated for all solution pairs and are vacuous exactly when some $x_i(0)$ has a negative coordinate.
Proposition 2.1 assumes only that $\Lambda$ is diagonal with nonzero entries. All quantities depend on $|\Lambda|$ , so this covers the positive scaling of Harrison and Reiman.
Eq. (2.4) keeps the standing assumptions on $Q$ as on the page, although the equivalence does not use them.

A trivializing formalization would read (2.3) through a Bochner integral, which is $0$ for non-integrable integrands, or take suprema over unbounded families. The measure-zero encoding and the boundedness built into IsCadlagOn rule both out. A sorry-free check shows that Remark (2.1)'s jump example satisfies IsReflection.

Welcome contributions: a general API for càdlàg paths on $[0,T]$ (boundedness, measurability, running suprema), the one-dimensional Skorokhod lemma for càdlàg paths, and the Neumann series for transient substochastic matrices. All of these are reusable beyond this mission.

Selected references

H. Chen and W. Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993) 335–359. https://doi.org/10.1007/BF01149260
J. M. Harrison and M. I. Reiman, Reflected Brownian motion on an orthant, Annals of Probability 9 (1981) 302–308. https://doi.org/10.1214/aop/1176994428
M. I. Reiman, Open queueing networks in heavy traffic, Mathematics of Operations Research 9 (1984) 441–458. https://doi.org/10.1287/moor.9.3.441
H. Chen and A. Mandelbaum, Discrete flow networks: diffusion approximations and bottlenecks, Annals of Probability 19 (1991) 1463–1519. https://doi.org/10.1214/aop/1176990220

10 thms2 active usersReviewed

Completed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Approximation Algorithms for Combinatorial Problems III: The Worst-Case Ratio of the Weighted Algorithm B2Research Paper

Motivation

MAXIMUM SATISFIABILITY asks for a truth assignment satisfying as many clauses of a given set as possible. It was among the first NP-hard optimization problems for which an approximation algorithm came with a proven worst-case guarantee. In Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 1974, doi:10.1016/S0022-0000(74)80044-9), David S. Johnson set up a framework for measuring such guarantees and analyzed two heuristics for the problem. The second of these, algorithm B2, weights each clause by $2^{-|C|}$ and repeatedly sets a literal so that the heavier side is satisfied. On inputs whose clauses all have at least $k$ literals, it satisfies at least a $1 - 2^{-k}$ fraction of the optimum.

B2 is the ancestor of a line of work on MAX-SAT approximation:

1974. Johnson proves the $2^k/(2^k-1)$ bound for B2 on MS(k) and the $(k+1)/k$ bound for the unweighted greedy algorithm B1.
1994. Goemans and Williamson (SIAM J. Discrete Math. 7) present Johnson's algorithm as the derandomization, by conditional expectations, of the uniformly random assignment, and combine it with LP rounding to obtain a $3/4$ -approximation.
1999. Chen, Friesen and Zheng (JCSS 58) show that B2 is a $2/3$ -approximation on general inputs, sharper than the $1/2$ that Johnson's bound gives at $k = 1$ .

Setting

A literal is a variable $x_i$ or its negation $\bar x_i$ . A clause is a finite set of literals. A truth assignment is a set $T$ of literals containing no pair $\{x_i, \bar x_i\}$ ; it satisfies a clause $C$ when $C \cap T \ne \emptyset$ . An input is a finite set $S$ of clauses, and $S^*$ is the largest $|S'|$ over subsets $S' \subseteq S$ satisfied by one truth assignment. MS(k) is the restriction to inputs in which every clause contains at least $k$ distinct literals.

Algorithm B2 keeps a set SUB of satisfied clauses, a set LEFT of unsettled clauses, the literals LIT still available, and a weight $w(C)$ per clause, starting from $w(C) = 2^{-|C|}$ , $\mathrm{SUB} = \emptyset$ , $\mathrm{LEFT} = S$ . While some literal of LIT occurs in a clause of LEFT, it picks any such literal $y$ . Let YT be the clauses of LEFT containing $y$ and YF those containing $\bar y$ . If $\sum_{\mathrm{YT}} w \ge \sum_{\mathrm{YF}} w$ , it makes $y$ true, moves YT to SUB and doubles the weight of each clause of YF; otherwise it does the symmetric move with $\bar y$ . Finally it removes $y, \bar y$ from LIT. When no literal of LIT remains in LEFT it returns SUB.

The choice of $y$ is free, so several outputs may be choosable on one input. Johnson measures the algorithm by its worst choosable output, through the ratio $r(B2, S) = S^*/|\mathrm{SUB}|$ and its maximum $R[B2, \mathrm{MS}(k)](n)$ over inputs of size at most $n$ .

Formalization targets

Goal: Theorem 3, with the equality range corrected

For every $k \ge 1$ , every $S$ in MS(k) and every SUB choosable by B2 on $S$ ,

(2^k - 1)\,S^* \le 2^k\,|\mathrm{SUB}|,

and for every $k \ge 2$ there are $S$ in MS(k) and a choosable SUB with $|\mathrm{SUB}| > 0$ and

(2^k - 1)\,S^* = 2^k\,|\mathrm{SUB}|.

The paper states equality "for all sufficiently large $n$ " for every $k \ge 1$ . At $k = 1$ this is false: the ratio 2 would require every clause to be a unit clause and all clauses to be jointly satisfiable, and on such inputs B2 satisfies everything. The goal therefore asserts tightness for $k \ge 2$ . A separate item states that at $k = 1$ the ratio is never attained.

Milestones

Initially, the total weight of LEFT is at most $|S|/2^k$ .
No iteration increases the total weight of LEFT, so at halting it is still at most $|S|/2^k$ .
At halting, every clause left in LEFT has weight exactly $1$ .
At halting, $|\mathrm{LEFT}| \le |S|/2^k$ and $|\mathrm{SUB}| \ge |S|(1 - 2^{-k})$ .
The eight-clause instance for $k = 3$ has $S^* = 8$ and admits a choosable output of size $7$ .

Significance

The bound $1 - 2^{-k}$ is exactly the expected fraction of clauses a uniformly random assignment satisfies on MS(k). B2 attains it deterministically, and the proof bounds $|\mathrm{SUB}|$ against $|S|$ rather than against $S^*$ , a feature the paper points out. For $k = 3$ the constant $8/7$ was later shown by Håstad (2001) to be optimal among polynomial-time algorithms unless P = NP, so the guarantee of this 1974 algorithm is best possible for MAX-E3-SAT.

Formalizing the result produces a machine-checked potential-function argument for a nondeterministic algorithm: the invariant links each clause's weight to how many of its literals have been removed. The mission also records a correction to the printed statement at $k = 1$ . The paper's proof is complete; to our knowledge no machine-checked version exists.

Difficulty

The obvious argument follows the counting proof for algorithm B1 and compares clauses saved with clauses wounded in each step. It fails here: B2 can wound more clauses than it saves in a step, and the bound holds only in the weighted sense. The weight of a clause is not a static quantity. It is $2^{-|C|}$ times $2$ to the number of its literals already discarded, and this invariant must be carried through every step, including clauses that contain both $y$ and $\bar y$ . Tightness needs an explicit input and an explicit adversarial run that exploits the tie in Step 4, and then a proof that every assignment of the remaining variables kills exactly one clause.

Formalization scope

Literals and clauses. A literal is a pair (variable index in $\mathbb N$ , sign). Clauses are Finsets of literals, and an input is a Finset of clauses, so there are no duplicate clauses. Truth assignments are partial and consistent. $S^*$ is a maximum over the finite, nonempty family of satisfiable subsets.
B2 as a relation. B2 is a nondeterministic run relation, and "choosable" means reachable by finitely many steps from the initial state and halting. Step 3 allows a literal of either sign. The tie in Step 4 goes to $y$ , and the comparison and doublings use the weights before the update. Weights are rationals.
Size-free ratios. The size-dependent $R[B2, \mathrm{MS}(k)](n)$ is replaced by statements about every input (upper bound) and one attaining input (tightness). The two forms are equivalent because $R$ is a maximum over finitely many inputs and nondecreasing in $n$ .
No division. All ratios are multiplied out, so no division by zero can make a bound vacuous.
Trivializations ruled out. A deterministic tie-break in Step 3 or 4, or tightness at a single fixed $k$ , would be a weaker theorem and is not acceptable. So is stating only the upper bound.

The definitions (the MS layer, the run relation) can be reused by other MAX-SAT approximation results, and an identical MS layer appears in the companion mission on algorithm B1. Contributions welcome: proofs of the milestones, of the $k \ge 2$ tightness family, and of the $k = 1$ correction.

Selected references

D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9 (1974) 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
J. Chen, D. K. Friesen, H. Zheng, Tight bound on Johnson's algorithm for maximum satisfiability, J. Comput. System Sci. 58 (1999) 622–640. https://doi.org/10.1006/jcss.1998.1610
M. X. Goemans, D. P. Williamson, New 3/4-approximation algorithms for the maximum satisfiability problem, SIAM J. Discrete Math. 7 (1994) 656–666. https://doi.org/10.1137/S0895480192243516
J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001) 798–859. https://doi.org/10.1145/502090.502098

9 thms2 active usersReviewed

Analysis Harmonic Analysis Partial Differential Equations·Captain: mikedeng1

Notes on Partial Differential Equations II: The Newtonian Potential and Hölder Estimates for Poisson's EquationTextbook

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: the Hölder estimate (Theorem 2.28)

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

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

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

Milestones

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

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

with the integral absolutely convergent.

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

9 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XVII: Random-Horizon Consumption-Investment and the De Finetti Dividend ProblemTextbook

Motivation

An insurance company collects premia and pays claims each period; the difference is a random, signed quantity that can push the company's risk reserve up or down. At the start of every period, before that period's premia and claims are realized, the company's owners may pay themselves a dividend out of the current reserve — but once the reserve goes negative the company is ruined and stops operating for good. How should the owners time and size these payments to maximize the total expected discounted dividend paid out before ruin? This is the classical De Finetti dividend problem, one of risk theory's oldest optimization questions, and Chapter 9 §9.2 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) solves its fully discrete-time version by identifying the exact combinatorial shape of the optimal policy — not just proving one exists. This mission also covers §9.1, a different application of Chapter 7's contracting theory to a consumption-investment problem whose planning horizon is itself random rather than fixed or infinite.

Setting

The dividend model is a stationary Markov Decision Model on the integers: the state $x \in \mathbb Z$ is the current risk reserve, the action $a \in \{0,1,\dots,x\}$ (for $x \ge 0$ ; only $a=0$ is available once ruined) is the dividend paid, the reward is $r(x,a):=a$ , and the reserve evolves by i.i.d. increments $Z_n$ (premia minus claims) after the dividend is deducted. Because the reward is bounded by an explicit function of the state (Lemma 9.2.2), Chapter 7's general existence theory applies directly, and the value function $J_\infty$ satisfies a genuine Bellman equation. The chapter's real content begins once existence is established: Theorem 9.2.3 pins down enough analytic structure of $J_\infty$ and its largest-maximizing policy $f^*$ (monotonicity, a Lipschitz-type inequality, and a self-consistency identity) to drive a purely combinatorial argument that $f^*$ 's shape is a finite alternation of "pay nothing" and "pay down to a fixed level" intervals — a band-policy (Definition 9.2.5). Section 9.1's random-horizon consumption-investment model reuses the same Chapter 7 machinery in a different setting: the usual $(c,a)$ (consumption, portfolio) decision each period, but where the horizon itself ends after each period with probability $1-p$ , making the effective one-period discount $\beta p$ rather than $\beta$ .

Formalization targets

The goal, Theorem 9.2.9, states the section's main claim in one sentence: the stationary policy $(f^*,f^*,\dots)$ is optimal and is a band-policy. Short as it is stated, its proof assembles every earlier result of the section. The milestones supply that assembly, in order: Lemma 9.2.2 gives the model's bounding function and the resulting integrability/convergence facts; Theorem 9.2.3 gives the value-function bounds and the self-consistency identity $f^*(x-f^*(x))=0$ ; Corollary 9.2.4 checks the two sign-definite degenerate cases directly from Theorem 9.2.3; Proposition 9.2.6 proves the top threshold $\xi := \sup\{x \mid f^*(x)=0\}$ is finite (not merely well-defined) and that $f^*$ is a simple barrier above it; Proposition 9.2.8 proves the increment property below $\xi$ that forces each band's shape; and Theorem 9.2.10 (a postscript refinement, stated after the goal) shows the wave lengths are bounded once the reserve's downward jumps are themselves bounded, collapsing to a single barrier-policy in the extreme case. Theorem 9.1.1, the random-horizon consumption-investment verification theorem, is included as a full item but is not a milestone of this goal, since its content and proof belong to a different, disjoint model — see Difficulty.

Significance

Band-policies and the discrete-time De Finetti dividend problem have no substrate anywhere in Mathlib or on the platform, and the result is a genuinely deep, classical one: a discrete-time analogue of the continuous-time De Finetti barrier-strategy theory, obtained here by pure dynamic-programming argument rather than the stochastic-calculus techniques the continuous-time theory usually relies on. The mission is explicit that the goal's conclusion is the general band-policy structure, not the strictly weaker barrier-policy special case that Theorem 9.2.10 b) proves only under an extra hypothesis (bounded downward jumps) — stating the goal with a barrier-policy conclusion instead would understate what Theorem 9.2.9 actually proves.

Difficulty

The central formalization challenge is Definition 9.2.5's own combinatorial intricacy: a band-policy is specified by an alternating chain of thresholds $0 \le c_0 < d_1 \le c_1 < d_2 \le \dots \le d_n \le c_n$ with a positive-width gap condition on every wave, and the policy's four piecewise branches case-split on which wave (if any) the current state falls into. This mission renders it existentially over the witnessing $(n,c,d)$ rather than as one closed-form function, a faithful but more verbose transcription that avoids conflating the different branch conditions. A second difficulty is Proposition 9.2.6's own finiteness claim: $\xi$ is a supremum over a subset of $\mathbb N_0$ that could, in principle, be unbounded, and Mathlib's convention for sSup over the naturals returns a finite junk value ( $0$ ) even for an unbounded set — using it directly would silently trivialize " $\xi<\infty$ " into a claim that is true regardless of the proposition's actual mathematical content. This mission instead states the proposition by exhibiting the finite value of $\xi$ directly, so that " $\xi$ is finite" survives as genuine content that the theorem's proof must establish. A third difficulty is scope: Theorem 9.1.1's random-horizon consumption-investment model shares no state space, action space, or definitions with the dividend model of the goal, despite both appearing in this chunk's assigned page range; it is formalized as a genuine application of a locally-restated copy of Chapter 7's contracting theory, but is excluded from the milestone list proper since it plays no role in the goal's own proof.

Formalization scope

The dividend model's transition law is built from Mathlib's PMF (probability mass function) type on $\mathbb Z$ , which supplies the "probabilities sum to one" fact automatically rather than as a separate hypothesis. J_\infty, \delta, and every finite-horizon value function throughout this mission use this whole book series' Filter.limsup-of-truncations convention for infinite-horizon reward, restated locally (own namespace copy, per this series' file-ownership boundary) from chunk 07a's identical apparatus rather than imported. The consumption-investment model of §9.1 is formalized with the number of risky assets $d$ as an explicit type parameter and its admissible-portfolio and domain restrictions as separate, citable fields rather than folded silently into the reward or transition definitions.

Selected references

N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
B. De Finetti, "Su un'impostazione alternativa della teoria collettiva del rischio", Transactions of the XVth International Congress of Actuaries, 1957 (the original continuous-time dividend problem this chapter's discrete-time analogue is modeled on).
H. Schmidli, Stochastic Control in Insurance, Springer, 2008 (cited by Remark 9.2.1 for the reduction from a continuous dividend-payout action space to the integer setting used throughout this section).
H. U. Gerber, "Games of economic survival with discrete- and continuous-income processes", Operations Research, 1972 (an early discrete-time treatment of the same class of problems, in the spirit this chapter's own model follows).

11 thms2 active usersReviewed

Analysis Partial Differential Equations·Captain: mikedeng1

Notes on Partial Differential Equations I: Mean Values, Maximum Principles and Analyticity of Harmonic FunctionsTextbook

Motivation

Laplace's equation $\Delta u = 0$ is the prototype of an elliptic partial differential equation. Its solutions, the harmonic functions, describe equilibrium states in potential theory (gravitation, electrostatics, steady heat flow), are the real and imaginary parts of holomorphic functions in the plane, and are the stationary states of Brownian motion. Many qualitative properties of general elliptic equations — interior smoothing, maximum principles, Harnack-type inequalities — are first seen, and most cleanly proved, for the Laplacian.

This mission covers §2.1–2.3 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014, author's copy), which follow Evans, Partial Differential Equations, §2.2 (AMS GSM 19) and Gilbarg–Trudinger, Elliptic Partial Differential Equations of Second Order, Ch. 2 (Springer). The chain runs from the mean value property to interior derivative estimates with explicit constants and ends with the real-analyticity of harmonic functions in any dimension; the maximum principles and Liouville's theorem are consequences on the same definitions. The results are classical (Gauss, Liouville, Weyl, Harnack; nineteenth and early twentieth century) and are in every graduate PDE course.

Setting

Fix $n \in \mathbb{N}$ and write $\mathbb{R}^n$ for Euclidean space with Lebesgue measure. For $x \in \mathbb{R}^n$ and $r > 0$ , $B_r(x) = \{y : |y - x| < r\}$ is the open ball and $\partial B_r(x) = \{y : |y - x| = r\}$ the sphere. For an open set $\Omega \subseteq \mathbb{R}^n$ write $B_r(x) \Subset \Omega$ when the closed ball $\overline{B}_r(x)$ is contained in $\Omega$ .

The Laplacian of a twice differentiable $u : \Omega \to \mathbb{R}$ is $\Delta u = \sum_{i=1}^n \partial_i^2 u$ . A function $u \in C^2(\Omega)$ is harmonic in $\Omega$ if $\Delta u = 0$ there, subharmonic if $\Delta u \ge 0$ and superharmonic if $\Delta u \le 0$ (Definition 2.4).

The averages of $u$ over a ball and a sphere are

⨍_{B_r(x)} u\,dx = \frac{1}{\alpha_n r^n}\int_{B_r(x)} u\,dx, \qquad ⨍_{\partial B_r(x)} u\,dS = \frac{1}{n\alpha_n r^{n-1}}\int_{\partial B_r(x)} u\,dS,

where $\alpha_n$ is the volume of the unit ball and $dS$ is surface measure. A continuous $u$ has the mean-value property (2.3) in $\Omega$ if $u(x)$ equals both averages whenever $B_r(x) \Subset \Omega$ .

For a multi-index $\alpha = (\alpha_1, \dots, \alpha_n) \in \mathbb{N}_0^n$ of order $|\alpha| = \alpha_1 + \cdots + \alpha_n$ , $\partial^\alpha u$ differentiates $u$ $\alpha_i$ times in the $i$ -th coordinate. A function is real-analytic in $\Omega$ if near every point of $\Omega$ it equals the sum of a convergent power series.

Formalization targets

Goal: analyticity (Theorem 2.10)

If $u \in C^2(\Omega)$ is harmonic in an open set $\Omega \subseteq \mathbb{R}^n$ , then $u$ is real-analytic in $\Omega$ .

Milestones

Theorem 2.1 (mean value property): if $u$ is harmonic and $B_r(x) \Subset \Omega$ , then $u(x) = ⨍_{B_r(x)} u\,dx = ⨍_{\partial B_r(x)} u\,dS$ .
Theorem 2.2 (converse): a continuous function with the mean-value property is $C^\infty$ and harmonic.
Theorem 2.7: $|\partial_i u(x)| \le \dfrac{n}{r}\max_{\overline{B}_r(x)}|u|$ for harmonic $u$ and $B_r(x) \Subset \Omega$ .
Theorem 2.9: for $|\alpha| = k \ge 1$ ,

|\partial^\alpha u(x)| \le \frac{n^k e^{k-1} k!}{r^k}\max_{\overline{B}_r(x)}|u|.

Corollary 2.8 (Liouville): a bounded harmonic function on $\mathbb{R}^n$ is constant.
Theorem 2.5: $u(x) \le$ both averages for subharmonic $u$ , $\ge$ for superharmonic $u$ .
Theorem 2.13 (strong maximum principle): a subharmonic function on a connected open set that attains a global maximum is constant.
Theorem 2.17 (weak maximum principle): on a bounded connected open set, a harmonic $u \in C^2(\Omega) \cap C(\overline{\Omega})$ satisfies $\max_{\overline{\Omega}} u = \max_{\partial\Omega} u$ and $\min_{\overline{\Omega}} u = \min_{\partial\Omega} u$ .

Theorems 2.1, 2.2, 2.7 and 2.9 lie on the path to the goal; the others are further results on the same definitions.

Significance

The result. Analyticity means that a harmonic function is determined on a connected domain by its germ at one point (Corollary 2.11). It is the model case of analytic hypoellipticity for elliptic operators with analytic coefficients. The derivative estimates of Theorem 2.9, with a constant growing like $k!$ , are the quantitative content: they are Cauchy-type estimates in several real variables and underlie compactness of families of harmonic functions and interior regularity arguments. The maximum principles give uniqueness for the Dirichlet problem (Theorem 2.18), and Liouville's theorem in $\mathbb{R}^n$ is the classification of bounded entire harmonic functions.

Formalizing it. Mathlib defines the Laplacian and harmonicity on inner product spaces and proves that harmonic functions on $\mathbb{C}$ are real parts of holomorphic functions, hence analytic; the Prove2Me corpus contains the mean value property and Liouville's theorem for functions on $\mathbb{C}$ (two dimensions, circle averages). Nothing in Mathlib or on the platform covers harmonic functions on $\mathbb{R}^n$ for general $n$ : no mean value property over balls and spheres in $\mathbb{R}^n$ , no derivative estimates, no maximum principle, no analyticity. All statements here are proved results; the work is formalizing the known proofs.

Difficulty

The two-dimensional route through holomorphic functions does not exist for $n \ge 3$ : there is no complex structure to borrow, so analyticity must come from the real-variable estimates of Theorem 2.9 and a remainder estimate for the multivariable Taylor expansion. Those estimates need the mean value property on balls and spheres of $\mathbb{R}^n$ , which requires surface measure on spheres, polar coordinates and the divergence theorem on a ball — tools that Mathlib has only in part. Theorem 2.9 asks for the constant $n^k e^{k-1}k!/r^k$ exactly, not merely some constant: the $k$ -dependence is the whole point, since a bound that grows faster than $k!$ times a geometric factor does not make the Taylor series converge. The converse Theorem 2.2 needs mollification. The weak maximum principle needs that the boundary of a bounded nonempty open set in $\mathbb{R}^n$ is nonempty and that the closure is compact.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; an open set is Ω : Set (EuclideanSpace ℝ (Fin n)) with IsOpen Ω. Functions are u : EuclideanSpace ℝ (Fin n) → ℝ of which only the values on $\Omega$ (or $\overline{\Omega}$ ) matter.
" $u \in C^2(\Omega)$ harmonic in $\Omega$ " is Mathlib's InnerProductSpace.HarmonicOnNhd u Ω; $\Delta$ is Mathlib's laplacian; $C^\infty$ is ContDiffOn ℝ ∞ (smooth, not analytic); real-analytic in $\Omega$ is AnalyticOnNhd ℝ u Ω.
$B_r(x) \Subset \Omega$ is 0 < r ∧ Metric.closedBall x r ⊆ Ω, never the open ball. The ball average is Mathlib's set average over Metric.ball x r; the sphere average is defined in polar form over the unit sphere with Mathlib's surface measure volume.toSphere. The mean-value property requires both identities of (2.3).
Coordinates are 0-based (i : Fin n); $\partial_i u(x)$ is the Fréchet derivative applied to the $i$ -th basis vector, and $\partial^\alpha$ applies these repeatedly, $\alpha_i$ times in coordinate $i$ .
$\max_{\overline{B}_r(x)}|u|$ in Theorems 2.7 and 2.9 is expressed by an arbitrary bound $M$ of $|u|$ on the closed ball; since the maximum is attained, this is equivalent. In Theorem 2.17 each equality of maxima is stated as attainment of the maximum over $\overline{\Omega}$ at a point of $\partial\Omega$ .
Theorem 2.9 is stated for $k = |\alpha| \ge 1$ : at $k = 0$ the printed bound reads $|u(x)| \le e^{-1}\max|u|$ , which fails for constants. The hypothesis $n \ge 1$ is added where the statement mentions a sphere (Theorems 2.1, 2.5) or a boundary (Theorem 2.17), which are empty in $\mathbb{R}^0$ .
A trivializing reading is excluded: the balls are closed balls of positive radius inside $\Omega$ , the averages are normalized integrals of continuous functions over sets of positive finite measure, and analyticity is required at every point of $\Omega$ rather than on one ball.

Needed infrastructure, reusable well beyond this mission: surface measure and polar coordinates on spheres of $\mathbb{R}^n$ , the divergence theorem on balls, mollification of continuous functions, and multivariable Taylor expansion with remainder in multi-index form. Contributions of any of these as separate lemmas are welcome.

Selected references

J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, Chapter 2. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
L. C. Evans, Partial Differential Equations, 2nd ed., AMS Graduate Studies in Mathematics 19, 2010, §2.2. https://doi.org/10.1090/gsm/019
D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Springer Classics in Mathematics, 2001, Chapter 2. https://doi.org/10.1007/978-3-642-61798-0
Q. Han and F. Lin, Elliptic Partial Differential Equations, 2nd ed., Courant Lecture Notes 1, AMS, 2011. https://doi.org/10.1090/cln/001

12 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XVI: Piecewise Deterministic Markov Decision ProcessesTextbook

Motivation

Every mission in this series so far has treated a control problem that already lives in discrete time: a decision maker observes a state, chooses an action, and the process moves to a new state at the next integer time step. Many real systems evolve in continuous time instead — a machine that runs deterministically until it randomly breaks down and is repaired into a new condition, an inventory that drains continuously until a random demand arrives, a population that grows deterministically between random catastrophic events. Chapter 8 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) shows that an entire class of such continuous-time control problems — Piecewise Deterministic Markov Decision Processes, where the state moves along a deterministic, controlled flow between randomly-timed jumps to a new state — can be solved by exactly the discrete-time machinery this book's series has already built, once the problem is re-expressed as a Markov Decision Model at the jump times themselves. This mission covers that embedding and its consequences (§8.2), and a simpler, discrete-state special case, the continuous-time Markov Decision Chain, treated with both an infinite and a finite time horizon (§8.3).

Setting

A Piecewise Deterministic Markov Decision Model (Definition 8.1.1) consists of a Borel state space $E$ , a Borel control space $U$ , a deterministic drift $\mu(x,u)$ governing the flow $\varphi^\alpha_t(x)$ between jumps, a Poisson jump clock of rate $\lambda$ , a kernel $Q$ giving the distribution of the post-jump state, a reward rate $r$ , and a discount rate $\beta$ . A control is a whole measurable function $\alpha : \mathbb R_{\ge0} \to U$ fixed at each jump time and applied until the next one — so the "action space" of the embedded discrete-time problem is itself a function space, a genuinely new technical wrinkle this book's earlier chapters never face. Embedding at the jump times produces a discrete-time Markov Decision Model $(E,A,Q',r')$ whose reward and kernel are themselves integrals of the original data against the flow (Eqs. (8.4)-(8.5)); Chapter 7's infinite-horizon existence theory, already developed for a general Borel state space, applies directly to this embedded model once its own compactness and semicontinuity hypotheses are checked. Checking them forces a further enlargement of the control space to the relaxed controls $R$ — measurable functions into probability measures on $U$ rather than $U$ itself — which is compact in a suitable topology where the space of literal control functions is not.

Formalization targets

The goal, Theorem 8.2.6, is the chapter's central existence result: given a continuous upper bounding function with the discrete embedded model's own contraction-type condition and a package of continuity/compactness assumptions, the value function of the model embedded with relaxed controls is bounded, upper semicontinuous, and a genuine fixed point of the maximal- reward operator, and an optimal relaxed Markov policy exists. The milestones build up to it and extend past it: Theorem 8.2.1 establishes the foundational fact that the continuous-time expected reward of the original process equals the discrete-time embedded model's own value — the correspondence every other result in the chapter relies on; Lemma 8.2.5 is the technical semicontinuity-preservation step the goal's proof needs; Theorem 8.2.7 upgrades the goal's relaxed optimal policy to a genuine, nonrelaxed one under an uncontrolled-flow or convexity condition; Theorem 8.2.8 gives the classical Hamilton-Jacobi-Bellman verification technique as an alternative, differential route to the same value function. Section 8.3's continuous-time Markov Decision Chain — the same theory specialized to a countable state space, transition rates in place of a kernel, and an uncontrolled flow — is covered for both an infinite horizon (Theorem 8.3.1) and, the more finance-relevant case, a finite horizon with a terminal reward (Theorems 8.3.2-8.3.3).

Significance

Piecewise Deterministic Markov Processes have no substrate anywhere in Mathlib or on the platform, and this mission's content is a genuine method, not just a specialization of existing results: it shows how to reduce an entire continuous-time control problem to the discrete-time theory already available, at the cost of enlarging the state of the discrete embedded problem's own data (which becomes an integral against a whole flow, not a pointwise value) and enlarging the control space when compactness is needed for existence. This mission is careful to keep two distinctions the book itself insists on separate: relaxed versus nonrelaxed controls (Theorem 8.2.6 produces only the former; recovering the latter is Theorem 8.2.7's own, harder, conditional content), and the general Piecewise Deterministic model of §8.1-8.2 versus the simpler, discrete-state Markov Decision Chain of §8.3, which is a genuinely different structure (sums over a countable state space rather than integrals against a controlled flow), not an instance of the general model specialized after the fact.

Difficulty

The central formalization challenge is representing the continuous-time expected reward $V^\pi(x)$ (Eq. (8.2)) faithfully, since the book itself only asserts the existence of a probability space carrying the jump-time/post-jump-state process with a specified conditional law, citing general marked-point-process theory rather than constructing it. This mission builds that probability-space data directly — via Mathlib's conditional expectation, conditioning on the current post-jump state — rather than treating $V^\pi$ as a bare hypothesis-only quantity, so that Theorem 8.2.1's value-equality claim is a genuine, non-vacuous correspondence between two independently-defined objects (a continuous-time path functional and a discrete-time recursion) rather than true by definitional fiat. A second, compounding difficulty is that the same correspondence must be built twice — once for the general flow-driven process (§8.2) and again, independently, for the discrete-state jump process of the finite-horizon chain (§8.3) — since the two models share no state-space structure. A third difficulty specific to Theorem 8.2.8 is that its Hamilton-Jacobi-Bellman verification argument is genuinely differential (a process generator built from a gradient, a self-referential closed-loop control solving its own ODE), unlike every other result in this chapter, which works through the discrete-time embedding alone.

Formalization scope

The book's own topology on the control-function space $A$ (the coarsest making certain integrals measurable) and the Young topology on the relaxed-control space $R$ (which the book cites as making $R$ separable, metric and compact, without reconstructing it) are not rebuilt from scratch; continuity/compactness hypotheses that need a topology on these spaces are stated directly against the pointwise/product topology on the underlying function types, a faithful but representationally simpler stand-in documented in MODERATION_NOTES.md. The embedded kernel $Q'$ (Eqs. (8.4), (8.7)) is bundled as data satisfying its own defining integral identity rather than literally constructed as a mixture of pushforward measures — a routine but heavy argument that would add no mathematical content beyond the formula itself. This mission's own goal (Theorem 8.2.6) explicitly produces a relaxed-control optimal policy, not a nonrelaxed one: stating it with a $U$ -valued policy instead would silently substitute Theorem 8.2.7's strictly harder, conditionally-true conclusion for Theorem 8.2.6's own unconditional one, exactly the trivializing formalization this chapter's own structure warns against.

Selected references

N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
M. H. A. Davis, Markov Models and Optimization, Chapman & Hall, 1993 (the standard reference for Piecewise Deterministic Markov Processes, cited by the book for extensions of this chapter's basic model).
A. A. Yushkevich, "On reducing a jump controllable Markov model to a model with discrete time", Theory of Probability and its Applications, 1980 (the topology on the control-function space $A$ cited by Definition 8.1.1's own construction).
H. J. Kushner and P. G. Dupuis, Numerical Methods for Stochastic Control Problems in Continuous Time, 2nd ed., Springer, 2001 (the Young topology and the Chattering Theorem, cited by Remark 8.2.3).
N. Bäuerle and U. Rieder, "Optimal control of piecewise deterministic Markov processes with finite time horizon", in Modern Trends of Controlled Stochastic Processes: Theory and Applications, 2010 (cited for the finite-horizon extension of this chapter's model, applied in chunk 09b's Sections 9.3-9.4).

16 thms2 active usersReviewed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis VI: Quasi M-Convex Functions and the Quasi-Proximity TheoremTextbook

Motivation

Convexity is normally defined additively — a function's value at a mixture is bounded by the mixture of its values — but many of the properties that make convexity useful in optimization (a local minimum is global, level sets are well-behaved) survive under a much weaker, purely ordinal notion: quasi-convexity, which compares function values rather than adding them. A nondecreasing rescaling of a convex function is generally not convex, but it is always quasi-convex — so a theory built only on ordinal comparisons automatically covers every such rescaling for free, at the cost of a more delicate proof architecture (since the algebraic cancellations available to additive convexity are no longer available).

Chapter 6's second half asks exactly how far this idea extends in the discrete setting: does the M-convexity exchange axiom have an ordinal, quasi-convex relaxation that still supports the same strong minimization theory — an optimality criterion, a minimizer-cut lemma, and, most significantly, a proximity theorem with the same explicit distance bound? This mission formalizes the chapter's answer: yes, and the relevant relaxed class, functions satisfying condition (SSQM $_{\ne}$ ), is large enough to include every strictly increasing rescaling of an M-convex function, a class the M-convex theory of chunk 06 alone says nothing about.

Setting

Let $V$ be a finite ground set and $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain. Building on chunk 06's M-convex exchange axiom (M-EXC[Z]), this chapter introduces several ordinal relaxations. $f$ is weakly quasi M-convex, satisfying (QMw), if for every pair of distinct points $x, y \in \operatorname{dom} f$ there exist $u$ in the positive support and $v$ in the negative support of $x - y$ with $f(x - \chi_u + \chi_v) \le f(x)$ or $f(y + \chi_u - \chi_v) \le f(y)$ — an "or" where (M-EXC[Z]) demands an additive inequality. Two further conditions restrict attention to points of different function value and sharpen the conclusion to a three-way trichotomy (strictly better on one side, or exactly tied on both): (SSQM $_{\ne}$ ) quantifies universally over $u$ (as in (M-EXC[Z])), while (SSQM $_{\ne,w}$ ) quantifies existentially over both $u$ and $v$ (as in (QMw)). The linear perturbation of $f$ by $p : V \to \mathbb R$ is $f[p](x) = f(x) - \langle p, x \rangle$ .

Formalization targets

Goal: Theorem 6.78 (the quasi M-proximity theorem)

Let $f$ satisfy (SSQM $_{\ne}$ ), $n = |V|$ , $\alpha$ a positive integer. If $x_\alpha \in \operatorname{dom} f$ satisfies $f(x_\alpha) \le f(x_\alpha + \alpha(\chi_v - \chi_u))$ for all $u, v \in V$ , then $\arg\min f \ne \emptyset$ and there is $x^* \in \arg\min f$ with $\|x_\alpha - x^*\|_\infty \le (n-1)(\alpha - 1)$ — verbatim the same conclusion, and the same exact bound, as chunk 06's Theorem 6.37(1), now established for the strictly larger class satisfying (SSQM $_{\ne}$ ) rather than the M-convex exchange axiom itself.

Milestones: Theorems 6.68(2), 6.76, 6.77

Theorem 6.68(2): $f$ satisfies (M-EXC[Z]) if and only if every linear perturbation $f[p]$ satisfies (QMw) — quantifying exactly how much weaker (QMw) is pointwise, and how the gap closes once quantified over every perturbation. Theorem 6.76 (the quasi M-optimality criterion): the direct analogue of chunk 06's Theorem 6.26 for the quasi-convexity classes — a purely pairwise local check still characterizes global (or, in the (QMw) case, strict unique) optimality. Theorem 6.77 (the quasi M-minimizer cut): chunk 06's Theorem 6.28 continues to hold verbatim when its M-convexity hypothesis is replaced by (SSQM $_{\ne}$ ) — the structural fact the proximity theorem's proof is built from survives the relaxation intact.

Significance

The result itself. The proximity theorem is the result algorithms actually use: a scaling algorithm for minimizing quasi-convex functions of this kind inherits exactly the same correctness guarantee, with exactly the same distance bound, as the M-convex case — this is a genuine broadening of chapter 10's algorithmic reach, not a restatement dressed in weaker hypotheses. Every strictly increasing scalar transformation of an M-convex objective (a common modeling device — re-expressing a cost in utility units, or applying a monotone risk measure) now falls under a proximity theorem, whereas prior to this chapter's relaxation such a transformation would generally destroy M-convexity itself and leave optimization theory silent on the transformed problem.

Formalizing it. No matching item exists on the platform for quasi M-convexity in any of its forms. Formalizing Theorem 6.78 requires first pinning down (SSQM $_{\ne}$ ) exactly (there are six closely related axiom variants in this section of the book, only three of which — (QMw), (SSQM $_{\ne}$ ), (SSQM $_{\ne,w}$ ) — are needed for this mission's chosen results), and this mission also captures, via Theorem 6.68(2), the precise sense in which these relaxed conditions are strictly weaker than plain M-convexity while remaining tightly connected to it.

Difficulty

The natural first instinct, given how close the quasi-convexity axioms look to (M-EXC[Z]), is to try to prove Theorem 6.78 by directly imitating chunk 06's proof of Theorem 6.37 line by line. This mostly works — the proof structure (fix a target coordinate, build a chain of strictly decreasing values via repeated exchange steps, bound the chain's length using the scaled hypothesis) survives verbatim — but every step that chunk 06's proof took by adding two instances of the exchange inequality together must be replaced by an ordinal argument, since (SSQM $_{\ne}$ ) only ever asserts a disjunction of value comparisons, never an additive inequality relating four function values simultaneously the way (M-EXC[Z])'s $f(x)+f(y) \ge f(x-\chi_u+\chi_v)+f(y+\chi_u-\chi_v)$ does. The book's proof handles this by working with strict inequalities and the trichotomy structure of (SSQM $_{\ne}$ ) directly rather than algebraic cancellation — the same overall architecture, but every arithmetic step rebuilt as a case analysis on which disjunct of (SSQM $_{\ne}$ ) fires.

Formalization scope

This mission builds directly on chunk 06's published items (CharVec, SuppPos, SuppNeg, DomZ, MExchangeAxiom, ArgMin), per the platform's textbook convention that a later chapter of the same book imports an earlier one's definitions rather than redrafting them; its own namespace DiscreteConvex.MConvexFunctions.Quasi nests under chunk 06's DiscreteConvex.MConvexFunctions accordingly. Δf(z;v,u) (Eq. (6.2)) is never reified as a separate object; every occurrence is unfolded directly into an f-value comparison, avoiding WithTop ℝ subtraction throughout, consistent with chunk 06's own convention.

A trivializing formalization of the goal would silently strengthen (SSQM $_{\ne}$ ) back to plain M-convexity (making this mission redundant with chunk 06's Theorem 6.37) or loosen the exact bound $(n-1)(\alpha-1)$ to an unspecified function of $n, \alpha$ ; neither is done. Six axiom variants appear in this section of the book ((QM), (SSQM), (QMw), (SSQM $_w$ ), (SSQM $_{\ne}$ ), (SSQM $_{\ne,w}$ )); only the three actually needed by this mission's four items are drafted, and Theorem 6.68's first part (an implication chain among the other three) is left out — see MODERATION_NOTES.md. Contributions building the polyhedral M-convex-function bridge (§6.11–6.12, Theorems 6.59–6.64), the level-set characterizations (Theorems 6.72, 6.74), or the scaled quasi M-minimizer cut (Theorem 6.79, the direct generalization of Theorem 6.77 drafted here) are welcome.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
M. Avriel, W. E. Diewert, S. Schaible, I. Zang, Generalized Concavity, Plenum Press, 1988.

8 thms2 active usersReviewed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XV: Optimal Play in Red-and-Black and the Gittins IndexTextbook

Motivation

Chapter 7's abstract machinery — contracting Markov Decision Models, the Structure Theorem, value iteration with an explicit convergence rate — earns its keep by solving concrete problems. Section 7.6 works through four kinds of application: a return to the classical cash-balance inventory problem, now over an infinite horizon; the "red-and-black" gambling problem, where a player tries to reach a target fortune before going bankrupt; and, most substantially, the infinite-horizon two-armed bandit, where the general theory reveals something genuinely surprising — the qualitatively optimal policy can be computed one arm at a time.

Setting

Every application here specializes the general infinite-horizon, contracting-model machinery of chunks 07a/07b to a concrete transition structure. The cash-balance model orders inventory up to a level $a$ at linear cost, incurs a holding/shortage cost, then absorbs a random demand. The red-and-black model bets a fraction of a bounded fortune on a biased coin, absorbing at bankruptcy or at the target. The bandit model reconsiders the Beta-Bernoulli two-armed bandit of chunk 05b, now over an infinite horizon with a genuine discount $\beta<1$ : the key new tool is the K-stopping problem, a fictitious single-arm decision problem where, at every stage, the decision maker may either pull the arm or retire with a fixed payment $K$ . The Gittins index $I(m,n)$ is the smallest such payment at which retiring immediately is already as good as continuing.

Formalization targets

The goal, Theorem 7.6.10, is the Gittins index theorem for this book's two-armed bandit: always pulling the arm with the higher index is optimal for the full infinite-horizon problem. The milestones build the machinery it needs — the index's definition (Definition 7.6.5) and its equivalent representation as a supremum over stopping times (Theorem 7.6.6), the K-stopping value function's monotonicity/convexity/differentiability properties (Proposition 7.6.7), the index's optimal-stopping-set and indifference characterizations (Corollary 7.6.8), the two-arm joint stopping value's parallel structure (Proposition 7.6.9), and a fixed-point recasting useful for computation (Proposition 7.6.11) — plus, independently, the cash-balance and casino-game applications (Theorems 7.6.1-7.6.4), which use the general theory but not the bandit-specific machinery.

Significance

The Gittins index theorem's real content, emphasized by the book's own remark, is not merely that an optimal policy exists but how little computation it needs: instead of solving one optimization problem over the bandit's full four-dimensional joint state space $\mathbb N_0^2 \times \mathbb N_0^2$ , the decision maker solves two independent two-dimensional single-arm problems and compares two numbers. This mission's formalization of the goal is built specifically to keep that separation visible — each arm's index is computed from a single, shared KStoppingValue structure applied to that arm's own state alone, never from a function that happens to take the whole joint state as an argument. The proof route here (via the K-stopping problem's explicit fixed-point characterization, Definition 7.6.5 and Proposition 7.6.11) is a genuinely different construction from the platform's existing Gittins-index theorems (BanditAlgorithm.gittins_index_theorem and related), which are built via Whittle's retirement/charge-accounting argument — checked directly and found to define the index differently enough that this mission drafts its own theorems rather than treat that construction as prior art.

Difficulty

The K-stopping value function $J(m,n;K)$ and the two-arm joint value $\tilde J(x;K)$ are both genuine fixed points of an infinite-horizon Bellman equation with no finite backward recursion to fall back on (the "stopping" option, rather than a terminal condition, is what makes the horizon infinite); this mission bundles them as data satisfying their own defining fixed-point equations, the same convention this series uses throughout for such objects. A second difficulty is Theorem 7.6.6's supremum over stopping times: without a canonical path measure for the underlying Markov chain (not built anywhere in this series), the two expectations the theorem compares are represented as data satisfying the positivity a genuine expectation must have, over an explicit, elementary notion of stopping time (a function of the whole observed path, adapted in the sense that whether it has fired by time $n$ depends only on the path up to $n$ ) — a faithful, if representational, rendering of the theorem's genuinely path-dependent content.

Formalization scope

The cash-balance model (Theorem 7.6.1) explicitly cites chunk 02d's finite-horizon critical-level sequences as a hypothesis rather than re-deriving them, since this mission's own content is the infinite-horizon extension, not a second proof of the finite-horizon theory those sequences come from. The casino-game theorems (7.6.2-7.6.4) state optimality for the specific, named timid and bold strategies, not for an unnamed "some optimal policy" — the theorems' entire content is that these particular policies, not merely some optimal one, are best in their regime. The bandit model's posterior mean and Bayes-update operator are kept identical in substance to chunk 05b's finite-horizon Beta-Bernoulli model (restated, since chunks cannot import each other's Lean), so a reader can see this section is solving the same underlying statistical model, now over an infinite horizon.

Selected references

N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
J. C. Gittins, "Bandit processes and dynamic allocation indices," Journal of the Royal Statistical Society, Series B, 1979 (the original index construction this section's K-stopping-problem approach reformulates).
P. Whittle, "Multi-armed bandits and the Gittins index," Journal of the Royal Statistical Society, Series B, 1980 (the retirement-option construction the platform's existing Gittins theorems use, a different proof route from this chunk's own).
L. E. Dubins and L. J. Savage, How to Gamble If You Must: Inequalities for Stochastic Processes, McGraw-Hill, 1965 (the classical red-and-black problem, Theorems 7.6.2-7.6.4).

14 thms2 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis V: The M-Optimality Criterion and the Proximity TheoremTextbook

Motivation

Scaling algorithms are one of the standard techniques for solving discrete optimization problems efficiently: instead of searching a huge integer domain directly, an algorithm first solves a coarsened version of the problem — checking optimality only against neighbors reached by a large step size $\alpha$ — and then refines the resulting approximate solution down to the true optimum. This strategy is only as good as the guarantee that a coarse-scale local optimum is provably close to a true, fine-scale global optimum; without such a guarantee, refinement could require an unbounded number of steps. Results providing this guarantee are called proximity theorems, and they are a standard tool across combinatorial optimization, from network flow scaling algorithms to submodular function minimization.

M-convex functions, the subject of this chapter, are exactly the class of discrete convex functions for which the classical local-optimality test of chapter 3 (checking a full neighborhood of up to $3^n-1$ sign patterns) sharpens to a much smaller, purely pairwise test: checking $f(x) \le f(x - \chi_u + \chi_v)$ for every pair of coordinates $u, v$ . This mission formalizes the chapter's central definitional equivalence (Theorem 6.2), this pairwise optimality criterion (Theorem 6.26), a structural minimizer-cut lemma (Theorem 6.28), and the chapter's capstone, the M-proximity theorem (Theorem 6.37) — the result that makes M-convex scaling algorithms provably correct, with an explicit, dimension-and-scale-only distance bound between a coarse-scale local optimum and a true global minimizer.

Setting

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

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

An M $^\natural$ -convex function is one whose lift $\tilde f$ to the extended ground set $\tilde V = \{0\} \cup V$ — defined by $\tilde f(x_0, x) = f(x)$ when $x_0 = -x(V)$ , and $+\infty$ otherwise — is M-convex; equivalently (Theorem 6.2, below) $f$ satisfies the axiom (M $^\natural$ -EXC[Z]), a variant of (M-EXC[Z]) that additionally allows a single-coordinate move ( $u$ alone, with no compensating $v$ ). Every M-convex function is M $^\natural$ -convex, but not conversely. For $\alpha$ a positive integer, a point satisfies the scaled local optimality condition at scale $\alpha$ if $f(x_\alpha) \le f(x_\alpha + \alpha(\chi_v - \chi_u))$ for all relevant $u, v$ — a check against neighbors $\alpha$ steps away rather than adjacent ones.

Formalization targets

Goal: Theorem 6.37 (the M-proximity theorem)

Assume $\alpha$ is a positive integer and $n = |V|$ .

\text{(1) } f \text{ M-convex, } f(x_\alpha) \le f(x_\alpha + \alpha(\chi_v-\chi_u))\ \forall u,v \implies \exists x^* \in \arg\min f,\ \|x_\alpha - x^*\|_\infty \le (n-1)(\alpha-1),

\text{(2) } f \text{ M}^\natural\text{-convex, same hypothesis over } u,v \in V \cup \{0\} \implies \exists x^* \in \arg\min f,\ \|x_\alpha - x^*\|_\infty \le n(\alpha-1).

Both bounds are exact and specific to their hypothesis class; replacing either with an unspecified function of $n$ and $\alpha$ would discard exactly the content chapter 10's algorithms rely on.

Milestones: Theorems 6.2, 6.26, 6.28

Theorem 6.2: M $^\natural$ -convexity (defined via the lift) is equivalent to the direct exchange axiom (M $^\natural$ -EXC[Z]) — the chapter's central definitional theorem, needed to work with M $^\natural$ -convex functions without repeatedly invoking the lift construction. Theorem 6.26 (the M-optimality criterion): global optimality of $f$ at $x$ is equivalent to a purely pairwise local check, $f(x) \le f(x-\chi_u+\chi_v)$ for all $u,v$ (plus, in the M $^\natural$ case, $f(x) \le f(x\pm\chi_v)$ ). Theorem 6.28 (the M-minimizer cut): from any point and any coordinate pair minimizing a one-step exchange, one can certify a coordinate-wise bound that some global minimizer must satisfy — the structural fact underlying both the domain-reduction algorithm and, via the same proof technique, the proximity theorem itself.

Significance

The result itself. Theorem 6.26 already sharpens chapter 3's local-to-global criterion (checking a full $3^n-1$ -point neighborhood) to an $O(n^2)$ -size pairwise check — the minimum spanning tree optimality criterion is a direct special case. The proximity theorem builds on this to control what happens when the local check is only performed at a coarse scale $\alpha$ : it guarantees that scaling-based algorithms, which alternate between coarse-scale local search and scale reduction, terminate with a guaranteed-close approximation at every stage, with an explicit linear-in- $n$ , linear-in- $\alpha$ error bound rather than a qualitative "eventually converges" guarantee.

Formalizing it. No matching item exists on the platform for M-convex functions, the exchange axiom, or a discrete proximity theorem of this kind. This mission gives the first formal statement of the M-optimality criterion and the M-proximity theorem, together with the exchange-axiom / lift-based-definition equivalence (Theorem 6.2) that the rest of the M-convex function theory (chunks 07, and indirectly 10–14) is built on.

Difficulty

The natural first attempt at Theorem 6.37 is to try a direct coordinatewise argument: since the scaled hypothesis holds for every pair $u, v$ , one might hope to bound $|x_\alpha(v) - x^*(v)|$ coordinate by coordinate independently. This does not work, because a single application of the exchange axiom only ever improves $f$ by trading one coordinate down and one other coordinate up simultaneously — there is no way to move a single coordinate toward a minimizer in isolation without accounting for where the compensating mass goes. The actual proof instead fixes a target coordinate $v$ , constructs a chain of strictly decreasing function values $y_0 = x_\alpha, y_1, \ldots, y_k$ by repeatedly applying (M-EXC[Z]) against a fixed near-optimal point $x^*$ (exactly the technique of Theorem 6.28's proof), and then bounds how far each other coordinate can move along this chain using the scaled hypothesis itself, before summing those bounds via the M-convex domain's hyperplane constraint $x(V) =$ constant to recover the bound on $v$ . The chain construction, not a per-coordinate estimate, is what makes the linear-in- $n$ bound provable at all.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is (V → ℤ) → WithTop ℝ. M $^\natural$ -convexity is represented via an explicit lift to Option V (none standing for the extended ground set's new element $0$ ), matching the book's own primary definition; the direct exchange-axiom form is a separate predicate related to it by Theorem 6.2, not conflated with it. `‖x_\alpha - x^*|_\infty \le c$ is stated pointwise.

A trivializing formalization of the goal would replace either exact bound, $(n-1)(\alpha-1)$ or $n(\alpha-1)$ , with an unspecified asymptotic bound, or merge the two hypothesis classes into a single weaker statement; neither is done here. Propositions establishing dom f as an M-convex set, the M/M $^\natural$ relationship (Theorem 6.3), and several structural closure properties are cut from this mission's scope (not needed by the chosen items' statements — see MODERATION_NOTES.md) but are natural targets for a follow-on mission or for chunk 07, which builds directly on this chunk's exchange-axiom vocabulary. Contributions building the arg min f M-convexity corollary (Proposition 6.29) or the scaled minimizer cut (Theorem 6.39, the direct generalization of Theorem 6.28 drafted here) are welcome.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
D. S. Hochbaum, "Lower and upper bounds for the allocation problem and other nonlinear optimization problems," Mathematics of Operations Research, 19(2), 1994, pp. 390–409.

14 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XIII: Contracting Infinite-Horizon Markov Decision ModelsTextbook

Motivation

Every mission in this series so far has treated a finite-horizon decision problem: an investor or planner with a fixed, known number of periods left. Many of the most important applications — perpetual investment, an infinitely-repeated inventory or maintenance problem, a firm that never stops operating — have no natural end date at all. Chapter 7 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) builds the theory needed to make sense of "the value of a decision problem that never ends," and does so on a general Borel state space rather than a finite one. This mission covers the chapter's first three sections: the general infinite-horizon setup, the semicontinuous existence theory that makes it usable, and the sharper contraction-based theory that is the chapter's, and arguably the whole book's, theoretical center.

Setting

An infinite-horizon Markov Decision Model reuses the same data $(E,A,D,Q,r,\beta)$ as the finite-horizon models of earlier chapters, but drops the terminal reward and applies a single (possibly randomized) decision rule at every one of infinitely many stages. Its performance criterion, $J_\infty(x) := \sup_\pi \mathbb E^\pi_x\big[\sum_{k=0}^\infty \beta^kr(X_k,f_k(X_k)) \big]$ , is only meaningful once an integrability condition (Assumption (A)) and a convergence condition (Assumption (C)) rule out the sum diverging or the finite-horizon approximations failing to settle down. Both conditions follow automatically once the model has an upper bounding function $b$ — a function controlling both the size of the reward and how fast the transition kernel can grow $b$ itself — with $\beta\alpha_b < 1$ , the manageable special case that covers both the classical bounded-reward discounted case and the case of a non-positive reward.

Formalization targets

The goal, Theorem 7.3.5 (Structure Theorem), is the chapter's capstone: under a genuine bounding function (a two-sided reward bound making the space $IB_b$ of finite-weighted-norm functions a Banach space) with $\beta\alpha_b < 1$ , and one abstract structural hypothesis — a closed class $IM \subset IB_b$ containing $0$ , mapped into itself by the Bellman operator $T$ , on which a maximizing action always exists — Banach's fixed point theorem delivers existence, uniqueness, an explicit geometric convergence rate for value iteration, and existence of an optimal stationary policy, all at once. The milestones build up to it in three stages: the general infinite-horizon machinery (Lemmas 7.1.4-7.1.5, Theorems 7.1.6-7.1.8 — reward iteration, a verification theorem, and a structure theorem under an abstract structure assumption that is not yet tied to any checkable property of the model); the semicontinuous existence theory that gives primitive, checkable conditions implying that abstract assumption (Theorem 7.2.1 and its two corollaries, including a genuine policy iteration conclusion); and the contracting theory proper (Lemma 7.3.3's contraction estimate, Theorem 7.3.4's sharpened verification theorem, and Theorem 7.3.6's continuous specialization of the goal).

Significance

The goal is the direct, general-Borel-space generalization of what finite-state dynamic programming theorems already on the platform (BertsekasDP.discounted_main_theorem, BertsekasDP.ssp_main_theorem) establish only for a finite state and action space, where Banach's theorem is applied directly on $\mathbb R^n$ : this mission's content is that the same conclusions — including the same explicit geometric convergence rate for value iteration — hold on an arbitrary Borel state space, the moment one abstract, structural condition is checked. That condition is not vacuous or automatic: Example 7.2.4 (cited but not itself formalized, being an unnumbered worked counterexample rather than a numbered result) shows that without compactness of the feasible-action correspondence, the naive Structure Assumption of Chapter 2 is not enough and value iteration can converge to the wrong limit ( $J \ne J_\infty$ ). Theorems 7.1.8's Structure Assumption (SA) is built precisely to rule this out, and Theorem 7.2.1's semicontinuity/ compactness conditions are the practical, checkable sufficient conditions for it.

Difficulty

The central formalization challenge is representing $J_\infty^\pi$ , the genuine infinite-horizon expected discounted reward, without constructing a canonical infinite-horizon path measure from the model's transition kernel — a substantial undertaking the book itself sidesteps by proving (via an appendix result, Theorem B.1.1, not itself reproved here) that $J_\infty^\pi$ equals the limit of the finite-horizon truncations $J_n^\pi$ . This mission takes that limit characterization as its own definition, via Filter.limsup for the same total, junk-safe reasons this book's series has used throughout (no canonical path measure anywhere in chunks 02a, 05a, 05b, 06). A second, genuinely new difficulty is Ls, the "upper limit of a sequence of sets" that drives every policy-iteration conclusion: it is a statement about accumulation points of a sequence of points, one drawn from each set in the sequence, not the more familiar set-theoretic limsup of a sequence of sets — getting this distinction right is the entire content of what "policy iteration" asserts.

Formalization scope

Every operator, bounding-function class, and value function of §7.1-7.3 is restated (not imported) in this chunk's own namespace from the finite-horizon originals of chunks 02a/02b, adapted to drop the time index and bake the discount into the one-stage operator directly, per this chapter's own presentation. The contracting theory's genuinely real-valued Banach-space objects ( $T_f'$ , $T'$ , $IB_b$ , the weighted norm $\|\cdot\|_b$ ) are kept separate from the general theory's EReal-valued objects ( $T_f$ , $T$ , $IM(E)$ ), matching the book's own distinction between a value function that is a priori only known to avoid $+\infty$ and one known to be genuinely finite everywhere. Part (d) of the goal — the explicit geometric convergence rate — is stated in full, not weakened to bare qualitative convergence, since a formalization that dropped it would lose exactly the fact (used again by this book's own Theorem 7.5.12, a different chunk) that makes value iteration a genuine numerical method with a computable error bound rather than merely an existence argument.

Selected references

N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. II, 4th ed., Athena Scientific, 2012 (the finite-state discounted/SSP theorems this goal generalizes).
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (analytic measurability of $J_\infty$ , $J$ ; cited by the book for this chapter's foundational measure-theoretic facts).
K. Hinderer, Foundations of Non-stationary Dynamic Programming with Discrete Time Parameter, Lecture Notes in Operations Research and Mathematical Systems 33, Springer, 1970 (Theorem 18.4, cited for the fact that history-dependent policies do not improve on Markov ones).

16 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning Operations Research+1·Captain: mikedeng1

A Stochastic Quasi-Newton Method for Large-Scale Optimization: The Expected Suboptimality Bound of the SQN MethodResearch Paper

Motivation

Training a statistical model by empirical risk minimization means minimizing an average of $N$ losses over a parameter vector $w\in\mathbb R^n$ , where both $N$ and $n$ can be in the millions. Stochastic gradient descent (SGD) is the standard method: each step uses the gradient of a small random batch of losses. It is cheap per step but sensitive to the scaling of the problem. Quasi-Newton methods such as L-BFGS correct the scaling in deterministic optimization, but naive stochastic versions are unstable, because differences of noisy gradients are poor curvature estimates.

Byrd, Hansen, Nocedal and Singer (SIAM J. Optim. 26(2), 2016) proposed the stochastic quasi-Newton (SQN) method. It decouples the two estimates: gradients come from small batches at every step, while curvature pairs are formed only every $L$ steps, from averaged iterates and subsampled Hessian–vector products. The paper's analysis (Section 3) shows that the method keeps the $O(1/k)$ expected suboptimality rate of SGD on strongly convex problems. The same eigenvalue bound was obtained independently by Mokhtari and Ribeiro (JMLR 16, 2015). Bottou, Curtis and Nocedal later gave a general treatment of such preconditioned stochastic methods (SIAM Review 60(2), 2018).

Setting

Let $f_1,\dots,f_N:\mathbb R^n\to\mathbb R$ be twice continuously differentiable losses and

F(w)=\frac1N\sum_{i=1}^N f_i(w).

For a sample $\mathcal S\subseteq\{1,\dots,N\}$ of size $b$ , the minibatch gradient is $\nabla F_{\mathcal S}(w)=\frac1b\sum_{i\in\mathcal S}\nabla f_i(w)$ . For a sample $\mathcal S_H$ of size $b_H$ , the subsampled Hessian is $\nabla^2F_{\mathcal S_H}(w)=\frac1{b_H}\sum_{i\in\mathcal S_H}\nabla^2 f_i(w)$ .

Assumption 1 requires constants $0<\lambda,\Lambda$ with $\lambda I\prec\nabla^2F_{\mathcal S_H}(w)\prec\Lambda I$ for every $w$ and every Hessian sample. It also requires a bound $\gamma^2$ on the second moment of the stochastic gradient. $w^*$ denotes the minimizer of $F$ .

Algorithm 2 turns correction pairs $(s_j,y_j)$ into a matrix $H_t$ . With $\tilde m=\min\{t,M\}$ , it starts from $\frac{s_t^Ty_t}{y_t^Ty_t}I$ and applies the BFGS update

H\leftarrow(I-\rho_js_jy_j^T)H(I-\rho_jy_js_j^T)+\rho_js_js_j^T,\qquad\rho_j=\frac1{y_j^Ts_j},

for $j=t-\tilde m+1,\dots,t$ .

Algorithm 1 (SQN) runs for $k=1,2,\dots$ . It draws a gradient sample $\mathcal S_k$ and steps

w^{k+1}=w^k-\alpha^kH\nabla F_{\mathcal S_k}(w^k),

where $H=I$ for $k\le2L$ and $H=H_t$ , $t=\lfloor(k-1)/L\rfloor-1$ , afterwards. Every $L$ iterations it forms the block average $\bar w_t$ of the last $L$ iterates and a new pair

s_t=\bar w_t-\bar w_{t-1},\qquad y_t=\nabla^2F_{\mathcal S_{H,t}}(\bar w_t)\,s_t .

Samples are drawn independently and uniformly among the subsets of their size. The step length is $\alpha^k=\beta/k$ .

Formalization targets

Goal: Corollary 3.3, with a corrected constant

There are $0<\mu_1\le\mu_2$ , depending only on the problem data, such that every matrix Algorithm 1 applies satisfies $\mu_1I\prec H\prec\mu_2I$ . Moreover, for every $\beta>1/(2\mu_1\lambda)$ ,

E[F(w^k)-F(w^*)]\le\frac{Q_c(\beta)}k\qquad(k\ge1),

Q_c(\beta)=\max\Big\{\frac{\Lambda\mu_2^2\beta^2\gamma^2}{2(2\mu_1\lambda\beta-1)},\ \Lambda\mu_2^2\beta^2\gamma^2,\ F(w^1)-F(w^*)\Big\}.

The constants $\mu_1,\mu_2$ are not fixed numerically. The goal asserts a rate of order $1/k$ with an explicit constant in terms of them.

Milestones

(3.8)–(3.10): the curvature bounds $\lambda\|s\|^2\le y^Ts\le\Lambda\|s\|^2$ and $\lambda\le\|y\|^2/y^Ts\le\Lambda$ for Hessian-product pairs.
(3.11) and (3.12): the trace bound and Powell's determinant formula for the direct L-BFGS matrices.
Lemma 3.1: $\mu_1I\prec H_t\prec\mu_2I$ uniformly along every run.
(3.18): expected descent for the general Newton-like iteration $w^{k+1}=w^k-\alpha^kH_k\nabla f(w^k,\xi^k)$ .
(3.19): $2\lambda[F(w)-F(w^*)]\le\|\nabla F(w)\|^2$ .
(3.22): the recursion $\phi_{k+1}\le(1-2\alpha^k\mu_1\lambda)\phi_k+\frac\Lambda2(\alpha^k\mu_2)^2\gamma^2$ .
Theorem 3.2: the $Q_c(\beta)/k$ rate for the Newton-like iteration.

Significance

The corollary says that curvature information costs nothing in rate. With uniformly bounded preconditioners and the $\beta/k$ schedule, the SQN method converges in expectation at the same order as SGD, which is the order known to be optimal for this class of problems. Lemma 3.1 is the reusable part: it holds for any L-BFGS matrix built from pairs whose curvature is controlled by a bounded Hessian. Theorem 3.2 applies to every stochastic method whose preconditioner is fixed before the sample is drawn and has uniformly bounded spectrum.

The formalization adds three things. First, it states the result correctly. As printed, Theorem 3.2 is false and Assumption 1(3) cannot be satisfied (see Formalization scope), and the mission states and labels the repaired versions. Second, it gives a machine-checked statement of the SQN algorithm itself, which is not currently formalized anywhere. Third, it provides L-BFGS and preconditioned-SGD infrastructure that later missions on stochastic second-order methods can reuse. To our knowledge none of these results has a machine-checked proof.

Difficulty

The natural first idea is to feed the iterates of Algorithm 1 to a standard SGD rate theorem. This fails for two reasons. The preconditioner $H_t$ depends on the past iterates and on independent Hessian samples, so the analysis needs a filtration in which $H_t$ is known before the gradient sample is drawn. Also, the rate proof itself is an induction that breaks in the first iterations, which is exactly where the printed argument goes wrong.

On the linear-algebra side, the difficulty is a lower bound on the smallest eigenvalue of $H_t$ that is uniform over all runs and all $t$ . The curvature bounds on each individual pair do not give it directly, because the BFGS updates compound across the memory window. The expectation side needs conditional expectations of vector-valued functions and a descent inequality under a Hessian bound, neither of which Mathlib packages for this setting.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin n), matrices are Matrix (Fin n) (Fin n) ℝ acting through Matrix.toEuclideanLin, and $A\prec B$ is (B - A).PosDef. Hessians are fderiv ℝ (gradient f) w. Indices $k,t$ start at $1$ as in the paper. In the corollary, $E$ is an exact finite average over sample histories, and "almost surely" means "on every history". Theorem 3.2 uses a general probability space with a filtration. $H_k$ and $w^k$ are $\mathcal F_k$ -measurable, the sample $\xi^k$ is $\mathcal F_{k+1}$ -measurable, and unbiasedness is a conditional expectation. Integrability of $F(w^k)$ is part of each conclusion, so a junk-zero integral cannot satisfy it.

Two corrections to the paper, each labelled in the item titles and notes:

Iterate-wise $\gamma$ . Assumption 1(3) says $E_\xi\|\nabla f(w,\xi)\|^2\le\gamma^2$ for all $w$ . Together with unbiasedness and $\lambda$ -strong convexity on $\mathbb R^n$ , this forces $\lambda\|w-w^*\|\le\|\nabla F(w)\|\le\gamma$ for every $w$ , which is impossible. The mission imposes the bound at the iterates, conditionally on the past, which is how the proof uses it.
Constant $Q_c(\beta)$ . The induction after (3.22) multiplies by $1-2\beta\mu_1\lambda/k$ , which is negative for $k<2\beta\mu_1\lambda$ . Counterexample: $n=1$ , $f_{1,2}(w)=(w\mp1)^2/2$ , $H_k=I$ , $w^1=0$ , $\beta=2$ , $\gamma^2=5$ . Then $F(w^2)-F(w^*)=2>Q(2)/2=5/3$ , and the example survives perturbing the constants so that every strict inequality holds. The middle entry of $Q_c$ repairs it, and $Q_c=Q$ whenever $2\mu_1\lambda\beta\le3/2$ .

Smaller conventions:

The pairs must satisfy $s_t\neq0$ , since Algorithm 2 is undefined otherwise.
Hessian samples have size $b_H\ge1$ ; the empty sample makes (2.3) a $0/0$ .
The corollary's undefined $\mu_2$ is Lemma 3.1's constant, enlarged together with $\mu_1$ to cover the initial $H=I$ steps.
The block average of Algorithm 1 is used, not Eq. (2.1).

Trivializing encodings are ruled out: $H_t$ is Algorithm 2 applied to Algorithm 1's own pairs, not an arbitrary bounded matrix, and the second-moment bound is not imposed for all $w$ .

Needed infrastructure, all welcome as contributions: the symmetry and spectral bounds of Hessians of $C^2$ functions, trace and determinant identities for BFGS updates, the descent lemma from a Hessian upper bound, conditional-expectation manipulations for adapted iterations, and the reduction of Algorithm 1 with uniform finite sampling to the abstract iteration.

Selected references

R. H. Byrd, S. L. Hansen, J. Nocedal, Y. Singer, A Stochastic Quasi-Newton Method for Large-Scale Optimization, SIAM J. Optim. 26(2):1008–1031, 2016. https://doi.org/10.1137/140954362
A. Mokhtari, A. Ribeiro, Global Convergence of Online Limited Memory BFGS, J. Mach. Learn. Res. 16:3151–3181, 2015. https://jmlr.org/papers/v16/mokhtari15a.html
L. Bottou, F. E. Curtis, J. Nocedal, Optimization Methods for Large-Scale Machine Learning, SIAM Review 60(2):223–311, 2018. https://doi.org/10.1137/16M1080173
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust Stochastic Approximation Approach to Stochastic Programming, SIAM J. Optim. 19(4):1574–1609, 2009. https://doi.org/10.1137/070704277
M. J. D. Powell, Some global convergence properties of a variable metric algorithm for minimization without exact line searches, in Nonlinear Programming, SIAM-AMS Proc. IX, 1976, pp. 53–72.

13 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XII: Terminal Wealth and Mean-Variance under Partial ObservationTextbook

Motivation

Every portfolio-choice model treated so far in this series assumes the investor knows the exact law governing the market's returns. Real investors do not: the drift of a stock, the regime a market is in, or the probability of an up-move in a simplified binomial model is itself uncertain and must be learned from the very prices being observed. Bäuerle and Rieder's Chapter 6 (Markov Decision Processes with Applications to Finance, Springer, 2011) is the book's synthesis of two threads developed separately earlier: Chapter 5's reduction of a partially observable decision problem to an ordinary one on an enlarged "belief" state space, and Chapter 4's classical solutions of terminal-wealth utility maximization and dynamic mean-variance portfolio choice. Combining them answers a natural question with no simple a priori answer: how does not knowing which market you are in change the qualitatively optimal way to invest, and can the closed-form solutions of the fully-observed theory be recovered, term for term, once the unknown factor is replaced by a belief about it?

Setting

The market has an unobservable factor Y (state space E_Y) driving the vector of relative risks Z ∈ ℝ^d of d risky assets: given Y_n = y, the next return Z_{n+1} has a density q_R(y,\cdot), and Y itself evolves via its own transition density q_Y(y,\cdot), jointly — crucially, this joint law depends only on y, never on wealth or the action taken. An investor observes only the stock prices (equivalently, the return history), never Y itself. Bayes' rule turns this into a filtering problem: the investor's belief ρ_n \in \mathbb P(E_Y) about the current factor is updated one return at a time by an operator Φ(ρ,z) that depends only on the current belief and the newly observed return — a genuine simplification of Chapter 5's general Bayes operator, forced by the market's own structure. The pair (x_n,ρ_n) — observable wealth and current belief — is then an ordinary, fully observed state for an ordinary Markov Decision Model, and every value function and optimal policy of this chapter lives on that enlarged state space.

Formalization targets

The goal, Theorem 6.2.3, solves the dynamic mean-variance problem (MV): minimize the variance of terminal wealth X_N subject to a target expectation \mathbb E[X_N] \ge \mu, under partial observation. It is reached by a Lagrangian embedding into an auxiliary quadratic-loss problem QP(b), solved explicitly in Theorem 6.2.2, whose value function factors as ((xS^0_N/S^0_n)-b)^2 d_n(\rho) for a belief-only sequence (d_n) satisfying the backward recursion (6.7); Lemma 6.2.1 shows this sequence always lies strictly between 0 and 1, which is exactly what makes the final variance formula and Lagrange multiplier well-posed. The remaining milestones develop the parallel terminal-wealth theory of §6.1: the general structure theorem (Theorem 6.1.1), its power- and logarithmic-utility closed forms (Theorems 6.1.2, 6.1.7), and — for the specific binomial market with an unknown up-probability — a likelihood-ratio monotonicity result for the filter update (Lemma 6.1.4) and a comparison between the partially and completely observed optimal investment fractions (Theorem 6.1.5).

Significance

The chapter's organizing insight is that partial observation does not require a new theory: once the belief is added as a state coordinate, every general result already proved for fully observed Markov Decision Models — the Bellman equation, the existence of optimal Markov policies, the Lagrangian embedding technique for mean-variance problems — applies unchanged. What is genuinely new, and genuinely non-trivial, is checking that the reduced model inherits the structural hypotheses (monotonicity, boundedness, positive-definiteness of covariance matrices) those general theorems require, expressed now as conditions on the belief-indexed quantities Φ(ρ,z), d_n(\rho), \ell_n(\rho), C_n(\rho) rather than on the original, unobserved factor. Theorem 6.1.5's comparison result is a genuinely new phenomenon with no fully-observed analogue at all: it quantifies, in the two opposite directions dictated by the sign of the risk-aversion parameter γ, how residual uncertainty about the market itself changes the qualitatively optimal amount to invest — the discrete-time analogue of a continuous-time result in the literature this book cites (Sass and Haussmann 2004).

Difficulty

The recurring difficulty across every result in this mission is that the reduced model's state space E_X \times \mathbb P(E_Y) includes a space of probability measures as one coordinate, and every quantity that must be shown well-defined, monotone, or bounded is a functional on that space, not a function on a concrete Euclidean set. Formalizing the mean-variance recursion (6.7) in particular is a three-way mutual computation — a scalar d_n(\rho), a vector \ell_n(\rho), and a matrix C_n(\rho), each an integral against the same belief-dependent predictive law of the next return, each feeding the next stage's version of all three — where Lemma 6.2.1's strict-inequality bound is not a bookkeeping detail but exactly the fact that keeps C_n(\rho) invertible and the whole construction from breaking down. Theorem 6.2.3 itself is the hardest single step: verifying that the specific constant b^* the Lagrangian method selects makes the mean constraint bind at exact equality, and that the resulting variance is the true constrained minimum (not merely a feasible value), is exactly the non-trivial content a superficial restatement of Theorem 6.2.2 at an unspecified b would silently discard.

Formalization scope

Every value function of this chapter — the terminal-wealth maximization of §6.1, the quadratic loss QP(b) and the mean-variance problem (MV) of §6.2 — is built from one shared history-dependent value-function scaffold, parametrized by its terminal payoff (the utility U, a quadratic loss, or the raw first/second moment), its rate sequence (constant in §6.1, non-stationary in §6.2), and its feasible-action correspondence, rather than four separately re-derived constructions. Optimal fractions in the binomial sub-model (Lemma 6.1.4, Theorem 6.1.5) are characterized as any maximizer of the relevant one-step concave problem rather than through the closed-form solution the book's own proof derives via machinery from a different, unavailable chunk (Lemma 4.2.9) — the comparison and monotonicity results proved here are facts about any such maximizer, not about that specific formula. A formalization that assumed the reduced model's filter update or covariance structure directly, rather than deriving it from the market's own return and factor densities via the Bayes operator Φ, would trivialize every result in this mission; none of the items here take that shortcut.

Selected references

N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
R. Sass and U. G. Haussmann, "Optimizing trading strategies with respect to drawdown in the hidden Markov model," Statistics & Decisions, 2004.
N. Bäuerle and U. Rieder, "Portfolio optimization with unobservable Markov-modulated drift process," Journal of Applied Probability, 2007.
V. Runggaldier, W. Trivellato, and T. Vargiolu, "A Bayesian adaptive control approach to parameter estimation and optimal portfolio selection," in Mathematical Finance, Trends in Mathematics, Birkhäuser, 2002 (the binomial-market source this chapter's §6.1 example specializes).

14 thms2 active usersReviewed

Completed

Combinatorics Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis IV: Discrete Separation for L-Convex SetsTextbook

Motivation

The classical separating hyperplane theorem says that any two disjoint convex sets in $\mathbb R^n$ can be separated by a hyperplane with an arbitrary real normal vector. When the sets in question are not arbitrary convex sets but the integer points of specially structured discrete sets, one can sometimes ask for much more: not merely that a separator exists, but that it can be chosen from a small, structured, dimension-independent family regardless of the size or shape of the sets being separated. Results of this kind — "discrete separation theorems" — are a recurring and often surprising theme in combinatorial optimization, playing the role that the ordinary separation theorem plays in continuous convex analysis, but with genuinely combinatorial content beyond it.

L-convex sets, introduced by Murota as part of the discrete convex analysis framework, are one of the two dual families of well-behaved discrete convex sets studied in the book (the other being M-convex sets, chunk 04 of this series). They are defined by a lattice-closure axiom together with translation invariance, and they correspond one-to-one to integer-valued distance functions satisfying the triangle inequality — objects long familiar from network flow theory and shortest-path duality, even though the L-convexity terminology is not traditionally used there. This mission formalizes the chapter's central results, culminating in Theorem 5.9: two disjoint L-convex sets can always be separated by a vector with entries in $\{-1, 0, 1\}$ , no matter how large or complicated the sets are.

Setting

Let $V$ be a finite ground set. A nonempty set $D \subseteq \mathbb Z^V$ is an L-convex set if it satisfies the sublattice axiom (SBS[Z]) — $p, q \in D \implies p \vee q,\ p \wedge q \in D$ , where $\vee, \wedge$ are componentwise maximum and minimum — and the translation axiom (TRS[Z]) — $p \in D \implies p \pm \mathbf 1 \in D$ , where $\mathbf 1$ is the all-ones vector. A distance function $\gamma : V \times V \to \mathbb R \cup \{+\infty\}$ satisfies $\gamma(v,v) = 0$ for every $v$ ; it satisfies the triangle inequality if $\gamma(v_1,v_2) + \gamma(v_2,v_3) \ge \gamma(v_1,v_3)$ for all $v_1, v_2, v_3$ . The admissible-potential polyhedron of $\gamma$ is

D(\gamma) = \{p \in \mathbb R^V : p(v) - p(u) \le \gamma(u,v)\ (\forall u \ne v)\}.

The convex hull of a discrete set $D \subseteq \mathbb Z^V$ is written $\bar D \subseteq \mathbb R^V$ .

Formalization targets

Goal: Theorem 5.9 (discrete separation for L-convex sets)

If $D_1, D_2 \subseteq \mathbb Z^V$ are disjoint L-convex sets, there exists $x^* \in \{-1,0,1\}^V$ such that

\inf\{\langle p, x^*\rangle : p \in D_1\} - \sup\{\langle p, x^*\rangle : p \in D_2\} \ge 1.

Dropping the $\{-1,0,1\}^V$ restriction and allowing an arbitrary real separator would recover the classical separation theorem for convex sets, which holds regardless of L-convexity and carries no discrete-convexity content; the three-valued restriction is the weakest correct strengthening and is kept in full.

Milestones: Theorems 5.2, 5.5, 5.7

Theorem 5.2: an L-convex set is hole free ( $D = \bar D \cap \mathbb Z^V$ ) — its integer points are exactly the integer points of its own convex hull. Theorem 5.5: $D$ is L-convex if and only if $D = D(\gamma) \cap \mathbb Z^V$ for some integer-valued distance function $\gamma$ satisfying the triangle inequality — L-convex sets and such distance functions are two descriptions of the same object, the discrete analogue of chunk 04's M-convex-set / submodular- function correspondence. Theorem 5.7 (parts (1), (4)): L-convex sets are closed under intersection in the strongest sense — the convex hulls intersect exactly where the sets do, and a nonempty intersection of L-convex sets is again L-convex.

Significance

The result itself. Theorem 5.9 packs two claims into one, as the book itself points out: the separator is forced into $\{-1,0,1\}^V$ (explicit in the statement), and disjoint L-convex sets satisfy "convexity in intersection" — their convex hulls are already disjoint whenever the sets themselves are (implicit, and necessary for the stated inequality to be possible at all). The $\{-1,0,1\}$ structure connects directly to combinatorial duality in network flows: L-convex polyhedra are, without the name, a familiar object there, and a $\{-1,0,1\}$ -separator corresponds to a signed cut or a negative-cost cycle in an associated graph. Theorem 5.5's correspondence is the L-convex mirror of chunk 04's M-convex/submodular correspondence, and the book explicitly flags that the two will be unified into a single conjugacy relationship in a later chapter (Note 5.6) — this mission's formalization of the L-side is a prerequisite for that later unification.

Formalizing it. No matching item exists on the platform (searches for "L-convex", "distance function", and "negative cycle" return only unrelated results — number-theoretic distance estimates, polytope graph metrics, shortest-path graph structures — none matching the combinatorial L-convexity/discrete-separation content here). This mission gives the first formal statement of L-convex sets and their central separation theorem. Notably, Theorem 5.9's own statement — unlike the analogous M-convex Theorem 4.18 — needs none of the distance-function machinery that its proof uses; only the L-convexity axiom itself appears in the goal, making its formal statement comparatively lean even though the underlying mathematics is just as deep.

Difficulty

The natural first attempt at Theorem 5.9 is to try to construct $x^*$ directly from the structure of $D_1, D_2$ — for instance, from a normal vector to a real separating hyperplane, rounded coordinatewise. This does not work: rounding an arbitrary real separator gives no control over its entries, and there is no reason a rounded vector should still separate. The book's actual proof instead represents $D_1, D_2$ via distance functions $\gamma_1, \gamma_2$ (Theorem 5.5), combines them into $\gamma_{12} = \min(\gamma_1, \gamma_2)$ , and extracts the separator from a shortest negative cycle in the associated graph: the vertices of the cycle alternate between the two sets' "tight" arcs, and the alternating $\pm 1$ pattern around the cycle is exactly the $\{-1,0,1\}$ vector $x^*$ — with the cycle's negativity translating directly into the required gap of at least $1$ . Locating the right combinatorial object (a shortest negative cycle, not an arbitrary one) is what pins the separator down to a vector supported on a single alternating cycle rather than an arbitrary $\{-1,0,1\}$ pattern, and is the step a naive rounding or linear-algebra argument has no analogue of.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $D \subseteq \mathbb Z^V$ is a Set (V → ℤ). Distance functions take values in WithTop ℝ; the goal's infimum and supremum are taken in EReal (a complete lattice), since L-convex sets are always infinite (translation invariance along the all-ones direction), so an ℝ-valued supremum/infimum would silently return a junk value on an unbounded set. The conclusion is stated as $\sup_{D_2}\langle p,x^*\rangle + 1 \le \inf_{D_1}\langle p,x^*\rangle$ , an addition-based reformulation of the book's subtraction inequality that avoids EReal's ⊤ - ⊤ ambiguity while remaining equivalent whenever both sides are finite.

A trivializing formalization of the goal would drop the $\{-1,0,1\}^V$ constraint on $x^*$ (recovering the classical, L-convexity-independent separation theorem) or fix a single coordinate pattern rather than asserting existence over the full three-valued family; neither is done here. Theorem 5.5 is stated existentially rather than via the book's named bijection $\Phi, \Psi$ (a documented scope reduction, parallel to chunk 04's treatment of Theorem 4.15), and Theorem 5.7 is drafted with only its two representation-independent clauses (parts (1) and (4); see MODERATION_NOTES.md). Contributions building the distance-function/admissible- potential apparatus needed for Theorem 5.7's remaining clauses, or the L-convex/integrally-convex bridge (Theorem 5.10, needing chunk 03's vocabulary), are welcome.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.

12 thms2 active usersReviewed

Algorithmic Game Theory Convex Optimization Operations Research+1·Captain: mikedeng1

Existence of an Equilibrium for a Competitive Economy II: Equilibrium Exists When Every Consumer Can Supply Productive LaborResearch Paper

Motivation

A competitive equilibrium is a list of production plans, consumption plans and prices at which every firm maximizes profit, every consumer maximizes utility within the budget, and no market has excess demand. Whether such prices exist at all is the consistency question behind general equilibrium theory, the welfare theorems, and applied equilibrium models used in policy analysis. Arrow and Debreu gave the first proof of existence for a model with production, private ownership and general convex preferences (Econometrica 22, 1954), using Debreu's existence theorem for abstract economies (PNAS 38, 1952).

Their Theorem I assumes that every consumer initially holds a positive amount of every commodity (Assumption IV.a). The authors call this "clearly unrealistic" (p. 280): a household does not hold every good, and most households own little beyond their labor. Theorem II, the subject of this mission, removes that assumption. It only asks that every consumer be able to supply some type of labor that is always productive of a commodity everyone desires. This is the version of the existence theorem that allows a wage-earner economy.

Timeline. Wald (1935–36) proved existence for special production models. Nash (1950) proved existence of equilibrium points for finite games, and Debreu (1952) extended it to abstract economies, in which each player's feasible set depends on the others' choices. Arrow and Debreu (1954) proved Theorems I and II. McKenzie's independent existence proof was published the same year (Econometrica 22, 1954).

Setting

There are $l$ commodities, $n$ producers and $m$ consumers; vectors live in $\mathbb R^l$ and $x\leqq y$ is componentwise. Producer $j$ has a production set $Y_j$ . Consumer $i$ has a consumption set $X_i$ , a utility $u_i$ on $X_i$ , an endowment $\zeta_i$ and profit shares $\alpha_{ij}$ . Write $Y=\sum_jY_j$ , $X=\sum_iX_i$ , $\zeta=\sum_i\zeta_i$ , and let $P=\{p\geqq0,\ \sum_hp_h=1\}$ be the price simplex. A competitive equilibrium $(x_1^*,\dots,x_m^*,y_1^*,\dots,y_n^*,p^*)$ satisfies four conditions. Each $y_j^*$ maximizes $p^*\cdot y_j$ on $Y_j$ . Each $x_i^*$ maximizes $u_i$ on $\{x_i\in X_i: p^*\cdot x_i\le p^*\cdot\zeta_i+\sum_j\alpha_{ij}p^*\cdot y_j^*\}$ . The price vector satisfies $p^*\in P$ . Finally $z^*=\sum x_i^*-\sum y_j^*-\zeta\leqq0$ and $p^*\cdot z^*=0$ .

The assumptions of Theorem II are as follows. I: production sets are closed, convex and contain $0$ ; $Y\cap\Omega=\{0\}$ (no output without input); $Y\cap(-Y)=\{0\}$ (no reversible production). II: each $X_i$ is closed, convex and bounded below. III: $u_i$ is continuous, has no satiation point, and satisfies $u_i(tx+(1-t)x')>u_i(x')$ whenever $u_i(x)>u_i(x')$ and $0<t<1$ . IV.b: shares are nonnegative and sum to one for each firm. Two sets of commodities are defined from the data. The set $\mathcal D$ contains the commodities always desired by every consumer: from any $x_i\in X_i$ , adding some positive amount of the commodity stays in $X_i$ and raises $u_i$ . The set $\mathcal P$ contains the types of productive labor: for every $y\in Y$ , (a) $y_h\le0$ , and (b) some $y'\in Y$ satisfies $y'_{h'}\ge y_{h'}$ for all $h'\ne h$ and $y'_{h''}>y_{h''}$ for some $h''\in\mathcal D$ . The remaining assumptions are:

IV′.a: each consumer has some $x_i\in X_i$ with $x_i\leqq\zeta_i$ and $x_{hi}<\zeta_{hi}$ for some $h\in\mathcal P$ ;
V: some $x\in X$ and $y\in Y$ satisfy $x_h<y_h+\zeta_h$ for every $h$ ;
VI: $\mathcal D\ne\emptyset$ ;
VII: $\mathcal P\ne\emptyset$ .

Formalization targets

Goal: Theorem II (§4.5, p. 281)

\text{Assumptions I–III, IV}',\ \text{V–VII}\ \Longrightarrow\ \exists\,(x^*,y^*,p^*)\ \text{satisfying Conditions 1–4.}

Milestones (§5, pp. 282–287)

They follow the paper's proof. Let $\pi=|\mathcal P|$ and $P^\varepsilon=\{p\in P: p_h\ge\varepsilon\ \forall h\in\mathcal P\}$ for $0<\varepsilon\le1/(2\pi)$ . Let $E^\varepsilon$ be the abstract economy in which consumers maximize utility under budget constraints, producers maximize profit, and a market participant chooses $p\in P^\varepsilon$ to maximize $p\cdot z$ . The milestones are:

§5.0 (1). On $P^\varepsilon$ every consumer can spend strictly less than $p\cdot\zeta_i$ .
§5.1.1 (5). Equilibrium points of $E^\varepsilon$ satisfy $x^*-y^*\leqq\zeta'$ for a vector $\zeta'$ independent of $\varepsilon$ .
§5.2.0. The attainable sets relative to $\zeta'$ are bounded.
§5.2.1. The truncated economy $\tilde E^\varepsilon$ has an equilibrium point.
§5.2.2 (3)–(5). An equilibrium point of $\tilde E^\varepsilon$ is one of $E^\varepsilon$ .
§5.3.0 (2). If $p^*_h>\varepsilon$ for all $h\in\mathcal P$ , the point is a competitive equilibrium.
§5.3.2 (1). Limits of equilibrium points as $\varepsilon\to0$ are quasi-equilibria for consumers.
§5.3.4 (3). If the floors bind, some desired commodity has limit price $0$ .
§5.3.4 (6). If the floors bind, limit consumption minimizes expenditure over $X_i$ .
§5.3.5. For some $\varepsilon$ the floor does not bind.

Significance

Theorem II is the existence theorem for a competitive economy in which consumers may own nothing but their labor. It shows that the survival assumption IV.a can be traded for conditions on labor, desirability and the possibility of an overall excess supply. Section 5.3.3 of the paper also isolates the quasi-equilibrium, in which utility maximization under the budget is replaced by cost minimization at a given utility level. That notion is used in later existence and welfare arguments.

The theorem has been proved since 1954; this mission does not reopen it. The work here is the machine-checked proof. The companion mission on Theorem I formalizes the shared model and Debreu's lemma. As of September 2026 neither theorem has a Lean formalization on the platform, and Mathlib contains no general equilibrium theory.

Difficulty

The obvious approach reuses the proof of Theorem I: build the abstract economy of consumers, producers and a price-choosing participant, and apply Debreu's lemma. That fails at the boundary of the price simplex. Without IV.a, a consumer's cheapest point in $X_i$ can cost as much as the endowment at some prices, so the budget correspondence is not continuous there and the lemma does not apply. The paper therefore keeps prices of productive labor at least $\varepsilon$ and must then show that the floor does not bind for some $\varepsilon$ . That is a limit argument as $\varepsilon\to0$ which uses Assumptions V, VI and VII together, and each of the milestones 7–9 is a step of it. Debreu's lemma itself needs a Kakutani-type fixed point theorem for correspondences, which Mathlib does not provide.

Formalization scope

Commodity vectors are Fin l → ℝ. Consumers are indexed by Fin m and producers by Fin n. The inner product is ⬝ᵥ. The paper's $x<y$ is strict in every component and is written componentwise, never as Lean's < on functions. $\mathcal D$ and $\mathcal P$ are computed from the economy, not supplied as parameters. Utilities are total functions, but every assumption on $u_i$ quantifies over $X_i$ only. "Maximizes" is membership plus an inequality against every feasible alternative; no supremum is used. $E$ , $E^\varepsilon$ and $\tilde E^\varepsilon$ are built by one constructor over the players Fin m ⊕ Fin n ⊕ Unit. The vector $\zeta'$ takes the lower bounds $\xi_i$ of Assumption II as an explicit argument. The milestones of §5.3 are stated for the limit of a sequence of equilibrium points, which is how the paper constructs them. Assumption V is dropped from every milestone except §5.3.5 and the goal. With V, the case assumption of §5.3.1 is contradictory and those milestones would hold vacuously.

A trivializing formalization is ruled out as follows. The assumptions are satisfiable with IV.a failing: a sorry-free check covers two goods, one consumer who owns nothing and can only supply labor, and one firm turning labor into the desired good. The goal therefore does not hold vacuously.

Needed infrastructure includes a Kakutani fixed point theorem or Debreu's lemma, compactness of truncated action sets, and sequential compactness arguments in $\mathbb R^l$ . AGT.brouwer_fixed_point is on the platform and can serve as a starting point. The lemma is reusable well beyond this mission. Contributions to any milestone, to the lemma, or to the boundedness results shared with Theorem I are welcome.

Selected references

K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3), 265–290, 1954. https://doi.org/10.2307/1907353
G. Debreu, A Social Equilibrium Existence Theorem, Proceedings of the National Academy of Sciences 38(10), 886–893, 1952. https://doi.org/10.1073/pnas.38.10.886
L. W. McKenzie, On Equilibrium in Graham's Model of World Trade and Other Competitive Systems, Econometrica 22(2), 147–161, 1954. https://doi.org/10.2307/1907352
J. F. Nash, Equilibrium Points in n-Person Games, Proceedings of the National Academy of Sciences 36(1), 48–49, 1950. https://doi.org/10.1073/pnas.36.1.48

16 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes XI: Bayesian Decision Models and Finite-Horizon BanditsTextbook

Motivation

A decision maker who does not know the true parameters of the system they are controlling — the success probability of a slot machine, the drift of an asset, the failure rate of a machine — faces a genuinely different problem from one who knows them: every action taken has two effects, an immediate payoff and a change in what is known. Formalizing this "explore versus exploit" tension precisely is the subject of Bayesian sequential decision theory, whose best-known instance is the multi-armed bandit problem (Robbins, 1952; Gittins and Jones, 1974). Bäuerle and Rieder's treatment (Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5) gives the finite-horizon Bayesian theory its cleanest general form: rather than analyzing each bandit variant from scratch, it builds one reduction — from a Markov Decision Model with an unknown parameter to an ordinary, fully observed Markov Decision Model on an enlarged "information state" — and one structural theorem that turns primitive monotonicity hypotheses on the original ingredients into monotonicity of the optimal policy in the information state. Two classical finite-horizon bandit results (Theorems 5.5.1, 5.5.2) then follow as applications, not separate proofs.

Setting

A Bayesian Model is a Markov Decision Model whose unobservable component is a single, never-changing, unknown parameter $\theta$ , drawn once from a prior distribution $Q_0$ on a parameter space $\Theta$ . Concretely: an observable state space $E_X$ , an action space $A$ , a disturbance space $Z$ with reference measure $\nu$ , a feasible set $D \subseteq E_X \times A$ , a deterministic transition $T^X : E_X \times A \times Z \to E_X$ , a disturbance density $q_Z(x,\theta,a,z)$ , a reward $r(x,\theta,a)$ , a terminal reward $g(x,\theta)$ , and a discount $\beta \in (0,1]$ .

Because $\theta$ is never observed directly, the decision maker's state of knowledge at stage $n$ is the posterior $\mu_n(\cdot \mid \tilde h_n)$ , the conditional law of $\theta$ given the full observable history $\tilde h_n = (x_0,a_0,z_1,\dots,x_n)$ . Bayes' rule updates this posterior one disturbance at a time; unrolling the update gives $\mu_n$ an explicit closed form as a product of likelihoods against the prior (Lemma 5.4.1), and the process $\mu_n(C\mid \cdot)$ , for any fixed event $C$ , is a martingale (Lemma 5.4.2) — it is, after all, a sequence of conditional expectations of the same random variable $\mathbf 1_{\theta \in C}$ against a refining amount of information.

Often the whole posterior is not needed to act optimally: a sufficient statistic $t_n$ compresses $\tilde h_n$ into a value in some space $I$ from which $\mu_n$ can still be recovered, and it is sequential if $t_{n+1}$ updates from only $(x_n, t_n, a_n, z_{n+1})$ . Given a sequential sufficient statistic, the information-based Markov Decision Model replaces the never-observed $\theta$ by the always-computable $t_n$ as the second state coordinate, giving an ordinary Markov Decision Model on $E_X \times I$ whose reward, terminal reward, and transition law are the original ones averaged against the current posterior $\hat\mu(\cdot\mid i)$ .

Formalization targets

\textbf{Theorem 5.4.10.} \quad \begin{aligned} &\text{Given: } D(\cdot) \text{ increasing; } q_Z(\cdot\mid\theta,a) \le_{lr} q_Z(\cdot\mid\theta',a) \text{ for } \theta \le \theta'\text{; } (x,z)\mapsto T^X(x,a,z),\\ &(\theta,x)\mapsto r(\theta,x,a),\ (\theta,x)\mapsto g(\theta,x) \text{ increasing; every increasing } v \in IB_b^+ \text{ has a maximizer in } \Delta.\\ &\text{Then: } IM := \{v \in IB_b^+ \mid v \text{ increasing}\} \text{ and } \Delta \text{ satisfy the Structure Assumption.} \end{aligned}

This is the weakest, most reusable form of the result: it names exactly the primitive hypotheses on the original model's ingredients under which the reduced model's Bellman equation holds and its value function and an optimal policy are monotone in the information state — without fixing which bandit or estimation problem those ingredients come from. Theorems 5.5.1 and 5.5.2 are downstream applications kept as milestones, not additional goals: proving the general theorem subsumes verifying its hypotheses in each concrete case.

Significance

Every one of the classical finite-horizon two-armed-bandit results — "switch to the arm with higher posterior mean once the advantage function is nonnegative," "never abandon a winning arm," "once you commit to the known arm, never leave it" — is, in this book's organization, a one-page corollary of Theorem 5.4.10 plus a routine (if occasionally fiddly) check of its five hypotheses on a two- or four-dimensional concrete state space. The theorem is what makes the qualitative behavior of an optimal bandit policy provable in general, rather than re-derived by induction for each new bandit variant.

Formalizing it also isolates, in one place, exactly which comparison of distributions (likelihood-ratio order, not the weaker stochastic order) makes the reduction go through, and exactly which practically checkable joint-density condition (MTP2) implies it (Lemma 5.4.9) — a genuinely reusable piece of probability theory beyond Markov decision theory.

Difficulty

The obvious first idea — "the information state's order is defined via the likelihood ratio order on posteriors, so just check the transition kernel is stochastically monotone and invoke the general increasing-model theorem of Chapter 2" — hides the actual difficulty: the state space of the reduced model is $E_X \times I$ , and $I$ is itself a space of posterior distributions, so "the transition kernel is monotone" is a statement about how the whole posterior moves when a new observation arrives, not a fact about $E_X$ alone. The crux is showing that the sequential-sufficient-statistic update $\hat\Phi$ is jointly increasing in the current information state and the new disturbance — and this is exactly where Lemma 5.4.9's MTP2 characterization does the real work: MTP2 of the disturbance density in $(z,\theta)$ is what turns "a good disturbance is more likely under a good $\theta$ " into "an increasing information state produces an increasing posterior update," without which the hypotheses on $D$ , $T^X$ , $r$ , $g$ alone would not propagate to the enlarged state space at all.

Formalization scope

The Bayesian Model, its posterior, and the information-based model are formalized as they are introduced in the book: BayesModel bundles the primitive data (disturbance density, prior, reward, discount); Posterior bundles the filter $(\mu_n)$ as data satisfying its defining one-step Bayes update, rather than constructed from a canonical probability space, matching how MDPFinance.POMDP.FilterData (chunk 05a) treats the general Bayes operator; the Structure Assumption, Bellman operators, and bounding-function machinery of Chapter 2 are restated specialized to the stationary form the information-based model needs. " $\Theta, Z \subseteq \mathbb R$ " and " $q_Z$ independent of $x$ " (the "Monotonicity Results" subsection's own standing simplifications) are carried as explicit hypotheses of Lemma 5.4.9 and the goal, not silently dropped. A formalization that merely assumed the reduced model's disturbance kernel monotone, rather than deriving it via Lemma 5.4.9 from the checkable hypothesis on $q_Z$ , would trivialize the theorem; this one keeps hypothesis (ii) exactly as the book states it. The two bandit applications (Theorems 5.5.1, 5.5.2) are formalized as self-contained concrete finite (countable-state, finite-action) Markov Decision Models, since the book itself reduces them to explicit recursions before stating the results — no general measure-theoretic machinery is needed there. Reusable beyond this mission: the likelihood-ratio order and MTP2 definitions (LikelihoodRatioOrder, IsMTP2), applicable to any Bayesian comparison result.

Selected references

N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
H. Robbins, "Some aspects of the sequential design of experiments," Bulletin of the American Mathematical Society, 58(5), 1952, 527-535.
J. C. Gittins and D. M. Jones, "A dynamic allocation index for the sequential design of experiments," in Progress in Statistics, 1974.
A. Müller and D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002 (the book's own reference for the likelihood-ratio order and MTP2 functions, Appendices A.3, B.3).

21 thms2 active usersReviewed

Completed

Combinatorics Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis III: Edmonds's Intersection TheoremTextbook

Motivation

Matroid intersection is one of the founding results of combinatorial optimization: given two matroids on a common ground set, the largest common independent set can be found in polynomial time, and its size equals the minimum of a natural upper bound ranging over all subsets — a min-max theorem in the spirit of König's theorem and Menger's theorem, but for a strictly richer combinatorial structure. Jack Edmonds proved this in 1970, and Jack Edmonds and Rick Giles's subsequent generalization to submodular flows, together with André Frank's discrete separation theorem for submodular and supermodular set functions (1982), placed matroid intersection inside a single unifying framework: submodular function duality. This framework explains, in one stroke, matroid intersection, the base-exchange structure of matroids, and a family of other combinatorial min-max theorems that had previously seemed unrelated.

Murota's Discrete Convex Analysis develops this framework as the theory of M-convex sets: sets of integer vectors satisfying a lattice-exchange axiom that turns out to be exactly equivalent to being the integer points of a base polyhedron of an integer-valued submodular set function. This mission formalizes the chapter's central results: the equivalence of four variant forms of the exchange axiom (Theorem 4.3), the M-convex set / submodular function correspondence (Theorem 4.15), Frank's discrete separation theorem (Theorem 4.17), and Edmonds's intersection theorem itself (Theorem 4.18) — the deepest duality result in the theory of submodular functions and the historical origin of the M-convexity concept that the rest of the book generalizes to real-valued functions.

Setting

Let $V$ be a finite ground set. A set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ with $\rho(\emptyset) = 0$ and $\rho(V) < +\infty$ is submodular (the class $S[\mathbb R]$ ) if

\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y) \qquad (X, Y \subseteq V).

Its base polyhedron and submodular polyhedron are

B(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ (\forall X \subseteq V),\ x(V) = \rho(V)\}, \qquad P(\rho) = \{x \in \mathbb R^V : x(X) \le \rho(X)\ (\forall X \subseteq V)\},

where $x(X) = \sum_{v \in X} x(v)$ ; a supermodular function $\mu$ is one with $-\mu$ submodular. A nonempty set $B \subseteq \mathbb Z^V$ is an M-convex set if it satisfies the exchange axiom (B-EXC[Z]): for $x, y \in B$ and $u$ in the positive support of $x-y$ , there is $v$ in the negative support of $x-y$ with both $x - \chi_u + \chi_v \in B$ and $y + \chi_u - \chi_v \in B$ , where $\chi_u$ is the characteristic vector of $u$ . A polyhedron $P \subseteq \mathbb R^V$ is integral if $P = \operatorname{conv}(P \cap \mathbb Z^V)$ .

Formalization targets

Goal: Theorem 4.18 (Edmonds's intersection theorem)

For submodular set functions $\rho_1, \rho_2 \in S[\mathbb R]$ ,

\max\{x(V) : x \in P(\rho_1) \cap P(\rho_2)\} = \min\{\rho_1(X) + \rho_2(V \setminus X) : X \subseteq V\},

with both sides attained. If $\rho_1, \rho_2$ are integer valued, $P(\rho_1) \cap P(\rho_2)$ is an integral polyhedron and the maximum is attained at an integer point. Dropping the integrality clause and stating only the real max-min equality would leave ordinary LP duality with no discrete content at all; this mission keeps it in the goal at every strength the book proves it.

Milestones: Theorems 4.3, 4.15, 4.17

Theorem 4.3: the exchange axiom (B-EXC[Z]) is equivalent to three variants that impose the exchange condition asymmetrically or only for distinct vectors — groundwork establishing that M-convexity does not depend on which variant is taken as primitive. Theorem 4.15: $B$ is M-convex if and only if $B = B(\rho) \cap \mathbb Z^V$ for some integer-valued submodular $\rho$ — M-convex sets and integer-valued submodular set functions are two descriptions of the same combinatorial object. Theorem 4.17 (Frank): if a submodular $\rho$ dominates a supermodular $\mu$ pointwise, a single vector $x^*$ separates them ( $\rho \ge x^* \ge \mu$ pointwise on every subset), integrally when $\rho, \mu$ are integer valued — derived, in the book, as a direct corollary of the goal theorem.

Significance

The result itself. Edmonds's intersection theorem is the min-max theorem underlying polynomial-time matroid intersection (a matroid's rank function is submodular, so the classical matroid intersection theorem is the special case $\rho_1, \rho_2$ both matroid rank functions), and its generality — arbitrary submodular set functions, not just matroid ranks — is what lets Frank's discrete separation theorem, and through it a wide range of combinatorial duality results in network flows, scheduling, and matroid theory, be derived as corollaries rather than proved from scratch each time. The integrality clause specifically is the fact that makes these duality theorems combinatorial: it guarantees that optimal fractional solutions to the underlying linear program can always be taken integral, without which the connection to discrete optimization would be lost.

Formalizing it. No matching item exists on the platform (searches for "submodular set function", "base polyhedron", "matroid intersection" return no relevant hits; Mathlib's Combinatorics/Matroid/ develops matroid rank functions, a special case, but not general submodular set functions or their polyhedra). This mission gives the first formal statement of the theorem at its natural generality, together with the M-convex-set viewpoint that motivates the rest of the book, and Frank's separation theorem as an explicit worked corollary.

Difficulty

The real-valued half of Theorem 4.18 is ordinary LP duality applied to a cleverly chosen primal program (maximize $\langle p, x\rangle$ over $P(\rho_1) \cap P(\rho_2)$ ) and its dual — routine once the right LP is written down. The integrality half is where the combinatorics enters: an optimal dual solution can always be chosen supported on a chain in each $\rho_i$ 's effective domain (an extremal argument maximizing a strictly convex potential over the optimal dual face), and the incidence matrix of a chain of subsets is totally unimodular — this is the fact, external to ordinary LP theory, that forces an integral optimal solution to exist whenever the data ( $\rho_1, \rho_2$ ) are integral. A proof that stops at real-valued LP duality, however carefully done, misses this step entirely and cannot produce the integrality clause; total unimodularity of a chain's incidence matrix is the one piece of combinatorics doing all the discrete work in an otherwise classical convex-duality argument.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; subsets are Finset V, vectors are V → ℝ/V → ℤ. Submodular functions take values in WithTop ℝ (exactly $\mathbb R \cup \{+\infty\}$ ); supermodular functions in WithBot ℝ; comparisons across the two use an explicit embedding into EReal. The max/min in the goal are stated via IsGreatest/IsLeast sharing a common EReal witness, so that "both sides attained, at the same value" — not merely "sup equals inf" — is what the Lean statement asserts, which is essential since the integrality clause's whole content is about which point attains the maximum.

A trivializing formalization of the goal would drop the integrality clause (leaving unqualified LP duality) or replace IsGreatest/IsLeast with a bare supremum/infimum equality (losing the "is attained" content the second half of the theorem needs); both are avoided. Theorem 4.15 is stated as the existential "iff" (some integer submodular $\rho$ realizes $B$ ) rather than reifying the book's own named bijection $\Phi, \Psi$ explicitly — a deliberate, documented scope reduction of that one milestone (see MODERATION_NOTES.md), not of the goal. Contributions building the explicit $\Phi$ map, the Lovász extension (needed for Theorem 4.16, not drafted here), or M-convex-set infrastructure reusable by chunks 06–07 (M-convex functions, which build on this chapter's vocabulary) are welcome.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
J. Edmonds, "Submodular functions, matroids, and certain polyhedra," in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, pp. 69–87.
A. Frank, "An algorithm for submodular functions on graphs," Annals of Discrete Mathematics, 16, 1982, pp. 97–120.

20 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Markov Decision Processes X: Partially Observable Markov Decision Processes and FilteringTextbook

Motivation

Every model in Chapters 2-4 assumed the controller sees the whole state before acting. Real control problems rarely offer that: a machine's true wear level, a customer's private valuation, a hidden regime driving asset returns — these are exactly the situations a decision-maker must act on despite never observing them directly, learning about them only through their effect on what is observed. This is the subject of Partially Observable Markov Decision Processes (POMDPs), introduced independently in operations research (K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, 1965) and studied extensively since as the right model for sequential decisions under hidden state. The central difficulty such a process raises is structural, not just computational: the state includes a component the controller never sees, so the very theory built in Chapter 2 — which assumes the controller's policies can depend on the full current state — does not apply. Bäuerle and Rieder's Chapter 5 resolves this by an idea with a long pedigree in stochastic control (Bayesian filtering, going back to R. E. Kalman and R. S. Bucy's filtering theory, and D. Blackwell's 1965 discounted-dynamic-programming treatment of the "state of information"): replace the unobservable state by the controller's own belief about it — a probability distribution, updated at every step by Bayes' rule — and show the resulting belief-state process is once again an ordinary, fully observed Markov Decision Model.

Setting

A Partially Observable Markov Decision Model (Definition 5.1.1) has data $(E_X\times E_Y, A, D, Q, Q_0, r, g, \beta)$ : state $(x,y)\in E_X\times E_Y$ with $x$ observable and $y$ unobservable; feasible actions $D(x)$ depending only on $x$ ; a stochastic kernel $Q$ giving the joint law of the next state; initial law $Q_0$ of $Y_0$ ; rewards $r,g$ ; discount $\beta$ . A policy $\pi=(f_0,\dots,f_{N-1})\in\Pi_N$ (Definition 5.1.3) is a sequence of decision rules $f_n:H_n\to A$ , each depending only on the observable history $H_n=(x_0,a_0,\dots,x_n)$ — never on any $y_k$ . The objective

J_N^\pi(x) := \int \mathbb{E}_{xy}^\pi\Big[\sum_{n=0}^{N-1}\beta^n r(X_n,Y_n,A_n) + \beta^N g(X_N,Y_N)\Big] Q_0(dy), \qquad J_N(x):=\sup_{\pi\in\Pi_N} J_N^\pi(x)

(Equation (5.2)) carries an extra expectation over the unknown $Y_0$ that Chapter 2's objective never had.

Assuming $Q$ has a density $q$ against reference measures, the Bayes operator $\Phi$ and the filter recursion $\mu_0:=Q_0$ , $\mu_{n+1}(\cdot\mid h_n,a_n,x_{n+1}):=\Phi(x_n,\mu_n(\cdot\mid h_n),a_n,x_{n+1})$ (Equations (5.3)-(5.4)) compute the posterior law of $Y_n$ given everything observed, purely from the observable history. Theorem 5.2.1 confirms $\mu_n$ is genuinely this conditional law. The filtered Markov Decision Model (Definition 5.3.1) then treats $(x,\mu_n)\in E:=E_X\times\mathbb{P}(E_Y)$ as an ordinary, fully-observed state, with its own kernel $Q'$ (built from $\Phi$ and the marginal $Q^X$ ), reward $r'(x,\rho,a):=\int r(x,y,a)\rho (dy)$ , and terminal reward $g'(x,\rho):=\int g(x,y)\rho(dy)$ .

Formalization targets

Goal — Theorem 5.3.3

J_0'(x,\rho) = g'(x,\rho), \qquad J_n'(x,\rho) = \sup_{a\in D(x)}\Big[r'(x,\rho,a) + \beta\int J_{n-1}'(x',\rho')\,Q'(d(x',\rho')\mid x,\rho,a)\Big] \quad (1\le n\le N),

under the Structure Assumption of Theorem 2.3.8; and if $f_n'$ maximizes $J_{n-1}'$ for each $n$ , then $f_n^*(h_n):=f_{N-n}'(x_n,\mu_n(\cdot\mid h_n))$ defines a policy optimal for the original $N$ -stage POMDP. This is where the reduction pays off: an ordinary Bellman equation, of exactly the form Chapter 2 already solves, for a problem that had no Bellman equation at all in its original, partially-observed form.

Milestones

Lemma 5.2.2 (the filter-recursion identity, the technical engine behind everything that follows), Theorem 5.2.1 (the filter is truly the conditional law — without this, $\mu_n$ would be merely a formula, not a meaningful belief), and Theorem 5.3.2 (the value of the filtered model exactly equals the value of the original POMDP, policy for policy — without this, solving the filtered model would solve a different problem).

Significance

Theorem 5.3.3 is the standard justification, made precise, for the single most common technique in applied sequential decision-making under uncertainty: replace an unknown parameter or hidden state by a running Bayesian estimate, and optimize as if that estimate were the true state. This technique underlies applications from inventory control with unknown demand to adaptive clinical trial design, and Chapter 5's own closing application (two-armed Bernoulli bandits, taken up in chunk 05b) is a direct instance. The reduction also has real content beyond convenience: it shows the value is unchanged (Theorem 5.3.2), not merely that a good heuristic policy exists — the filtered model's optimum is the true POMDP optimum, not an approximation to it.

No result of this chapter has a machine-checked proof on Prove2Me at the time of writing, and no substrate exists for POMDPs, filtering, or Bayes-operator constructions on the platform. Formalizing this mission means building, from Mathlib's general kernel and probability-measure infrastructure, the first POMDP/filtering vocabulary on the platform: a policy class restricted to observable histories, a recursively-computable posterior, and the value-equality between a partially and a fully observed reformulation.

Difficulty

The obstacle is not any single hard inequality but a representational one: an admissible policy for the original problem is a function of a growing observable history, not of a fixed-size state, so the value function $J_N^\pi$ cannot be written as a simple recursion over a Markov chain the way every earlier chapter's could. The chapter's insight is that the belief $\mu_n$ — even though it is a probability-measure-valued object, not a point in a fixed Euclidean space — is itself Markov: $\mu_{n+1}$ depends on the observable history only through $(x_n,\mu_n)$ , never on more of the past. Recognizing this, and giving $\mathbb{P}(E_Y)$ the right measurable structure to serve as a genuine Borel state space, is what makes Definition 5.3.1's reformulation a legitimate Markov Decision Model rather than an informal analogy. A formalization that let $\mu_n$ 's type be an unstructured "distribution object" with no Borel structure, or that quietly assumed the value functions of the filtered model already satisfy the Bellman equation, would miss this content entirely.

Formalization scope

$E_X,E_Y,A$ are abstract measurable spaces; the transition kernel $Q$ is a genuine MeasureTheory.Kernel, not assumed to arise from an i.i.d.-noise-driven transition function (the form every earlier finance chapter's market used) — the chapter's own examples (Hidden Markov Models, Bayesian models) do not have that special form in general. Observable histories are represented as (junk-padded) sequences $\mathbb{N}\to E_X$ , $\mathbb{N}\to A$ rather than dependent finite tuples, with a decision rule's dependence on only the first $n{+}1$ / $n$ coordinates stated as an explicit locality condition; this avoids Fin-indexed-tuple bookkeeping while remaining exactly equivalent to the book's own $H_n\to A$ typing. The belief state $\rho$ is MeasureTheory.ProbabilityMeasure E_Y, giving $E_X\times\mathbb{P}(E_Y)$ a genuine measurable structure via its standard weak-topology Borel σ-algebra — the formalization scope this chunk's own pitfall demands, ruling out an ad hoc encoding of "the space of distributions." The Bayes operator $\Phi$ and the filtered kernel $Q'$ are carried as data (functions landing genuinely in ProbabilityMeasure/Kernel types) characterized by their defining ratio-of-integrals or pushforward formulas, rather than constructed by normalizing a raw measure inline — proving that normalization is a routine Fubini calculation the book itself does not spell out, and would be proof content misplaced in a definition. Theorem 5.2.1's conditional-probability statement is formalized via the book's own Equation (5.5) test-function identity rather than Mathlib's conditional-expectation-with-respect-to-a-sub-σ-algebra machinery, since the two are equivalent by the standard characterization of conditional expectation and the test-function form is what the book's own proofs actually use. The Structure Assumption of Theorem 2.3.8 is restated locally (existential value-function and decision-rule classes with its three defining clauses), per this project's rule against importing another chunk's copy of shared machinery. Reusable beyond this mission: the kernel-based expectation recursion (Ex/Vpi) is natural substrate for any later mission needing a Markov Decision Process driven by a genuinely abstract stochastic kernel rather than an i.i.d.-noise transition function. Contributions completing any milestone's sorry, or the goal's, are welcome.

Selected references

K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, Journal of Mathematical Analysis and Applications 10(1), 1965, https://doi.org/10.1016/0022-247X(65)90154-X
D. Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1), 1965, https://doi.org/10.1214/aoms/1177700285
R. E. Kalman, R. S. Bucy, New Results in Linear Filtering and Prediction Theory, Journal of Basic Engineering 83(1), 1961, https://doi.org/10.1115/1.3658902
N. Bäuerle, U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011, https://doi.org/10.1007/978-3-642-18324-9, Chapter 5, §§5.1-5.3

9 thms2 active usersReviewed

Completed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

Globally Convergent Type-I Anderson Acceleration for Nonsmooth Fixed-Point Iterations: The Stabilized Type-I Anderson Acceleration Converges to a Fixed Point of Every Nonexpansive MapResearch Paper

Motivation

Many first-order methods in optimization are fixed-point iterations $x^{k+1}=f(x^k)$ of a nonexpansive map $f:\mathbb R^n\to\mathbb R^n$ : proximal gradient descent, projected gradient descent, alternating projections, ISTA and Douglas–Rachford splitting (with the conic solver SCS as an instance) all have this form (Zhang, O'Donoghue, Boyd 2020, §4.2). The averaged (Krasnosel'skiĭ–Mann) iteration $x^{k+1}=(1-\alpha)x^k+\alpha f(x^k)$ converges to a fixed point whenever one exists, but it is often slow in its terminal phase. Anderson acceleration (AA) combines the last few iterates through a quasi-Newton update of an approximate Jacobian; it is used for electronic-structure computations and, in the stabilized form studied here, in the solver SCS 2.1. Its type-I variant (AA-I) is often faster in practice than the more studied type-II variant, but it can be numerically unstable, and no global convergence guarantee existed for it on nonsmooth problems.

Timeline (as recounted in the paper's related-work section):

1965. Anderson introduces the method for nonlinear integral equations (J. ACM 12).
1978. Gay and Schnabel prove local Q-superlinear convergence of a full-memory AA-I-type method (Broyden with projected updates), assuming $f$ continuously differentiable near the solution.
2009. Fang and Saad connect AA with multisecant Broyden methods and distinguish the two types (Numer. Linear Algebra Appl. 16).
2011. Walker and Ni show the essential equivalence of full-memory AA with GMRES for affine $f$ (SIAM J. Numer. Anal. 49); Rohwedder and Schneider prove local Q-linear convergence of limited-memory AA-II for differentiable $f$ .
2015. Toth and Kelley give local linear convergence of AA-II for contractive $f$ (SIAM J. Numer. Anal. 53).
2020. Zhang, O'Donoghue and Boyd introduce a stabilized AA-I method (Powell-type regularization, restart checking, safeguarding) and prove global convergence for every nonexpansive map with a fixed point, without differentiability (SIAM J. Optim. 30(4), 3170–3197; longer version arXiv:1808.03971).

Setting

Let $f:\mathbb R^n\to\mathbb R^n$ satisfy $\|f(x)-f(y)\|_2\le\|x-y\|_2$ for all $x,y$ (the Euclidean norm), and assume the solution set $X=\{x^\star\mid x^\star=f(x^\star)\}$ is nonempty. The residual is $g(x)=x-f(x)$ , $g_k=g(x^k)$ , and the averaged operator is $f_\alpha(x)=(1-\alpha)x+\alpha f(x)$ .

Powell's weight. For $\bar\theta\in(0,1)$ , $\phi_{\bar\theta}(\eta)=1$ if $|\eta|\ge\bar\theta$ and $\phi_{\bar\theta}(\eta)=(1-\operatorname{sign}(\eta)\bar\theta)/(1-\eta)$ otherwise, with $\operatorname{sign}(0)=1$ .

Window matrices. For vectors $s_0,\dots,s_{m_k-1}$ and $y_0,\dots,y_{m_k-1}$ , let $\hat s_i$ be their unnormalized Gram–Schmidt orthogonalization (3.2), $B^0=I$ , and

B^{i+1}=B^i+\frac{(\tilde y_i-B^is_i)\hat s_i^T}{\hat s_i^Ts_i},\qquad \tilde y_i=\theta^iy_i+(1-\theta^i)B^is_i,\qquad \theta^i=\phi_{\bar\theta}\Bigl(\frac{\hat s_i^T(B^i)^{-1}y_i}{\|\hat s_i\|_2^2}\Bigr).

The matrix norm $\|\cdot\|_2$ is the induced $\ell_2$ operator norm.

Algorithm 3.1 (AA-I-S-m). With parameters $\bar\theta,\tau,\alpha\in(0,1)$ , $D,\epsilon>0$ and max-memory $m\ge1$ : start from $H_0=I$ , $m_0=0$ , $n_{AA}=0$ , $\bar U=\|g_0\|_2$ and $x^1=\tilde x^1=f_\alpha(x^0)$ . At iteration $k\ge1$ , set $s_{k-1}=\tilde x^k-x^{k-1}$ and $y_{k-1}=g(\tilde x^k)-g(x^{k-1})$ , orthogonalize $s_{k-1}$ against the current window, and restart the window (memory back to $1$ , $H_{k-1}$ replaced by $I$ ) if the memory would exceed $m$ or $\|\hat s_{k-1}\|_2<\tau\|s_{k-1}\|_2$ . Then apply one Powell-regularized rank-one update to obtain $H_k$ and the trial point $\tilde x^{k+1}=x^k-H_kg_k$ . The trial point is accepted if $\|g_k\|_2\le D\bar U(n_{AA}+1)^{-(1+\epsilon)}$ (and $n_{AA}$ increases); otherwise $x^{k+1}=f_\alpha(x^k)$ .

Formalization targets

Goal: Theorem 4.1

\text{for every run of Algorithm 3.1:}\qquad \lim_{k\to\infty}x^k=x^\star\quad\text{for some } x^\star=f(x^\star).

The only hypotheses are nonexpansiveness of $f$ , $X\ne\emptyset$ and the parameter ranges. The limit is not specified: it depends on $x^0$ and the parameters.

Milestones

Lemma 3.2. Well-defined updates give $|\det B^{m_k}|\ge\bar\theta^{m_k}>0$ .
Lemma 3.3. If $\|y_i\|_2\le2\|s_i\|_2$ , $\|\hat s_i\|_2\ge\tau\|s_i\|_2$ and $m_k\le m$ , then $\|B^{m_k}\|_2\le3((1+\bar\theta+\tau)/\tau)^m-2$ .
Corollary 3.4. $\|H_k\|_2\le(3((1+\bar\theta+\tau)/\tau)^m-2)^{n-1}/\bar\theta^m$ (3.8).
Corollary 3.5. Along the algorithm, unless a solution is hit, (3.8) holds and $\mathrm{cond}(H_k)\le(3((1+\bar\theta+\tau)/\tau)^m-2)^n/\bar\theta^m$ .
Eq. (4.3). $\|x^k-y\|_2\le\|x^0-y\|_2+CD\bar U\sum_{i\ge0}(i+1)^{-(1+\epsilon)}$ for every $y\in X$ .
Eq. (4.6). $\lim_k\|g_k\|_2=0$ .
Eq. (4.7). $\|x^{k+1}-y\|_2^2\le\|x^k-y\|_2^2+\epsilon_k$ with $\epsilon_k\ge0$ summable.
§4.1, Step 2. $\|x^k-y\|_2$ converges for every $y\in X$ .

Significance

The theorem places a quasi-Newton acceleration scheme under the same hypotheses as the plain averaged iteration: nonexpansiveness and existence of a fixed point. It therefore applies at once to the nonexpansive examples of §4.2 of the paper (proximal gradient, projected gradient, alternating projections, ISTA, Douglas–Rachford splitting and SCS), with no smoothness, strong convexity or local assumption. The matrix bounds of Lemma 3.3 and Corollaries 3.4–3.5 are also of independent use: they give explicit, iteration-independent control of the approximate inverse Jacobians of a limited-memory type-I method, an assumption that other globalization frameworks (for example SuperMann) have to impose.

The result is proved in the paper; to our knowledge none of it is machine-checked. Mathlib has neither the Krasnosel'skiĭ–Mann iteration, nor Fejér monotonicity, nor any Anderson-type method. A formalization provides these pieces, checks the index bookkeeping of the restart and safeguard steps, and makes explicit the one place where the printed algorithm and the analysis disagree (line 9 at a window start; see below).

Difficulty

The accelerated step $\tilde x^{k+1}=x^k-H_kg_k$ need not decrease the distance to the solution set, so the Fejér argument for averaged iterations does not apply to it directly. The naive fix, bounding $\|H_kg_k\|_2$ , requires a bound on $\|H_k\|_2$ that holds uniformly along the run; without the Powell regularization $B_k$ can be singular, and without the restart rule $\|B_k\|_2$ can grow without bound as the window becomes nearly linearly dependent. The determinant and norm bounds of Lemmas 3.2–3.3 have to be established for arbitrary windows and then connected to the run of the algorithm, where the window, its orthogonalization and the matrices are defined by an intertwined recursion with resets. The safeguard then turns the uniform bound into a summable perturbation of a Fejér-monotone sequence, and the final step needs an Opial-type argument to pass from convergence of distances to convergence of the iterates.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so all vector norms are Euclidean; matrices are continuous linear maps with the operator norm; $u\hat s^T$ is rankOne ℝ u ŝ; $\det$ is LinearMap.det; inverses are Ring.inverse (zero on singular maps, excluded by Lemma 3.2). The orthogonalization (3.2) is InnerProductSpace.gramSchmidt. Nonexpansive is LipschitzWith 1 f. The algorithm is the predicate IsAAISRun, a deterministic recursion: every run is determined by $f$ , the parameters and $x^0$ , and a sorry-free check that runs exist (for $f=\mathrm{id}$ ) was built locally. The reset of $H_{k-1}$ in line 8 is local to its iteration. $\mathrm{sign}(0)=1$ is encoded explicitly. Constants are the paper's explicit expressions; no milestone replaces them with an existential constant.

Line 9. The paper prints $\tilde y_{k-1}=\theta_{k-1}y_{k-1}-(1-\theta_{k-1})g_{k-1}$ , derived from (3.3) through $B_{k-1}s_{k-1}=-g_{k-1}$ , which fails when the window starts afresh ( $m_k=1$ ). The mission uses (3.3) there: $\tilde y_{k-1}=\theta_{k-1}y_{k-1}+(1-\theta_{k-1})s_{k-1}$ when $m_k=1$ , and the printed formula when $m_k\ge2$ .

Milestones of §4.1 and Corollary 3.5 carry the hypothesis $f(x^k)\ne x^k$ for all $k$ , as the paper does ("we temporarily assume for simplicity that a solution to (1.1) is not found in finite steps"); the goal does not. A goal proved from an unsatisfiable run predicate, or one that assumes a bound on $\|H_k\|_2$ , contractivity of $f$ , or that the accelerated step is never taken, is not this theorem. Division by zero in Lean can only occur once a fixed point has been reached, after which all later iterates coincide.

Useful reusable infrastructure includes the Krasnosel'skiĭ–Mann inequality $\|f_\alpha(x)-y\|_2^2\le\|x-y\|_2^2-\alpha(1-\alpha)\|g(x)\|_2^2$ , quasi-Fejér monotone sequences and their convergence, and determinant and norm identities for rank-one updates (the matrix determinant lemma and Sherman–Morrison). Proofs of the window lemmas, of the run invariants (the window matrices coincide with the algorithm's $H_k^{-1}$ ) and of the convergence steps are all welcome.

Selected references

J. Zhang, B. O'Donoghue, S. Boyd, Globally Convergent Type-I Anderson Acceleration for Nonsmooth Fixed-Point Iterations, SIAM J. Optim. 30(4), 3170–3197, 2020. https://doi.org/10.1137/18M1232772
J. Zhang, B. O'Donoghue, S. Boyd, longer version, 2018. https://arxiv.org/abs/1808.03971
D. M. Gay, R. B. Schnabel, Solving systems of nonlinear equations by Broyden's method with projected updates, in Nonlinear Programming 3, Academic Press, 245–281, 1978 (reference [20] of the paper). https://doi.org/10.1137/18M1232772
D. G. Anderson, Iterative procedures for nonlinear integral equations, J. ACM 12(4), 547–560, 1965. https://doi.org/10.1145/321296.321305
H. Fang, Y. Saad, Two classes of multisecant methods for nonlinear acceleration, Numer. Linear Algebra Appl. 16(3), 197–221, 2009. https://doi.org/10.1002/nla.617
H. F. Walker, P. Ni, Anderson acceleration for fixed-point iterations, SIAM J. Numer. Anal. 49(4), 1715–1735, 2011. https://doi.org/10.1137/10078356X
A. Toth, C. T. Kelley, Convergence analysis for Anderson acceleration, SIAM J. Numer. Anal. 53(2), 805–819, 2015. https://doi.org/10.1137/130919398
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7

12 thms2 active usersReviewed