All missions

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

1. Eq. (5.9): $\Gamma$ is $C^\infty$ on $\mathbb{R}^n \times (0,\infty)$ and $\Gamma_t = \Delta\Gamma$.
2. 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$.
3. 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}$.
4. Theorem 5.9: $\|u(t)\|_{H^s} \le \|f\|_{H^s}$ for all $s \in \mathbb{R}$, $t \ge 0$.
5. 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}$.
6. 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}$.
7. 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'}}$.
8. 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

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

1. §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)$.
2. §3 (7)–(11): the transformed dynamics.
3. 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$.
4. Proposition 11: the same LMI with $aD_{\mathbf r}$ added, uniformly in $|a|\le C_0$.
5. Proposition 12 (corrected): the ISS estimate (17) in the time $s$.
6. 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

Motivation

Duality is the organizing principle of convex optimization: a minimization problem's optimal value equals a maximization problem's optimal value, and this coincidence, rather than being a lucky accident, follows from a separating-hyperplane argument that applies whenever the two problems' feasible regions are shaped compatibly enough. Werner Fenchel formalized this in the 1950s for pairs of convex and concave functions related by the Legendre-Fenchel transform, and the resulting Fenchel duality theorem specializes, for linear objectives over polyhedral feasible regions, to linear programming duality — the fact, central to the entire theory of combinatorial optimization, that a linear program's optimal value can always be certified from above and below by a pair of primal and dual feasible solutions. Murota's Discrete Convex Analysis (SIAM, 2003) collects this classical machinery, together with the integrality theory that lets it produce combinatorial (integer-valued) certificates rather than merely real ones, as the technical foundation the rest of the book builds its discrete theory on top of.

Setting

For $f : \mathbb R^n \to \mathbb R \cup \{+\infty\}$, the epigraph is $\operatorname{epi} f = \{(x,Y) : Y \ge f(x)\}$, and $f$ is convex iff $\operatorname{epi} f$ is a convex set; $f$ is proper if additionally its effective domain $\operatorname{dom} f = \{x : f(x) < +\infty\}$ is nonempty, and closed if $\operatorname{epi} f$ is topologically closed. A function $h : \mathbb R^n \to \mathbb R \cup \{-\infty\}$ is concave, proper, closed analogously via its hypograph. The convex conjugate is $f^\bullet(p) = \sup_x\{\langle p,x\rangle - f(x)\}$, and the concave conjugate $h^\circ(p) = \inf_x\{\langle p,x\rangle - h(x)\}$. The relative interior $\operatorname{ri} S$ of a set $S$ is the interior of $S$ relative to its affine hull. A function is polyhedral if its epigraph (or hypograph) is a finite intersection of half-spaces. Given an $m \times n$ matrix $A$, $b \in \mathbb R^m$, $c \in \mathbb R^n$, the primal and dual linear programs are $\min\{c^\top x : Ax=b,\ x\ge0\}$ and $\max\{b^\top y : A^\top y \le c\}$, with feasible regions $P$, $D$. A matrix is totally unimodular if every square submatrix has determinant $0$, $1$, or $-1$. A discrete set $S \subseteq \mathbb Z^n$ is hole free if $S = \bar S \cap \mathbb Z^n$, where $\bar S$ is the convex hull of $S$'s real embedding; the discrete Minkowski sum is $S_1+S_2 = \{x_1+x_2 : x_1\in S_1, x_2\in S_2\}$.

Formalization targets

Goal (Theorem 3.6, Fenchel duality). For proper convex $f$ and proper concave $h$ satisfying at least one of four alternative conditions — a relative-interior condition on $\operatorname{dom} f \cap \operatorname{dom} h$, a polyhedrality condition on the same, or the analogous pair of conditions on $\operatorname{dom} f^\bullet \cap \operatorname{dom} h^\circ$ together with closedness of $f$, $h$ —

$$\inf_x\{f(x)-h(x)\} = \sup_p\{h^\circ(p)-f^\bullet(p)\},$$

with the extremum on the appropriate side attained whenever the common value is finite. This is the mission's capstone: the four alternative hypotheses make it the most broadly applicable statement of the four convex-duality results in this mission, each of the other three being either a special case in substance (Theorem 3.5, separation, which 3.6 is proved from) or a literal specialization to linear data (Theorem 3.10, LP duality).

Supporting milestones. Theorem 3.2 (biconjugation: $f^\bullet$ is always closed proper convex, and $g^{\bullet\bullet}=g$ for closed proper convex $g$); Theorem 3.5 (the separation theorem for convex/concave functions, under two of Theorem 3.6's four hypotheses); Theorem 3.9 (the Farkas lemma, equality form); Theorem 3.10 (LP duality: weak duality, strong duality with attainment, and complementary slackness); Theorem 3.13 (total unimodularity of the constraint matrix guarantees an integral optimal solution whenever an optimal solution exists); Proposition 3.14 (an explicit potential function certifying a minimum-weight bipartite perfect matching, via the totally unimodular incidence-matrix LP); and Proposition 3.16 (for a translation-invariant family of hole-free discrete sets, the property that discrete disjointness implies closure disjointness is equivalent to the discrete Minkowski sum matching the integer points of the closures' Minkowski sum).

Significance

Fenchel duality is the single result from which the separation theorem, LP duality, and (via the totally-unimodular incidence matrix of a bipartite graph) the combinatorial duality underlying weighted bipartite matching all descend, in one unbroken chain of specialization; formalizing this chain in one mission exhibits that structure directly, rather than treating each result as an independent fact. Proposition 3.16 plays a different role: it is the chapter's warning that naive discrete analogues of convexity (hole-freeness) do not automatically inherit convexity's good closure properties under Minkowski sums, which is exactly the gap the book's later M-convexity and L-convexity machinery is built to close — this mission's Proposition 3.16 is therefore the motivating negative result for the rest of the book's positive theory, not a loose end. So far as a platform search shows, no existing formalization matches this chunk's specific combination of extended-valued (possibly $\pm\infty$) functions, the four-alternative Fenchel duality hypothesis, or the bipartite-matching-via-total-unimodularity argument; the one related platform result (VectorSpaceOpt.fenchel_duality, from Luenberger) is for real-valued functions on general normed spaces under a single relative-interior-and-solidness hypothesis, a different generality from the extended-valued, four-hypothesis statement here.

Difficulty

The naive approach to Theorem 3.6 tries to prove the duality gap is zero directly from the definitions of the two conjugates, which only gives the easy inequality $\inf \ge \sup$ (a one-line computation, shown in the book's own proof in three lines); the substantive content is the reverse inequality, and it genuinely fails without a constraint-qualification hypothesis like (a1)-(b2) — Example 3.8 in the book exhibits a convex/concave pair with $\inf = 0 \ne -1 = \sup$ when none of the four conditions hold. The book's actual route reduces Theorem 3.6 to the separation theorem (Theorem 3.5) applied to $f$ shifted down by the (assumed finite) infimum, which produces the separating affine function directly; this is why Theorem 3.5, although logically a special case in spirit, earns its own milestone rather than being subsumed silently.

Formalization scope

All convex and concave functions are represented uniformly as (V → ℝ) → EReal-valued (Fintype V), rather than mixing WithTop ℝ for convex and WithBot ℝ for concave functions, so that Theorem 3.2's biconjugate — whose properness is a conclusion, not an assumption — has a well-defined codomain without extra casts. Convexity is defined via the epigraph being a convex subset of the ordinary real vector space $(V\to\mathbb R)\times\mathbb R$ (Mathlib's Convex ℝ), following the book's own equivalent characterization, rather than unfolding the direct inequality definition, which would require a extended-arithmetic scalar-multiplication convention (0\cdot(+\infty)=0) that Mathlib does not provide for EReal. The relative interior is defined directly from the book's own metric-ball-intersected-with-affine-hull description, since Mathlib has no relative-interior primitive at the pinned revision. Polyhedra are finite intersections of explicit half-spaces. A bipartite perfect matching is represented as a bijection between the two vertex sides restricted to the edge set — a faithful, not narrower, representation since every perfect matching between equal-size parts arises this way. The formalization does not trivialize: Theorem 3.6's four hypotheses are carried in full (not reduced to the easiest single case), and no result is stated only for finite-valued (never $\pm\infty$) functions, which would discard the entire point of the extended-value convex-analysis framework this chapter sets up for the rest of the book. Infrastructure needed beyond Mathlib's Convex, Matrix, and EReal API: all epigraph/hypograph, conjugate, relative-interior, and polyhedral apparatus is defined fresh in DiscreteConvex.IntegralConvexityB; a contribution proving any of the seven milestones independently, or supplying Mathlib-quality relative-interior lemmas, would be a natural entry point.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 3.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

Motivation

Real investors do not merely accumulate wealth for a single terminal payoff; they consume along the way, and the market they invest in is rarely a single fixed statistical regime for years at a time — bull and bear markets, business cycles, and volatility regimes shift the distribution of returns. Bäuerle and Rieder's §4.3 extends the terminal-wealth theory of chunk 04a by adding a consumption choice at every stage (the Ramsey/Merton consumption-investment problem), and §4.4 extends it again by letting the return distribution itself depend on a hidden, Markov-modulated environment state. Both extensions are shown to be genuine instances of the same abstract finite-horizon Markov Decision Process machinery from Chapter 2 — the joint consumption-investment choice and the extra regime coordinate change the state and action spaces, but not the proof strategy, which is exactly the point.

Setting

The consumption-investment problem: state $E := \mathrm{dom}\,U_p$ (wealth), action $\mathbb{R}_{\ge0}\times\mathbb{R}^d$ (consumption $c$, amounts $a$ invested), transition $T_n(x,c,a,z) = (1+i_{n+1})(x-c+a\cdot z)$, reward $r_n(x,c,a) := U_c(c)$, terminal reward $g_N := U_p$. Value functions $V_n(x) := \sup_\pi \mathbb{E}^\pi_{n,x}[\sum_{k=n}^{N-1} U_c(c_k(X_k)) + U_p(X_N)]$. The one-period sub-problem: $D(x) := \{(c,a) : 0\le c\le x,\ (1+i)(x-c+a\cdot R)\in\mathrm{dom}\,U_p \text{ a.s.}\}$, $u(x,c,a) := U_c(c) + \mathbb{E}[U_p((1+i)(x-c+a\cdot R))]$, $v(x) := \sup_{(c,a)\in D(x)} u(x,c,a)$.

The regime-switching extension (§4.4): an environment process $(Y_n)$, a finite-state Markov chain with transition probabilities $p_{jk}$, modulates the risky-asset return law: given $Y_n=j$, the next relative risk $R_{n+1}$ has law $Q_j$, and $(R_{n+1},Y_{n+1})$ has joint law $Q_j(dz)p_{jk}$ given $Y_n=j$, $Y_{n+1}=k$. The augmented state is $(x,j) \in [0,\infty)\times E_Y$; value functions $J_n(x,j)$ are defined analogously, with the recursion incorporating a finite sum over the next regime.

Formalization targets

Goal — Theorem 4.3.3

$$V_N = U_p, \qquad V_n(x) = \sup_{(c,a)\in D_n(x)} \bigl[U_c(c) + \mathbb{E}\,V_{n+1}\bigl((1+ i_{n+1})(x-c+a\cdot R_{n+1})\bigr)\bigr],$$

with $V_n$ strictly increasing, strictly concave, continuous, and an optimal strategy realized by per-stage maximizers. This is chunk 04a's Theorem 4.2.2 with consumption added, and every closed-form corollary below specializes it.

Eight milestones: the one-period existence/regularity theorem (Theorem 4.3.1); the zero-mean special case (Theorem 4.3.5); power- and logarithmic-utility closed forms (Theorems 4.3.6, 4.3.7); the regime-switching generalization of the goal itself (Theorem 4.4.1), its power-utility closed form (Theorem 4.4.2), and two comparative-statics results on how the optimal policy moves across regimes under a stochastic order (Theorems 4.4.4, 4.4.5).

Significance

Theorem 4.3.3's consumption-investment structure theorem is the basis for every result about optimal spending and saving under uncertainty; its power/log closed forms (Theorems 4.3.6/4.3.7) recover the classical facts that a power-utility investor consumes and invests constant fractions of current wealth (myopic, wealth-independent policy fractions) while a log-utility investor's optimal consumption fraction, $1/(N-n+1)$, is the textbook "consume your remaining horizon's worth" rule. The regime-switching extension (§4.4) is the discrete-time analogue of Hamilton's regime-switching models, now standard in empirical finance; Theorems 4.4.4-4.4.5 give a rigorous comparative-statics answer to "does a riskier regime call for more or less stock exposure," using the increasing-concave stochastic order rather than a first- moment heuristic — the mathematically correct notion of "regime $k$'s returns dominate regime $j$'s for every risk-averse (concave, monotone) preference," not merely "regime $k$ has a higher mean."

No result of this chunk was found on the platform (searched "consumption investment", "regime switching", "stochastic order"). The proofs largely mirror chunk 04a's (the book itself says so explicitly for Theorems 4.3.1, 4.3.7, 4.4.2), so this mission's contribution is the precise joint-choice statement of each result and, for the comparative-statics theorems, the correct increasing-concave order (≤_icv, Definition B.3.9c) rather than the plain concave order (≤_cv) chunk 02c already needed for a different theorem — the two are genuinely different relations and must not be conflated.

Difficulty

The naive approach to the goal decouples the consumption and investment choices into two independent optimizations; the book's own proof shows they do separate at the level of the per-stage optimization (Theorem 4.3.6's proof: the transformed problem factors into a consumption fraction $\zeta$ and an investment fraction $\alpha$ optimized independently once the wealth scale is normalized out), but the admissible sets remain jointly constrained ($0\le c\le x$ interacts with the investable amount $x-c$), so treating them as literally independent unconstrained problems would silently solve an easier, different problem. For the regime-switching comparative statics (Theorem 4.4.5), the natural first attempt tries to prove monotonicity of $d_n(j)$ in $j$ directly from $Q_j\le_{\mathrm{icv}}Q_k$ alone; the book's own induction needs both hypotheses simultaneously (the environment chain's own stochastic monotonicity, governing how the regime itself evolves, and the return-distribution order, governing the one-period objective) — Theorem 4.4.4's monotonicity of $\alpha^*(j)$ handles the second factor of the induction's product (Eq. (4.22)) while the chain's stochastic monotonicity handles the first; dropping either hypothesis breaks the induction step.

Formalization scope

The consumption-investment vocabulary (ConsumptionInvestmentMarket, its value function, the one-period sub-problem) mirrors chunk 04a's pure-investment TerminalWealthMarket pattern exactly, extended to a joint $(c,a)$ action. The regime-switching model (RegimeSwitchingMarket) represents the finite regime set $E_Y$ abstractly (a Fintype with a row-stochastic transition matrix p : EY → EY → ℝ, not a PMF/product-measure construction on the joint disturbance): the book's own formula for $J_n^\pi$ is already a finite sum over the next regime of an integral against $Q_j$, so this is the direct, faithful representation and needs no additional measure-theoretic machinery — Jpi/J are built via an accumulator recursing through this finite-sum-of-integrals at each step (the natural generalization of chunk 04a's EFromToAcc pattern to a kernel that depends on an evolving state coordinate, rather than an exogenous process). Theorem 4.4.4/4.4.5 introduce LEIncreasingConcaveOrder (Definition B.3.9c) fresh, since chunk 02c's stochastic-order triple (≤_st/≤_cv/≤_cx) does not include the increasing-concave order this chunk's theorems actually use — reusing one of those three would silently substitute a different hypothesis, exactly the trap the chunk brief warns against. IsStochasticallyMonotoneChain (Definition B.3.13) is likewise restated fresh for a finite chain given by its transition matrix.

No trivializing formalization: D_n(x) is a genuine joint constraint on (c,a) (not two independent unconstrained choices); the six closed-form theorems (4.3.6, 4.3.7, 4.4.2, plus the comparative-statics pair) each state their own explicit recursion for $d_n$ — matching the brief's own note that the index-base convention is not uniform across them (Theorem 4.3.6 gives $d_N$ and recurses backward; Theorem 4.4.2 gives $d_0(j)$ and recurses forward) — encoded exactly as each theorem states it, not standardized to one direction.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. https://doi.org/10.1007/978-3-642-18324-9
• J. D. Hamilton, "A new approach to the economic analysis of nonstationary time series and the business cycle", Econometrica, 1989 (the regime-switching framework §4.4 specializes to a portfolio-choice setting).

Motivation

Stochastic approximation is the family of recursive algorithms that locate a zero of a function observed only through noisy evaluations. It goes back to Robbins and Monro (1951) and today underlies stochastic gradient descent, temporal-difference learning, Q-learning and actor–critic methods in reinforcement learning, and models of learning by boundedly rational agents.

The standard analysis is the O.D.E. method (Ljung 1977; see Kushner and Yin 1997): the interpolated iterates are compared with the solutions of an ordinary differential equation, and convergence of the algorithm follows from the stability of that ODE. The method has one well-known gap. It assumes, rather than proves, that the iterates remain bounded with probability one. In applications this stability hypothesis is often the hardest part: for asynchronous Q-learning and adaptive critic algorithms, almost sure boundedness had been proved only for discounted cost or after adding a projection step (Borkar and Meyn, p. 460).

Borkar and Meyn (SIAM J. Control Optim. 38 (2000)) close this gap with a scaling argument borrowed from the fluid-model approach to the stability of queueing networks (Dai 1995; Dai and Meyn 1995). They show that boundedness itself follows from the asymptotic stability of the origin for a second, "fluid-limit" ODE obtained by rescaling the drift. This mission formalizes that stability theorem for tapering step sizes, and the convergence theorem that follows from it.

Setting

Fix $d\ge 0$ and work in $\mathbb R^d$ with the Euclidean norm. Let $h:\mathbb R^d\to\mathbb R^d$ and let $\{a(n)\}_{n\ge0}$ be a deterministic sequence of positive step sizes. On a probability space $(\Omega,\mathcal F,\mathsf P)$, random vectors $X(n)$ and $M(n)$ satisfy the stochastic approximation recursion

$$X(n+1) = X(n) + a(n)\big[h(X(n)) + M(n+1)\big], \qquad n\ge0. \tag{1.1}$$

Its mean ODE is $\dot x = h(x)$ (1.2). For $r>0$ the scaled field is $h_r(x)=h(rx)/r$, with the scaled ODE $\dot x = h_r(x)$ (1.4).

• (A1) $h$ is Lipschitz; $h_r(x)\to h_\infty(x)$ as $r\to\infty$ for every $x$; and the origin is an asymptotically stable equilibrium of the fluid-limit ODE $\dot x = h_\infty(x)$ (1.5).
• (A2) With $\mathcal F_n$ the history of the iterates up to time $n$, $\{M(n)\}$ is a martingale difference sequence, $\mathsf E[M(n+1)\mid\mathcal F_n]=0$, and for some constant $C_0<\infty$, $\mathsf E[\|M(n+1)\|^2\mid\mathcal F_n]\le C_0(1+\|X(n)\|^2)$.
• (TS) Tapering step sizes: $0<a(n)\le1$, $\sum_n a(n)=\infty$, $\sum_n a(n)^2<\infty$.

A point $x^*$ is globally asymptotically stable for $\dot x = h(x)$ if it is a Lyapunov-stable equilibrium and every solution converges to it.

Formalization targets

Goal: Theorem 2.2 (almost sure convergence)

Under (A1), (A2) and (TS), if $\dot x=h(x)$ has a unique globally asymptotically stable equilibrium $x^*$, then for every initial condition $X(0)\in\mathbb R^d$,

$$X(n)\longrightarrow x^* \qquad \text{almost surely.}$$

The goal contains no constants and no rates, only the qualitative conclusion.

Milestone: Theorem 2.1 (i) (almost sure boundedness)

Under (A1), (A2) and (TS), for every initial condition,

$$\sup_n \|X(n)\| < \infty \qquad \text{almost surely.}$$

Milestones: the lemmas of Section 4.1

• Lemma 4.1: the fluid-limit ODE is globally exponentially asymptotically stable.
• Lemma 4.2: the piecewise ODE solutions $\hat\phi$, $\phi^\infty$ used for comparison are bounded by a constant independent of the initial condition.
• Lemma 4.3 (i), (ii): two discrete Bellman–Gronwall inequalities.
• Lemma 4.4: for large scale $r$, every solution of $\dot x = h_r(x)$ from the unit ball is $\epsilon$-small on a window $[T,T+1]$.
• Lemma 4.5: the rescaled iterates have uniformly bounded second moments, and the rescaled noise sum $\xi$ is an $L^2$-bounded martingale.
• Lemma 4.6: almost surely the rescaled interpolated iterates $\phi$ track $\hat\phi$ and stay bounded.

Significance

The result. Theorem 2.1 (i) turns the stability hypothesis of the O.D.E. method into a checkable condition on a deterministic ODE. Theorem 2.2 then gives convergence to $x^*$ with no a priori boundedness assumption. The paper applies this to reinforcement learning, obtaining the first convergence proof for asynchronous Q-learning and adaptive critic algorithms for average-cost Markov decision processes (the asynchronous extension, Theorem 2.5, is sketched in the paper and is not part of this mission). The same fluid-limit criterion is now a textbook tool; see Borkar, Stochastic Approximation: A Dynamical Systems Viewpoint (2008), Chapter 3.

Formalizing it. The theorems are proved in the paper, and the proofs are short but rely on several standard facts stated informally: uniform convergence of $h_r$ to $h_\infty$ on compact sets, continuous dependence of ODE solutions on initial data and on the vector field, and the martingale convergence theorem. No machine-checked version of the O.D.E. method or of this stability criterion is known to exist. A formal development would give a verified link between discrete-time stochastic recursions, martingale convergence in Mathlib, and the stability theory of Lipschitz ODEs.

Difficulty

The obvious approach is to compare the iterates with solutions of $\dot x = h(x)$ over windows of fixed ODE time and to control the accumulated noise by martingale convergence. This fails without boundedness: the noise bound in (A2) grows with $\|X(n)\|$, so the deviation from the ODE can only be controlled relative to the current size of the iterate, and nothing prevents the iterates from escaping to infinity.

A second difficulty is that the hypothesis (A1) concerns only the fluid limit $h_\infty$, which describes the drift at infinite scale. It says nothing directly about $h$ at any finite state, and nothing about the noise. Any argument therefore has to transfer information from the limit $r\to\infty$ to the recursion at random, path-dependent scales, uniformly over those scales, while the noise is controlled only relative to the current size of the iterate. In Lean this involves ODE comparison and Gronwall estimates on a random partition of the time axis, conditional second-moment estimates for a rescaled recursion, and a vector-valued $L^2$ martingale convergence argument, none of which is available off the shelf for this setting.

Formalization scope

The state space is EuclideanSpace ℝ (Fin d). An ODE solution is a forward solution on $[0,\infty)$: the derivative is taken within $[0,\infty)$ at each $t\ge0$, which makes solutions continuous there. Stability notions are the standard ones (Lyapunov stability; asymptotic, global asymptotic and global exponential stability, the last in the form $\|x(t)-x^*\|\le b e^{-\delta t}\|x(0)-x^*\|$). All vector fields in the mission are Lipschitz, so forward solutions exist and are unique, and quantifying over "every solution" is meaningful.

The filtration in (A2) is the natural filtration of the iterates. Because $a(n)>0$, it carries the same information as the paper's $\sigma(X(i),M(i),i\le n)$. (A2) includes integrability of $M(n+1)$ and $\|M(n+1)\|^2$, so that the conditional expectations are meaningful. The theorems quantify over every probability space and every noise process satisfying (A2); the goal and Theorem 2.1 (i) take a deterministic initial condition, as the paper does. Stating the goal for a particular noise model (no noise, or i.i.d. noise) would be a different and much weaker theorem, and is ruled out. "$\sup_n\|X(n)\|<\infty$" is boundedness above of the set of norms, not a real supremum, which Lean sets to $0$ on unbounded sets. Second-moment suprema in Lemma 4.5 are taken in $[0,\infty]$.

The proof objects of Section 4.1 (time grid $t(n)$, blocks $m(j)$ and $T(j)$, scales $r(j)$, the interpolation $\phi$, the rescaled iterates and noise sum) are separate definitions built from the step sizes and the sample path, as on the page. The piecewise ODE solutions $\hat\phi$ and $\phi^\infty$ are characterized by a predicate, and the lemmas hold for every function satisfying it.

Useful infrastructure, reusable beyond this mission: Lipschitz ODE comparison and continuous-dependence estimates in Mathlib's ODE library, uniform convergence of $h_r$ on compact sets, the discrete Gronwall lemmas, and $L^2$-bounded vector-valued martingale convergence. Contributions are welcome on any milestone. The two Gronwall lemmas and Lemma 4.1 are self-contained entry points.

Selected references

• V. S. Borkar and S. P. Meyn, The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning, SIAM J. Control Optim. 38(2):447–469, 2000. https://doi.org/10.1137/S0363012997331639
• H. Robbins and S. Monro, A Stochastic Approximation Method, Ann. Math. Statist. 22(3):400–407, 1951. https://doi.org/10.1214/aoms/1177729586
• L. Ljung, Analysis of Recursive Stochastic Algorithms, IEEE Trans. Automat. Control 22(4):551–575, 1977. https://doi.org/10.1109/TAC.1977.1101561
• H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997. https://doi.org/10.1007/978-1-4899-2696-8
• J. G. Dai, On Positive Harris Recurrence of Multiclass Queueing Networks: A Unified Approach via Fluid Limit Models, Ann. Appl. Probab. 5(1):49–77, 1995. https://doi.org/10.1214/aoap/1177004828
• J. G. Dai and S. P. Meyn, Stability and Convergence of Moments for Multiclass Queueing Networks via Fluid Limit Models, IEEE Trans. Automat. Control 40(11):1889–1904, 1995. https://doi.org/10.1109/9.471210
• V. S. Borkar, Stochastic Approximation: A Dynamical Systems Viewpoint, Cambridge University Press / Hindustan Book Agency, 2008. https://doi.org/10.1007/978-93-86279-38-5

Motivation

Scheduling jobs on unrelated machines so as to minimize the makespan (the time at which the last machine finishes) is one of the central problems of approximation algorithms. For the general problem, Lenstra, Shmoys and Tardos (1990) gave a 2-approximation and showed that no polynomial-time algorithm achieves a factor below $3/2$ unless P = NP; closing the gap between $3/2$ and $2$ has been open since.

The restricted assignment problem is the special case in which every job $j$ has a single size $p_j$ and may only run on a given set $\Gamma(j)$ of machines. The $3/2$ hardness already holds here, and the best known algorithms were still $2$-approximations. Every linear program previously used for the problem has integrality gap $2$, so a better LP lower bound was the natural target.

Svensson (2011) showed that the configuration LP of Bansal and Sviridenko (2006), whose variables assign whole sets of jobs to machines, has integrality gap at most $33/17 \approx 1.9412$. Its optimum therefore gives a polynomial-time estimate of the optimal makespan within a factor strictly better than $2$.

• 1990: Lenstra, Shmoys, Tardos, 2-approximation for unrelated machines, and $3/2$ hardness already for restricted assignment.
• 2006: Bansal and Sviridenko introduce the configuration LP for the max–min variant (the Santa Claus problem).
• 2008: Feige shows the configuration LP has constant integrality gap for restricted Santa Claus, and Asadpour, Feige and Saberi (2008) give a local search proof of a factor-4 gap.
• 2011: Svensson adapts that local search to makespan and proves the gap $33/17$ for restricted assignment (arXiv:1011.1168).

Setting

An instance consists of finite sets $J$ (jobs) and $M$ (machines), sizes $p_j \ge 0$, and for each job a set $\Gamma(j) \subseteq M$. A schedule is a map $\sigma : J \to M$ with $\sigma(j) \in \Gamma(j)$. The load of machine $i$ is $\sum_{j : \sigma(j) = i} p_j$, and the makespan is the largest load. $\mathrm{OPT}$ is the least makespan of a schedule.

For a target makespan $T$, a configuration for machine $i$ is a set $C \subseteq J$ of jobs that may all run on $i$ ($i \in \Gamma(j)$ for $j \in C$) with $p(C) = \sum_{j \in C} p_j \le T$. Write $\mathcal C(i,T)$ for the set of configurations. The configuration LP asks for $x_{i,C} \ge 0$ with

$$\text{[C-LP]}\qquad \sum_{C \in \mathcal C(i,T)} x_{i,C} \le 1 \quad (i \in M), \qquad \sum_{i \in M}\ \sum_{C \in \mathcal C(i,T),\ C \ni j} x_{i,C} \ge 1 \quad (j \in J).$$

Its dual has variables $y_i, z_j \ge 0$ and constraints $y_i \ge \sum_{j \in C} z_j$ for all $i$ and $C \in \mathcal C(i,T)$. $\mathrm{OPT}_{LP}$ is the least $T$ at which [C-LP] is feasible, and $\mathrm{OPT}_{LP} \le \mathrm{OPT}$.

In the Lean development these are configs Γ p T i, CLPFeasible Γ p T, CLPDualFeasible Γ p T y z and schedLoad p σ i, in the namespace RestrictedAssignment.Svensson.

Formalization targets

Goal: Theorem 4.1

For every instance with $p \ge 0$ and every $T \ge 0$,

$$\text{[C-LP] feasible at } T \ \Longrightarrow\ \exists\, \sigma : J \to M,\ \ \sigma(j) \in \Gamma(j)\ \forall j,\quad \sum_{j : \sigma(j) = i} p_j \le \tfrac{33}{17}\, T \ \ \forall i .$$

Equivalently $\mathrm{OPT} \le \tfrac{33}{17}\,\mathrm{OPT}_{LP}$. The statement is scale-free and does not define $\mathrm{OPT}_{LP}$.

Milestones

The milestones follow the paper's proof, which normalizes $\mathrm{OPT}_{LP} = 1$ and sets $R = 16/17$:

1. a dual solution with $\sum_i y_i < \sum_j z_j$ makes [C-LP] infeasible;
2. the local search, Algorithm 2 (ExtendSchedule), keeps its partial schedule valid (load at most $1 + R$, at most one big job per machine);
3. when the algorithm has no potential move, an explicit pair $(y^*, z^*)$ is dual feasible (Claim 4.7) and has $\sum y^* < \sum z^*$ (Claim 4.8);
4. hence, if [C-LP] is feasible, a potential move always exists (Lemma 4.6);
5. the algorithm has no infinite run (Lemma 4.9);
6. [C-LP] feasible at $T = 1$ gives a schedule of makespan at most $1 + 16/17$.

Three facts from Section 2 complete the list: normalization by scaling, $\mathrm{OPT}_{LP} \le \mathrm{OPT}$, and monotonicity of feasibility in $T$.

Significance

The theorem shows that the configuration LP is a strictly stronger relaxation than those behind the factor-$2$ algorithms. With the known polynomial-time approximate solvability of the LP, it gives a polynomial-time algorithm that estimates the optimal makespan of restricted assignment within $33/17 + \epsilon$. The local search in the proof finds a schedule of the same quality, but it is not known to run in polynomial time. Later work lowered the constant to $11/6$ (Jansen and Rohwedder, 2017) along the same lines.

The result is proved on paper. As far as known, no part of it has a machine-checked proof. Formalizing it gives:

• a reusable definition of the configuration LP and its dual certificate;
• a precise, nondeterministic model of a local search whose termination rests on a lexicographic potential;
• a check of a proof that has many cases. The formalization already exposed two edge cases:
  • Claim 4.8 fails when $j_{\mathrm{new}}$ has size $0$ and no admissible machine;
  • the termination proof needs positive job sizes. With a job of size $0$, the algorithm can move it back and forth between two tied machines forever.

The milestones are stated with the corresponding hypotheses.

Difficulty

The obvious approach, rounding a fractional configuration solution, loses a factor $2$. If each machine takes one configuration and the collisions of jobs chosen twice or not at all are repaired, the repair can double a load. This is where every earlier LP-based bound stalls.

The milestones along the paper's route are hard for two reasons. First, the dual pair $(y^*, z^*)$ rounds job sizes down by class (big to $11/17$, medium to $9/17$). Proving $\sum y^* < \sum z^*$ requires a case analysis over how each blocked machine came to be blocked. The two claims are therefore false for arbitrary states of the search and hold only for states the algorithm actually reaches, so the invariants of reachable states have to be formalized too. Second, the search both adds and removes blockers, so no simple quantity decreases at every step. Termination needs a potential defined on the whole history of the search.

Formalization scope

Jobs and machines are finite types with decidable equality, sizes are real numbers with $p_j \ge 0$, and admissible machines are a Finset per job. Schedules are total maps $J \to M$ with $\sigma(j) \in \Gamma(j)$ stated explicitly. Partial schedules are maps $J \to$ Option M. Constants are exact rationals in $\mathbb R$. Values of moves live in Lex (ℝ × ℝ).

Algorithm 2 is a step relation Step, not a function. The move of minimum lexicographic value is a hypothesis on the chosen pair, so every tie-breaking rule is covered. The blocker tree is stored as its list of blockers in insertion order. Claims 4.7, 4.8 and Lemma 4.6 quantify over states reachable from the initial state, as their proofs require. Lemma 4.9 asserts that no infinite run exists.

Three statements would trivialize the goal, and the formalization rules them out:

• a schedule allowed to use machines outside $\Gamma(j)$;
• a target $T < 0$;
• an LP missing either constraint row.

Theorem 1.1 (polynomial time), the separation oracle, and Section 3's two-size case are not part of the mission.

Useful contributions include:

• the weak-duality certificate;
• the scaling and monotonicity facts;
• the invariants of reachable states (each job lies in at most one blocker, blockers on a machine are never reassigned while present);
• the two claims and the termination argument.

The configuration LP definitions are reusable for the Santa Claus problem and for bin packing.

Selected references

• O. Svensson, Santa Claus Schedules Jobs on Unrelated Machines, arXiv:1011.1168v2, 2011; SIAM J. Comput. 41(5), 2012. https://arxiv.org/abs/1011.1168
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Math. Programming 46, 1990. https://doi.org/10.1007/BF01585745
• N. Bansal, M. Sviridenko, The Santa Claus problem, STOC 2006. https://doi.org/10.1145/1132516.1132522
• A. Asadpour, U. Feige, A. Saberi, Santa Claus meets hypergraph matchings, APPROX 2008; ACM Trans. Algorithms 8(3), 2012. https://doi.org/10.1145/2229163.2229168
• K. Jansen, L. Rohwedder, On the configuration-LP of the restricted assignment problem, SODA 2017. https://arxiv.org/abs/1611.01934

Motivation

Mission III's Theorem 6.2 — "fluid limit stability implies SPN stability" — converts a probabilistic stability question into a real-analysis question, but it only supplies the generic fluid equations (6.1)-(6.6), which hold under any control policy and therefore say nothing policy-specific: (6.1)-(6.6) alone never force a fluid path to reach zero. To actually prove a concrete queueing network stable, one must first identify the extra fluid equation a specific policy forces on every fluid limit path, and prove that this extra equation genuinely holds — a task the book calls "justifying" the equation "through the same fluid limit procedure used in the proof of Theorem 6.5." J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) carries out this derivation for four control-policy families in Chapter 7, laying the groundwork every later stability chapter of the book (feedforward networks, the Rybko–Stolyar boundary, back-pressure, proportional fairness, task allocation) builds on.

The first-come-first-served (FCFS) analysis traces to Rybko and Stolyar's 1992 fluid-scaling argument and was first stated in closed form as Eq. (2.6) of M. Bramson's 1996 paper on FCFS queueing networks; Bramson also showed by example (1994) that FCFS networks can be unstable even under the standard load condition, motivating the need for a precise fluid-equation characterization rather than an informal one.

Setting

A queueing network (Section 2.6) is an SPN with one activity per buffer: buffer/class $i$ is served by a unique pool $p(i)$, and on completion a class-$i$ job becomes class $j$ with probability $P_{ij}$ (the routing matrix). $I(k)$ denotes the set of classes served by pool $k$. The fluid equations (6.1)-(6.6) specialize accordingly: consumption is the identity ($\hat D = \hat F$) and the output matrix is $\Gamma_{ij} = P_{ji}$.

Three control-policy families are studied. A policy is non-idling if no server sits idle while a job waits in one of its buffers. A static buffer priority (SBP) policy is non-idling and additionally orders same-pool classes by a fixed priority permutation $\sigma$, always serving the highest-priority non-empty class first; it is non-preemptive if a job's service, once begun, is never interrupted by a later higher-priority arrival. Under FCFS, jobs at a pool are served strictly in arrival order — the workload-based analysis of Section 7.3. Section 7.4 studies a fourth, more general family: a unitary network (one service type per class) under a relaxed control policy $\beta = h(\hat z)$, where $\hat z$ is the updated job-count vector and $h$ is any capacity-respecting, degree-zero-homogeneous function (Assumption 7.6) — a family general enough to include non-idling and SBP policies as special cases, and to anticipate the proportionally fair allocation studied in Chapters 9-10.

Formalization targets

Goal: Theorem 7.5 — the FCFS fluid equation

For a queueing network under FCFS control, every fluid limit path $(\hat D, \hat F, \hat T, \hat Z)$ satisfies (6.1)-(6.6) and

$$\hat D_i\big(t + \hat W_k(t)\big) = \hat G_i(t), \qquad t \ge 0,\ i \in I(k),\ k \in K,$$

where $\hat G_i(t) = \lambda_i t + \sum_j P_{ji}\hat D_j(t)$ is the fluid arrival rate into class $i$ and $\hat W_k(t) = \sum_{i \in I(k)} m_i \hat Z_i(t)$ is pool $k$'s fluid-scaled immediate workload. This is the weakest natural target: an identity that pins down exactly the time-shift FCFS imposes, without asserting anything about how quickly or whether the fluid model reaches zero (that is left to the Lyapunov arguments of later chapters, once this equation is in hand).

Supporting milestones

Theorem 7.2 (non-idling): $\sum_{i\in I(k)} \hat Z_i(t) > 0$ forces pool $k$'s aggregate service rate to run at full capacity $b_k$. Theorem 7.3 (non-preemptive SBP): the same conclusion with $I(k)$ sharpened to the priority set $H(j)$ (Eq. 7.5), for every buffer $j$. Theorem 7.8 (general relaxed control): under Assumption 7.6, $\hat Z_i(t) > 0$ forces $\hat T_i$'s derivative to equal $h_i(\hat Z(t))$ exactly — the common generalization from which the non-idling and SBP fluid equations both follow as special cases of a suitable $h$.

Significance

The result itself. Theorem 7.5 is the precise bridge that lets FCFS-specific stability questions be attacked by the Lyapunov-function method Theorem 6.2 licenses: without a closed-form fluid equation, "does an FCFS network satisfy the standard load condition stably?" has no tractable deterministic reformulation. Bramson's 1994 example (an FCFS network unstable despite satisfying the standard load condition) shows the equation's content is not vacuous — FCFS fluid limits genuinely can misbehave, and this equation is precisely what any subsequent stability or instability argument for FCFS networks must reason about.

Formalizing it. No result about FCFS, non-idling, static-buffer-priority, or general relaxed control policies exists on Prove2Me (q=first-come-first-served, q=FCFS, q=priority policy all return zero hits, consistent with triage.json's record that none of this book's Chapters 6-14 machinery is on the platform). This mission is a from-scratch formalization of queueing networks, their three named control-policy families, and the four policy-specific fluid equations Chapter 7 derives for them.

Difficulty

The obvious shortcut for Theorem 7.3 — reuse Theorem 7.2's hypothesis and conclusion verbatim with $I(k)$ replaced by $H(j)$ — conflates the preemptive and non-preemptive SBP policies: Remark 7.4 explicitly notes the underlying pathwise identity (7.4) (used directly by Theorem 7.2) holds unconditionally under preemption but only asymptotically, via a vanishing-remainder argument bounding the leftover processing time of interrupted-but-continuing jobs, under non-preemption — the theorem actually being formalized is about the harder, non-preemptive case. For Theorem 7.5, the central difficulty is that FCFS's defining property is a genuinely time-shifted identity (departures at $t + \hat W_k(t)$ match arrivals at $t$), not a same-instant conditional statement like the non-idling and SBP equations — an approach that tried to state FCFS as a same-instant condition on $\hat T$ or $\hat D$ alone, without introducing the auxiliary workload process $\hat W$, could not express the theorem's actual content. A further subtlety Theorem 7.8's proof flags directly (Remark 7.9) is that the tempting converse — "$\hat Z_i(t) = 0$ implies zero service rate" — is false in general (a corrected version appears only later, as Lemma 8.9); this mission's goal and milestone statements are careful to assert only the one-directional implication the book actually proves.

Formalization scope

Mission III's fluid-limit-path apparatus (Definition 6.6, u.o.c. convergence) is restated locally in this chapter's own namespace rather than imported, since drafts in this series do not import one another; the restatement is trimmed to the four raw processes $(D^x,F^x,T^x,Z^x)$ this chapter's proofs need, omitting mission III's "delayed random walk" machinery. The non-idling and non-preemptive-SBP hypotheses are both formalized via one shared predicate, FullyUtilized, applied to different index sets ($I(k)$ vs. $H(j)$) — the pathwise full-utilization identity (7.4) that each policy's proof establishes for its own priority classes, taken as a hypothesis rather than re-derived from a lower-level model of server scheduling (Chapter 2's construction of the service-starting mechanism is out of scope for this chapter, exactly as it was for mission III's SPNProcessFamily). Likewise, the FCFS goal theorem hypothesizes the raw identity (7.12) (rewritten via the material-balance equation to avoid needing the raw arrival process) and the fluid-scaled limit of the raw workload process (7.17), rather than re-deriving either from the "delayed random walk" $V$ of Eq. (6.47). A formalization that dropped the workload shift $\hat W_k(t)$ from Theorem 7.5's conclusion, or that stated Theorem 7.8's converse implication (which Remark 7.9 explicitly disclaims), would each be an unfaithful trivialization or overstatement ruled out here. QueueingNetworkData, ProcessFamily, FullyUtilized, and SatisfiesAssumption76 are the primary reusable contributions of this mission; contributions completing the four by sorry proofs — each of which needs the u.o.c.-convergence and dominated-convergence arguments mission III's own proofs still lack — are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• M. Bramson, "Convergence to equilibria for fluid models of FIFO queueing networks," Queueing Systems 22 (1996), 5–45.
• M. Bramson, "Instability of FIFO queueing networks," Annals of Applied Probability 4 (1994), 414–431.
• A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.

Motivation

A stochastic processing network (SPN) is the general model behind manufacturing lines, call centers, computer systems, communication networks and hospital wards: a collection of buffers holding waiting work, a collection of activities (servers) that consume items from buffers and produce items into others, and stochastic primitives — arrival processes and service requirements — that drive the whole system forward in continuous time. Before any control policy can be designed, evaluated, or proved to work, the modeler needs a single, unambiguous, checkable notion of what it means for such a system to be stable: to settle into statistical equilibrium rather than pile up work without bound.

The difficulty is that "stability" has several natural, superficially different candidate definitions — positive recurrence of the underlying Markov chain, existence of a unique stationary distribution, convergence in distribution of queue lengths — each convenient for a different purpose (positive recurrence for verifying via drift criteria, a stationary distribution for computing long-run averages, distributional convergence for interpreting simulation output). J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' own pre-publication draft, 2020-4-2, http://spnbook.org) opens its technical development by proving these candidates coincide, so that the rest of the book — and, in practice, most stability results for queueing networks published since Rybko and Stolyar's and Dai's foundational work in the 1990s — can speak of "SPN stability" as one well-posed property.

Setting

An SPN has $I$ buffers, indexed $1, \dots, I$, and $J$ activities (service types), indexed $1, \dots, J$. External work arrives into buffer $i$ according to a counting process $E_i(t)$; activity $j$, whenever engaged, requires a service time and produces an output vector into the buffers on completion. The baseline stochastic assumptions (Assumption 2.1) specify these primitives precisely: the $I$ external arrival processes are independent Poisson processes with rates $\lambda_1, \dots, \lambda_I \ge 0$ (no arrivals into a buffer with rate $0$); for each activity $j$, the matched pairs of processing variables — service time and output vector, $(v_j(\ell), \varphi_j(\ell))_{\ell \ge 1}$ — form an i.i.d. sequence with finite means $m_j = \mathbb{E}[v_j(1)] > 0$ and $\Gamma_j = \mathbb{E}[\varphi_j(1)] \ge 0$; each such pair has a joint phase-type distribution (realized as the absorption time and terminal mark of a finite-state continuous-time Markov chain, per Appendix D.9); and the initial processing variables, the arrival process, and the $J$ processing-variable sequences are, collectively, mutually independent.

Under a fixed control policy, the SPN generates two continuous-time processes: the service-count process $N(t) \in \mathbb{Z}_+^J$ and the buffer-contents process $Z(t) \in \mathbb{Z}_+^I$. Assumption 3.1 (Markov representation) requires these to be embeddable in a richer, irreducible Markov chain $X = \{X(t), t \ge 0\}$ on a countable state space $\mathcal{X}$: a function $f : \mathcal{X} \to \mathbb{Z}_+^J \times \mathbb{Z}_+^I$ with $(N(t), Z(t)) = f(X(t))$ on every sample path, whose level sets $B(z) = \{x : f(x) = (n,z)\ \text{for some } n\}$ are finite for every buffer-content vector $z$, and which has at least one empty state $x^\ast$ with $f(x^\ast) = (0,0)$.

Formalization targets

Goal: Proposition 3.5 — equivalent definitions of stability

$$X \text{ positive recurrent} \iff X \text{ has a unique stationary distribution } \pi \iff Z(t) \text{ converges in distribution to a non-defective limit},$$

and, when these hold, for every bounded $h : \mathcal{X} \to \mathbb{R}$ and every initial distribution of $X(0)$,

$$\Pr\left\{ \lim_{t \to \infty} \frac{1}{t} \int_0^t h(X(s))\, ds = \bar h \right\} = 1, \qquad \bar h := \sum_{x \in \mathcal{X}} \pi(x)\, h(x).$$

Definition 3.6 then names an SPN stable exactly when these equivalent conditions hold — the weakest possible target, since it commits to no particular one of the three characterizations, only to their joint truth or falsity.

Supporting milestones

Two strong laws of large numbers for the primitive stochastic elements (Propositions 2.2 and 2.3) — the arrival counts $E_i(t)/t \to \lambda_i$ and the processing-variable sample means $\frac{1}{n}\sum_{\ell \le n} v_j(\ell) \to m_j$, $\frac{1}{n}\sum_{\ell \le n} \varphi_j(\ell) \to \Gamma_j$ — and two structural results about the ambient chain: Lemma 3.7, a drift-type sufficient condition for positive recurrence that foreshadows the fluid-model methodology of later chapters, and Proposition 3.9, a sufficient condition (reachability of the empty state) for the irreducibility that Assumption 3.1 itself demands.

Significance

The result itself. Proposition 3.5 is what turns "is this queueing network stable?" into a single question rather than three potentially different ones, and it licenses every later chapter of the book (and a large fraction of the queueing-theory literature going back to the 1990s fluid-limit program of Rybko–Stolyar, Dai, and others) to prove stability via whichever characterization is most convenient — typically positive recurrence via a Lyapunov drift argument — while concluding all three, including the practically important long-run-average SLLN. Every one of the thirteen other missions in this series builds directly on Definition 3.6: their goal theorems all conclude "the SPN is stable," meaning exactly the three-way equivalence established here.

Formalizing it. No result in this mission or its milestones has a prior formal counterpart on Prove2Me: a search for "positive recurrent," "stationary distribution Markov chain," and "irreducible Markov chain" surfaced only MarkovMixing's PositiveRecurrent predicate, defined for a countable-state discrete-time chain — a different object from Assumption 3.1's continuous-time ambient chain, reused here only conceptually (as the pattern for a mean-return-time definition), not as a Lean dependency. This mission is a from-scratch formalization of the model (baseline stochastic assumptions, Markov representation) and of positive recurrence, stationary-distribution uniqueness, and distributional convergence for it.

Difficulty

The obvious first attempt — define $X$ as an arbitrary countable-state Markov chain and directly import a Mathlib theorem relating its recurrence, its stationary distribution, and long-run convergence — fails because Mathlib currently has no general countable-state continuous-time Markov chain theory of the kind Appendix D of the book develops (its own finite-state CTMC stationary-distribution result is unproven substrate, not applicable to a countably infinite state space). The formalization instead works at the level of the chain's embedded discrete-time jump chain, which is where Lean's PMF-based machinery is available, and states the three equivalent conditions and the SLLN conclusion directly as hypotheses to be discharged, rather than inheriting them from a pre-existing continuous-time framework. A second difficulty is Assumption 2.1(d)'s independence clause, which is a genuine three-way mutual independence of $\sigma$-algebras (initial processing variables, arrival process, and the collection of all $J$ processing-variable sequences), not the pairwise independence a careless reading might substitute — a weaker hypothesis here would silently make later derivations in the series unsound.

Formalization scope

The ambient chain's state space Xstate is an arbitrary countable type ([Countable Xstate], not Fintype) — no result may assume finiteness anywhere. The chain itself is represented by its one-step jump kernel jump : Xstate → PMF Xstate (stepIter gives $n$-step iteration, Irreducible requires every state to reach every other in finitely many jump-chain steps); positive recurrence is mean return time under jump, defined via the standard first-return-time renewal decomposition. IsStable is defined as positive recurrence of the jump chain — one of the three equivalent conditions — with the goal theorem itself certifying the equivalence, so the choice carries no loss of faithfulness. Buffer contents and service counts are Fin I → ℕ and Fin J → ℕ-valued, matching the book's $\mathbb{Z}_+^I$, $\mathbb{Z}_+^J$. A formalization that took IsStable to mean, say, only distributional convergence of $Z$ (dropping the chain-level characterizations) would be a strictly weaker, trivializing shortcut — ruled out here by proving all three equivalent and stating the SLLN as part of the same goal theorem. The definitions in this mission (BaselineAssumptions, MarkovRepresentation, IsStable) are the shared substrate every other mission of the series is built on, and are the primary reusable contribution; contributions completing the by sorry proofs, particularly of the goal theorem (which the book proves via appeal to general CTMC theory in its Appendix D, not reproduced here), are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
• J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.