All missions

Motivation

Gradient methods are the workhorse of large-scale nonlinear optimization and of the training of statistical models. In practice the direction actually used is rarely the exact negative gradient: it may be scaled, computed incrementally one data component at a time, or perturbed by approximation error. The classical convergence theory of such methods often assumes that the iterates stay bounded, that the objective is bounded below, or that the errors vanish at a prescribed rate, and these assumptions must then be checked separately for each method.

Bertsekas and Tsitsiklis (2000) proved convergence results for gradient methods with errors that need none of these assumptions. Their deterministic result (Proposition 1) allows a general descent direction together with an error whose size is proportional to the stepsize, and concludes that either the objective values diverge to $-\infty$ or they converge and the gradients tend to zero. It applies, among others, to the incremental gradient method for a sum of functions (Proposition 2 of the same paper), which underlies backpropagation-style training. The stochastic counterpart (Proposition 3, zero-mean errors) is the subject of a companion mission.

Setting

Throughout, $f:\mathbb R^n\to\mathbb R$ is a continuously differentiable function whose gradient is Lipschitz continuous: for some constant $L$,

$$\|\nabla f(x)-\nabla f(\bar x)\|\le L\|x-\bar x\|\qquad\forall x,\bar x\in\mathbb R^n. \tag{2.1}$$

Here $\|\cdot\|$ is the Euclidean norm and $x'y$ the standard inner product. The gradient method with errors generates a sequence of iterates

$$x_{t+1}=x_t+\gamma_t(s_t+w_t),\qquad t=0,1,\dots,$$

where $\gamma_t>0$ is the stepsize, $s_t$ is a descent direction and $w_t$ is an error vector. Nothing is assumed about how $s_t$ and $w_t$ are produced, beyond the two conditions below, which hold for some positive scalars $c_1,c_2,p,q$ and every $t$:

$$c_1\|\nabla f(x_t)\|^2\le-\nabla f(x_t)'s_t,\qquad\|s_t\|\le c_2\bigl(1+\|\nabla f(x_t)\|\bigr), \tag{2.2}$$ $$\|w_t\|\le\gamma_t\bigl(q+p\|\nabla f(x_t)\|\bigr). \tag{2.3}$$

The stepsizes are diminishing in the standard sense:

$$\sum_{t=0}^\infty\gamma_t=\infty,\qquad\sum_{t=0}^\infty\gamma_t^2<\infty.$$

A stationary point of $f$ is a point $\bar x$ with $\nabla f(\bar x)=0$; a limit point of $(x_t)$ is the limit of some subsequence.

Formalization targets

Goal: Proposition 1 (p. 630)

Under (2.1), (2.2), (2.3) and the stepsize conditions, either

$$f(x_t)\to-\infty,$$

or else $f(x_t)$ converges to a finite value and

$$\lim_{t\to\infty}\nabla f(x_t)=0.$$

Furthermore, every limit point of $(x_t)$ is a stationary point of $f$.

Milestones

The milestones follow the paper's own argument, in order.

1. Lemma 1 (p. 629). For real sequences with $W_t\ge0$, $Y_{t+1}\le Y_t-W_t+Z_t$ and $\sum_{t=0}^T Z_t$ convergent, either $Y_t\to-\infty$, or $Y_t$ converges and $\sum_t W_t<\infty$.
2. (2.4) (p. 630). Under (2.1), $f(x+z)\le f(x)+z'\nabla f(x)+\tfrac L2\|z\|^2$ for all $x,z$.
3. (2.5) (p. 631). For some $\beta_1,\beta_2>0$ and all sufficiently large $t$, $f(x_{t+1})\le f(x_t)-\gamma_t\beta_1\|\nabla f(x_t)\|^2+\gamma_t^2\beta_2$.
4. (2.6) (p. 631). Either $f(x_t)\to-\infty$, or $f(x_t)$ converges and $\sum_t\gamma_t\|\nabla f(x_t)\|^2<\infty$.
5. After (2.6) (p. 631). If $f(x_t)\not\to-\infty$, then $\liminf_{t\to\infty}\|\nabla f(x_t)\|=0$.

Significance

The result. Proposition 1 separates two concerns that are usually entangled: what the method guarantees, and what must be known about $f$. It concludes stationarity of all limit points and convergence of the gradients to zero without assuming that the iterates are bounded or that $f$ is bounded below; when $f$ is bounded below the first alternative is excluded and $\nabla f(x_t)\to0$ follows outright. Because $s_t$ need not be the negative gradient and $w_t$ need not vanish faster than the stepsize, the result covers scaled gradient methods, incremental gradient methods for sums of functions, and gradient methods with deterministic approximation error. The descent inequality (2.4) and the deterministic supermartingale-type Lemma 1 are standard tools that recur throughout optimization theory.

Formalizing it. The proposition is proved in the paper; it has not been machine-checked. A formal proof would give a reusable, verified convergence theorem for a broad class of first-order methods on $\mathbb R^n$, together with a formal descent lemma for functions with Lipschitz gradient, which Mathlib does not currently state in this form, and a deterministic Robbins–Siegmund-type lemma for sequences.

Difficulty

The summability estimate (2.6) gives only $\liminf\|\nabla f(x_t)\|=0$. Passing to $\lim\nabla f(x_t)=0$ is the main step: the obvious argument (a summable series $\sum_t\gamma_t\|\nabla f(x_t)\|^2$ with $\sum_t\gamma_t=\infty$ forces the gradient norms to zero) is false in general, because a nonnegative sequence with these two properties may still have infinitely many large terms. What is missing is a bound on how far $\|\nabla f(x_t)\|$ can travel while the stepsizes are small, and only (2.1) and (2.2)–(2.3) together supply it. A second difficulty is that there is no boundedness of the iterates: every estimate must hold globally, and the error $w_t$ is controlled only relative to $\|\nabla f(x_t)\|$, which may be unbounded along the sequence.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $x'y$ is the real inner product ⟪x, y⟫_ℝ, and $\nabla f$ is Mathlib's gradient f; the hypothesis ContDiff ℝ 1 f makes it the true gradient. The paper's statement is for $\mathbb R^n$ and the formalization does not generalize to Hilbert spaces.
• The standing assumption (2.1) of §2 is part of every statement about $f$, as LipschitzWith L (gradient f) with L : ℝ≥0; this is equivalent to (2.1) for some real constant.
• The sequences $x_t,s_t,w_t$ and $\gamma_t$ are arbitrary data indexed from $t=0$, constrained only by the recursion and by (2.2), (2.3), $\gamma_t>0$ (all four constants $c_1,c_2,p,q$ are positive, as printed).
• $\sum_t\gamma_t=\infty$ is divergence of the partial sums to $+\infty$; $\sum_t\gamma_t^2<\infty$ is summability of nonnegative terms. In Lemma 1 the convergence of $\sum_t Z_t$ is convergence of the partial sums, not absolute convergence, since $Z_t$ may change sign.
• $\lim\inf$ is written out as "for every $\epsilon>0$, infinitely often below $\epsilon$", avoiding junk values of a lim inf of an unbounded sequence. Limit points are cluster points of the sequence.
• "Every limit point is stationary" is a separate conjunct, outside the dichotomy, exactly as on the page.
• The constants $\beta_1,\beta_2$ in (2.5) are existential. The milestones (2.5) and (2.6) retain the stepsize hypotheses of Proposition 1, where the paper derives them.
• A trivializing formalization would drop the "$-\infty$" alternative or require $f$ bounded below; neither is done. Instances satisfying all hypotheses with $f(x_t)\to-\infty$ and $\nabla f\not\to0$ exist (a linear $f$), so the first alternative is genuinely needed.
• Out of scope: Proposition 2 (the incremental gradient method of §3), which is a corollary of the goal, and the stochastic results of §4–§5.

Contributions welcome: proofs of the descent lemma and Lemma 1 (both reusable well beyond this mission), and of the steps (2.5)–(2.6) and the excursion argument.

Selected references

• D. P. Bertsekas and J. N. Tsitsiklis, Gradient Convergence in Gradient Methods with Errors, SIAM Journal on Optimization 10(3):627–642, 2000. https://doi.org/10.1137/S1052623497331063
• D. P. Bertsekas, Nonlinear Programming, 2nd ed., Athena Scientific, 1999.
• H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8

Motivation

A stochastic approximation algorithm is a recursion

$$x_{n+1}-x_n=\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$$

in $\mathbb R^d$, where $F$ is a vector field, $\gamma_n$ are small step sizes and $U_{n+1}$ is noise. Such recursions go back to Robbins and Monro's root-finding scheme (Robbins–Monro 1951) and underlie stochastic gradient descent, temporal-difference learning, adaptive control and learning in games. The ODE method studies them by comparing the iterates with the trajectories of $\dot x=F(x)$.

Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (and the iterates are bounded, or $F$ is Lipschitz and bounded on a neighbourhood of them), the interpolated process is an asymptotic pseudotrajectory of the flow of $F$. A probabilistic step then verifies A1 for concrete noise models. This mission formalizes the first such verification, Proposition 4.2: martingale difference noise with bounded $q$-th moments and step sizes with $\sum_n\gamma_n^{1+q/2}<\infty$. The result is described as a particular case of a general theorem of Métivier and Priouret (1987); the same estimates reappear later in the notes.

Setting

Let $\{\gamma_n\}_{n\ge1}$ be a deterministic sequence with $\gamma_n\ge0$, $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$ (a step sequence). Put $\tau_0=0$, $\tau_n=\sum_{i=1}^n\gamma_i$, and let

$$m(t)=\sup\{k\ge0:\ t\ge\tau_k\}$$

be the index of the step that contains time $t\ge0$. For a sequence $\{U_n\}_{n\ge1}$ define the piecewise constant processes $\bar U(t)=U_{m(t)+1}$ and $\bar\gamma(t)=\gamma_{m(t)+1}$, so that step $n+1$ occupies the time interval $[\tau_n,\tau_{n+1})$ of length $\gamma_{n+1}$.

Assumption A1 asks that for every $T>0$

$$\lim_{n\to\infty}\sup\Big\{\Big\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\|:\ k=n+1,\dots,m(\tau_n+T)\Big\}=0,$$

or, in the form the notes call equivalent, $\lim_{t\to\infty}\Delta(t,T)=0$ for every $T>0$, where

$$\Delta(t,T)=\sup_{0\le h\le T}\Big\|\int_t^{t+h}\bar U(s)\,ds\Big\|.$$

Let $(\Omega,\mathcal F,P)$ be a probability space with a nondecreasing sequence $\{\mathcal F_n\}$ of sub-$\sigma$-algebras, and $F:\mathbb R^d\to\mathbb R^d$ continuous. A sequence $\{x_n\}$ given by the recursion above is a Robbins–Monro algorithm if $\gamma$ is deterministic, $U_n$ is $\mathcal F_n$-measurable, and $E(U_{n+1}\mid\mathcal F_n)=0$.

Formalization targets

Goal: Proposition 4.2

For a Robbins–Monro algorithm and some real $q\ge2$, if

$$\sup_nE\big(\|U_{n+1}\|^q\big)<\infty\qquad\text{and}\qquad\sum_n\gamma_n^{1+q/2}<\infty,$$

then with probability one the realised noise sequence satisfies A1, in both of its forms, simultaneously for all $T>0$.

Milestones

1. Eq. (13), an instance of Burkholder's inequality with a universal constant $C_q$:

$$E\Big\{\sup_{n<k\le m(\tau_n+T)}\Big\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\|^q\Big\}\le C_q\,E\Big\{\Big[\sum_{i=n}^{m(\tau_n+T)-1}\gamma_{i+1}^2\|U_{i+1}\|^2\Big]^{q/2}\Big\}.$$

2. Inequality (14), for finite families with $\alpha_i\ge0$, $u>1$, $0<\delta<1$:

$$\Big(\sum_i|\alpha_i\beta_i|\Big)^u\le\Big(\sum_i\alpha_i^{\delta u/(u-1)}\Big)^{u-1}\sum_i\alpha_i^{(1-\delta)u}|\beta_i|^u.$$

3. Eq. (16): for every $T>0$ there is $C(q,T)$ with $E(\Delta(t,T)^q)\le C(q,T)\int_t^{t+T}\bar\gamma^{q/2}(s)\,ds$ for all $t\ge0$.
4. Eq. (17): $\sum_{k\ge0}E(\Delta(kT,T)^q)<\infty$ for every $T>0$.
5. Block comparison: $\Delta(t,T)\le2\Delta(kT,T)+\Delta((k+1)T,T)$ for $kT\le t<(k+1)T$.

Significance

Proposition 4.2 is the standard sufficient condition under which the ODE method applies to stochastic gradient-type recursions with martingale noise. With $q=2$ it covers step sizes with $\sum\gamma_n^2<\infty$ (for example $\gamma_n=1/n$) and noise with bounded variance; larger $q$ trades stronger moment assumptions for slower decay of the steps, down to $\sum\gamma_n^{1+q/2}<\infty$. Combined with Proposition 4.1 it shows that the interpolated process of a Robbins–Monro algorithm with bounded iterates is almost surely an asymptotic pseudotrajectory of the flow of $F$; the limit set theorems of the notes then locate the limit points of the algorithm.

The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would supply reusable pieces that Mathlib currently lacks, most notably a Burkholder (or Burkholder–Davis–Gundy) inequality for discrete-time vector martingales in $L^q$, and the continuous-time bookkeeping of the step processes $\bar U$, $\bar\gamma$ and the noise deviation $\Delta$, shared by the other missions of this series.

Difficulty

The obvious argument controls each window by Doob's $L^2$ maximal inequality and sums over windows. That works for $q=2$ only. For $q>2$ the second moment of the window sums is not summable under $\sum\gamma_n^{1+q/2}<\infty$, and one needs an $L^q$ maximal inequality whose right-hand side is the $q/2$-th moment of the square function. That inequality, Burkholder's, is not in Mathlib. Converting the square function into the moment bound requires a Hölder-type inequality with tuned exponents, and passing from the discrete sums to $\Delta(t,T)$ requires handling partial steps at both ends of $[t,t+h]$. A second subtlety is that A1 quantifies over all $T>0$: the almost-sure statement must hold on a single event of full probability for every $T$, not on an event that depends on $T$.

Formalization scope

The space is $\mathbb R^d$ as EuclideanSpace ℝ (Fin d); time is real; $q$ is a real number with $q\ge2$, and all powers are real powers of nonnegative quantities. The sequences $\gamma$ and $U$ are indexed by $\mathbb N$, and their values at $0$ are unused, as the paper indexes them from $1$. The filtration is a Mathlib Filtration ℕ, $U_{n+1}$ is required to be $\mathcal F_{n+1}$-strongly measurable and integrable, and the martingale difference condition is $E(U_{n+1}\mid\mathcal F_n)=0$ almost surely. Expectations of nonnegative quantities, the suprema in A1 and $\Delta$, and the moment bound are taken in $[0,\infty]$, so no default value of a non-integrable expectation or of an empty supremum can make a statement hold vacuously; the supremum over an empty range of $k$ is $0$.

The following readings are excluded and are not acceptable formalizations: a moment hypothesis that holds vacuously, a conditional expectation hypothesis on non-integrable noise, the conclusion "for each $T$, A1 holds almost surely" in place of "almost surely, A1 holds for all $T$", and $q$ fixed to $2$ or restricted to integers.

All hypotheses are satisfiable: $U=0$, $x=0$, $F=0$ and $\gamma_n=1/n$ with $q=2$ satisfy every one of them.

Contributions welcome: a general Burkholder inequality for discrete-time martingales in finite-dimensional spaces (reusable well beyond this mission), lemmas on the step processes and $\Delta$ (measurability, local integrability, additivity), and the proofs of the milestones.

Selected references

• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
• M. Métivier and P. Priouret, Théorèmes de convergence presque sûre pour une classe d'algorithmes stochastiques à pas décroissant, Probability Theory and Related Fields 74 (1987), 403–428.
• D. L. Burkholder, Distribution function inequalities for martingales, Annals of Probability 1 (1973), 19–42. https://doi.org/10.1214/aop/1176997023
• D. W. Stroock, Probability Theory: An Analytic View, Cambridge University Press, 1993.
• H. Robbins and S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586
• H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997.

Motivation

The irrationality measure $\mu(\pi)$ is the supremum of the $\mu$ for which $|\pi - p/q| < q^{-\mu}$ has infinitely many rational solutions $p/q$. Every irrational number has $\mu \ge 2$ (Dirichlet), almost every real number has $\mu = 2$, and it is conjectured that $\mu(\pi) = 2$. Known upper bounds:

• Mahler (1953): $42$, the first proof that $\pi$ is not a Liouville number.
• Mignotte (1974): $20.6$.
• Chudnovsky (1982): $19.8899944\ldots$
• Rhin–Viola (1993): $14.797074$.
• Hata (1993): $8.016045\ldots$
• Salikhov (2008): $7.606308\ldots$
• Zeilberger–Zudilin (2020): $7.103205334137\ldots$, the current record.

The campaign's first proved value is Mahler's $42$. This entry records Salikhov's bound.

Formalization target

The campaign template with the value $7.606309$ filled in: PiIrrationality.UpperBound (7.606309 : ℝ), i.e. $\mu(\pi) \le 7.606309$.

Value. The bound is quoted as $7.606308\ldots$ (e.g. by Zeilberger–Zudilin), a truncation. This entry rounds the last digit up to $7.606309$.

How the bound arises

Salikhov uses integrals of rational functions that are symmetric under a group of transformations (in the spirit of Rhin–Viola), which gives larger arithmetic savings in the common denominators than Hata's construction.

Significance

Each step down the list replaces Mahler's approximations with a sharper family. Formalizing $7.606309$ would build reusable explicit machinery: integral constructions of rational approximations to $\pi$, bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.

Selected references

• V. Kh. Salikhov, On the irrationality measure of $\pi$, Russian Math. Surveys 63 (2008), no. 3, 570–572.
• K. Mahler, On the approximation of $\pi$, Indag. Math. 15 (1953), 30–42.
• F. Beukers, A rational approach to $\pi$, Nieuw Arch. Wiskd. (5) 1 (2000), 372–379.
• Source table: https://teorth.github.io/optimizationproblems/constants/7a.html

Motivation

The irrationality measure $\mu(\pi)$ is the supremum of the $\mu$ for which $|\pi - p/q| < q^{-\mu}$ has infinitely many rational solutions $p/q$. Every irrational number has $\mu \ge 2$ (Dirichlet), almost every real number has $\mu = 2$, and it is conjectured that $\mu(\pi) = 2$. Known upper bounds:

• Mahler (1953): $42$, the first proof that $\pi$ is not a Liouville number.
• Mignotte (1974): $20.6$.
• Chudnovsky (1982): $19.8899944\ldots$
• Rhin–Viola (1993): $14.797074$.
• Hata (1993): $8.016045\ldots$
• Salikhov (2008): $7.606308\ldots$
• Zeilberger–Zudilin (2020): $7.103205334137\ldots$, the current record.

The campaign's first proved value is Mahler's $42$. This entry records Zeilberger–Zudilin's bound.

Formalization target

The campaign template with the value $7.103205334138$ filled in: PiIrrationality.UpperBound (7.103205334138 : ℝ), i.e. $\mu(\pi) \le 7.103205334138$.

Value. The paper states its bound as $7.103205334137\ldots$, a truncation. This entry rounds the last digit up to $7.103205334138$ so that the goal follows from the published proof.

How the bound arises

Zeilberger and Zudilin modify Salikhov's integrals and use the Almkvist–Zeilberger algorithm (creative telescoping) to find recurrences for them, then optimise the arithmetic and analytic estimates. This is the current record.

Significance

Each step down the list replaces Mahler's approximations with a sharper family. Formalizing $7.103205334138$ would build reusable explicit machinery: integral constructions of rational approximations to $\pi$, bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.

Selected references

• D. Zeilberger, W. Zudilin, The irrationality measure of $\pi$ is at most $7.103205334137\ldots$, Moscow J. Combin. Number Theory 9 (2020), no. 4, 407–419. https://arxiv.org/abs/1912.06345
• K. Mahler, On the approximation of $\pi$, Indag. Math. 15 (1953), 30–42.
• F. Beukers, A rational approach to $\pi$, Nieuw Arch. Wiskd. (5) 1 (2000), 372–379.
• Source table: https://teorth.github.io/optimizationproblems/constants/7a.html

Motivation

The irrationality measure $\mu(\pi)$ is the supremum of the $\mu$ for which $|\pi - p/q| < q^{-\mu}$ has infinitely many rational solutions $p/q$. Every irrational number has $\mu \ge 2$ (Dirichlet), almost every real number has $\mu = 2$, and it is conjectured that $\mu(\pi) = 2$. Known upper bounds:

• Mahler (1953): $42$, the first proof that $\pi$ is not a Liouville number.
• Mignotte (1974): $20.6$.
• Chudnovsky (1982): $19.8899944\ldots$
• Rhin–Viola (1993): $14.797074$.
• Hata (1993): $8.016045\ldots$
• Salikhov (2008): $7.606308\ldots$
• Zeilberger–Zudilin (2020): $7.103205334137\ldots$, the current record.

The campaign's first proved value is Mahler's $42$. This entry records Hata's bound.

Formalization target

The campaign template with the value $8.016046$ filled in: PiIrrationality.UpperBound (8.016046 : ℝ), i.e. $\mu(\pi) \le 8.016046$.

Value. The paper computes the exponent as $7.016045\ldots + 1$ and states the rounded bound $8.0161$. This entry rounds the computed value's last digit up to $8.016046$, which is still below the paper's $8.0161$ and above $8.016045\ldots$.

How the bound arises

Hata obtains simultaneous approximations to $1, \pi, \log 2$ from complex contour integrals of Legendre type, with extra arithmetic savings from primes that divide the coefficients to a predictable extent. His linear-form measure is $7.016045\ldots$, giving $\mu(\pi) \le 8.016045\ldots$ (stated in the paper as $8.0161$). It stood as the record for about fifteen years.

Significance

Each step down the list replaces Mahler's approximations with a sharper family. Formalizing $8.016046$ would build reusable explicit machinery: integral constructions of rational approximations to $\pi$, bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.

Selected references

• M. Hata, Rational approximations to $\pi$ and some other numbers, Acta Arith. 63 (1993), no. 4, 335–349. http://matwbn.icm.edu.pl/ksiazki/aa/aa63/aa6344.pdf
• K. Mahler, On the approximation of $\pi$, Indag. Math. 15 (1953), 30–42.
• F. Beukers, A rational approach to $\pi$, Nieuw Arch. Wiskd. (5) 1 (2000), 372–379.
• Source table: https://teorth.github.io/optimizationproblems/constants/7a.html

Motivation

A stochastic approximation algorithm is a recursion $x_{n+1}=x_n+\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$ with decreasing steps $\gamma_n$ and noise $U_n$. Stochastic gradient descent, the Robbins–Monro procedure, reinforcement-learning updates and learning dynamics in games all have this form. The ODE method compares such a recursion with the deterministic dynamics $\dot x=F(x)$. Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) do this in two steps. First, the limit set of the interpolated process is internally chain transitive for the semiflow of $F$ (Theorem 5.7, the subject of mission 1 of this series). Second, internally chain transitive sets are located using properties of the dynamics alone.

The most common tool in the second step is a Lyapounov function: a function that decreases strictly along every trajectory outside a set $\Lambda$ and is constant on $\Lambda$. Proposition 6.4 of the notes states exactly when such a function forces every internally chain transitive set into $\Lambda$. It is the step behind the convergence of stochastic gradient algorithms to critical points (Corollary 6.7) and behind convergence results for learning in potential games.

Timeline.

• Conley (Isolated Invariant Sets and the Morse Index, CBMS 38, 1978) introduced chain recurrence and the attractor–repeller description of it.
• Benaïm and Hirsch (J. Dyn. Diff. Eq. 8, 1996) identified limit sets of asymptotic pseudotrajectories with internally chain transitive sets.
• Benaïm (SIAM J. Control Optim. 34, 1996) developed the dynamical-systems approach to stochastic approximation built on these notions.
• Bowen (J. Differential Equations 18, 1975) characterized chain transitivity by the absence of proper attractors, the content of Proposition 5.3 of the notes.
• The 1999 notes state the Lyapounov criterion in the form used here, for semiflows on arbitrary metric spaces.

Setting

Let $(M,d)$ be a metric space, with no compactness or completeness assumed. A semiflow $\Phi$ on $M$ is a continuous map $\mathbb R_+\times M\to M$, $(t,x)\mapsto\Phi_t(x)$, with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$.

• A set $A$ is invariant if $\Phi_t(A)=A$ for every $t\ge0$. For an invariant $\Lambda$, the restriction $\Phi|\Lambda$ is the semiflow $\Phi$ acting on $\Lambda$.
• For $\delta,T>0$, a $(\delta,T)$-pseudo-orbit from $a$ to $b$ is a list of points $y_0,\dots,y_k$ ($k\ge1$) and times $t_0,\dots,t_{k-1}\ge T$ with $d(y_0,a)<\delta$, $d(\Phi_{t_j}(y_j),y_{j+1})<\delta$ for $j<k$, and $y_k=b$.
• A set $L$ is internally chain transitive if it is nonempty, compact and invariant, and for all $a,b\in L$ and all $\delta,T>0$ there is a $(\delta,T)$-pseudo-orbit of $\Phi|L$, so with every $y_i\in L$, from $a$ to $b$.
• An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ on which $\mathrm{dist}(\Phi_t x,A)\to0$ uniformly. Its basin is the set of points $x$ with $\mathrm{dist}(\Phi_t x,A)\to0$.
• Let $\Lambda\subset M$ be compact and invariant. A continuous $V:M\to\mathbb R$ is a Lyapounov function for $\Lambda$ if $t\mapsto V(\Phi_t(x))$ is constant for $x\in\Lambda$ and strictly decreasing for $x\notin\Lambda$.

Formalization targets

Goal: Proposition 6.4

Let $\Lambda$ be compact invariant and $V$ a Lyapounov function for $\Lambda$, and assume that $V(\Lambda)$ has empty interior in $\mathbb R$. Then for every internally chain transitive set $L$,

$$L\subset\Lambda\qquad\text{and}\qquad V|_L\ \text{is constant}.$$

Milestones

1. Lemma 5.2. If $U$ is open with compact closure and $\Phi_T(\overline U)\subset U$ for some $T>0$, there is an attractor $A\subset U$ whose basin contains $\overline U$.
2. Proposition 5.3. For nonempty $\Lambda$: internally chain transitive $\iff$ connected and internally chain recurrent $\iff$ compact invariant, and $\Phi|\Lambda$ has no proper attractor.
3. The claim of the proof of 6.4. For $L$ internally chain transitive and $v^*=\inf_L V$: $L\cap\Lambda\ne\emptyset$ and $v^*=\inf_{L\cap\Lambda}V$.
4. The sublevel step of the proof of 6.4. For every $c>v^*$ with $c\notin V(\Lambda)$, $V<c$ on all of $L$.

Significance

The result. Proposition 6.4 converts a statement about real numbers, that $V(\Lambda)$ has empty interior, into a statement about dynamics: the chain recurrent behaviour of $\Phi$ is confined to $\Lambda$. With Theorem 5.7 it gives the following. If $\Phi$ has such a Lyapounov function, then the limit set of any precompact asymptotic pseudotrajectory, in particular of a bounded stochastic approximation process, lies in $\Lambda$, and $V$ is constant on it. When $\Lambda$ is the set of equilibria and $V(\Lambda)$ is Lebesgue-null by Sard's theorem, this is the convergence of stochastic gradient algorithms to connected sets of critical points (Corollary 6.7). Remark 6.5 gives a flow on the circle with a strict Lyapounov function, where the circle itself is internally chain transitive. So the empty-interior hypothesis cannot be removed.

Formalizing it. The result is proved, in the notes and in the earlier literature. No machine-checked version of chain recurrence for semiflows on metric spaces, Conley's attractor lemma, or Bowen's characterization of chain transitive sets is known to us. The mission therefore adds the following:

• a formal definition layer for these notions on Mathlib's Flow;
• formal proofs of Lemma 5.2 and Proposition 5.3, which are reused across this series (missions 1 and 6);
• the Lyapounov criterion itself.

Difficulty

The obvious argument does not work. It runs: $V$ decreases along trajectories, so along an orbit in $L$ the value of $V$ must settle on $\Lambda$. But points of an internally chain transitive set are joined only by pseudo-orbits. At each of the $k$ jumps, $V$ may increase by an amount that is small but not controlled in number, so monotonicity of $V$ along true trajectories says nothing directly about $L$. Remark 6.5 shows that the conclusion is genuinely false without a condition on $V(\Lambda)$. The difficulty is therefore global: pseudo-orbits that climb back up $V$ through many small jumps must be excluded using information about the restricted semiflow $\Phi|L$ as a whole, not the monotonicity of $V$ along single trajectories. Milestones 1 and 2 are the general facts about chain transitive sets that this requires, and their own proofs involve compactness and uniform-continuity estimates over arbitrarily long pseudo-orbits.

Formalization scope

• Representation. $M$ is any MetricSpace, and the semiflow is Flow ℝ≥0 M.
• Invariance is equality $\Phi_t(A)=A$ for every $t$, not inclusion.
• Pseudo-orbits have at least one trajectory piece ($k\ge1$), times $\ge T$, an exact endpoint, and, in the internal notions, all their points in the set.
• Nonemptiness. Internally chain transitive and internally chain recurrent sets are nonempty by definition. Accordingly, Proposition 5.3 assumes $\Lambda\neq\emptyset$ and Lemma 5.2 assumes $U\neq\emptyset$.
• Lyapounov function. The predicate contains the standing assumptions of its definition: $\Lambda$ is compact and invariant, $V$ is continuous, $V(\Phi_t x)=V(x)$ on $\Lambda$, and $t\mapsto V(\Phi_t x)$ is strictly antitone off $\Lambda$.
• Empty interior is interior (V '' Λ) = ∅ in $\mathbb R$, not countability, finiteness or measure zero.
• Infima are stated with IsGLB, not a real sInf.

The following formalizations are trivializing and are excluded:

• chains with no jumps, under which every point is chain recurrent;
• invariance as inclusion;
• a non-strict decrease condition, under which constant functions are Lyapounov functions and the goal is false;
• chains of $\Phi$ that leave $L$, a strictly weaker notion;
• quantifying only over limit sets instead of every internally chain transitive set.

A complete development needs elementary facts about ω-limit sets of points of a compact invariant set: they are nonempty, compact and invariant. It also needs the attractor construction $A=\bigcap_{t\ge0}\overline{\bigcup_{s\ge t}\Phi_s(U)}$ and the open sets $\{y: x\hookrightarrow_{\delta,T}y\}$ used in Proposition 5.3. These are reusable for any work on Conley theory. Contributions of any of these lemmas, or of proofs of the milestones in any order, are welcome.

Selected references

• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Benaïm, M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218613
• M. Benaïm, A dynamical system approach to stochastic approximations, SIAM J. Control Optim. 34 (1996), 437–472. https://doi.org/10.1137/S0363012993253534
• C. Conley, Isolated Invariant Sets and the Morse Index, CBMS Regional Conference Series in Mathematics 38, AMS, 1978. https://doi.org/10.1090/cbms/038
• R. Bowen, ω-limit sets for Axiom A diffeomorphisms, J. Differential Equations 18 (1975), 333–339. https://doi.org/10.1016/0022-0396(75)90065-0

Motivation

Reinforcement learning formulates control as maximizing reward accumulated over time. For continuing tasks, where interaction never terminates, the standard textbook objective is the discounted return with a discount rate $\gamma < 1$. Chapter 10 of Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018), argues that once values are approximated by a function of features rather than stored per state, this objective is the wrong one, and it proposes the average-reward setting, long standard in dynamic programming (Puterman, Markov Decision Processes, 1994), as its replacement.

The central piece of evidence is a short calculation printed in the box The Futility of Discounting in Continuing Problems (p. 254). If one tries to rescue discounting by averaging discounted values over the states the policy actually visits, the resulting objective is a constant multiple of the average reward, so the discount rate has no effect on which policy is preferred. This mission formalizes that calculation together with the definitions of §10.3 that it rests on, and the two exercises of §10.3 that illustrate the differential value (10.13).

Setting

A finite MDP has finite state set $\mathcal S$, finite action set $\mathcal A$, finite reward set $\mathcal R \subset \mathbb R$ and dynamics $p(s', r \mid s, a)$, a probability distribution over next state and reward for each state–action pair (3.2)–(3.3). Write $p(s' \mid s, a) = \sum_r p(s', r\mid s,a)$. A policy $\pi(a \mid s)$ is a distribution over actions for each state. It turns the MDP into a Markov chain with transition matrix $P_\pi(s, s') = \sum_a \pi(a\mid s)\, p(s'\mid s,a)$ and expected one-step reward $r_\pi(s) = \sum_a \pi(a\mid s)\sum_{s',r} p(s',r\mid s,a)\, r$, so that $\Pr\{S_t = s\mid S_0=s_0\} = P_\pi^t(s_0,s)$ and $\mathbb E[R_{t+1}\mid S_0 = s_0] = (P_\pi^t r_\pi)(s_0)$.

A stationary distribution of $\pi$ is a probability vector $\mu$ on $\mathcal S$ with

$$\sum_s \mu(s)\sum_a \pi(a\mid s)\,p(s'\mid s,a) = \mu(s') \quad\text{for all } s' \qquad (10.8).$$

The average reward of $\pi$ is

$$r(\pi) = \lim_{h\to\infty}\frac1h\sum_{t=1}^h \mathbb E[R_t\mid S_0, A_{0:t-1}\sim\pi] \quad (10.6), \qquad r(\pi) = \sum_s \mu_\pi(s)\sum_a\pi(a\mid s)\sum_{s',r}p(s',r\mid s,a)\,r \quad (10.7),$$

the second form holding when the steady-state distribution $\mu_\pi(s) = \lim_{t\to\infty}\Pr\{S_t = s\}$ exists and does not depend on $S_0$ (an ergodic MDP).

The discounted value function is $v^\gamma_\pi(s) = \mathbb E_\pi\big[\sum_{k\ge0}\gamma^k R_{t+k+1}\mid S_t = s\big]$, and the objective of the box is

$$J(\pi) = \sum_s \mu_\pi(s)\, v^\gamma_\pi(s).$$

Finally, the differential value of a state (10.13) is $v_\pi(s) = \lim_{\gamma\to1}\lim_{h\to\infty}\sum_{t=0}^h\gamma^t\big(\mathbb E_\pi[R_{t+1}\mid S_0 = s] - r(\pi)\big)$.

Formalization targets

Goal: the futility of discounting

For $0 \le \gamma < 1$, every policy $\pi$ and every stationary distribution $\mu_\pi$ of $\pi$,

$$J(\pi) = \sum_s \mu_\pi(s)\, v^\gamma_\pi(s) = \frac{1}{1-\gamma}\, r(\pi),$$

and therefore, for a fixed $\gamma$ and policies $\pi, \pi'$ with their own stationary distributions,

$$J(\pi) \le J(\pi') \iff r(\pi) \le r(\pi').$$

Milestones

1. (10.6)–(10.7): if $\Pr\{S_t = s\mid S_0 = s_0\}\to\mu(s)$ for all $s_0, s$, then from every start both $\lim_t \mathbb E[R_t]$ and the Cesàro limit (10.6) exist and equal the $\mu$-sum.
2. (10.8): such a limit $\mu$ is a stationary distribution.
3. (3.14): $v^\gamma_\pi$ satisfies the Bellman equation, the step "(Bellman Eq.)" of the box.
4. Offset invariance (p. 250): the differential Bellman equations for $v_\pi, q_\pi, v_*, q_*$ and the differential TD errors (10.10)–(10.11) are unchanged when all values are shifted by a constant.
5. Exercise 10.6: for expected rewards $1,0,1,0,\dots$ from $\mathsf A$ and $0,1,0,1,\dots$ from $\mathsf B$, the average reward is $\tfrac12$, the limit (10.7) and a steady-state distribution do not exist, and $v_\pi(\mathsf A) = \tfrac14$, $v_\pi(\mathsf B) = -\tfrac14$.
6. Exercise 10.7: in the three-state ring with reward $+1$ on arrival in $\mathsf A$, the average reward is $\tfrac13$ and the differential values are $v(\mathsf A) = -\tfrac13$, $v(\mathsf B) = 0$, $v(\mathsf C) = \tfrac13$.

The book prints no answers to Exercises 10.6 and 10.7; the values above were computed for this mission.

Significance

The result itself. The identity shows that the discount rate cannot enter the ranking of policies once performance is measured over the on-policy state distribution: any objective of the form "discounted value averaged over where the policy goes" is the average reward up to a positive factor. The book draws from it the conclusion (p. 253) that $\gamma$ changes from a problem parameter to a solution-method parameter, and that discounting algorithms with function approximation, which do not optimize this averaged objective, are not guaranteed to optimize average reward either. Milestones 1–2 connect the closed form of $r(\pi)$ to its definition as a long-run rate; milestone 4 explains why differential methods determine values only up to an offset; the exercises show that (10.13) gives finite differential values in periodic chains where the differential return (10.9) has no limit.

Formalizing it. The results are classical and elementary, but the book's derivation is informal: it takes the Bellman equation for granted, sums a geometric series of equalities, and leaves implicit which distribution $\mu_\pi$ is meant and when (10.6) and (10.7) agree. This mission fixes each of those points: $v^\gamma_\pi$ is defined from returns, the identity is proved for every stationary distribution, and the ergodicity hypothesis is made the exact limit condition the text states. No machine-checked version of these statements is known to exist; the platform's Markov-chain and average-reward libraries (Puterman's unichain optimality equation, Doeblin convergence) state different results.

Difficulty

The box reads as a chain of equalities, and each individual step is short. The one step that is not algebra is "(Bellman Eq.)": with $v^\gamma_\pi$ defined as an expected discounted return, the Bellman equation requires exchanging an infinite sum with a finite expectation and shifting the index of a convergent series, which needs absolute convergence for $\gamma < 1$ and bounded rewards. The final line, which unrolls $J = r + \gamma J$ into a geometric series, is only valid because $J$ is finite. For milestone 1, the book's hypothesis is the existence of an $S_0$-independent limiting distribution, not irreducibility or aperiodicity; replacing it by either would change the statement. The exercises require the iterated limit in (10.13) to be computed explicitly: the inner limit is a periodic series summed in closed form, and the outer limit is a removable singularity at $\gamma = 1$.

Formalization scope

The Lean development lives in the namespace SuttonBartoRL.AverageReward. States, actions and rewards are finite; one action set serves every state; the dynamics are the four-argument $p(s', r\mid s,a)$. Probabilities $\Pr\{S_t = s\mid S_0 = s_0\}$ and $\mathbb E[R_{t+1}\mid S_0=s_0]$ are computed from the matrix powers $P_\pi^t$. The discounted value $v^\gamma_\pi$ is a real series $\sum_k \gamma^k (P_\pi^k r_\pi)(s)$; it is not defined as the solution of the Bellman equation, since that definition would reduce the goal to three lines of algebra. The average reward and $J$ take the state distribution $\mu$ as an explicit argument; the goal holds for every stationary distribution of $\pi$ and assumes no ergodicity, which is all the box uses (under ergodicity $\mu_\pi$ is the unique one). $\gamma = 0$ is allowed. The differential value (10.13) is stated as the existence of both limits with the given value, with $\gamma \to 1$ from below, so no default value of a nonexistent limit can make a statement true. The optimality equations use a nonempty action set. The sum $\sum_{t=1}^h \mathbb E[R_t]$ of (10.6) is written with the index shifted to $t = 0,\dots,h-1$.

The Lean does not formalize a trajectory probability space: expectations and probabilities are the matrix expressions above, which is what they equal for a Markov chain. The Exercise 10.6 hypothesis constrains expected rewards of one policy, which is all the exercise uses.

Reusable parts: the finite-MDP layer duplicates the one drafted for the other missions of this series and is expected to be merged with it; the Cesàro and stationary-distribution lemmas of milestones 1–2 are general facts about finite Markov chains. Contributions welcome: proofs of any milestone, and a proof of the goal from milestone 3.

Selected references

• R. S. Sutton, A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §§10.3–10.4, pp. 249–254. http://incompleteideas.net/book/the-book-2nd.html
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
• S. Mahadevan, "Average reward reinforcement learning: foundations, algorithms, and empirical results", Machine Learning 22, 159–195, 1996. https://doi.org/10.1007/BF00114727

Motivation

Convex duality in optimization rests on one transformation: to a convex function $f$ one associates the function $\varphi(\xi) = \sup_x(\Sigma x\xi - f(x))$, which records, for each slope $\xi$, the best affine lower bound of $f$ with that slope. Lagrangian duality, the duality theory of linear and conic programming, the analysis of first-order methods through smoothness and strong convexity of conjugates, and the dual representations of risk measures and divergences all read off properties of $f$ from properties of $\varphi$. Each of these uses needs one fact: that the transformation loses no information, so that applying it twice returns $f$.

That fact, for functions on $\mathbb R^n$, is the theorem of W. Fenchel's five-page note On conjugate convex functions (Canad. J. Math. 1 (1949) 73–77). Its timeline:

• 1912. W. H. Young proves the inequality $ab \le F(a) + G(b)$ for a pair of mutually inverse increasing functions $F', G'$ of one variable (Proc. R. Soc. Lond. A 87, 1912).
• 1949. Fenchel defines the conjugate of a convex function on a convex subset of $\mathbb R^n$, without any differentiability, and proves that conjugation is a symmetric correspondence on convex functions that are semi-continuous from below and whose domain is closed relative to the function (Fenchel 1949).
• 1965. J.-J. Moreau develops conjugation for convex functions with values in $(-\infty, +\infty]$ on a real Hilbert space, together with the proximal map (Bull. SMF 93, 1965); the biconjugation theorem in this generality is called the Fenchel–Moreau theorem.
• 1970. R. T. Rockafellar's Convex Analysis makes the conjugate the central object of finite-dimensional convex analysis (Princeton, 1970).

Setting

Points of $\mathbb R^n$ are $x = (x_1,\dots,x_n)$, and $\Sigma x\xi = x_1\xi_1 + \dots + x_n\xi_n$.

A standing pair $(G, f)$ consists of a set $G \subseteq \mathbb R^n$ and a real function $f$ defined in $G$ such that

1. $G$ is nonempty and convex;
2. $f$ is convex on $G$: $f((1-\theta)x' + \theta x'') \le (1-\theta)f(x') + \theta f(x'')$ for $x', x'' \in G$, $0 < \theta < 1$;
3. $f$ is semi-continuous from below on $G$: $\liminf_{x \to x^*,\, x \in G} f(x) \ge f(x^*)$ for $x^* \in G$;
4. $G$ is closed relative to $f$: $f(x) \to +\infty$ as $x \to x^*$ within $G$, for every boundary point $x^*$ of $G$ not in $G$.

$G$ need be neither open, nor closed, nor bounded. The paper writes the lower limit as a "lim" with a bar under it; the milestone texts write it $\lim_{x\to x^*}$, and it always means $\liminf$.

The conjugate pair of $(G, f)$ is

$$\Gamma = \{\xi \in \mathbb R^n : x \mapsto \Sigma x\xi - f(x) \text{ is bounded above on } G\}, \qquad \varphi(\xi) = \sup_{x \in G}\bigl(\Sigma x\xi - f(x)\bigr)\quad (\xi \in \Gamma).$$

The same construction applied to $(\Gamma, \varphi)$ gives the pair $(G^*, f^*)$, with $f^*(x) = \sup_{\xi\in\Gamma}(\Sigma\xi x - \varphi(\xi))$. An interior point of $G$ is a point of the relative interior of $G$, its interior within its affine hull.

In Lean: IsClosedConvexPair G f, conjDomain G f $= \Gamma$, conjFun G f $= \varphi$, and $(G^*, f^*)$ is conjDomain (conjDomain G f) (conjFun G f), conjFun (conjDomain G f) (conjFun G f).

Formalization targets

Goal: Fenchel's theorem (§3, p. 75)

For every standing pair $(G, f)$:

$$(\Gamma,\varphi) \text{ is a standing pair},\qquad \Sigma x\xi \le f(x) + \varphi(\xi)\ \ (x\in G,\ \xi\in\Gamma), \tag{5}$$

with equality for some $\xi \in \Gamma$ at every interior point $x$ of $G$;

$$G^* = G, \qquad f^*(x) = f(x)\ \ (x \in G);$$

and every standing pair $(\Gamma', \varphi')$ whose conjugate pair is $(G, f)$ equals $(\Gamma, \varphi)$.

Milestones, in the order of the proof

1. (5), with no hypothesis on $(G, f)$.
2. $\Gamma \ne \emptyset$, and $\varphi(\xi) = \Sigma x^\circ\xi - f(x^\circ)$ for some $\xi\in\Gamma$ at each interior point $x^\circ$.
3. $\Gamma$ and $\varphi$ are convex.
4. $\varphi$ is semi-continuous from below and $\Gamma$ is closed relative to $\varphi$.
5. (6): $G \subseteq G^*$ and $f^* \le f$ on $G$.
6. Two convex functions, semi-continuous from below on $G$ and equal at the interior points of $G$, are equal on $G$.
7. $f^* = f$ on $G$.
8. (7): $\sup_{\xi\in\Gamma}(\Sigma\xi x^\circ - \varphi(\xi)) = \infty$ for every $x^\circ \notin G$.

Significance

The theorem identifies, among convex functions on convex subsets of $\mathbb R^n$, exactly the class on which conjugation is a bijection and an involution. It is the finite-dimensional base case of the Fenchel–Moreau theorem and underlies Fenchel's duality theorem for $\inf(f - g)$, the conjugate-based optimality conditions of convex programming, and the inversion of gradients of conjugate differentiable convex functions (the paper's §6, the Legendre transformation). The pair form is also how the result is used in practice: the conjugate of a function finite on a set comes with an explicit domain $\Gamma$, and the theorem says that domain determines and is determined by $G$.

The result has been proved for 75 years. What a formalization adds is the theorem in Fenchel's own form: a real-valued function on an explicit convex domain rather than an extended-real function on all of $\mathbb R^n$, the domain identity $G^* = G$ together with the identity of values, and the attainment of equality in (5) at relative-interior points. Machine-checked versions of biconjugation exist in other forms: for extended-real functions on Hilbert spaces, for finite convex functions on all of $\mathbb R^n$, and for functions on a set with a closed restricted epigraph over continuous linear functionals. None of them states the domain identity or the attained equality, and none is in the paper's pair form.

Difficulty

Milestones 1, 3, 4 and 5 follow from the definition of the conjugate alone. The content sits in three places.

• Supporting hyperplanes at relative-interior points. When $G$ is lower-dimensional, the topological interior of $G$ is empty, and a supporting hyperplane must be produced inside the affine hull of $G$ and then extended. Points that are interior to a segment of $G$ but on its relative boundary do not suffice.
• Passing from the interior to the boundary of $G$. Equality $f^* = f$ at interior points does not by itself give equality at boundary points of $G$; it needs semi-continuity from below of both functions and convexity along segments ending at the boundary point.
• $G^* \subseteq G$. Points outside the closure of $G$ and boundary points of $G$ not in $G$ behave differently: a boundary point cannot be separated from $G$ by a hyperplane, and the inclusion there depends on the condition that $G$ be closed relative to $f$. Without that condition the inclusion is false: for $G = (0, 1]$ and $f \equiv 0$, the point $0$ lies in $G^*$.

Formalization scope

• $\mathbb R^n$ is Fin n → ℝ with its product topology, which is the Euclidean one; $\Sigma x\xi$ is Mathlib's x ⬝ᵥ ξ. The paper's $\Sigma\xi x$ in $G^*, f^*$ is ξ ⬝ᵥ x, equal by commutativity.
• $f$ is a total function (Fin n → ℝ) → ℝ, but every hypothesis and conclusion concerns its values on $G$ only: ConvexOn ℝ G f, LowerSemicontinuousOn f G, and Tendsto f (𝓝[G] x) atTop for x ∈ closure G \ G.
• $\varphi$ is the real sSup, which is $0$ on unbounded sets; it is evaluated only on $\Gamma$.
• Three readings are fixed and disclosed in the goal's Formalization Note:
  • (P1) $G$ is nonempty. The paper assumes it tacitly and proves $\Gamma \neq \emptyset$.
  • (P2) Interior points are relative-interior points (intrinsicInterior ℝ G). The paper's segment definition makes the equality clause false, and the topological interior makes it vacuous for lower-dimensional $G$.
  • (P3) Uniqueness is stated as the symmetry gives it. The literal "one and only one $\Gamma$, $\varphi$ with these properties, (5) and equality at interior points" is false: for $G = [0,1]$, $f \equiv 0$, the pair $\Gamma' = \{0\}$, $\varphi'(0) = 0$ also qualifies.
• A statement of the goal that asserts only $f^* = f$ on $G$ and drops $G^* = G$ is a different and much weaker theorem; the goal carries the domain identity.
• Needed infrastructure: supporting hyperplanes to convex sets at relative-interior points (Mathlib has separation theorems for Fin n → ℝ and the intrinsic interior), affine minorants of convex functions on lower-dimensional domains, and the boundary-limit argument of milestone 6. All of these are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome.

Selected references

• W. Fenchel, On conjugate convex functions, Canadian Journal of Mathematics 1 (1949), 73–77. https://doi.org/10.4153/CJM-1949-007-x
• W. H. Young, On classes of summable functions and their Fourier series, Proceedings of the Royal Society of London A 87 (1912), 225–229. https://doi.org/10.1098/rspa.1912.0076
• J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bulletin de la Société Mathématique de France 93 (1965), 273–299. https://doi.org/10.24033/bsmf.1625
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

A manufacturer that makes one product to stock faces random demand, can produce at most $b$ units per period, and can store at most $U$ units. The classical result without the production limit is that a base-stock policy is optimal: raise inventory to a fixed level $\bar y$ each period. With a production limit, the natural modification is to produce up to $\bar y$ when that is possible and to produce at full capacity otherwise. Federgruen and Zipkin (1986) proved that this modified base-stock (critical-number) policy is optimal under the long-run average-cost criterion, for discrete demand with a general convex cost. Production-capacity models of this type are standard in operations management texts, and the result underlies the computational and comparative-static work that followed, starting with Part II of the same paper, which treats discounted costs.

Timeline.

• 1950s–60s: optimality of base-stock (critical-number) policies for uncapacitated periodic-review models; see Heyman and Sobel's Stochastic Models in Operations Research, Vol. II (1984).
• 1986: Federgruen and Zipkin, Part I (average cost, MOR 11(2):193–207) and Part II (discounted cost, MOR 11(2):208–215) establish the capacitated case. Part I handles the unbounded state space with a general average-cost theory for countable-state Markov decision processes by Federgruen, Schweitzer and Tijms (1983).

Setting

Time is divided into periods $t = 0, 1, \dots$. The demands $D_0, D_1, \dots$ are independent copies of a random variable $D$ with values in $\{0, 1, 2, \dots\}$ and probability mass function $p(j)$; write $\mu = E(D)$ and $P(j) = \Pr\{D \le j\}$. At the start of period $t$ the inventory is an integer $x_t$ (negative values are backorders). The decision maker raises it to

$$y_t \in Y(x_t) = \{y \in \mathbb Z : x_t \le y \le x_t + b,\ y \le U\},$$

pays the expected one-period cost $G(y_t)$, and demand is subtracted: $x_{t+1} = y_t - D_t$. The order cost per unit is set to zero, as in the paper; this loses no generality because every policy with finite average cost has the same average order cost.

The standing assumptions are: $G \ge 0$ is convex and $G(y) \to \infty$ as $|y| \to \infty$ (Assumption 1); the characteristic function of $D$ is analytic at the origin (Assumption 2), and $0 < \mu$; $G(y) \le A + B|y|^\rho$ for some positive integer $\rho$ (Assumption 3); $b > \mu$ and $P(b) < 1$ (Assumption 4). The smallest global minimizer of $G$ is $\bar y^\infty$, and $U \ge \bar y^\infty$.

A Markov policy is a sequence $\pi = (\pi_0, \pi_1, \dots)$ of maps with $\pi_t(x) \in Y(x)$. The critical-number policy with critical number $\bar y$ is $\delta[\bar y](x) = \max(x, \min(\bar y, x + b))$. A stationary policy $\delta$ is strongly optimal with average cost $g$ if, from every initial state $x \le U$, its average cost $t^{-1}E\{\sum_{i<t} G(y_i)\}$ converges to $g$, while every Markov policy has lim-inf average cost at least $g$ from every initial state.

The analysis uses the operators $Rv(y) = G(y) + E\,v(y - D)$ and $Sv(x) = \min_{y \in Y(x)} Rv(y)$, and the optimality equation

$$g + v(x) = Sv(x),\qquad x \le U. \tag{6}$$

For an interval $\iota = [l, u]$, $H_\iota v(x)$ is the largest expected sum of $v(y_t)$, over policies forced to produce at capacity below $l$ and to produce nothing above $u$, until the inventory first returns to $\iota$.

Formalization targets

Goal: Theorem 1 (p. 202)

There exist $g^*$, $v^*$ and $y^* \ge \bar y^\infty$ such that $(g^*, v^*)$ solves (6), $v^*$ is convex with global minimizer $y^*$, and

$$\delta^* = \delta[y^*] \text{ is strongly optimal with average cost } g^*.$$

The $y^*$ in the optimality claim is the minimizer constructed in part (a).

Milestones

• Lemma 2(a)–(c) (pp. 196–197): a normal-tail inequality and two series estimates.
• Lemma 3 (p. 198): if $v(x) = O(|x|^q)$ then $H_\iota v(x) = O(|x|^{q+3})$.
• Corollary 1 (p. 200): $H_\iota 1 = O(|x|^3)$ and $H_\iota G = O(|x|^{\rho+3})$, both finite.
• Corollary 2 (p. 201): $(t+1)^{-1}P[\delta_{0t}]\cdots P[\delta_{tt}](H_\iota 1 + H_\iota G)(x) \to 0$.
• Lemma 4 (p. 201): reachability of every state in $[L, U - D_-]$ under some policy that produces at capacity below $L$.
• Lemma 5 (p. 202): $S$ and $Q$ preserve the class $V$ of convex functions of growth $O(|x|^{\rho+3})$ that are nonincreasing below $\bar y^\infty$.

Significance

The result. Theorem 1 reduces an infinite-state average-cost control problem to a one-parameter search over critical numbers. The paper then evaluates the average cost of $\delta[\bar y]$ by a renewal formula, proves it convex in $\bar y$ (Theorem 2), and in §5 extends optimality to unlimited storage. The strong form of optimality matters: it compares with every Markov policy from every starting state, and it compares lim-infs, not only lim-sups.

Formalizing it. The theorem has a published proof, but no machine-checked one, and its proof relies on external results that are themselves unformalized: the countable-state average-cost theory of Federgruen, Schweitzer and Tijms, a fixed-point theorem on a compact convex subset of a product space, and a large-deviation estimate quoted from Feller. A formal development produces reusable infrastructure: expected first-passage sums for integer-valued random walks with a reflecting control, polynomial moment bounds for them, and the convexity-preservation argument for capacitated value iteration.

Difficulty

The state space is unbounded below, so the finite-state theory of average-cost Markov decision processes does not apply, and the one-period cost is unbounded. The obvious approach, letting the discount factor tend to one in the discounted problem, needs uniform bounds on relative value functions. Those bounds come from the expected cost until the inventory returns to a fixed interval, and with capacity limits that expectation must be controlled with growth $O(|x|^{\rho+3})$ uniformly over a class of policies. This is the content of Lemma 3, whose proof combines a large-deviation estimate for the demand sums with a renewal-type recursion. A second obstacle is strong optimality: comparing with policies whose lim-inf average cost is smaller requires that the relative value function grows sublinearly along every admissible trajectory (Corollary 2).

Formalization scope

All objects are in the namespace FedergruenZipkin.AvgCost, defined in one file. States $x, y$ and the capacity $U$ are integers; demands are natural numbers with a real probability mass function p; $b$ is a positive natural number. Convexity on $\mathbb Z$ is the second-difference inequality. Expectations of a real function are series $\sum_j p(j)\,v(y-j)$; expected policy costs and hitting sums are $[0,\infty]$-valued and need no integrability side condition. Feasibility and all properties of value functions are required only on states $x \le U$, which are the only states visited. Assumption 2 is stated literally, as real-analyticity of $\theta \mapsto \sum_j p(j)e^{i\theta j}$ at $0$. The order cost is zero, as in the paper. $\bar y^\infty$ is a parameter characterised as the least minimizer of $G$, not an infimum.

"Strongly optimal" has no displayed definition in the paper; it is read from eq. (7) in the proof of Theorem 1(b): convergence of the average cost of $\delta^*$ to $g^*$ from every state, together with a lim-inf lower bound for every Markov (memoryless, possibly nonstationary) policy from every state. The class is neither widened to history-dependent policies nor narrowed to stationary ones. The goal additionally records that $E\,v^*(y-D)$ converges, that $v^*$ has growth $O(|x|^{\rho+3})$, and that $g^* \ge 0$; all three follow from the paper's proof.

A trivializing reading is ruled out: the existence of $g$, $v$ and $y^*$ is one existential, so $y^*$ cannot be decoupled from the solution of (6), and strong optimality includes the convergence of $\delta^*$'s own average cost to $g^*$, so $g = 0$ does not satisfy it vacuously.

Not posed: Lemma 1 (quoted from Feller, and replaceable by a Chernoff bound); the renewal formulas (10)–(11) and Theorem 2; and §5 (unlimited storage). Useful contributions include a formal theory of expected hitting sums for skip-free-upward random walks, and a proof of Lemma 3 by any route.

Selected references

• A. Federgruen and P. Zipkin, An Inventory Model with Limited Production Capacity and Uncertain Demands I. The Average-Cost Criterion, Mathematics of Operations Research 11(2):193–207, 1986. https://doi.org/10.1287/moor.11.2.193
• A. Federgruen and P. Zipkin, An Inventory Model with Limited Production Capacity and Uncertain Demands II. The Discounted-Cost Criterion, Mathematics of Operations Research 11(2):208–215, 1986. https://doi.org/10.1287/moor.11.2.208
• A. Federgruen, P. J. Schweitzer and H. C. Tijms, Denumerable Undiscounted Semi-Markov Decision Processes with Unbounded Rewards, Mathematics of Operations Research 8(2):298–314, 1983. https://doi.org/10.1287/moor.8.2.298
• D. P. Heyman and M. J. Sobel, Stochastic Models in Operations Research, Vol. II, McGraw-Hill, 1984.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.