Analysis

Motivation

Steady-state formulas describe a queue that has been running forever. Many practical questions are about a queue that has not: a call centre just after opening, a server just after a reset, a system under a burst of load. For these, the relevant quantity is the transient distribution $p_n(t) = \Pr\{N(t) = n\}$ of the number $N(t)$ in the system at a finite time $t$. It is also what determines how fast the steady state is approached, and it is needed for the busy period: the length of time a server stays busy once a customer arrives at an idle server.

For the single-server Markovian queue M/M/1 the transient distribution has an explicit closed form in modified Bessel functions. Its history is short and well documented. Ledermann and Reuter (1954) obtained it by spectral analysis of the birth–death process. Bailey (1954) found it by generating functions and Laplace transforms, and Champernowne (1956) by combinatorial methods. Bailey's route is the standard textbook derivation, and it is the one Gross, Shortle, Thompson and Harris outline in §2.11 of Fundamentals of Queueing Theory (4th ed., 2008). Abate and Whitt (1989) showed that computing with the resulting series is numerically delicate, which is one reason for having the formula pinned down exactly.

This mission formalizes §§2.11–2.12 of that book: the transient laws of M/M/1/1, M/M/1 and M/M/∞, and the M/M/1 busy period.

Setting

Customers arrive in a Poisson stream of rate $\lambda > 0$. Each service takes an exponential time of rate $\mu > 0$, and $\rho = \lambda/\mu$. The number in the system is a continuous-time Markov chain on $\{0, 1, 2, \dots\}$, and its state probabilities $p_n(t)$ satisfy the forward (differential–difference) equations. For M/M/1 started with $N(0) = i$ they are, for $t \ge 0$,

$$p_n'(t) = -(\lambda+\mu)p_n(t) + \lambda p_{n-1}(t) + \mu p_{n+1}(t)\ (n > 0), \qquad p_0'(t) = -\lambda p_0(t) + \mu p_1(t), \tag{2.72}$$

with $p_n(0) = 1$ if $n = i$ and $0$ otherwise. The other systems are variants:

• M/M/1/1, no waiting room: two states and equations (2.70).
• M/M/∞, ample service: the death rate in state $n$ is $n\mu$, giving (2.76).
• The busy-period system: (2.72) with $0$ made absorbing ($\lambda_0 = 0$) and $N(0) = 1$. Its $p_0(t)$ is the distribution function of the busy period $T_{bp}$.

A family $(p_n)$ solves a system on $[0,\infty)$ when each $p_n$ has, at every $t \ge 0$, the prescribed derivative (a right derivative at $t = 0$). It is a probability solution when $p_n(t) \ge 0$ and $\sum_n p_n(t) = 1$ for every $t \ge 0$. The modified Bessel function of the first kind is

$$I_n(y) = \sum_{k=0}^{\infty} \frac{(y/2)^{n+2k}}{k!\,(n+k)!}, \qquad I_{-n} = I_n,$$

and the Laplace transform of $f$ is $\bar f(s) = \int_0^\infty e^{-st} f(t)\,dt$ for $\operatorname{Re} s > 0$.

Formalization targets

Goal: the transient M/M/1 law, (2.75)

With $y = 2t\sqrt{\lambda\mu}$,

$$p_n(t) = e^{-(\lambda+\mu)t}\Big[\rho^{(n-i)/2} I_{n-i}(y) + \rho^{(n-i-1)/2} I_{n+i+1}(y) + (1-\rho)\rho^n \sum_{j=n+i+2}^{\infty} \rho^{-j/2} I_j(y)\Big].$$

The goal asserts five things for every $\lambda, \mu > 0$ and every $i$, with no restriction on $\rho$:

1. the series converges;
2. these functions solve (2.72);
3. they meet the initial condition;
4. they form a probability distribution at every $t$;
5. they are the only probability solution.

Milestones

1. (2.71): the M/M/1/1 solution $p_1(t) = \frac{\lambda}{\lambda+\mu}(1-e^{-(\lambda+\mu)t}) + p_1(0)e^{-(\lambda+\mu)t}$, and the matching formula for $p_0$.
2. (2.74) and Rouché's theorem: for $\operatorname{Re} s > 0$, the quadratic $(\lambda+\mu+s)z - \mu - \lambda z^2$ has exactly one zero in $|z| < 1$, namely $z_1 = (\lambda+\mu+s-\sqrt{(\lambda+\mu+s)^2-4\lambda\mu})/(2\lambda)$.
3. The transform of $p_0$: $\bar p_0(s) = z_1^{i+1}/(\mu(1-z_1))$.
4. The limit of (2.75): $p_n(t) \to (1-\rho)\rho^n$ if $\rho < 1$, and $p_n(t) \to 0$ if $\rho \ge 1$.
5. (2.77), M/M/∞: started empty, $p_n(t) = a(t)^n e^{-a(t)}/n!$ with $a(t) = (1-e^{-\mu t})\lambda/\mu$. The statement says that this family solves (2.76), is the unique probability solution, and has generating function $\exp((z-1)a(t))$.
6. The busy-period transform: $\bar p_0(s) = 2\mu/(s[\lambda+\mu+s+\sqrt{(\lambda+\mu+s)^2-4\lambda\mu}])$.
7. The busy-period density: $p_0'(t) = \sqrt{\mu/\lambda}\,e^{-(\lambda+\mu)t} I_1(2\sqrt{\lambda\mu}\,t)/t$.
8. (2.79): for $\lambda < \mu$, $E[T_{bp}] = 1/(\mu-\lambda)$ and $E[T_{bc}] = 1/\lambda + 1/(\mu-\lambda)$.

Significance

The formula (2.75) is the exact finite-time law of the most basic queue. It gives the rate at which M/M/1 approaches equilibrium, and it gives the distribution of the queue under overload ($\rho \ge 1$), where no steady state exists. It is the reference against which numerical transient methods, such as the uniformization of Chapter 8 of the same book, are checked. The busy-period density and its mean (2.79) enter server-utilisation and vacation models, and the Laplace-transform method used here recurs in the M/G/1 analysis of Chapter 5.

All of these results are classical and proved in the literature. None of them is machine-checked, as far as the platform's catalogue and Mathlib show. The chain from a countable system of linear ODEs, through generating functions and a root-location argument, to a Bessel series is a standard pattern in applied probability, and a formal version of it is what this mission adds. The formal statements also make explicit what the book leaves implicit: the sense in which the equations hold at $t = 0$, and the class in which the solution is unique.

Difficulty

The forward equations (2.72) form an infinite linear system. The obvious approach is to treat it like a finite system of ODEs, whose solution is a matrix exponential, and read off (2.75). That fails for two reasons. The generator is an infinite matrix, so its exponential needs a functional-analytic setting. And uniqueness is not automatic for infinite systems: it needs a class, such as probability solutions, and an argument that works in that class.

The Bessel form is a second, independent difficulty. The transform $\bar p_0(s)$ is fixed by a root-location argument in the complex plane. Inverting the transform, or verifying (2.75) directly, requires manipulating the three-term Bessel recurrence and exchanging infinite sums. The tail sum $\sum_{j} \rho^{-j/2} I_j$ has to be controlled uniformly enough to be differentiated term by term. For $\rho \ge 1$ the factor $(1-\rho)$ is non-positive, so the nonnegativity of $p_n(t)$ is not visible from the formula.

Formalization scope

Conventions committed to:

• Parameters. Rates are real with $\lambda, \mu > 0$, and $\rho = \lambda/\mu$. States are ℕ (Fin 2 for M/M/1/1).
• Solutions. "Solves on $[0,\infty)$" is HasDerivWithinAt on Set.Ici 0 at every $t \ge 0$. Uniqueness is asserted among solutions that are probability distributions at every time.
• Special functions. Half-integer powers of $\rho$ are real powers, and $I_{-m} = I_m$ is part of the definition. Laplace transforms are complex Bochner integrals over $(0,\infty)$, and each statement also asserts the integrability it needs. Square roots with positive real part are hypotheses $r^2 = (\lambda+\mu+s)^2 - 4\lambda\mu$, $\operatorname{Re} r > 0$.

The closed forms stated exactly as in the book are:

• (2.71);
• $z_1$ and $z_2$ of (2.74);
• $\bar p_0(s) = z_1^{i+1}/(\mu(1-z_1))$;
• (2.75), with the Bessel series of p.101;
• the M/M/∞ law and (2.77);
• the busy-period transform and density of p.102;
• (2.79).

The book derives (2.79) by a steady-state ratio argument valid for M/G/1. Here it is stated for M/M/1, as the mean of the explicit density.

A statement of (2.75) that only asserts the right-hand side is well defined, or checks only $n = 0$, is ruled out: the goal requires the ODE system, the initial condition, the probability property and uniqueness. For the same reason, the M/M/∞ law is tied to the system (2.76) and does not reduce to a Taylor expansion.

Needed infrastructure that Mathlib lacks:

• modified Bessel functions of integer order;
• Laplace transforms;
• a Rouché-type zero count or a direct root-location lemma;
• uniqueness for countable linear ODE systems with bounded or linearly growing rates.

The Bessel and Laplace definitions, and the uniqueness lemma for birth–death forward equations, are reusable beyond this mission. Contributions of those as separate lemmas are welcome.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§2.11–2.12, pp.97–103. https://doi.org/10.1002/9781118625651
• N. T. J. Bailey, "A continuous time treatment of a simple queue using generating functions", J. Royal Statistical Society B 16 (1954) 288–291. https://doi.org/10.1111/j.2517-6161.1954.tb00172.x
• W. Ledermann, G. E. H. Reuter, "Spectral theory for the differential equations of simple birth and death processes", Phil. Trans. Royal Society A 246 (1954) 321–369. https://doi.org/10.1098/rsta.1954.0001
• D. G. Champernowne, "An elementary method of solution of the queueing problem with a single server and constant parameters", J. Royal Statistical Society B 18 (1956) 125–128. https://doi.org/10.1111/j.2517-6161.1956.tb00217.x
• J. Abate, W. Whitt, "Calculating time-dependent performance measures for the M/M/1 queue", IEEE Trans. Communications 37 (1989) 1102–1104. https://doi.org/10.1109/26.41165

Motivation

Gradient methods assume a continuous gradient; subgradient methods assume convexity. Many objective functions met in practice satisfy neither. Shor's example is economic planning, where components of the objective are piecewise-smooth, not necessarily convex functions of a parameter describing the productivity of a unit, and where minimax formulations produce kinks as a rule (Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, §1.4, p. 17, DOI 10.1007/978-3-642-82118-9). Such problems need a class of functions wide enough to contain piecewise-smooth and minimax functions and narrow enough to carry a usable replacement for the gradient.

Shor's answer is the class of almost differentiable functions, introduced in his 1972 work and presented in §1.4 of the book, together with the almost-gradient, a limit of gradients taken at nearby points of differentiability. The capstone of the section, Theorem 1.15, connects this class with convex analysis: every convex function on $E_n$ is almost differentiable, and its almost-gradients are subgradients. This is what lets the later chapters treat convex minimization and almost-differentiable minimization with one set of tools. Clarke's generalized gradient of locally Lipschitz functions (Clarke 1975) is the closest relative; Shor's definition differs in requiring the gradient to be continuous on its domain (p. 19).

Setting

Let $E_n$ denote $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. For $f : E_n \to \mathbb{R}$, write $M = \{x \in E_n : f \text{ is differentiable at } x\}$ and $\nabla f(x)$ for the gradient at $x \in M$.

A function $f$ is almost differentiable if

1. on every bounded set $S$ it is Lipschitz: $|f(x) - f(y)| \le L_S \|x - y\|$ for $x, y \in S$, with a constant $L_S$ depending on $S$;
2. it is differentiable at Lebesgue-almost every point of $E_n$;
3. the map $x \mapsto \nabla f(x)$, restricted to $M$, is continuous.

An almost-gradient of $f$ at $x_0$ is a vector $g$ that is an accumulation point of a sequence $\nabla f(x_1), \nabla f(x_2), \dots$ with $x_k \in M$ and $x_k \to x_0$. The set of almost-gradients is $G(x_0)$. A generalized almost-gradient is a point of the closure of the convex hull of $G(x_0)$.

A vector $g$ is a subgradient of $f$ at $x_0$ if $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x \in E_n$; for convex $f$ the set of subgradients is the subdifferential $G_f(x_0)$.

In Lean these objects are AlmostDifferentiable f, almostGradients f x₀ and IsSubgradient f x₀ g in the namespace ShorNonsmooth.AlmostDiff, with $E_n$ = EuclideanSpace ℝ (Fin n).

Formalization targets

Goal: Theorem 1.15 (p. 18)

For convex $f : E_n \to \mathbb{R}$,

$$f \text{ is almost differentiable} \quad\text{and}\quad G(x_0) \subseteq G_f(x_0) \ \text{ for every } x_0 \in E_n .$$

The printed statement says the almost-gradients "coincide with" the subgradients. As a set equality this is false (for $f(x) = |x|$ on $E_1$, $G(0) = \{-1, 1\}$ while $G_f(0) = [-1, 1]$), and the book's proof establishes the inclusion. The goal is the inclusion.

Milestones

1. Proof of Theorem 1.15, display (p. 18). For convex $f$ differentiable at $x_k$: $f(x) - f(x_k) \ge (\nabla f(x_k), x - x_k)$ for all $x$.
2. Proof of Theorem 1.15 (p. 18). For convex $f$ and bounded $S$ there is $C$ with $|f'_v(x)| \le C\|v\|$ for all $x \in S$ and all $v$, the one-sided directional derivatives existing.
3. Proof of Theorem 1.15 (p. 18). A convex $f$ is differentiable almost everywhere and $\nabla f$ is continuous on $M$.
4. Theorem 1.14 (p. 18). For almost differentiable $f$, $G(x)$ is nonempty, bounded and closed at every $x$.
5. p. 19. For almost differentiable $f$, $\overline{\operatorname{conv}}\, G(x)$ is convex, bounded and closed.

Significance

The result. Theorem 1.15 embeds convex functions into the almost differentiable class and identifies each almost-gradient of a convex function as a subgradient. Consequently any method that only needs almost-gradients (limits of gradients at nearby differentiable points, which is what a numerical procedure can actually compute) produces valid subgradients when applied to a convex function. Theorem 1.14 supplies the compactness that makes $G(x)$ usable as a set-valued substitute for the gradient.

Formalizing it. All results here are classical and proved on paper. Mathlib contains Rademacher's theorem for Lipschitz functions (LipschitzWith.ae_differentiableAt) and local Lipschitz continuity of convex functions on open sets; it does not contain the continuity of the gradient of a convex function on its domain of differentiability, nor any notion of almost-gradient. The mission produces those, together with a formal record that the printed "coincide" is an inclusion. A formal proof of the true equality $G_f(x_0) = \overline{\operatorname{conv}}\, G(x_0)$ would be a welcome further contribution.

Difficulty

Two parts of the goal carry real content. The first is condition (c): the gradient of a convex function, restricted to the set where it exists, is continuous. The book cites this from the literature; it is not a consequence of Rademacher's theorem, which gives differentiability almost everywhere and says nothing about how gradients at nearby points relate. The second is condition (b) in a form Lean accepts: Rademacher's theorem in Mathlib is stated for globally Lipschitz functions, while a convex function on $E_n$ is only Lipschitz on bounded sets, so the almost-everywhere statement has to be assembled from local pieces. The passage from gradients to subgradients in the second conjunct is comparatively routine.

The analogous closure properties claimed on the same pages for sums, products and maxima of almost differentiable functions (Theorems 1.16 and 1.17) are false as printed and are not targets; see the formalization scope.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $n = 0$ is allowed and harmless. Functions are total and real-valued; convexity is ConvexOn ℝ Set.univ f.
• The gradient is Mathlib's gradient f x; condition (c) is ContinuousOn (gradient f) {x | DifferentiableAt ℝ f x}, continuity of the restriction in the subspace topology.
• Condition (a) is quantified over every bounded set with a set-dependent constant: ∀ S, Bornology.IsBounded S → ∃ L, LipschitzOnWith L f S. Condition (b) is ∀ᵐ x ∂volume, DifferentiableAt ℝ f x.
• An almost-gradient is a cluster point (MapClusterPt) of the gradient sequence, not its limit; the points $x_k$ may equal $x_0$.
• Subgradients are taken relative to the whole space, the domain of every function in this mission.
• The goal states the inclusion $G(x_0) \subseteq G_f(x_0)$ proved in the book. Stating the printed set equality would make the goal false; weakening the first conjunct to "locally Lipschitz and differentiable almost everywhere" would drop condition (c) and with it the substance of the theorem. Neither is acceptable.
• Theorem 1.16 (sums, differences, products) and Theorem 1.17 (maxima) are omitted: both are false for the class as defined. With $h(x) = x^2 \sin(1/x)$, the functions $h + |x|$ and $-|x|$ are almost differentiable but their sum $h$ is differentiable everywhere with a derivative discontinuous at $0$; and $\max(h - |x|,\, h - |x| + 2x) = h + x$. Theorem 1.18 (Mifflin's superposition theorem for semismooth functions) is cited from the literature without proof and rests on Clarke's generalized gradient; it is outside this mission.

Infrastructure that is reusable beyond this mission: continuity of the gradient of a convex function on its domain; Rademacher's theorem for locally Lipschitz functions on $E_n$; the almost-gradient set and its compactness. Contributions that prove these as standalone lemmas are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985. https://doi.org/10.1007/978-3-642-82118-9
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, Theorem 25.5 (continuity of the gradient of a convex function). https://doi.org/10.1515/9781400873173
• F. H. Clarke, Generalized gradients and applications, Transactions of the American Mathematical Society 205 (1975), 247–262. https://doi.org/10.1090/S0002-9947-1975-0367131-6
• H. Rademacher, Über partielle und totale Differenzierbarkeit von Funktionen mehrerer Variabeln und über die Transformation der Doppelintegrale, Mathematische Annalen 79 (1919), 340–359. https://doi.org/10.1007/BF01498415

Motivation

In the theory of Markov decision chains two cost criteria dominate: the discounted cost, in which a cost incurred at time $n$ is weighted by $\alpha^n$ for a discount factor $\alpha \in (0,1)$, and the average cost, the long-run cost per unit time. A standard route to average cost optimal policies is to solve the discounted problem and let $\alpha \to 1^-$. That route needs a precise link between the two criteria for a single sequence of expected costs $u_0, u_1, u_2, \dots \ge 0$: the discounted cost multiplied by $1-\alpha$ on one side, the running average on the other. Appendix A.4 of Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) supplies this link as Theorem A.4.2, and the book invokes it whenever it passes from discounted to average cost (for instance in Chapter 6, where it is applied to $u_n = E_\theta[C(X_n, A_n)]$).

The result belongs to classical summability theory.

• Abelian direction. Convergence of averages implies convergence of the power-series (Abel) means: a consequence of Abel's and Frobenius's theorems on power series (19th century).
• Tauber (1897). The first converse, under a growth condition on the terms.
• Hardy and Littlewood (1914). The converse for Cesàro means of nonnegative terms, the "Hardy–Littlewood Tauberian theorem".
• Karamata (1930). A short proof of that converse by polynomial approximation, reproduced in Titchmarsh, The Theory of Functions (1939, pp. 227–229). The book follows this proof.
• Widder (1941). The continuous-time (Laplace transform) version.
• Sennott (1986b). A proof of the discrete statement, cited by the book as its source for Theorem A.4.2.

Setting

Let $u_0, u_1, u_2, \dots$ be nonnegative terms $u_n \in [0, \infty]$ with $u_0 < \infty$. For $\alpha \in [0, \infty)$ the power series

$$U(\alpha) = \sum_{n=0}^{\infty} \alpha^n u_n \in [0, \infty]$$

always has a sum, possibly $+\infty$, because its partial sums increase. Its radius of convergence is $R = (\limsup_{n} u_n^{1/n})^{-1} \in [0,\infty]$. The partial sums are $w_n = \sum_{k=0}^{n-1} u_k$ for $n \ge 1$. Two ways of averaging the sequence are compared:

• the Cesàro means $w_n / n$, as $n \to \infty$;
• the Abel means $(1-\alpha) U(\alpha)$, as $\alpha \to 1^-$ (from below).

For the constant sequence $u_n \equiv B$ both equal $B$. In the Lean development these are U, radius, w, cesaroMean and abelMean in the namespace SennottDP.Tauberian, all valued in ℝ≥0∞. The proof also uses the function $r$ of Fig. A.1, equal to $0$ on $(0, e^{-1})$ and to $1/x$ on $[e^{-1}, 1)$.

Formalization targets

Goal: Theorem A.4.2

$$\liminf_{n\to\infty} \frac{w_n}{n} \le \liminf_{\alpha\to 1^-} (1-\alpha)U(\alpha) \le \limsup_{\alpha\to 1^-} (1-\alpha)U(\alpha) \le \limsup_{n\to\infty} \frac{w_n}{n}, \tag{A.28}$$

and the following are equivalent: (i) all terms in (A.28) are equal and finite; (ii) $\lim_n w_n/n$ exists and is finite; (iii) $\lim_{\alpha \to 1^-} (1-\alpha)U(\alpha)$ exists and is finite.

No growth or boundedness condition on $u_n$ is assumed: nonnegativity is the only Tauberian condition.

Milestones

1. Remark A.3.3: the geometric series. $R = 1$, $U(\alpha) = B/(1-\alpha)$ and $B\sum_n n\alpha^n = B\alpha/(1-\alpha)^2$.
2. Remark A.3.1: inside the radius of convergence, $U$ is differentiable term by term, and the derived series has the same radius.
3. Eq. (A.31): $\big(\sum \alpha^n\big) U(\alpha) = \sum_n \alpha^n w_{n+1} = U(\alpha)/(1-\alpha)$.
4. Eq. (A.28): the Abelian inequalities on their own.
5. Eq. (A.26): $\int_0^1 r = 1$.
6. Lemma A.4.1: continuous $s^* \le r \le s$ with integrals within $\varepsilon$ of $1$.
7. Eqs. (A.35)–(A.36): if the Abel means tend to $L < \infty$, then $(1-\alpha)\sum_n \alpha^n u_n f(\alpha^n) \to L\int_0^1 f$ for $f(x) = x^k$.
8. The same statement for every $f$ continuous on $[0,1]$.
9. The same statement for $f = r$.
10. Example A.5.1: a $0/1$ block sequence with $\liminf w_n/n = 1/2$ and $\limsup w_n/n = 2/3$ (Choice One) or $1$ (Choice Two), for which the middle inequality of (A.28) is strict.

Significance

The result itself. Theorem A.4.2 lets every statement about $\lim_{\alpha\to1^-}(1-\alpha)V_\alpha$ for a discounted value be read as a statement about long-run average cost, and conversely. The strict cases of Example A.5.1 show why the book must work with $\liminf$ and $\limsup$ rather than limits: average costs of policies need not exist as limits, even for bounded costs.

Formalizing it. Mathlib contains Abel's theorem for convergent series (Mathlib/Analysis/Complex/AbelLimit.lean) and Cesàro convergence of convergent sequences, but no Tauberian theorem. The pinned checkout has no file mentioning "Tauberian", and neither does the platform. The mathematics has been proved since 1914. Formalizing it here adds:

• a machine-checked Hardy–Littlewood–Karamata theorem for nonnegative $[0,\infty]$-valued sequences;
• the $\liminf$/$\limsup$ comparison (A.28) with infinite values allowed;
• a reusable component for the average cost chapters of this series.

Difficulty

The Abelian inequalities (A.28) follow from rearranging the series. The converse (iii) ⇒ (ii) does not: the first idea, recovering $w_n/n$ from $(1-\alpha)U(\alpha)$ at $\alpha = 1 - 1/n$, fails, because knowing $U$ near $1$ controls only weighted averages of all the $u_k$, not a sharp truncation. Some positivity argument is unavoidable, since the converse fails for signed sequences (for example $u_n = (-1)^n n$). The sharp truncation at $n \approx (-\ln\alpha)^{-1}$ corresponds to the discontinuous weight $r$. Passing from polynomial weights to the jump function $r$ requires uniform approximation together with the nonnegativity of the $u_n$ at every step.

The infinite values add bookkeeping. A single $u_{n_0} = \infty$ makes every term of (A.28) infinite, and $R < 1$ forces $U(\alpha) = \infty$ on $(R,1)$.

Formalization scope

Conventions the statements commit to:

• Values. Terms $u : \mathbb{N} \to [0,\infty]$ (ℝ≥0∞) with $u_0 \ne \infty$. $U$, the Abel means, $w_n$ and the Cesàro means are ℝ≥0∞-valued, with ℝ≥0∞ sums (no summability side conditions).
• Limits. $\liminf$ and $\limsup$ are those of the complete lattice $[0,\infty]$, never real liminf. "Exists and is finite" means convergence in $[0,\infty]$ to some $L \ne \infty$.
• Discount factor. $\alpha \in \mathbb{R}_{\ge 0}$, and $\alpha \to 1^-$ is the filter 𝓝[<] 1.
• Index $n = 0$. $n \to \infty$ is atTop on $\mathbb{N}$; the value $w_0/0 = 0$ is irrelevant.
• The equivalence is List.TFAE.
• The function $r$. Its value at the jump is $r(e^{-1}) = e$ (Fig. A.1).
• Continuity. In Lemma A.4.1 and in the continuous-weight step, continuity is required on the closed interval $[0,1]$, which is what the Weierstrass approximation step uses. The book writes "$(0,1)$".
• Finite terms. Remark A.3.1 is stated for finite terms, which the book's discussion of the radius presumes.

A trivializing formalization is ruled out. Real-valued $\liminf$/$\limsup$ would make (A.28) hold by junk values on unbounded sequences; hypotheses such as boundedness of $u_n$ would replace the theorem by an easier special case; and a definition of "exists and is finite" allowing $L = \infty$ would make (ii) hold for $u_n = n$. None of these is used. As sanity checks: for $u_n \equiv 1$ all four terms of (A.28) equal $1$, and for $u_n = n$ all equal $\infty$ and (i)–(iii) all fail.

A complete development needs:

• Cauchy products of $[0,\infty]$-valued power series;
• the Weierstrass approximation theorem, which Mathlib has (polynomialFunctions.topologicalClosure);
• interval integrals of step-like functions;
• $\liminf$/$\limsup$ manipulation along 𝓝[<] 1.

Reusable beyond this mission: the ℝ≥0∞ power-series toolkit and the Karamata argument for general continuous weights (milestone 8). Contributions welcome: proofs of any milestone, and alternative proofs of (iii) ⇒ (ii).

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Appendix A.3–A.5, pp. 279–287. https://doi.org/10.1002/9780470317037
• E. C. Titchmarsh, The Theory of Functions, 2nd ed., Oxford University Press, 1939, pp. 227–229 (Karamata's proof).
• J. Karamata, "Über die Hardy–Littlewoodschen Umkehrungen des Abelschen Stetigkeitssatzes", Mathematische Zeitschrift 32 (1930), 319–320.
• G. H. Hardy and J. E. Littlewood, "Tauberian theorems concerning power series and Dirichlet's series whose coefficients are positive", Proc. London Math. Soc. (2) 13 (1914), 174–191.
• D. V. Widder, The Laplace Transform, Princeton University Press, 1941.
• L. I. Sennott, "A new condition for the existence of optimum stationary policies in average cost Markov decision processes — unbounded cost case", Proc. 25th IEEE Conference on Decision and Control, Athens, 1986, pp. 1719–1721 (cited by the book as Sennott 1986b).
• T. M. Liggett and S. A. Lippman, "Short notes: Stochastic games with perfect information and time average payoff", SIAM Review 11 (1969), 604–607. https://doi.org/10.1137/1011093

Motivation

Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) studies Markov decision chains with countably many states, finite action sets and unbounded nonnegative costs. Its main computational device, the approximating sequence method (Definition 2.5.1, p. 28), replaces the countable state space $S$ by an increasing sequence of state spaces $S_N$ and the transition law out of each state by distributions $P_j(N)$ on $S_N$ that converge pointwise to the original law. Every convergence argument of that method has the same shape: a sum $\sum_{j\in S_N} P_j(N)\,u(j,N)$, an expected cost or value under the $N$-th approximating model, must be shown to converge to $\sum_{j\in S} P_j\,u(j)$, or at least to satisfy a one-sided bound in the limit.

Appendix A, Sections A.1–A.2 (pp. 270–278), collects the analysis results used for this. The author proves them for sums over countable sets rather than general integrals, so they need no measure theory, and the proofs of the discounted-cost and average-cost approximation theorems (Chapters 4 and 8) cite them. This mission formalizes that appendix section as a self-contained unit.

Setting

Let $S$ be a countable set and $(P_j)_{j\in S}$ a probability distribution on $S$: $P_j\ge 0$ and $\sum_j P_j=1$. Values of functions are extended reals in $[-\infty,\infty]$, with the convention $0\cdot\infty=0$. For $u:S\to[-\infty,\infty]$, the weighted sum is

$$\sum_{j\in S}P_j\,u(j)=\sum_{j\in S}P_j\,u^+(j)-\sum_{j\in S}P_j\,u^-(j),$$

which is well defined, in $(-\infty,\infty]$, whenever the negative parts have finite weighted sum. In Lean this is wsum P u.

A family of approximating distributions for $(P_j)$ consists of

1. an increasing sequence of subsets $S_0\subseteq S_1\subseteq\cdots$ of $S$ with $\bigcup_N S_N=S$;
2. for each $N$, a probability distribution $(P_j(N))_{j\in S_N}$ on $S_N$;
3. pointwise convergence $\lim_{N\to\infty}P_j(N)=P_j$ for every $j\in S$.

Since the sets increase to $S$, a fixed state $j$ lies in $S_N$ for every large $N$, so $\liminf_N u(j,N)$ and $\lim_N u(j,N)$ make sense for a function $u(j,N)$ defined only for $j\in S_N$. In Lean these three conditions are the structure ApproxDist P SN Q, with Q N j $=P_j(N)$.

Formalization targets

Goal: Theorem A.2.6 (Generalized Dominated Convergence Theorem), p. 278

Under the approximating-distribution hypotheses, let $u(j,N)$ and $w(j,N)$ be finite with $|u(j,N)|\le w(j,N)$ for $j\in S_N$, let $u(j,N)\to u(j)$ and $w(j,N)\to w(j)$ for every $j$, and assume

$$\lim_{N\to\infty}\sum_{j\in S_N}P_j(N)\,w(j,N)=\sum_{j\in S}P_j\,w(j)<\infty.$$

Then

$$\lim_{N\to\infty}\sum_{j\in S_N}P_j(N)\,u(j,N)=\sum_{j\in S}P_j\,u(j).$$

Milestones, in the book's order

• Proposition A.1.3: $\liminf$ commutes with a minimum over a finite nonempty set; $\lim$ does too when all limits exist.
• Proposition A.1.5: $\liminf_N\sum_{j\in G}u(j,N)\ge\sum_{j\in G}\liminf_N u(j,N)$ for finite $G$ and $u>-\infty$, when the right side has no indeterminate form.
• Proposition A.1.7: the same inequality for countable sums of $[0,\infty]$-valued terms.
• Proposition A.1.8: the same, with the left sum over $S_N$ increasing to $S$.
• Proposition A.1.10: $\liminf u_n\le\liminf w_n/n\le\limsup w_n/n\le\limsup u_n$ for $w_n=\sum_{k<n}u_k$.
• Proposition A.2.1 (Fatou's lemma): $\liminf_N\sum_jP_j u(j,N)\ge\sum_jP_j\liminf_N u(j,N)$ for $u\ge -L$.
• Theorem A.2.3 (dominated convergence, with a convergent dominating sequence $w(j,N)$) and Corollary A.2.4 (fixed dominating function).
• Proposition A.2.5 (generalized Fatou's lemma):

$$\liminf_{N\to\infty}\sum_{j\in S_N}P_j(N)\,u(j,N)\ \ge\ \sum_{j\in S}P_j\,\liminf_{N\to\infty}u(j,N)\qquad(u\ge -L\text{ on }S_N).$$

• Corollary A.2.7: bounded convergence under approximating distributions.

Significance

The results. Proposition A.2.5 and Theorem A.2.6 are the two limit interchanges the approximating sequence method needs. The generalized Fatou inequality gives the lower bound on limits of value functions of the approximating models, and the generalized dominated convergence theorem identifies the limit of expected costs when a dominating function is available. Corollary A.2.7 gives the bounded case, and Proposition A.1.3 moves limits inside the minimization of an optimality equation. Proposition A.1.10 compares Cesàro averages with the sequence itself, which the average-cost chapters use.

Formalizing them. All statements are classical and proved in the book. A.1.7, A.2.1, A.2.3 and A.2.4 are, after translation, instances of Mathlib's Fatou lemma (MeasureTheory.lintegral_liminf_le) and dominated convergence theorem for a discrete measure. The mission states them in the book's discrete, extended-real form so later chapters can cite them by number. The versions in which the distribution and its support change with $N$ (A.2.5–A.2.7) are not in Mathlib in this form; the generalized dominated convergence theorem appears in the measure-theoretic literature (Royden, Real Analysis, Ch. 4) but has no Lean formalization. None of these statements has been formalized for this book.

Difficulty

For the generalized results, Mathlib's Fatou lemma and dominated convergence theorem do not apply directly: they fix one measure, while here both the weights $P_j(N)$ and the support $S_N$ change with $N$. The dominating function $w(j,N)$ also changes with $N$ and is not integrable uniformly in $N$; only the convergence of its expectations is assumed. For small $N$, $\sum_{j\in S_N}P_j(N)w(j,N)$ may even be infinite, and then $\sum_{j\in S_N} P_j(N)u(j,N)$ has no value.

A second difficulty is bookkeeping in the extended reals. Lower limits may be $\pm\infty$, products use $0\cdot\infty=0$, and a sum with a $+\infty$ term and a $-\infty$ term is undefined. The inequality of Proposition A.1.5 holds only when that indeterminate form is excluded. The bound $u\ge -L$ in A.2.1 and A.2.5 cannot be dropped: Examples A.1.9 and A.2.2 of the book show the inequalities fail without it.

Formalization scope

• Types. $S$ is any type with [Countable S]. Probabilities are ℝ≥0∞-valued with ∑' j, P j = 1, and $P_j(N)$ is Q N j. Extended-real values are EReal, and nonnegative extended values (A.1.7, A.1.8) are ℝ≥0∞. Limits and lower and upper limits are along atTop in ℕ. The book's $N\ge N_0$ convention (Remark A.1.2) needs nothing extra, since only large $N$ matter.
• Sums over $S_N$ are sums over $S$ of (SN N).indicator (Q N) times the function. Values of $u(j,N)$ and $P_j(N)$ for $j\notin S_N$ never enter any statement, and the hypotheses on $u$ ($u\ge -L$, $|u|\le w$) are imposed only on $S_N$, as in the book.
• Weighted sums are wsum, the difference of the weighted positive and negative parts, each in [0,∞]. When both are infinite the book's sum is undefined and wsum returns $-\infty$. Every sum used in a hypothesis or conclusion is defined, except possibly for finitely many $N$ in limit statements, where it does not matter.
• Limits of $u(j,N)$ and $w(j,N)$ are taken in EReal, since the book allows extended-real limits (p. 271). The hypotheses force them to be finite wherever $P_j>0$.
• Ruled out. Statements in which wsum returns its junk value $-\infty$ could make an inequality trivial. Every left-hand side here is a lower limit of sums whose negative parts are bounded, or a limit of eventually defined sums, so no statement holds only because of that junk value. Real-valued tsum with its junk value $0$ is not used anywhere.
• Welcome contributions. A proof of A.1.7 from lintegral_liminf_le for the counting measure, and lemmas relating wsum to Mathlib's tsum and to integrals against Measure.sum (fun j => P j • dirac j), can be reused by the other missions of this series.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Appendix A, pp. 270–278. https://doi.org/10.1002/9780470317037
• H. L. Royden, Real Analysis, 3rd ed., Macmillan, 1988, Chapter 4 (Fatou's lemma, generalized Lebesgue convergence theorem).
• The Mathlib Community, The Lean Mathematical Library, CPP 2020, https://doi.org/10.1145/3372885.3373824 (MeasureTheory.lintegral_liminf_le, MeasureTheory.tendsto_integral_of_dominated_convergence).

Motivation

In quantum mechanics the state of a system at time $t$ is $\psi(t) = \mathrm e^{-\mathrm itA}\psi$, where the Hamiltonian $A$ is a self-adjoint operator. The spectral theorem splits the Hilbert space into subspaces according to the type of the spectral measure of a vector (absolutely continuous, singularly continuous, pure point). That splitting is defined through measure theory, and it is not evident what it has to do with the motion of the system. The RAGE theorem, named after Ruelle (1969), Amrein and Georgescu (1973) and Enß (1978), answers this. Vectors in the continuous subspace are exactly the states that, on time average, leave every bounded region: the scattering states. Vectors in the pure point subspace are exactly the states that stay in a bounded region uniformly in time: the bound states. This dynamical characterization is the starting point of the geometric approach to scattering theory and of the modern theory of quantum dynamics and transport.

This mission formalizes Chapter 5 of Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009). The chapter covers the time evolution $\mathrm e^{-\mathrm itA}$ as a unitary group, Wiener's theorem on Fourier transforms of measures, and the abstract RAGE theorem with its Heisenberg-picture corollaries.

Setting

Let $\mathfrak H$ be a complex Hilbert space with inner product $\langle\cdot,\cdot\rangle$, conjugate linear in the first argument. An operator $A$ is a linear map defined on a subspace $\mathfrak D(A)$, its domain. $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A = A^*$. $\mathfrak L(\mathfrak H)$ denotes the bounded, everywhere defined operators.

A projection-valued measure $P$ assigns to each Borel set $\Omega \subseteq \mathbb R$ an orthogonal projection $P(\Omega)$, with $P(\mathbb R) = \mathbb I$ and $P(\bigcup_n \Omega_n)\psi = \sum_n P(\Omega_n)\psi$ for disjoint $\Omega_n$. The spectral measure of $\psi$ is the finite Borel measure $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle$. The spectral theorem says that every self-adjoint $A$ is $A = \int \lambda\, dP(\lambda)$ for a unique $P = P_A$. Then $\mathfrak D(A) = \{\psi \mid \int\lambda^2\, d\mu_\psi < \infty\}$ and $\langle\psi, A\psi\rangle = \int\lambda\, d\mu_\psi(\lambda)$. For a bounded Borel function $f$, $f(A)$ is the bounded operator with $\langle\psi, f(A)\psi\rangle = \int f\, d\mu_\psi$. The time evolution is $U(t) = \mathrm e^{-\mathrm itA}$, the case $f(\lambda) = \mathrm e^{-\mathrm it\lambda}$.

The spectral subspaces are

$$\mathfrak H_{ac} = \{\psi \mid \mu_\psi \ll \text{Lebesgue}\},\quad \mathfrak H_{sc} = \{\psi \mid \mu_\psi \text{ singular, without atoms}\},\quad \mathfrak H_{pp} = \{\psi \mid \mu_\psi \text{ supported on a countable set}\},$$

and the continuous subspace is $\mathfrak H_c = \mathfrak H_{ac} \oplus \mathfrak H_{sc}$. The projectors $P^{ac}, P^c, P^{pp}$ are the orthogonal projections onto these subspaces. $\sigma_p(A)$ is the set of eigenvalues of $A$.

A finite rank operator is a $K \in \mathfrak L(\mathfrak H)$ with finite dimensional range. The compact operators $\mathfrak C(\mathfrak H)$ are the norm closure of the finite rank operators. For $z$ in the resolvent set $\rho(A)$, $R_A(z) = (A - z)^{-1} \in \mathfrak L(\mathfrak H)$. An operator $K$ is relatively compact with respect to $A$ if $K R_A(z) \in \mathfrak C(\mathfrak H)$ for one $z \in \rho(A)$; in particular $\mathfrak D(A) \subseteq \mathfrak D(K)$. The Fourier transform of a finite complex Borel measure $\mu$ on $\mathbb R$ is $\hat\mu(t) = \int_{\mathbb R} \mathrm e^{-\mathrm it\lambda}\, d\mu(\lambda)$.

Formalization targets

Goal: the RAGE theorem (Theorem 5.7)

Let $A$ be self-adjoint and let $K_n \in \mathfrak L(\mathfrak H)$ be relatively compact operators converging strongly to $\mathbb I$. Then

$$\mathfrak H_c = \Big\{\psi \;\Big|\; \lim_{n\to\infty}\lim_{T\to\infty} \frac1T\int_0^T \|K_n\mathrm e^{-\mathrm itA}\psi\|\, dt = 0\Big\},\qquad \mathfrak H_{pp} = \Big\{\psi \;\Big|\; \lim_{n\to\infty}\sup_{t\ge0} \|(\mathbb I - K_n)\mathrm e^{-\mathrm itA}\psi\| = 0\Big\}.$$

Milestones

• Theorem 5.1. $U(t) = \mathrm e^{-\mathrm itA}$ is a strongly continuous one-parameter unitary group. $\lim_{t\to0}\frac1t(U(t)\psi - \psi)$ exists iff $\psi \in \mathfrak D(A)$, and then it equals $-\mathrm iA\psi$. $U(t)\mathfrak D(A) = \mathfrak D(A)$ and $AU(t) = U(t)A$.
• Theorem 5.4 (Wiener). $\displaystyle\lim_{T\to\infty}\frac1T\int_0^T|\hat\mu(t)|^2\,dt = \sum_{\lambda\in\mathbb R}|\mu(\{\lambda\})|^2$, and the sum is finite.
• Lemma 5.5. $\mathfrak C(\mathfrak H)$ is a closed $*$-ideal in $\mathfrak L(\mathfrak H)$.
• Theorem 5.6. For relatively compact $K$ and $\psi \in \mathfrak D(A)$: $\frac1T\int_0^T\|K\mathrm e^{-\mathrm itA}P^c\psi\|^2dt \to 0$ and $\|K\mathrm e^{-\mathrm itA}P^{ac}\psi\| \to 0$. For bounded $K$ this holds for all $\psi$.
• Theorem 5.8. $\displaystyle\lim_{T\to\infty}\frac1T\int_0^T \mathrm e^{\mathrm itA}K\mathrm e^{-\mathrm itA}\psi\,dt = \sum_{\lambda\in\sigma_p(A)}P_A(\{\lambda\})KP_A(\{\lambda\})\psi$ for $\psi \in \mathfrak D(A)$, and for all $\psi$ if $K$ is bounded.
• Corollary 5.9. Under the RAGE assumptions, the iterated time averages of $\mathrm e^{\mathrm itA}K_n\mathrm e^{-\mathrm itA}\psi$ and of $\mathrm e^{\mathrm itA}(\mathbb I - K_n)\mathrm e^{-\mathrm itA}\psi$ converge to $P^{pp}\psi$ and to $P^c\psi$.

Significance

The RAGE theorem connects the spectral types of the Hamiltonian with observable long-time behaviour. For Schrödinger operators $-\Delta + V$ on $L^2(\mathbb R^n)$, taking $K_n$ to be multiplication by the indicator of the ball of radius $n$ gives a sequence of relatively compact operators. The theorem then says that states in $\mathfrak H_c$ spend, on time average, a vanishing fraction of time in every ball, while states in $\mathfrak H_{pp}$ stay uniformly localized. Enß's proof of asymptotic completeness for short-range potentials rests on this characterization. The same argument, through Wiener's theorem, is used to relate the fractal dimensions of spectral measures to rates of quantum transport. Theorem 5.8 and Corollary 5.9 describe the asymptotic observables of the Heisenberg picture.

These results are classical and proved in the literature. They are not formalized. Mathlib has neither a spectral theorem nor a functional calculus for unbounded self-adjoint operators, and no decomposition of a Hilbert space by spectral type. What the platform has are Stone's theorem in the separate BookProof development (for weakly measurable groups, with its own structure of unbounded self-adjoint operators) and the discrete-time von Neumann mean ergodic theorem for contractions. The mean ergodic theorem is related to Theorem 5.8 with $K = \mathbb I$ but is a different statement. This mission formalizes the continuous-time, spectral-type-resolved statements.

Difficulty

The two sides of the RAGE characterization are defined in unrelated terms. $\mathfrak H_c$ and $\mathfrak H_{pp}$ are defined by properties of the scalar measures $\mu_\psi$, while the conditions in (5.14) concern norms of vectors moving under a unitary group and seen through operators that are only relatively compact. Wiener's theorem controls scalar quantities $\langle\varphi, \mathrm e^{-\mathrm itA}\psi\rangle$. Passing to norms $\|K\mathrm e^{-\mathrm itA}\psi\|$ needs compactness, and relative compactness only gives compactness after composing with a resolvent, which is where the restriction to $\mathfrak D(A)$ in Theorems 5.6 and 5.8 comes from. The pure point characterization needs control that is uniform in $t \ge 0$, so a limit over $n$ has to be exchanged with a supremum over all times. The limits in (5.14) and (5.19)–(5.20) are iterated, not joint, and a naive exchange of the two limits is not justified. Summing over $\sigma_p(A)$ in (5.18) needs an unconditionally convergent sum over a possibly uncountable index set. Wiener's theorem itself needs a Fubini argument for a complex measure against its conjugate.

Formalization scope

The formalization uses Lean 4 with Mathlib. Operators are partially defined linear maps (LinearPMap, H →ₗ.[ℂ] H) on a complex Hilbert space. Self-adjointness is Mathlib's IsSelfAdjoint, which includes density of the domain. The Hilbert space is not assumed separable.

The spectral theorem is not part of this mission. Every statement about $A$ takes a projection-valued measure $P$ on the Borel sets of $\mathbb R$ as data, together with the hypothesis that $A = \int\lambda\, dP(\lambda)$: $\mathfrak D(A) = \{\psi \mid \int\lambda^2 d\mu_\psi < \infty\}$ and $\langle\psi, A\psi\rangle = \int\lambda\,d\mu_\psi$ there. This is the form the spectral theorem guarantees, and it makes $P_A = P$. The time evolution $\mathrm e^{-\mathrm itA}$ is the bounded operator $P(\lambda \mapsto \mathrm e^{-\mathrm it\lambda})$, determined by its quadratic form, and $\mathrm e^{\mathrm itA}$ is its value at $-t$. Nothing else the book derives is assumed.

The spectral subspaces are sets of vectors defined only from the spectral measures, as above, and $\mathfrak H_c$ is the set of sums of a vector of $\mathfrak H_{ac}$ and a vector of $\mathfrak H_{sc}$. A formalization that defined $\mathfrak H_c$ or $\mathfrak H_{pp}$ by the dynamical conditions of (5.14) would make the goal a tautology; that is ruled out here. $P^c$, $P^{ac}$, $P^{pp}$ are the orthogonal projections onto the closed linear spans of these sets. Compact operators are the norm closure of the finite rank operators (the book's definition), not Mathlib's IsCompactOperator. Relative compactness asks for one $z \in \rho(A)$, its resolvent $R$, and a compact $C$ with $\operatorname{Ran} R \subseteq \mathfrak D(K)$ and $KR = C$. "$K$ bounded" means an everywhere defined $K \in \mathfrak L(\mathfrak H)$.

Iterated limits $\lim_n\lim_T$ are stated as: for every $n$ the inner limit exists, and the sequence of inner limits converges. The supremum over $t \ge 0$ is taken in $[0,\infty]$. Time averages use interval integrals, with Bochner integrals for vector-valued integrands; all integrands are continuous in $t$. Wiener's theorem uses Mathlib's ComplexMeasure ℝ and its vector-measure integral. The sum over $\lambda \in \mathbb R$ is an unconditional sum whose summability is part of the conclusion, and the sum over $\sigma_p(A)$ is an unconditional sum in $\mathfrak H$. The Fourier transform has the book's normalization.

A complete development needs a functional calculus for projection-valued measures (multiplicativity, strong continuity in the function argument), the reduction of $A$ by the spectral subspaces (Lemma 3.19), the Riemann–Lebesgue lemma for absolutely continuous measures, and the approximation of compact operators by finite rank ones. These pieces are reusable across the rest of the book, notably for scattering theory. Proofs of any milestone, and of such supporting lemmas, are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009. doi:10.1090/gsm/099. Chapter 5, pp. 123–132.
• D. Ruelle, A remark on bound states in potential-scattering theory, Il Nuovo Cimento A 61 (1969), 655–662. doi:10.1007/BF02819607.
• W. O. Amrein and V. Georgescu, On the characterization of bound states and scattering states in quantum mechanics, Helvetica Physica Acta 46 (1973), 635–658 (archive: e-periodica.ch).
• V. Enss, Asymptotic completeness for quantum mechanical potential scattering. I. Short range potentials, Communications in Mathematical Physics 61 (1978), 285–291. doi:10.1007/BF01940771.
• M. H. Stone, On one-parameter unitary groups in Hilbert space, Annals of Mathematics 33 (1932), 643–648. doi:10.2307/1968538.

Motivation

Periodic solutions are the simplest non-stationary long-time behaviour of an autonomous system $\dot x = f(x)$: limit cycles in oscillators and population models, closed orbits of conservative systems. The first question about a periodic orbit is whether it is stable. Poincaré introduced the first-return map on a transversal section, which turns this question into a question about a fixed point of a map in one dimension less. Floquet theory attacks the same question through the linear periodic system obtained by linearizing along the orbit. This mission formalizes Chapter 12, §§12.1–12.2 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012; author's preliminary version, DOI of the published book). That chapter proves the two approaches agree and derives the standard stability and persistence criteria from this.

Setting

Let $M \subseteq \mathbb{R}^n$ be open, $f \in C^k(M, \mathbb{R}^n)$ with $k \ge 1$, and let $\Phi(t, x)$ be the flow of $\dot x = f(x)$ with maximal intervals $I_x$: $t \mapsto \Phi(t,x)$ is the unique maximal solution with $\Phi(0,x) = x$. A point $x_0 \in M$ is periodic with period $T > 0$ if $\Phi(T, x_0) = x_0$ and $\Phi(t, x_0) \neq x_0$ for $0 < t < T$. Its orbit $\gamma(x_0) = \{\Phi(t, x_0)\}$ is then a closed curve.

Linearization along the orbit. Put $A(t) = df_{\Phi(t, x_0)}$, a $T$-periodic matrix. The first variational equation is $\dot y = A(t) y$, and $\Pi_{x_0}(t, t_0)$ denotes its principal matrix solution: $\partial_t \Pi = A(t)\Pi$, $\Pi(t_0, t_0) = \mathbb{I}$. The monodromy matrix based at $\Phi(t_0,x_0)$ is

$$M_{x_0}(t_0) = \frac{\partial \Phi_T}{\partial x}\big(\Phi(t_0, x_0)\big).$$

The Poincaré map. A transversal section is $\Sigma = \{x \in U \mid S(x) = 0\}$ with $U$ open, $S \in C^k(U)$, $\partial S/\partial x \ne 0$ and $(\partial S/\partial x)\, f \neq 0$ on $\Sigma$. If $x_0 \in \Sigma$ there is a $C^k$ return time $\tau$ near $x_0$ with $\tau(x_0) = T$ and $\Phi(\tau(y), y) \in \Sigma$. The Poincaré map is

$$P_\Sigma(y) = \Phi(\tau(y), y).$$

Its derivative $dP_\Sigma(x_0)$ is a linear map of the $(n-1)$-dimensional tangent space $T_{x_0}\Sigma = \ker \frac{\partial S}{\partial x}(x_0)$ into itself.

Stability. The orbit $\gamma$ is stable if every neighborhood $U$ of $\gamma$ contains a neighborhood $V$ of $\gamma$ from which solutions stay in $U$ for all $t \ge 0$. It is asymptotically stable if moreover $d(\Phi(t,x), \gamma) \to 0$ for all $x$ in some neighborhood of $\gamma$. A periodic orbit is hyperbolic if $dP_\Sigma(x_0)$ has no eigenvalue on the unit circle.

Formalization targets

Goal: Theorem 12.4

For every $t_0 \in \mathbb{R}$,

$$\chi_{M_{x_0}(t_0)}(X) = (X - 1)\,\chi_{dP_\Sigma(x_0)}(X),$$

where $\chi$ is the characteristic polynomial. So the eigenvalues of $dP_\Sigma(x_0)$ together with the single value $1$ are exactly the eigenvalues of the monodromy matrix, with multiplicities. In particular they depend neither on the section $\Sigma$ nor on the base point on the orbit.

Milestones

• Lemma 12.1. $\Pi_{x_0}(t,t_0) = \frac{\partial\Phi_{t-t_0}}{\partial x}(\Phi(t_0,x_0))$, and $f(\Phi(t,x_0)) = \Pi_{x_0}(t,t_0) f(\Phi(t_0,x_0))$.
• Corollary 12.3. If every eigenvalue of $dP_\Sigma(x_0)$ has modulus $< 1$, then $\gamma(x_0)$ is asymptotically stable.
• Corollary 12.5. $\det dP_\Sigma(x_0) = \det M_{x_0}(t_0) \neq 0$, and $P_\Sigma$ is a local $C^k$ diffeomorphism of $\Sigma$ at $x_0$.
• Lemma 12.6. For $n = 2$, $\gamma(x_0)$ is asymptotically stable if $\int_0^T \operatorname{div} f(\Phi(t,x_0))\,dt < 0$ and unstable if the integral is positive.
• Lemma 12.7. If $f(x,0)$ has a hyperbolic periodic orbit through $x_0$ and $f(x,\mu)$ is $C^k$, then on a neighborhood of $\mu = 0$ there is a $C^k$ family $x_0(\mu)$ with $x_0(0) = x_0$ and each $x_0(\mu)$ periodic for $f(\cdot,\mu)$.

Significance

The result. Theorem 12.4 is the bridge between the two standard tools for periodic orbits. The Floquet multipliers of $\dot y = A(t)y$ can often be computed or estimated, for instance through Liouville's formula $\det M_{x_0}(t_0) = \exp\int_0^T \operatorname{div} f(\Phi(t,x_0))\,dt$. The Poincaré map is where the dynamics is decided, for instance through the fixed-point stability theory of maps. Corollaries 12.3 and 12.5 and Lemma 12.6 are the resulting stability tests. Lemma 12.7 is the structural-stability statement for hyperbolic orbits that bifurcation theory starts from. Theorems 12.8–12.10 (stable manifolds of periodic orbits) build on the same objects.

Formalizing it. All results are classical and proved in the book. None has a machine-checked proof on the platform or, as far as is known, in Mathlib, which has neither Poincaré maps nor the linearization of flows along orbits. The work is a formalization of the known proofs. It needs differentiability of the flow with respect to initial conditions, and that part is reusable across the whole of qualitative ODE theory.

Difficulty

The algebra of Theorem 12.4 is short. The two linear maps act on different spaces: $M_{x_0}(0)$ on $\mathbb{R}^n$, and $dP_\Sigma(x_0)$ on the hyperplane $T_{x_0}\Sigma$. That hyperplane is in general not orthogonal to $f(x_0)$, not a coordinate hyperplane, and not invariant under $M_{x_0}(0)$. Any comparison has to go through the derivative of $y \mapsto \Phi(\tau(y), y)$, which involves the derivative of the implicitly defined return time. Behind all this sits the differentiability of $\Phi$ in $x$ and the variational equation it satisfies, which Mathlib does not provide for local flows. For the stability milestones, the delicate step is passing from the discrete iterates of $P_\Sigma$ on $\Sigma$ back to the continuous flow near the whole orbit. That requires uniform control over one period.

Formalization scope

The state space is Fin n → ℝ. Norm-dependent notions (distance to the orbit, neighborhoods) do not depend on the choice of norm. The flow is local: IsMaximalFlow f M I Φ characterizes $\Phi$ and $I_x$ by maximality and uniqueness, and $\Phi$'s values outside its domain are never used. Derivatives are Mathlib's fderiv. The section $\Sigma$ is the book's general $\{S = 0\}$ with $(\partial S/\partial x)f \neq 0$, not a hyperplane chosen orthogonal to $f(x_0)$. The return time $\tau$ is any $C^k$ function on a neighborhood of $x_0$ with $\tau(x_0) = T$ and $\Phi(\tau(y),y) \in \Sigma$; such a function agrees with the book's $\tau$ near $x_0$. $dP_\Sigma(x_0)$ is an endomorphism L of LinearMap.ker (fderiv ℝ S x₀) that agrees with the derivative of $y \mapsto \Phi(\tau(y), y)$ there (IsPoincareDerivative). Theorems 12.4 and 12.5 assert that it exists. Eigenvalues are complex roots of characteristic polynomials.

Conventions and readings:

• The goal compares characteristic polynomials, so multiplicities count. Equality of eigenvalue sets, a statement at a single convenient $t_0$, or a hyperplane section would each be weaker than the book's theorem and do not count as solving the goal.
• The monodromy matrix is $\frac{\partial\Phi_T}{\partial x}(\Phi(t_0,x_0))$. The book prints $\Phi_{T-t_0}$ on p. 316, a typo inconsistent with (12.5) and (12.8).
• "Periodic orbit" means positive least period. Fixed points are excluded, since there is no transversal section through them. In dimension $n \le 1$ no such orbit exists, and the statements are vacuous there as in the book.
• "Hyperbolic periodic orbit" is not defined in the preliminary version. The definition used is the one the proof of Lemma 12.7 uses: no eigenvalue of $dP_\Sigma(x_0)$ on the unit circle, for some transversal section.
• Lemma 12.7: "in a sufficiently small neighborhood of $0$" is read as: there exists an open $W \ni 0$ inside the parameter set on which $x_0(\cdot)$ is $C^k$. The parameter lies in $\mathbb{R}^p$.
• Corollary 12.5: "local diffeomorphism at $x_0$" is read as: $P_\Sigma$ maps $W \cap \Sigma$ bijectively onto $W' \cap \Sigma$ for open $W, W' \ni x_0$, with an inverse that is the restriction of a $C^k$ map on $W'$.
• (12.1) is stated for all $x$ in a neighborhood of the orbit. The book writes $U(x_0)$ right after introducing $U(\gamma(x_0))$.

Needed infrastructure: existence, uniqueness and $C^k$ dependence on initial conditions for local flows; the implicit function theorem (Mathlib); characteristic polynomials and determinants of endomorphisms of finite-dimensional subspaces (Mathlib); Liouville's formula; stability of fixed points of $C^1$ maps with contracting linearization. Contributions of any of these as standalone lemmas are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012. https://doi.org/10.1090/gsm/140 (preliminary version: https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf)
• H. Poincaré, Mémoire sur les courbes définies par une équation différentielle, J. Math. Pures Appl. (3) 7 (1881) 375–422. http://www.numdam.org/item/JMPA_1881_3_7__375_0/
• G. Floquet, Sur les équations différentielles linéaires à coefficients périodiques, Ann. Sci. ÉNS (2) 12 (1883) 47–88. https://doi.org/10.24033/asens.220
• P. Hartman, Ordinary Differential Equations, 2nd ed., SIAM Classics in Applied Mathematics 38, 2002. https://doi.org/10.1137/1.9780898719222