All missions

Motivation

A reproducing kernel Hilbert space (RKHS) is a Hilbert space of functions in which evaluation at each point is a continuous functional. Each such space is determined by its kernel, and in practice spaces are usually given by their kernels: Gaussian or Sobolev kernels in kernel methods and Gaussian-process regression, the Bergman and Szegő kernels in complex analysis. A recurring question is therefore how a relation between two function spaces reads on their kernels. When is one space contained in another? When do two kernels define the same space?

N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) answers both questions. §7 (pp. 354–356) compares a class with a contractively included subclass. §13 (C) (pp. 382–383) uses Banach's closed graph theorem to remove the contractivity assumption. The answer is an order relation between kernels, checkable on finite point sets. It is the standard tool for comparing RKHSs: Part II of the paper (§2, p. 387) applies §7, Theorem II to compare Bergman kernels of nested plane domains.

Setting

Let $X$ be an arbitrary set (no topology, no measure). A function $K : X\times X\to\mathbb C$ is a positive matrix if

$$\sum_{i,j=1}^n K(y_i,y_j)\,\bar\xi_i\,\xi_j\ \ge 0$$

for every finite family $y_1,\dots,y_n\in X$ and every $\xi_1,\dots,\xi_n\in\mathbb C$. For two kernels, $K_1\ll K$ means that $K-K_1$ is a positive matrix.

A class with a reproducing kernel is a complex Hilbert space $F$ of functions $X\to\mathbb C$ for which there is a function $K$ with $K(\cdot,y)\in F$ and $f(y) = (f,K(\cdot,y))$ for all $f\in F$ and $y\in X$. The scalar product $(f,g)$ is linear in $f$. Every such $K$ is a positive matrix, and by Moore's theorem (§2 (4)) every positive matrix is the kernel of exactly one such class. A linear class of functions is an (R.K.)-class if some norm makes it a Hilbert space with a reproducing kernel. Such a class carries many admissible norms, and correspondingly many kernels.

In the Lean development, $F$ is a Mathlib RKHS ℂ H X ℂ instance on a complete complex inner product space H. The class of functions is Set.range (⇑ : H → X → ℂ). The scalar kernel is kernelFn H x y = RKHS.kernel H x y 1, and $K_1\ll K$ is AronszajnRK.Limits.KernelLE K₁ K (the series' shared definition).

Formalization targets

Goal: Corollary IV₂ of §13

For classes $F, F_1$ with reproducing kernels $K, K_1$:

$$F_1\subset F \iff \exists\, M>0:\ K_1\ll MK .$$

The constant $M$ is left unspecified: it measures the norm of the inclusion operator and has no canonical value.

Milestones, in attack order

1. ≪ is a partial ordering of the positive matrices (§7, p. 354).
2. §7, Theorem I: if $K_1\ll K$, then $F_1\subset F$ and $\|f_1\|_1\ge\|f_1\|$.
3. §7, Theorem II: if a linear class $F_1\subset F$ is a Hilbert space with $\|f_1\|_1\ge\|f_1\|$, then $F_1$ has a reproducing kernel $K_1\ll K$.
4. §13 (C), p. 382: the norm $c\|\cdot\|$ corresponds to the same class, with kernel $c^{-2}K$.
5. §13 (C), Lemma: the identity correspondence from $F_1\cdot F_2\subset F_1$ to $F_2$ is a closed linear transformation.
6. §13 (C), Theorem IV: if $F_1\subset F$ are (R.K.)-classes, then $\|f\|\le M\|f\|_1$ on $F_1$ for some $M>0$, whatever admissible norms are chosen.
7. §13 (C), Corollary IV₁: any two admissible norms on one (R.K.)-class are equivalent.
8. §13 (C), Corollary IV₃: $F_1 = F$ iff $mK\ll K_1\ll MK$ for some $m,M>0$.
9. §13 (D), Theorem VI: intersections and sums of (R.K.)-classes are (R.K.)-classes.

Significance

The result. Corollary IV₂ reduces inclusion of infinite-dimensional function spaces to positivity of finite matrices. Corollary IV₃ says when two kernels give the same space, as sets of functions with equivalent norms. Kernel-method theory uses these facts to compare hypothesis spaces of different kernels. In complex analysis they compare Bergman spaces of nested domains, since the restricted kernel of a larger domain is dominated by the kernel of a smaller one (Part II, §2, p. 387, of the paper). Theorem VI makes (R.K.)-classes a lattice under intersection and sum.

Formalizing it. All statements are classical and have been proved since 1950. To our knowledge none is machine-checked. Mathlib has RKHSs, their kernels, positive semidefiniteness of kernels and the construction of a space from a kernel. It has no comparison theorem between two RKHSs, and no characterization of an RKHS by its kernel up to inclusion or equality of function sets. This mission adds these. As a by-product it produces the closed-graph argument for RKHS inclusions in a form that other missions can reuse.

Difficulty

The sufficiency direction ($K_1\ll MK \Rightarrow F_1\subset F$) does not follow from the definitions alone. Domination is a statement about finite quadratic forms; membership of a function of $F_1$ in $F$ is a statement about an infinite-dimensional space, and nothing pointwise connects the two. The paper's argument rests on the sum theorem of §6, the goal of a separate mission in this series.

The necessity direction cannot start from an assumed norm inequality, because the two norms are a priori unrelated. Producing the constant $M$ needs the closed graph theorem together with the fact that norm convergence in an RKHS implies pointwise convergence. A direct estimate of $\sum K_1(y_i,y_j)\bar\xi_i\xi_j$ against $\sum K(y_i,y_j)\bar\xi_i\xi_j$ from the inclusion alone has no route to a uniform constant.

Formalization scope

• Scalars and spaces. All scalars are complex and $X$ is an arbitrary type. A class with a reproducing kernel is an RKHS ℂ H X ℂ instance on a complete complex inner product space H. The function of f : H is ⇑f.
• Scalar product. Mathlib's ⟪f, g⟫_ℂ is conjugate-linear in f, so Aronszajn's $(f,g)$ is ⟪g, f⟫_ℂ, and the reproducing property is ⟪k y, f⟫_ℂ = f y.
• Inclusion and norm comparison. "$F_1\subset F$" is inclusion of the sets of functions. A norm comparison $\|f\|\le M\|f\|_1$ is stated between the elements of the two spaces that are the same function.
• Positivity. Positive matrices are Matrix.PosSemidef over the index type X. Its quadratic form over finitely supported vectors is exactly the paper's. Over $\mathbb C$ it includes Hermitian symmetry, which nonnegativity implies. $MK$ is fun x y => (M : ℂ) * K x y with real $M>0$.
• The goal and Corollary IV₃. "$F$, $F_1$ the corresponding classes" of positive matrices $K$, $K_1$ is read as: arbitrary RKHSs whose kernels are $K$, $K_1$. By Moore's uniqueness theorem this is the same statement.
• Theorem II. $F_1$ is not assumed to carry an RKHS instance, since having a kernel is the conclusion. It is a complex Hilbert space with an injective linear map into the functions of $F$.
• Theorem IV and Corollary IV₁ quantify over all admissible norms, i.e. all RKHSs with the given function sets.
• Closedness of a transformation is the paper's sequential definition (§13 (C), p. 382), stated on a submodule that need not be closed.
• (R.K.)-class means: equals the set of functions of some RKHS in the universe of $X$.
• Rescaling milestone. It asserts that a rescaled RKHS exists, and that every RKHS with the same functions and the rescaled norm has the rescaled kernel.

Trivializations ruled out. No statement defines a class as RKHS.OfKernel K and then asserts that its kernel is K. Classes are always compared through their sets of functions and norms. "$F_1\subset F$" is never weakened to the existence of some injection $H_1\to H$.

Substrate. Mathlib's RKHS, RKHS.kernel, RKHS.kerFun, RKHS.kerFun_inner, RKHS.posSemidef_kernel, RKHS.OfKernel, Matrix.PosSemidef (with .add, .smul), Banach's LinearMap.continuous_of_isClosed_graph, and the continuous functional calculus (CFC.sqrt, for the square root $(I-L)^{1/2}$ in the proof of Theorem II). The sum theorem of §6, used in the proof of Theorem I, is the goal of mission I of this series. Contributions of that theorem and of reusable lemmas on RKHS inclusions are welcome.

Selected references

• N. Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
• S. Banach, Théorie des opérations linéaires, Monografje Matematyczne 1, Warsaw, 1932 (closed graph theorem, as cited on p. 382).
• V. I. Paulsen and M. Raghupathi, An Introduction to the Theory of Reproducing Kernel Hilbert Spaces, Cambridge Stud. Adv. Math. 152, Cambridge University Press, 2016 (modern treatment of the inclusion criterion). https://doi.org/10.1017/CBO9781316219232

Why the copy count matters

Shadow tomography asks for predictions of many specified measurements of an unknown quantum state, while using as few prepared copies of that state as possible. The requested output is a list of acceptance probabilities, not a full description of the state. A procedure might exploit the fact that these are only $M$ numbers, even when the state has dimension $D$. The natural question is how far this saving can go. Aaronson's paper gives upper bounds and separates two sources of difficulty: one already present for ordinary probability distributions, and one arising from noncommuting quantum measurements.

This mission concerns the first source. It formalizes Theorem 16, which says that even when the state and every requested measurement are diagonal in the same basis, the number of copies must grow with $\min\{D,\log M\}/\varepsilon^2$ in the relevant asymptotic regime. In that special case, the unknown state is an ordinary distribution on $D$ outcomes. The theorem therefore puts a limit on any proposed improvement to shadow tomography that would promise fewer copies in all instances.

States, measurements, and estimates

A mixed state $\rho$ on a $D$-dimensional system is a positive semidefinite $D\times D$ complex matrix with trace one. A two-outcome measurement is represented by an effect $E$ satisfying $0\preceq E\preceq I$; it accepts $\rho$ with probability $\operatorname{Tr}(E\rho)$. When $\rho$ is diagonal, its diagonal entries are the probabilities of the $D$ basis outcomes. When $E$ is diagonal too, it specifies a randomized yes-or-no test on those outcomes. These conventions are stated in Section 3 of the paper.

Given effects $E_1,\ldots,E_M$, a shadow-tomography strategy measures $k$ independent copies $\rho^{\otimes k}$ and outputs estimates $b_1,\ldots,b_M$. It succeeds on $\rho$ when every estimate differs from $\operatorname{Tr}(E_i\rho)$ by at most $\varepsilon$. The lower bound requires success probability at least $2/3$ for every diagonal mixed state. The strategy may make a joint quantum measurement on all copies and may choose its estimates from its observed outcome. This is the same measurement model used in Problem 1.

Formalization targets

Classical special-case lower bound

The goal is the classical clause of Theorem 16. There are absolute constants $c>0$ and $N_0$ such that, for $D\ge N_0$, $\log_2 M\ge N_0$, and $0<\varepsilon\le1/6$, there are $M$ diagonal effects with 0/1 entries, corresponding to the known Boolean functions in Section 6.1, for which every strategy successful on all diagonal states must use

$$k\ge c\,\frac{\min\{D,\log_2 M\}}{\varepsilon^2}.$$

The hard measurements are chosen before the strategy is quantified. The statement therefore also rules out a strategy with a smaller copy count that works uniformly for all quantum states and measurements. Its constants and threshold express the $\Omega$ notation in Theorem 16, rather than specifying a numerical optimum.

Supporting targets

Four milestones come from the proof on pages 20–21: the high-probability overlap bound for independently chosen half-size subsets (Eq. (1)); the acceptance probability of a subset under its associated biased distribution; an upper bound on the mutual information between the hidden subset index and the observed samples; and the exact entropy formula with a quadratic entropy deficit. These statements expose the combinatorial and information-theoretic parts of the lower bound while leaving the goal as the paper's copy-complexity result.

What the result supplies

Theorem 16 sets a floor for shadow tomography that survives even when all operators commute. Any uniform copy bound for the full quantum task must respect this floor. The result also distinguishes the difficulty of predicting many properties of a distribution from the extra difficulty possible for noncommuting states and measurements, which the paper treats in a separate lower bound. Section 6 presents both bounds.

A complete formalization would give machine-checked statements and proofs for the finite subset construction, the entropy calculation, the information inequality, and the reduction from a successful quantum measurement procedure on diagonal states to a lower bound on $k$. The theorem is proved on paper; these draft statements are open Lean goals and do not claim that its proof has been machine checked. The finite-distribution and information-theory infrastructure is reusable for other lower bounds based on hidden-index families.

Where the argument is delicate

Counting how many possible measurements there are does not by itself show that samples reveal enough about which distribution generated them. The lower bound needs a quantitative relation between estimation accuracy and information about a hidden index, while each individual sample carries limited information. The paper's printed overlap condition (1) is too weak for the next displayed $\varepsilon/2$ estimate: at its boundary it gives $\varepsilon$. The milestone preserves Eq. (1) as printed; closing the goal requires the correspondingly sharper overlap fact with $N/24$, which follows from the same type of concentration statement after adjusting its constant. The printed assertion that learning the index requires mutual information at least $\log_2 K$ is also imprecise at success probability $2/3$; a quantitative decoding inequality is needed. Neither incorrect display is a draft milestone.

Formalization scope

Matrices are indexed by Fin D. WildeQIT.IsDensityOperator supplies the mixed-state predicate $\rho\succeq0$ and $\operatorname{Tr}(\rho)=1$. Diagonal states and effects use the standard matrix diagonal predicate. An effect is positive semidefinite together with its complement. The tensor power uses functions Fin k → Fin D as basis indices; at $k=0$ it is a one-by-one identity matrix. A strategy is a finite-outcome POVM on that tensor power, followed by a real estimate vector for each outcome. The output values are not restricted to $[0,1]$: clipping them to this interval cannot worsen an estimate of a probability. No restriction to classical estimators is placed in the goal; that would change the allowed strategies before the theorem has been proved.

The asymptotic threshold excludes the one-dimensional and single-measurement corners where the claimed rate does not describe the problem. The bound $\varepsilon\le1/6$ keeps the biased distributions used on page 20 nonnegative; $\varepsilon\ge1/2$ would permit a zero-copy constant estimate. Subset milestones require even $N$ or explicitly require a half-size subset, so $N/2$ has its intended meaning. The natural logarithm appears nowhere in the lower-bound rate; entropy, mutual information, and $\log_2 M$ use base two. At zero probability the entropy convention is $0\log 0=0$.

The finite distributions, entropy, conditional entropy, and mutual information reuse the published WildeQIT definitions. Contributions that prove the four source milestones, establish the sharper overlap fact, or supply the quantitative decoding step are welcome. The goal must retain its order of quantifiers: one hard measurement family, then every strategy, with success demanded on every diagonal state.

Selected references

• Scott Aaronson, Shadow Tomography of Quantum States, arXiv preprint arXiv:1711.01053v2, 2018. Preprint.

Motivation

A learning algorithm is judged by its generalization error: the expected loss of the hypothesis it outputs on a fresh example. That quantity depends on an unknown distribution, so it is estimated from the training data, by the empirical error (the average loss on the training set) or the leave-one-out error (the average loss on each training point of the hypothesis trained without it). Classical learning theory controls the gap between these estimates and the true error uniformly over a hypothesis class, through its VC dimension or covering numbers. Such bounds say nothing useful about algorithms that search very large or infinite-dimensional spaces, such as support vector machines and regularization networks in a reproducing kernel Hilbert space.

Bousquet and Elisseeff (JMLR 2 (2002) 499–526) replaced the capacity of the class by a property of the algorithm, its stability: how much its output changes when one training example is removed. Their exponential bound for uniformly stable algorithms is the starting point of the stability approach to generalization, which was later used for stochastic gradient descent (Hardt, Recht and Singer, 2016) and differential privacy, and sharpened by Feldman and Vondrák (2019) and Bousquet, Klochkov and Zhivotovskiy (2020).

Timeline. Rogers and Wagner (1978) and Devroye and Wagner (1979) bounded the leave-one-out error of local rules such as k-nearest neighbours through their stability. McDiarmid (1989) proved the bounded-differences inequality. Lugosi and Pawlak (1994) combined it with smoothed error estimates. Kearns and Ron (1999) named hypothesis and error stability and related them to the VC dimension. Bousquet and Elisseeff (2002) introduced uniform stability and proved the exponential bounds this mission formalizes.

Setting

Let $Z = X \times Y$ be a measurable space of labelled examples with an unknown probability distribution $D$. A training set $S = (z_1, \dots, z_m)$ is drawn from $D^m$. A learning algorithm $A$ maps a training set to a hypothesis $A_S : X \to Y'$. It is deterministic and symmetric: it depends on the training set only as a multiset, so it is a function Multiset (X × Y) → (X → Y'), defined for training sets of every size. For a cost $c$, the loss of a hypothesis $f$ at $z = (x, y)$ is $\ell(f, z) = c(f(x), y)$.

Given $S$, write $S^{\setminus i}$ for $S$ with its $i$-th example removed, and $S^i$ for $S$ with $z_i$ replaced by an independent draw $z_i' \sim D$. The three errors are

$$R = \mathbb E_{z \sim D}[\ell(A_S, z)], \qquad R_{\mathrm{emp}} = \frac1m \sum_{i=1}^m \ell(A_S, z_i), \qquad R_{\mathrm{loo}} = \frac1m \sum_{i=1}^m \ell(A_{S^{\setminus i}}, z_i).$$

An algorithm has uniform stability $\beta$ at sample size $m$ (Definition 6) if for every $S \in Z^m$, every $i$ and every $z \in Z$,

$$|\ell(A_S, z) - \ell(A_{S^{\setminus i}}, z)| \le \beta .$$

As a function of the sample size this constant is written $\beta_m$.

Formalization targets

Goal: Theorem 12

If $A$ has uniform stability $\beta$ and $0 \le \ell(A_S, z) \le M$ for all $z$ and all training sets $S$, then for every $m \ge 1$ and $\delta \in (0,1)$, each of the following holds, separately, with probability at least $1 - \delta$ over $S \sim D^m$:

$$R \le R_{\mathrm{emp}} + 2\beta + (4m\beta + M)\sqrt{\frac{\ln(1/\delta)}{2m}}, \qquad (11)$$ $$R \le R_{\mathrm{loo}} + \beta + (4m\beta + M)\sqrt{\frac{\ln(1/\delta)}{2m}}. \qquad (12)$$

Milestones

1. McDiarmid's inequality (Theorem 2): for measurable $F : Z^m \to \mathbb R$ with $|F(S) - F(S^i)| \le c_i$, $P_S[F - \mathbb E_S F \ge \epsilon] \le e^{-2\epsilon^2/\sum_i c_i^2}$.
2. Uniform stability $\beta$ implies $|\ell(A_S, z) - \ell(A_{S^i}, z)| \le 2\beta$ (p. 504).
3. Lemma 7: the bias identities for $\mathbb E_S[R - R_{\mathrm{emp}}]$, $\mathbb E_S[R(A,S^{\setminus i}) - R_{\mathrm{loo}}]$ and $\mathbb E_S[R - R_{\mathrm{loo}}]$.
4. $R - R_{\mathrm{emp}}$ and $R - R_{\mathrm{loo}}$ have bounded differences $c_i = 4\beta + M/m$.
5. $\mathbb E_S[R - R_{\mathrm{emp}}] \le 2\beta$ and $\mathbb E_S[R - R_{\mathrm{loo}}] \le \beta$.
6. The tail bounds $P_S[R - R_{\mathrm{emp}} > \epsilon + 2\beta] \le \exp(-2m\epsilon^2/(4m\beta+M)^2)$ and the leave-one-out analogue.

Significance

When $\beta = O(1/m)$ both bounds are $O(1/\sqrt m)$, with constants that do not depend on any capacity of the hypothesis space. Later sections of the paper show that Tikhonov regularization in a reproducing kernel Hilbert space has $\beta = O(1/(\lambda m))$, so the theorem gives generalization bounds for support vector regression, kernel ridge regression and, through a smoothed loss, soft-margin classification. The theorem is also the template for later stability bounds: the decomposition into a bias term controlled by stability and a deviation term controlled by a concentration inequality recurs throughout the literature.

The result has been proved since 2002, and replace-one variants appear in textbooks (Mohri, Rostamizadeh and Talwalkar, Foundations of Machine Learning, Theorem 14.2; Shalev-Shwartz and Ben-David, Chapter 13). On Prove2Me the replace-one textbook version is not formalized, and Mathlib at the platform's environment has no McDiarmid inequality. This mission asks for a machine-checked proof of the paper's remove-one version with its exact constants, and a reusable McDiarmid inequality with per-coordinate constants.

Difficulty

The deterministic steps (the bias identity and the bounded-differences estimates) are short on paper. The central difficulty is McDiarmid's inequality itself: it needs a martingale argument along the coordinates of a product measure, or an equivalent tensorization of conditional sub-Gaussian bounds, with the Doob martingale $\mathbb E[F \mid z_1, \dots, z_k]$ expressed through partial integration over Measure.pi. Hoeffding's inequality for sums, which Mathlib has, does not apply directly: $R - R_{\mathrm{emp}}$ is not a sum of independent terms. A second, bookkeeping difficulty is Lemma 7: the identities rest on exchanging $z_i$ with $z_i'$ and on the symmetry of $A$, which in Lean means measure-preserving coordinate permutations of $D^m \otimes D$ and multiset equalities such as $S^{i\,\setminus i} = S^{\setminus i}$.

Formalization scope

Conventions committed to by the Lean statements:

• An algorithm is a function of a multiset; this is how symmetry is encoded. Samples are Fin m → X × Y, and $S^i$ is Function.update.
• The law of $S$ is Measure.pi (fun _ => D) with D a probability measure; $z_i'$ and $z$ are independent draws, integrated against the product (Measure.pi fun _ => D).prod D.
• The paper's standing assumption that all functions are measurable is one hypothesis: $(S, z) \mapsto \ell(A_S, z)$ is measurable for every sample size. With the bound $0 \le \ell(A_T, z) \le M$ for training sets $T$ of every size, every expectation is a genuine integral, so no bound can hold because a non-integrable expectation defaults to $0$.
• Uniform stability quantifies over every sample, every index and every point, not almost every one.
• "With probability at least $1 - \delta$" means the $D^m$-measure of the failure set is at most $\delta$. The two bounds (11) and (12) are separate statements, joined by a conjunction; they are not claimed for one joint event.
• The paper assumes $\beta_m$ is non-increasing in $m$ and bounds $\beta_{m-1}$ by $\beta_m$ (p. 504). The leave-one-out bound (12) and its milestones carry the explicit hypothesis of uniform stability $\beta$ at size $m-1$; the empirical bound (11) does not.
• McDiarmid's inequality sums $c_i^2$ over $i = 1, \dots, m$; the paper's printed upper index $n$ is a slip.
• When a displayed tail bound has a zero denominator, its formal statement uses the limiting bound $0$. In McDiarmid's inequality this is the constant-function case; in the stability tails the loss is identically zero.

The stability notion is the paper's remove-one notion. A formalization with replace-one stability would prove a different theorem with different constants, and the published FoundationsML_Stability_UniformlyStable (replace-one) is therefore not used.

The development needs the published loss, empirical-error and generalization-error definitions from Foundations of Machine Learning, a McDiarmid inequality on product measures (reusable for any bounded-differences argument), and the coordinate-exchange lemmas for Measure.pi behind Lemma 7. Contributions of a general McDiarmid inequality, of exchangeability lemmas for product measures, and of proofs of any milestone are welcome.

Selected references

• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Series 141 (1989) 148–188. https://doi.org/10.1017/CBO9781107359949.008
• L. Devroye and T. Wagner, Distribution-free performance bounds for potential function rules, IEEE Trans. Inform. Theory 25 (1979) 601–604. https://doi.org/10.1109/TIT.1979.1056087
• M. Kearns and D. Ron, Algorithmic stability and sanity-check bounds for leave-one-out cross-validation, Neural Computation 11 (1999) 1427–1453. https://doi.org/10.1162/089976699300016304
• M. Hardt, B. Recht and Y. Singer, Train faster, generalize better: stability of stochastic gradient descent, ICML 2016. https://arxiv.org/abs/1509.01240
• V. Feldman and J. Vondrák, High probability generalization bounds for uniformly stable algorithms with nearly optimal rate, COLT 2019. https://arxiv.org/abs/1902.10710
• O. Bousquet, Y. Klochkov and N. Zhivotovskiy, Sharper bounds for uniformly stable algorithms, COLT 2020. https://arxiv.org/abs/1910.07833
• M. Mohri, A. Rostamizadeh and A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 14.

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 step sizes $\gamma_n$ and a noise term $U_{n+1}$. Recursions of this form appear in stochastic gradient methods, adaptive control, learning in games (fictitious play, reinforcement learning) and urn models. The ODE method compares the iterates with the solutions of $\dot x=F(x)$. In Benaïm's lecture notes (Benaïm 1999), the comparison is phrased through the continuous-time interpolated process $X$. Under standard noise conditions, $X$ is almost surely an asymptotic pseudotrajectory of the flow of $F$, and its limit set is almost surely internally chain transitive.

That theorem constrains where the process may end up. It does not say which of several candidate sets the process actually reaches. When the ODE has several attractors, for example several stable equilibria of a learning dynamic or several stable compositions of an urn, an application needs to know that each attractor is reached with positive probability. Section 7 of the notes answers this question. The answer is a criterion of attainability: if the process can, with positive probability and at arbitrarily late times, enter the basin of an attractor, then it converges to that attractor with positive probability.

Timeline.

• Kushner and Clark (1978) proved convergence statements for processes that visit a compact subset of the domain of attraction of an asymptotically stable equilibrium infinitely often.
• Arthur, Ermoliev and Kaniovski (1983) and Pemantle (1990) studied urn processes whose limit points depend on the trajectory.
• Benaïm (1997) and Duflo (1997, Random Iterative Models) developed the attainability argument for general stochastic approximation processes.
• Benaïm (1999) states it for arbitrary attractors of a semiflow on a locally compact metric space, under a single conditional shadowing condition (24).

Setting

Let $(M,d)$ be a metric space and let $\Phi=(\Phi_t)_{t\ge0}$ be a semiflow on $M$: a continuous map $(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 all $t\ge0$, and positively invariant if $\Phi_t(A)\subset A$.
• An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ on which $\operatorname{dist}(\Phi_tx,A)\to0$ uniformly. Its basin $B(A)$ is the set of points $x$ with $\operatorname{dist}(\Phi_tx,A)\to0$.
• A continuous curve $X:\mathbb R_+\to M$ is an asymptotic pseudotrajectory if $\sup_{0\le h\le T}d(X(t+h),\Phi_h(X(t)))\to0$ as $t\to\infty$, for every $T>0$.
• The limit set of $X$ is $L(X)=\bigcap_{t\ge0}\overline{X([t,\infty))}$.
• For $T>0$, $d_X(T)=\sup_{k\in\mathbb N}d(\Phi_T(X(kT)),X(kT+T))$.

Now let $X=(X(t))_{t\ge0}$ be a process on a probability space $(\Omega,\mathcal F,P)$ with continuous paths in $M$, adapted to a filtration $(\mathcal F_t)_{t\ge0}$. The standing assumption of Section 7 is that for all $\delta>0$, $T>0$ and $t\ge0$,

$$P\Big(\sup_{s\ge t}\ \sup_{0\le h\le T}d\big(X(s+h),\Phi_h(X(s))\big)\ge\delta\ \Big|\ \mathcal F_t\Big)\le w(t,\delta,T)\tag{24}$$

for a function $w\ge0$ with $w(t,\delta,T)\downarrow0$ as $t\to\infty$.

A point $p$ is attainable if $P(\exists s\ge t: X(s)\in U)>0$ for every $t>0$ and every open neighbourhood $U$ of $p$. $\mathrm{Att}(X)$ is the set of attainable points.

Formalization targets

Goal: Theorem 7.3, first statement

If $M$ is locally compact, $A$ is an attractor of $\Phi$, and $\mathrm{Att}(X)\cap B(A)\neq\emptyset$, then

$$P\big(L(X)\subset A\big)>0 .$$

This statement contains no constants and no rates, so it does not depend on how (24) is quantified for a particular algorithm.

Theorem 7.3, second statement

If $U$ is open and relatively compact with $\overline U\subset B(A)$, there are $T,\delta>0$, depending only on $U$ (and on $\Phi$, $A$), such that for every process satisfying the standing assumption and every $t\ge0$

$$P\big(L(X)\subset A\big)\ge\big(1-w(t,\delta,T)\big)\,P\big(\exists s\ge t:\ X(s)\in U\big).$$

Milestones

• Lemma 6.8. For a nonempty compact $K\subset B(A)$ there are $T,\delta>0$ such that every asymptotic pseudotrajectory with $X(0)\in K$ and $d_X(T)<\delta$ has $L(X)\subset A$.
• Lemma 7.1, in three parts:
  • $\mathrm{Att}(X)$ is closed;
  • it is positively invariant;
  • it contains $L(X)$ almost surely.

Significance

The result. Theorem 7.3 turns a question about the long-run limit of a random process into a question about where the process can go. Attainability is usually checked by a controllability argument: the noise can push the iterates in every direction. For urn processes with an urn function mapping the simplex into its interior, every point is attainable (Example 7.2 of the notes). Then every attractor of the mean ODE is reached with positive probability. Combined with nonconvergence results for unstable sets (Section 9 of the notes), this characterizes the possible limits of many learning and urn processes. Theorem 7.3 is the positive half of that picture.

Formalizing it. The theorem has a published proof (p. 32 of the notes) and no machine-checked version. A formal proof needs the following:

• a precise reading of the conditional shadowing condition (24) as a conditional expectation of an indicator;
• the stopping-time decomposition of the event $\{\exists s\ge t: X(s)\in U\}$ over dyadic times;
• the deterministic Lemma 6.8, which rests on the limit set theorem for precompact asymptotic pseudotrajectories (Theorem 5.7 of the notes, the subject of mission 1 of this series).

Difficulty

The obvious argument says: once $X$ enters a compact part of the basin, the flow carries it into $A$. That fails because $X$ is not a trajectory of the flow. Each window of length $T$ adds an error, and errors over infinitely many windows can push the process out of the basin.

Two things are needed instead:

• A uniform version of the deterministic statement, with $T$ and $\delta$ fixed in advance from the compact set alone. This is Lemma 6.8, which needs local compactness of $M$ and the structure of limit sets of asymptotic pseudotrajectories.
• A probabilistic step that applies (24) at the random time when $X$ first enters $U$. That time is not a stopping time on a continuum, and conditioning at it needs care.

A naive union bound over all times is useless: it does not use the conditional form of (24).

Formalization scope

• The semiflow is Mathlib's Flow ℝ≥0 M on a metric space; local compactness is LocallyCompactSpace M.
• The process is X : ℝ≥0 → Ω → M with continuous paths. The paper's alternative of càdlàg paths is not covered.
• Adaptedness is Borel measurability of $X(t)$ with respect to $\mathcal F_t$, for a Mathlib Filtration ℝ≥0. $P$ is a probability measure.
• The suprema in (24) and in $d_X(T)$ are computed in $[0,\infty]$ with the extended distance, so that "sup $\ge\delta$" and "sup $<\delta$" are exact even when the supremum is infinite or not attained.
• The conditional probability in (24) is the conditional expectation of the indicator of the event. The event is required to be measurable, so the condition cannot hold vacuously through a junk conditional expectation.
• $w$ is required to be both nonincreasing in $t$ and convergent to $0$.
• The events $\{L(X)\subset A\}$ and $\{\exists s\ge t: X(s)\in U\}$ are measured with $P$ as an outer measure, so no measurability hypothesis is added for them.
• In the second statement of Theorem 7.3, $T$ and $\delta$ are chosen before the probability space, the process, $w$ and $t$.
• Invariance in the definition of an attractor is the equality $\Phi_t(A)=A$, not inclusion.
• The almost-sure clause of Lemma 7.1 is stated for separable $M$. Without separability it cannot be proved in ordinary set theory.

These choices rule out the trivializing formalizations: a conditional-probability hypothesis that holds vacuously, invariance read as inclusion, constants $T,\delta$ that depend on the process or on $t$, and a probability bound $w$ without monotonicity.

A complete development needs:

• limit sets of asymptotic pseudotrajectories and the fact that an internally chain transitive set meeting the basin of an attractor lies in the attractor (shared with missions 1 and 5 of this series);
• measurability of path functionals of continuous processes;
• conditioning on events of the form $\{\tau=t_n(k)\}$ at dyadic times.

The first and second are reusable well beyond this mission. Contributions toward either, and alternative proofs of Lemma 6.8, 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, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
• M. Benaïm, Vertex-reinforced random walks and a conjecture of Pemantle, Annals of Probability 25 (1997), 361–392. https://doi.org/10.1214/aop/1024404292
• M. Duflo, Random Iterative Models, Applications of Mathematics 34, Springer, 1997. https://doi.org/10.1007/978-3-662-12880-0
• H. J. Kushner, D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8
• 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

The Hlawka inequality for Schatten $p$-norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge90$, also holds for every real $p\ge89$. This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the cutoff-90 mission already covers every $p\ge90$, the new work is the range from 89 to 90.

The argument for $p\ge90$ was reached by tightening its estimates step by step, starting from 256. With its current choices those estimates stop working below 90, and nobody has yet found a way past that point. It is not known whether 90 is a real limit of the method or only of the choices made so far, so this mission is the smallest test of whether the cutoff can move at all. The accepted proof for $p\ge90$ and its research note are the natural starting point. The goal theorem below gives the exact statement.

This is an open entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 89 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
• Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library
• Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

• The accepted sharp diagonal bound for every real p ≥ 90.
• The accepted real coordinate bound for every real p ≥ 90.
• The accepted diagonal Schatten norm identity.

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