Functional Analysis

Motivation

Reproducing kernel Hilbert spaces are the function spaces of kernel methods in statistics and machine learning (Gaussian-process regression, support vector machines, kernel mean embeddings), of the Bergman and Szegő spaces of complex analysis, and of the theory of positive-definite functions. In all of these, bounded operators on the space (covariance operators, integral operators, projections onto subspaces, multiplication operators) are handled through functions of two points rather than through abstract operators. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) gives, in its §11, the dictionary between bounded operators on a space with a reproducing kernel and their kernels, and characterizes the kernels of bounded symmetric operators with prescribed bounds. Aronszajn credits the ideas of the section to E. H. Moore.

Setting

Let $E$ be an arbitrary set and let $F$ be a class of complex-valued functions on $E$ that forms a complex Hilbert space with scalar product $(f, g)$, linear in $f$ and conjugate-linear in $g$. A reproducing kernel of $F$ is a function $K : E \times E \to \mathbb{C}$ such that, for every $y \in E$, the function $K(\cdot, y)$ belongs to $F$ and

$$f(y) = (f, K(\cdot, y)) \qquad \text{for every } f \in F.$$

Such a kernel exists exactly when every point evaluation $f \mapsto f(y)$ is continuous.

For a bounded linear operator $L$ on $F$, with adjoint $L^*$ defined by $(Lf, g) = (f, L^* g)$, the kernel of $L$ is

$$\Lambda(x, y) = L^*_x K(x, y),$$

the value at $x$ of the element $L^*(K(\cdot, y))$ of $F$. By the reproducing property, $Lf(y) = (f, \Lambda(\cdot, y))$ for every $f \in F$ and $y \in E$, so $L$ is determined by $\Lambda$.

A function $P : E \times E \to \mathbb{C}$ is a positive matrix if $\sum_{i,j} \overline{\xi_i}\, P(y_i, y_j)\, \xi_j \ge 0$ for every finite family of points $y_i \in E$ and complex numbers $\xi_i$. For two arbitrary functions $\Lambda_1, \Lambda_2$ on $E \times E$, one writes $\Lambda_1 \ll \Lambda_2$ if $\Lambda_2 - \Lambda_1$ is a positive matrix. A bounded operator $L$ is symmetric if $L = L^*$, and positive if $(Lf, f) \ge 0$ for every $f$. A symmetric $L$ has lower bound $\ge m$ and upper bound $\le M$ if

$$m\,(f, f) \le (Lf, f) \le M\,(f, f) \qquad \text{for every } f \in F.$$

A kernel $\Lambda$ is hermitian symmetric if $\Lambda(x, y) = \overline{\Lambda(y, x)}$.

Formalization targets

Goal: §11, Theorem I (p. 373)

For an arbitrary hermitian symmetric function $\Lambda : E \times E \to \mathbb{C}$ and real numbers $m, M$:

$$\exists\, L \text{ bounded, symmetric, with } \Lambda = L^*_x K(x,y) \text{ and } m(f,f) \le (Lf,f) \le M(f,f)\ \ \forall f \quad\Longleftrightarrow\quad mK \ll \Lambda \ll MK .$$

The function $\Lambda$ is not assumed to have $\Lambda(\cdot, y) \in F$; that membership is part of what the condition yields.

Milestones

1. §11, (3): the kernel of the adjoint, $\Lambda^*(y, z) = \overline{\Lambda(z, y)}$.
2. §11, (6): $L$ is symmetric if and only if $\Lambda$ is hermitian symmetric.
3. §11, (7): $L$ is positive if and only if $\Lambda$ is a positive matrix.
4. §11, (4): the kernel of a composition, $\Lambda(y, z) = (\Lambda_1(x, z), \overline{\Lambda_2(y, x)})_x$ for $L = L_1 L_2$.
5. §11, Theorem II: if $L_n u \to L u$ weakly for every $u$, then $\Lambda_n \to \Lambda$ pointwise; if $\|L_n - L\| \to 0$, then $\Lambda_n \to \Lambda$ uniformly on every set of couples $(x, y)$ on which $K(x, x)$ and $K(y, y)$ are uniformly bounded.
6. §11, Theorem III, first sentence: for complete orthonormal systems $\{g'_m\}$, $\{g''_n\}$ and $\alpha_{mn} = (g''_n, L g'_m)$,

$$\Lambda(x, y) = \lim_{p, q \to \infty} \sum_{m=1}^{p} \sum_{n=1}^{q} \alpha_{mn}\, g'_m(x)\, \overline{g''_n(y)} .$$

Significance

Theorem I identifies, by finite quadratic-form inequalities alone, which functions of two points are kernels of bounded symmetric operators and with which spectral bounds. It reduces statements about operators (boundedness, positivity, operator inequalities $mI \le L \le MI$) to statements about finitely many evaluations of kernels, the form in which they are checked in practice, for instance when a covariance or integral operator is shown to be bounded and positive from its kernel. The milestones make the correspondence $L \mapsto \Lambda$ a usable calculus: adjoints become conjugate transposes, composition becomes a scalar product in the middle variable, and limits of operators become limits of kernels.

All of these results are proved in the paper. None is formalized: Mathlib has reproducing kernel Hilbert spaces (RKHS), adjoints, positive operators and positive semidefinite matrices over arbitrary index types, but no kernel of an operator and none of the statements above. The mission produces machine-checked proofs of the §11 dictionary and of Theorem I.

Difficulty

The necessity half of Theorem I and milestones (3), (6), (4) follow from the reproducing property. The sufficiency half is where the work is: $\Lambda$ is an arbitrary function, and the hypothesis $mK \ll \Lambda \ll MK$ is only about finite families of points. One has to produce an operator on all of $F$. The obvious attempt, defining $L$ on the dense span of the functions $K(\cdot, y)$ by the kernel and extending by continuity, needs the bound $|(\,L f, g)| \le C\|f\|\|g\|$ on that span, which does not follow directly from the two one-sided inequalities on the diagonal forms. The positivity of $\Lambda - mK$ and $MK - \Lambda$ does not by itself give the membership $\Lambda(\cdot, y) \in F$, which the definition of the kernel of an operator requires. In milestone (7), positivity of an operator is a statement about all of $F$, while positivity of the kernel only sees finite combinations of kernel functions; the passage between them uses density of these combinations.

Formalization scope

• The space is Mathlib's RKHS ℂ H X ℂ: a complex Hilbert space H whose elements are functions X → ℂ on an arbitrary type X (no topology, no measure, not assumed nonempty), with continuous evaluations. The scalar kernel is the series' shared definition AronszajnRK.Sum.kernelFn H x y := RKHS.kernel H x y 1; the function $K(\cdot, y)$ is the element RKHS.kerFun H y 1.
• The kernel of L : H →L[ℂ] H is opKernel L x y := (adjoint L) (kerFun H y 1) x. Mathlib's ⟪u, v⟫_ℂ is conjugate-linear in u, so the paper's $(f, g)$ is ⟪g, f⟫_ℂ, and every formula with a scalar product or a bar has been rewritten in that order. On a one-point $E$ with $F = \mathbb{C}$, $K = 1$ and $L = cI$, the kernel is $\bar c$.
• Positive matrices and $\ll$ are Matrix.PosSemidef of Matrix.of Λ over the index type X (finitely supported test vectors, ComplexOrder on ℂ); no finiteness of X is assumed.
• Symmetric is IsSelfAdjoint L. "Positive" in (7) is ∀ f, 0 ≤ ⟪f, L f⟫_ℂ in ComplexOrder (real and nonnegative), without assuming self-adjointness, as in the paper. The bounds in Theorem I are bounds of the quadratic form, m‖f‖² ≤ Re⟪f, L f⟫ ≤ M‖f‖², not of the operator norm. The paper does not assume $m \le M$ and neither does the statement: for $m > M$ both sides hold exactly when $F = \{0\}$ and $\Lambda = 0$.
• In (4) the statement asserts that the functions $x \mapsto \Lambda_1(x, z)$ and $x \mapsto \overline{\Lambda_2(y, x)}$ are elements of H, and that the kernel of L₁ ∘L L₂ is their scalar product.
• Weak convergence in Theorem II is ⟪v, Lₙ u⟫ → ⟪v, L u⟫ for all u, v; uniform convergence is ‖Lₙ − L‖ → 0 in operator norm.
• In Theorem III the orthonormal systems are HilbertBasis with arbitrary index types, and the double limit is taken along growing finite sets of indices in both variables. For systems indexed by $\mathbb{N}$ this contains the paper's $\lim_{p,q}$ over $\{1..p\}\times\{1..q\}$; the general form also covers finite-dimensional spaces. The second sentence of Theorem III (kernels in $F \otimes \overline{F}$ correspond to operators of finite norm) needs the direct product $F \otimes \overline F$ and is not stated.
• A trivializing formalization is ruled out: Theorem I quantifies over every hermitian function $\Lambda$, not over functions already known to be kernels of operators, and the right-hand side is the finite-matrix condition, not a statement about an operator built from $\Lambda$.
• Not stated: the decomposition (8)–(9) into hermitian parts and the remark on general bounded operators (p. 374), and formula (5). Available substrate: RKHS, RKHS.kerFun_inner, RKHS.kerFun_dense, RKHS.posSemidef_kernel, ContinuousLinearMap.adjoint, ContinuousLinearMap.IsPositive and isPositive_iff_complex, HilbertBasis, Matrix.PosSemidef. Contributions welcome: a general lemma that a function $\Lambda$ with $0 \ll \Lambda \ll K$ is the kernel of an operator $0 \le L \le I$, and the inclusion theorem $K_1 \ll K \Rightarrow F_1 \subset F$, both reusable beyond this mission.

Selected references

• N. Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), no. 3, 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
• E. H. Moore, General Analysis, Part II, Mem. Amer. Philos. Soc. 1 (1939).
• V. I. Paulsen and M. Raghupathi, An Introduction to the Theory of Reproducing Kernel Hilbert Spaces, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781316219232

Motivation

In the mid-1990s, neural networks trained by gradient descent were observed to generalize well even when the number of weights far exceeded the number of training examples. The classical theory could not explain this: VC-dimension bounds for networks grow with the number of parameters, so for large networks they are vacuous. Bartlett's paper (IEEE Trans. Inform. Theory 44 (1998)) showed that, for classification with a margin, what controls generalization is the size of the weights, not the size of the network. Its two main technical results are a margin bound in terms of the fat-shattering dimension (Theorem 2, the subject of mission I of this series) and a bound on the fat-shattering dimension of networks with bounded weights (Theorem 17, the subject of this mission). The same idea of weight-norm capacity control underlies much of the later theory of margins, boosting and kernel methods.

Timeline. Kearns and Schapire (1994) introduced the fat-shattering dimension. Alon, Ben-David, Cesa-Bianchi and Haussler (1997) bounded ℓ∞ covering numbers by it. Bartlett, Kulkarni and Posner (1997) gave the matching lower bound on ℓ1 covering numbers used here as Lemma 19. Maurey's approximation lemma (reported by Pisier, 1981) was used by Jones (1992) and Barron (1993) for approximation by networks, and by Lee, Bartlett and Williamson (1996) for covering numbers of convex hulls. Bartlett (1998) combined these into Theorem 17.

Setting

Let $X$ be a set and $H$ a class of functions $X\to\mathbb R$. For $\gamma>0$, a sequence $x=(x_1,\dots,x_m)\in X^m$ is $\gamma$-shattered by $H$ if there is $r\in\mathbb R^m$ such that for every $b\in\{-1,1\}^m$ some $h\in H$ satisfies $(h(x_i)-r_i)b_i\ge\gamma$ for all $i$. The fat-shattering dimension is

$$\operatorname{fat}_H(\gamma)=\max\{m:\ H\ \gamma\text{-shatters some }x\in X^m\}\in\mathbb N\cup\{\infty\}.$$

A cover of a class $F$ at scale $\varepsilon$ for a pseudometric $\rho$ on functions is a set $T$ of functions such that every $f\in F$ has some $t\in T$ with $\rho(t,f)<\varepsilon$; $\mathcal N(F,\varepsilon,\rho)$ is the least size of a cover. For a sample $x\in X^m$ the pseudometrics $d_{\ell_\infty(x)}$, $d_{\ell_1(x)}$, $d_{\ell_2(x)}$ are the maximum, the mean, and the root mean square of $|f(x_i)-g(x_i)|$ over $i$, and the uniform covering numbers are $\mathcal N_p(F,\varepsilon,m)=\max_{x\in X^m}\mathcal N(F,\varepsilon,d_{\ell_p(x)})$.

The hidden units form a nonempty class $F$ of functions $X\to[-M/2,M/2]$. For $A>0$ the two-layer network class with ℓ1-bounded output weights is

$$H=\Big\{\sum_{i=1}^Nw_if_i:\ N\in\mathbb N,\ f_i\in F,\ \sum_{i=1}^N|w_i|\le A\Big\}.$$

In Lean these are BartlettNN.Margin.fat, BartlettNN.Margin.coverNum and BartlettNN.Margin.Ninf (shared with mission I), and BartlettNN.FatNet.N1, BartlettNN.FatNet.N2 and BartlettNN.FatNet.combos F A.

Formalization targets

Goal: Theorem 17

There is a universal constant $c$ such that for every $X$, $F$, $M$, $A>0$ and $\gamma>0$ with $d=\operatorname{fat}_F(\gamma/(32A))\ge1$,

$$\operatorname{fat}_H(\gamma)\le\frac{cM^2A^2d}{\gamma^2}\ln^2\Big(\frac{MAd}{\gamma}\Big).$$

The constant is left unspecified, as in the paper, so that the goal survives any improvement of the numerical constants.

Milestones (in the order the proof uses them)

1. Lemma 19 (cited from Bartlett–Kulkarni–Posner): for $[0,1]$-valued $F$ with $\operatorname{fat}_F(4\gamma)\ge d$, $\log_2\mathcal N_1(F,\gamma,d)\ge d/32$.
2. Lemma 20, (5): for $d=\operatorname{fat}_F(\gamma/4)$ and $m\ge2+2d\log_2(32M/\gamma)$, $\log_2\mathcal N_2(F,\gamma,m)<1+d\log_2(4emM/(d\gamma))\log_2(9mM^2/\gamma^2)$.
3. Lemma 21 (Maurey): in a Hilbert space, a point of the closed convex hull of a set of norm at most $b$ is within $\sqrt{c/k}$ of an average of $k$ points of the set, for every $c>b^2-\|h\|^2$.
4. Lemma 22: $\log_2\mathcal N_2(H,\gamma,m)\le(2M^2A^2/\gamma^2)\log_2(2\mathcal N_2(F,\gamma/(2A),m)+1)$.
5. Inequality (6): if $m=\operatorname{fat}_H(4\gamma)\ge2+2d\log_2(64MA/\gamma)$ with $d=\operatorname{fat}_F(\gamma/(8A))$, then $m\le(64M^2A^2/\gamma^2)(3+d\log_2(8emMA/\gamma)\log_2(36mM^2A^2/\gamma^2))$.

Significance

Theorem 17 bounds the capacity of a network class without reference to the number of hidden units $N$. With Theorem 2 (mission I) it gives misclassification bounds for networks with small weights that hold for networks of any size, and by iteration it yields the bounds for deep sigmoid networks of Theorem 28 (mission III). Its method — upper-bound ℓ2 covering numbers through Maurey's lemma and compare with a lower bound in terms of fat-shattering — is a template for bounding the fat-shattering dimension of convex hulls in general.

The results are proved in the paper (Lemmas 19 and 21 by citation). None of them is formalized: the platform has no fat-shattering dimension, no uniform sample covering numbers of function classes, and only a finite-dimensional, diameter-based form of Maurey's lemma (HighDimProb.Appetizer.approx_caratheodory), which is not Lemma 21. This mission produces machine-checked statements of all five ingredients and of the theorem.

Difficulty

The obvious route would bound $\operatorname{fat}_H$ through a VC-type count of the network's parameters, which fails because $N$ is unbounded. The paper's route needs a lower bound on covering numbers by the fat-shattering dimension (Lemma 19, a combinatorial packing argument not proved in the paper), an upper bound by the fat-shattering dimension at a finer scale (Lemma 20, which goes through the Alon et al. scale-sensitive Sauer lemma and a quantization argument), and a probabilistic approximation argument in the empirical $L_2$ space (Lemmas 21 and 22). The final step solves a transcendental inequality (6) for $m$, with care at the boundary where the logarithm is small.

Formalization scope

• Functions are maps X → ℝ; fat is valued in ℕ∞, so an unbounded shattering is $\infty$, not a junk $0$. Labels $\pm1$ are Bool read through pm (true ↦ 1); sequences are indexed by Fin m (0-based).
• Covers are external (finite sets of arbitrary functions $X\to\mathbb R$) with the strict inequality of Definition 3; the covering number is $\infty$ when no finite cover exists. The ℓ1 and ℓ2 distances carry the factor $1/m$. Mathlib's Metric.coveringNumber (closed balls, metric types) is not used.
• Bounds of the form "$\log_2\mathcal N\le B$" are stated for every finite value of $\mathcal N$, and where the paper's bound implies finiteness (Lemmas 20, 22, Theorem 17) finiteness is part of the conclusion.
• The constant $c$ of Theorem 17 is quantified before $X$, $F$, $M$, $A$, $\gamma$ and $d$; a constant chosen after them would make the statement trivially true.
• Corrections of the printed statement. Theorem 17 is stated for $\gamma>0$ (printed $\gamma\ge0$, under which the bound is meaningless) and $A>0$ (printed $A\ge0$, under which $\gamma/(32A)$ is undefined). Implicit positivity ($M>0$, $\gamma>0$, $A>0$) in Lemmas 20, 22 and (6) is stated as hypotheses. Inequality (6) is copied as printed, with $\log_2(8emMA/\gamma)$.
• In Theorem 17 the logarithm is natural (the base is absorbed by $c$); (5) and (6) use $\log_2$.
• Lemma 21 is stated in a complete real inner product space, with "convex closure" read as the closure of the convex hull.

Contributions welcome: proofs of the five milestones and of the goal, and reusable infrastructure on fat-shattering and covering numbers of function classes.

Selected references

• P. L. Bartlett, The Sample Complexity of Pattern Classification with Neural Networks: The Size of the Weights is More Important than the Size of the Network, IEEE Trans. Inform. Theory 44(2), 1998, 525–536. https://doi.org/10.1109/18.661502
• N. Alon, S. Ben-David, N. Cesa-Bianchi, D. Haussler, Scale-sensitive dimensions, uniform convergence, and learnability, J. ACM 44(4), 1997, 615–631. https://doi.org/10.1145/263867.263927
• P. L. Bartlett, S. R. Kulkarni, S. E. Posner, Covering numbers for real-valued function classes, IEEE Trans. Inform. Theory 43(5), 1997, 1721–1724. https://doi.org/10.1109/18.623181
• M. J. Kearns, R. E. Schapire, Efficient distribution-free learning of probabilistic concepts, J. Comput. Syst. Sci. 48(3), 1994, 464–497. https://doi.org/10.1016/S0022-0000(05)80062-5
• W. S. Lee, P. L. Bartlett, R. C. Williamson, Efficient agnostic learning of neural networks with bounded fan-in, IEEE Trans. Inform. Theory 42(6), 1996, 2118–2132. https://doi.org/10.1109/18.556601
• A. R. Barron, Universal approximation bounds for superpositions of a sigmoidal function, IEEE Trans. Inform. Theory 39(3), 1993, 930–945. https://doi.org/10.1109/18.256500

Motivation

An orthogonal projection onto a closed subspace is straightforward to describe when that subspace is given directly. It is less straightforward when the subspace is specified as the closed sum of two others: a vector can have contributions from both, and the two component projections generally do not commute. In §12 of Aronszajn's 1950 paper, this problem arises while expressing the reproducing kernel of a sum of two closed subspaces of a reproducing-kernel Hilbert space through their individual kernels. The projection formula is the analytic heart of that calculation. It also gives a series whose finite partial sums can be applied without first describing a basis for the closed sum.

Aronszajn states the result for closed subspaces of a complex Hilbert space of functions. The projection identity itself uses only Hilbert-space geometry; evaluation at a point and the reproducing property enter when the operator formula is translated into a kernel formula later in the section. This mission isolates the projection theorem so that the same formal result can be used both in that kernel calculation and in other settings with two closed subspaces.

Setting

Let $E$ be a complex Hilbert space and let $F_1,F_2$ be closed linear subspaces. The algebraic sum $F_1+F_2$ is the set of all $f_1+f_2$ with $f_i\in F_i$. It need not be closed. Write $F'=\overline{F_1+F_2}$ for its closure and $F_0=F_1\cap F_2$ for the intersection. All four subspaces are closed except possibly the algebraic sum itself. Let $P_1,P_2,P,P_0$ be the orthogonal projections onto $F_1,F_2,F',F_0$, respectively. Operator products denote composition, with the rightmost factor applied first; $(P_2P_1)^0$ is the identity.

The paper writes $F_1\oplus F_2$ for $F'$, even when $F_0$ is nonzero, and uses a distinct dotted plus for the algebraic sum. These symbols can look like a direct sum in newer notation. Here the definitions of $F'$ and $F_0$ remove that ambiguity. Aronszajn assumes complex scalars throughout Part I after §1, p. 343; the statements below keep that convention. Neither a topology on an underlying set of functions nor a measure is part of these operator assertions.

Formalization targets

The goal is the strong projection series, §12, Eq. (7). For each $f\in E$,

$$Pf=P_0f+\sum_{k=1}^{\infty}\left[P_1(P_2P_1)^{k-1}+P_2(P_1P_2)^{k-1}-(P_2P_1)^k-(P_1P_2)^k\right]f.$$

The sum means that its finite partial sums converge in the norm of $E$ for each fixed $f$. No operator-norm limit is claimed. The first term of the sum, at $k=1$, includes $P_1+P_2-P_2P_1-P_1P_2$ because both zero powers are identity operators.

Three source statements are milestones. Equation (1) is a finite identity that expresses a power of $(P-P_1)(P-P_2)$ through a partial sum and a power of $P_2P_1$. The paragraph following Eq. (4) identifies the strong limit of $(P_2P_1)^m$ as $P_0$. The paragraph before Eq. (7) asserts that $[(P-P_1)(P-P_2)]^m$ tends strongly to zero. Together these statements specify the finite and limiting parts of the displayed target. They require no assumption that $F_0$ is zero.

Significance

The formula describes the orthogonal projection onto a closed sum in terms of projections onto its two constituents. In Aronszajn's application, an orthogonal projection on a closed subspace determines that subspace's reproducing kernel; therefore the operator expansion supplies a kernel expansion without constructing a basis of the sum. It also makes explicit why an intersection term survives when the subspaces overlap. The result is proved in the 1950 paper; this mission asks for a Lean proof of that known result, with its convergence mode and closure convention made explicit.

A machine-checked development would provide a reusable complex-Hilbert-space statement for alternating projections and closed sums. Mathlib already provides closed submodules and their orthogonal projections, so the new contribution is the finite identity and the strong-limit claims connecting them. The resulting theorem can support the paper's later kernel expression, §12, Eq. (18), once the correspondence between bounded operators and kernels from §11 is available. Equation (18) is outside this mission's target list.

Difficulty

The algebraic sum of two closed subspaces can fail to be closed, so projecting onto it directly would leave the target undefined as a Hilbert-space orthogonal projection. Passing to its closure gives the correct target but does not imply the two projections commute or that their product has a uniform contraction factor. In particular, strong convergence of the powers and of the final series does not generally improve to convergence in operator norm. The later special case in §12, where the intersection is zero and the minimal angle is positive, has a stronger uniform-convergence conclusion; that extra angle condition is absent from Eq. (7).

The finite formula also has four terms per summand whose order matters. Reversing $P_1P_2$ and $P_2P_1$, beginning the power at $k$ rather than $k-1$, or omitting $P_0$ changes the statement. Even a proof of pointwise convergence of each selected term would not by itself establish the convergence of the bracketed partial sums in the target.

Formalization scope

The Lean representation is an arbitrary complex Hilbert space E with two ClosedSubmodule ℂ E objects. Mathlib's Submodule.starProjection supplies $P_1$ and $P_2$. Two small definitions name $P$ as projection onto the join of the closed submodules and $P_0$ as projection onto their meet. The closed-submodule join is the closure of the algebraic sum; the meet is the intersection. These definitions are computed from $F_1,F_2$, not independently quantified projections. The theorem quantifies over every vector $f$ and uses Filter.Tendsto along natural-number partial sums, giving norm convergence of the resulting vectors.

The source's ambient class has a reproducing kernel, but no step in Eqs. (1)–(7) uses point evaluations. The formal statements therefore apply to any complex Hilbert space, including the paper's RKHS. The stronger scope is explicit here and does not assert a new kernel identity. The $m$-th Lean partial sum uses indices $0,\ldots,m-1$ for the paper's $1,\ldots,m$; it has the same terms and is defined at $m=0$ as $P_0f$. The finite identity is stated only for $m\ge1$, as its $m=0$ version is false in general.

Eq. (1) on p. 375 is printed without the opening bracket of the summand (only the closing bracket appears); the formalization reads it as in Eq. (4) on p. 376, where both brackets are printed. There are two printing slips on p. 377: a running sentence drops brackets from the power of $(P-P_1)(P-P_2)$, and it prints $P\ominus P_2$ while discussing the projection $P-P_2$. The formalization follows the bracketed expression in Eqs. (1) and (4), using ordinary operator subtraction. The corresponding milestone preserves the printed wording. No assumption from the later angle analysis, especially $F_0=\{0\}$, is imported into these results. The series is stated through actual partial sums; it is not defined by an arbitrary RKHS chosen to have a desired kernel.

Selected references

• N. Aronszajn, Theory of Reproducing Kernels, Transactions of the American Mathematical Society 68 (1950), 337–404, §12, pp. 375–380. DOI: 10.1090/S0002-9947-1950-0051437-7.

Motivation

A seller with one good and one buyer whose valuation she does not know faces the simplest problem of mechanism design: choose a selling procedure, anticipating that the buyer will act in his own interest given what he knows. The textbook answer, "post the monopoly price", is usually derived by optimizing over prices alone. The question that opens Börgers' An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015, doi:10.1093/acprof:oso/9780199734023.001.0001) is whether the seller could do better with anything else: negotiation, lotteries, menus of price–probability pairs, or any extensive game she can commit to.

Chapter 2 answers this for one buyer, and in doing so introduces the tools the rest of the book, and most of auction theory, reuse: the revelation principle, the envelope characterization of incentive compatibility, payoff and revenue equivalence, and the virtual valuation. The book's exposition of §2.2 follows Manelli and Vincent (2007), and the nonlinear pricing model of §2.3 is due to Mussa and Rosen (1978, doi:10.1016/0022-0531(78)90085-6); both attributions are the book's own (§2.5, p.29).

Setting

The buyer's type $\theta$ is his valuation for the good. His utility is $\theta-t$ if he receives the good and pays $t$, and $-t$ if he only pays $t$. The seller's belief about $\theta$ is a cumulative distribution function $F$ with density $f$ on an interval $[\underline\theta,\bar\theta]$, $0\le\underline\theta<\bar\theta$, with $f(\theta)>0$ throughout and $F(\theta)=\int_{\underline\theta}^{\theta}f(x)\,dx$.

A direct mechanism is a pair $q:[\underline\theta,\bar\theta]\to[0,1]$, $t:[\underline\theta,\bar\theta]\to\mathbb R$: the buyer reports a type $\theta'$, receives the good with probability $q(\theta')$ and pays $t(\theta')$. Write $u(\theta)=\theta q(\theta)-t(\theta)$. The mechanism is incentive-compatible if $u(\theta)\ge\theta q(\theta')-t(\theta')$ for all $\theta,\theta'$, and individually rational if $u(\theta)\ge 0$ for all $\theta$. The seller's expected revenue is $\int_{\underline\theta}^{\bar\theta}t(\theta)f(\theta)\,d\theta$.

For the extreme-point argument, $\mathcal F$ denotes the space of functions on $[\underline\theta,\bar\theta]$ with the $L^1$ norm, and $M\subset\mathcal F$ the set of increasing functions with values in $[0,1]$. A point $x$ of a convex set $C$ is an extreme point if for every $y\neq 0$ at least one of $x+y$, $x-y$ lies outside $C$.

In the nonlinear pricing model of §2.3 the good is divisible, quantity $q\ge 0$ costs the seller $cq$ with $c>0$, and the buyer's utility is $\theta\nu(q)-t$, with $\nu(0)=0$, $\nu'>0$, $\nu''<0$, $\bar\theta\nu'(0)>c$ and $\lim_{q\to\infty}\bar\theta\nu'(q)<c$. The seller maximizes expected profit $\int(t-cq)f$. The distribution $F$ is regular if the virtual valuation $\theta-(1-F(\theta))/f(\theta)$ is increasing.

Formalization targets

Goal: Proposition 2.5, a posted price is optimal

If $p^*\in\arg\max_{p\in[\underline\theta,\bar\theta]}p(1-F(p))$, then the mechanism

$$q(\theta)=\begin{cases}1&\theta>p^*\\0&\theta<p^*\end{cases},\qquad t(\theta)=\begin{cases}p^*&\theta>p^*\\0&\theta<p^*\end{cases}$$

maximizes expected revenue among all incentive-compatible, individually rational direct mechanisms. The comparison class contains every randomized rule $q$ with values in $[0,1]$; the statement fixes no distribution and no constant.

Milestones on the way

1. Proposition 2.1: every mechanism and optimal buyer strategy can be replaced by a truthful direct mechanism with the same outcomes.
2. Lemmas 2.1–2.4: incentive compatibility forces $q$ increasing, $u$ increasing and convex with $u'=q$, and

$$u(\theta)=u(\underline\theta)+\int_{\underline\theta}^{\theta}q(x)\,dx,\qquad t(\theta)=t(\underline\theta)+\big(\theta q(\theta)-\underline\theta q(\underline\theta)\big)-\int_{\underline\theta}^{\theta}q(x)\,dx.$$

3. Propositions 2.2–2.3 and Lemma 2.5: these conditions characterize incentive compatibility; individual rationality reduces to $u(\underline\theta)\ge0$; at the optimum $t(\underline\theta)=\underline\theta q(\underline\theta)$.
4. Lemma 2.6, Proposition 2.4, Lemma 2.7: $M$ is compact and convex, a linear function continuous on a compact convex set attains its maximum at an extreme point, and the extreme points of $M$ are the $\{0,1\}$-valued functions.
5. Proposition 2.6: under regularity, $q(\theta)=0$ when $\nu'(0)\big(\theta-\tfrac{1-F(\theta)}{f(\theta)}\big)\le c$, otherwise $\nu'(q(\theta))\big(\theta-\tfrac{1-F(\theta)}{f(\theta)}\big)=c$, with $t(\theta)=\theta\nu(q(\theta))-\int_{\underline\theta}^{\theta}\nu(q(x))\,dx$, maximizes expected profit.

Significance

Proposition 2.5 says that the elementary monopoly price is not a restriction of the seller's options but the solution of the unrestricted design problem, including every lottery and every indirect procedure. Its one-buyer argument is the template for Myerson's optimal auction (Chapter 3 of the book), whose revenue formula is the multi-buyer form of Lemma 2.4. Proposition 2.6 exhibits the two standard features of screening, no distortion at the top and downward distortion below, which recur in regulation, insurance and contract theory.

All results of the chapter are classical and proved in the book. None of them is formalized on Prove2Me, and Mathlib has neither the revelation principle, the envelope lemma for incentive-compatible mechanisms, nor a maximum principle for linear functions on compact convex sets (Mathlib has the Krein–Milman lemma, IsCompact.extremePoints_nonempty, but not Bauer's maximum principle). The mission therefore produces the first machine-checked foundation for the one-agent screening model on which chapters 3, 4 and 11 of the book build.

Difficulty

The obvious argument for the goal compares the posted price with other posted prices; that comparison is one line and is not the theorem. The content is the comparison with randomized mechanisms: an arbitrary increasing $q$ with values in $[0,1]$ may do better than every deterministic threshold rule unless one shows that expected revenue is linear in $q$ and that its maximum over the infinite-dimensional set $M$ is attained at an extreme point. That step needs compactness of $M$ in $L^1$ and a maximum principle on compact convex sets in a normed space, neither of which is finite-dimensional linear programming. The envelope step (Lemma 2.3) needs absolute continuity of a convex function on a closed interval, including its endpoints, where $u$ need not be differentiable. For Proposition 2.6 the pointwise maximizer of the virtual surplus must be shown to be monotone and to satisfy incentive compatibility, which is where regularity enters.

Formalization scope

Types are real numbers; every function of the type is a total function $\mathbb R\to\mathbb R$ and every condition quantifies over $[\underline\theta,\bar\theta]$ only. "Increasing" means weakly increasing (the book's note 3). The distribution is a structure carrying the density $f$, positive and integrable on $[\underline\theta,\bar\theta]$ with total mass $1$, and $F$ tied to it by $F(\theta)=\int_{\underline\theta}^{\theta}f$. No measurability or integrability hypothesis is placed on mechanisms: incentive compatibility makes $q$ monotone and $t$ bounded and measurable, so every expected revenue is a genuine integral.

The explicit formulas are part of the statements: the posted-price mechanism of Proposition 2.5 with $p^*\in\arg\max p(1-F(p))$; the payment formulas of Lemmas 2.3–2.4 and Proposition 2.2; $t(\underline\theta)=\underline\theta q(\underline\theta)$ in Lemma 2.5; and in Proposition 2.6 the two-case rule for $q$ and the payment $t(\theta)=\theta\nu(q(\theta))-\int_{\underline\theta}^{\theta}\nu(q(x))\,dx$. The goal fixes $q(p^*)=1$, $t(p^*)=p^*$ for existence and quantifies over every incentive-compatible, individually rational completion at the tie.

The space $\mathcal F$ is $L^1([\underline\theta,\bar\theta])$ of almost-everywhere classes, because the book's $L^1$ "norm" on bounded functions vanishes on null functions; $M$ is the set of classes with an increasing $[0,1]$-valued representative, and Lemma 2.7 is an almost-everywhere statement, as the book's notes 4–6 already indicate. Proposition 2.4 is stated for a nonempty compact convex set in a real normed space and a linear map continuous on that set. The revelation principle models a general mechanism as the buyer's reduced strategy set, an arbitrary type, with a purchase probability and an expected payment for each strategy.

A goal that compared the posted price only with other posted prices, or only with deterministic mechanisms, would be trivial and is excluded: the competitors range over all incentive-compatible, individually rational direct mechanisms with $q$ valued in $[0,1]$.

Reusable beyond this mission: the one-agent envelope and revenue-equivalence lemmas (needed again in Chapters 3, 4 and 11), compactness of monotone functions in $L^1$, and the maximum principle for linear functions on compact convex sets. Contributions to any of these are welcome.

Selected references

• T. Börgers (with D. Krähmer and R. Strausz), An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015. doi:10.1093/acprof:oso/9780199734023.001.0001
• M. Mussa and S. Rosen, "Monopoly and product quality", Journal of Economic Theory 18(2), 1978. doi:10.1016/0022-0531(78)90085-6
• E. A. Ok, Real Analysis with Economic Applications, Princeton University Press, 2007 (Extreme Point Theorem, p.658), cited by the book at p.16.

Motivation

A multi-stage decision process is summarized by its optimal return function $f$, which satisfies a functional equation. In Chapters I and II of Dynamic Programming (Princeton University Press, 1957), Richard Bellman proves existence and uniqueness for particular processes: allocation of resources, gold mining. Chapter IV abstracts these arguments into theorems about whole classes of equations. The same scheme reappears in later chapters (multi-stage games, the calculus of variations) and in every later treatment of dynamic programming.

Two points explain why the chapter is still worth formalizing. First, uniqueness is always claimed within a stated function class, and the choice of class is part of the theorem: an equation of this kind can have many solutions, and only one of them lies in the class that the process singles out. Second, the chapter covers equations that are not contractions in the supremum norm, in particular Type One, where the shrinking happens in the state rather than in the function values.

Setting

Let $D \subseteq \mathbb{R}^N$ carry the Euclidean norm $\|p\|$, let $S$ be a nonempty set of decisions, and let $g, h : D \times S \to \mathbb{R}$ and $T : D \times S \to D$. The general equation (1.1) is

$$f(p) = \sup_{q \in S}\big[g(p,q) + h(p,q)\,f(T(p,q))\big].$$

Here $g$ is the one-stage return, $T(p,q)$ the next state and $h(p,q)$ a multiplier: a discount factor or a survival probability.

An equation is of Type One with constant $0 \le a < 1$ under the following conditions. $D$ contains the null vector $\theta$. $g$ is bounded on bounded parts of $D$, uniformly in $q$, and $g(\theta, q) = 0$. $|h| \le 1$. $\|T(p,q)\| \le a\|p\|$. Finally, with $v(c) = \sup_{\|p\| \le c}\sup_q |g(p,q)|$, the series $\sum_{n \ge 0} v(a^n c)$ converges for every $c$.

It is of Type Two under the following conditions. $g$ is bounded on bounded parts of $D$. On each bounded part, $|h| \le a < 1$ for some $a$. $T$ maps $D$ into $D$, and either $\|T(p,q)\| \le \|p\|$ or $D$ is bounded.

The successive approximations are $f_0(p) = \sup_q g(p,q)$ and $f_{n+1}(p) = \sup_q[g(p,q) + h(p,q) f_n(T(p,q))]$.

The equation of the third type of § 8 lives on the probability simplex $\Delta$ of distributions $p = (p_0, \dots, p_n)$, with vertices $x_k$. It reads

$$f(p) = \min\Big[\,1 + \sum_{k=0}^{n} p_k f(x_k),\ \min_{1 \le l \le M}\big[1 + f(T_l p)\big]\Big] \quad (p \ne x_0), \qquad f(x_0) = 0.$$

Each $T_l$ maps $\Delta$ into itself, and the $0$-th coordinate of $T_l p$ is never $1$. $f(p)$ is the minimal expected time to drive a system into state $0$ with certainty, by observing the state (cost $1$, then continuing from the observed vertex) or by applying one of the operations $T_l$ (cost $1$).

Formalization targets

Goal: Chapter IV, Theorem 1

For a Type One equation there is exactly one solution on $D$, among functions continuous at $\theta$ and zero there, of

$$f(p) = \sup_{q \in S}\big[g(p,q) + h(p,q)\,f(T(p,q))\big] \ (p \ne \theta), \qquad f(\theta) = 0.$$

It is the pointwise limit of the successive approximations from $f_0 = \sup_q g$, and also from any $f_0$ that is continuous and zero at $\theta$ and bounded on bounded parts of $D$. If $g$, $h$ and $T$ are continuous in $p$ on bounded portions of $D$, uniformly in $q$, the solution is continuous on every bounded portion of $D$.

Milestones

• Lemma 1 (the fundamental inequality): for nonnegative measures $dG$,

$$|f_2(p) - F_2(p)| \le \sup_q\Big[\,|g - h| + \int_{D} |f_1 - F_1|\,dG\Big].$$

• Theorem 2: a Type Two equation has a unique solution bounded in every finite part of $D$, obtained by successive approximations and continuous under the same conditions as in Theorem 1.
• Theorem 3 (stability, Type One): $\sup_{\|p\| \le c} |F - f| \le \sum_{n \ge 0} u(a^n c)$, where $u(c) = \sup_{\|p\| \le c}\sup_q |G - g|$.
• Theorem 4 (stability, Type Two, corrected): $\sup_{\|p\| \le c} |F - f| \le u(c)/(1-a)$.
• Lemma 2: two bounded solutions of the third-type equation satisfy $\sup_{p} |f(p) - g(p)| = \max_k |f(x_k) - g(x_k)|$.
• Theorem 5: if $\sum_{k=1}^n (T_l p)_k \le c_1 < 1$ for every $l$ and $p$, the third-type equation has a unique bounded solution, and it is positive off $x_0$.

Significance

Theorem 1 guarantees that the optimal return of a process whose decisions shrink the state is well defined and computable by iteration. It applies without assuming that the supremum over decisions is attained and without regularity of the maximizing decision. Theorems 3 and 4 give quantitative continuous dependence of the solution on the reward. This is what justifies approximating a process by a simpler one. Theorem 5 is a uniqueness result for an undiscounted minimum-time problem, where no contraction in the supremum norm is available.

All of these results are classical and proved in the book. None is formalized: the platform's related statements treat finite state spaces with a fixed policy (FoundationsML.ReinforcementLearning.bellman_equations_unique_solution), or Karlin's compact-decision-set setting with nonnegative rewards and an explicit vanishing-tail hypothesis (KarlinDP.Deterministic.unique_solution_of_vanishing_tail), or finite-state stochastic shortest paths (BertsekasDP.ssp_main_theorem). This mission adds machine-checked versions over a continuum of states and an arbitrary decision set, with the function classes stated exactly.

Difficulty

For Type One, the natural idea is to apply the Banach fixed-point theorem in the space of bounded functions. That fails: $|h| \le 1$ allows no contraction in the supremum norm, and the solution need not be bounded on $D$. Contraction happens only along trajectories, $\|T(p,q)\| \le a\|p\|$, so every estimate must be localized to balls $\|p\| \le c$ and summed along radii $a^n c$. Uniqueness then rests on continuity at $\theta$ rather than on a global norm.

The suprema over an arbitrary, possibly infinite, decision set are not attained in general, so no argument may select a maximizing decision. For the third-type equation, neither a contraction nor a shrinking of the state is available: the operations $T_l$ need not move $p$ towards $x_0$. Uniqueness among bounded solutions requires controlling how long a solution can keep choosing an operation other than observation.

Formalization scope

The state space is EuclideanSpace ℝ (Fin N), $D$ is a Set, the decision set is a nonempty type S, and functions are total, EuclideanSpace ℝ (Fin N) → ℝ. Only their values on $D$ matter, and uniqueness is asserted on $D$. The equation is encoded with IsLUB, so the supremum is genuine and has no junk value. The successive approximations and the radii $v(c)$, $u(c)$ use real iSup/sSup, evaluated only where the book's boundedness conditions hold. "Continuous at $\theta$" is continuity within $D$.

Conventions and corrections:

• In Type One the book writes "for some $a < 1$". The formalization takes $0 \le a < 1$, which loses no generality.
• Condition (1a) of both types is read for every radius $c_1$.
• "Continuous in $p$ in any bounded portion of $D$, uniformly for all $q$" is read as uniform equicontinuity on each $\{p \in D : \|p\| \le c\}$. For closed $D$ this is the pointwise reading.
• Theorem 4 is printed with "$|F(p) - (p)|$", a misprint for $|F(p) - f(p)|$. As printed, it is also false under the bounded-domain alternative of Type Two. Take $N = 1$, $D = [-2,2]$, $T \equiv 2$, $h \equiv \tfrac12$, $g \equiv 0$, and $G = 1$ at $p = 2$, $G = 0$ elsewhere. Then $|F(0) - f(0)| = 1$ while $u(1)/(1-a) = 0$. The formal statement adds that $T$ maps $\{p \in D : \|p\| \le c\}$ into the ball of radius $c$. This holds for every $c$ under the first alternative, where the statement is the book's.
• Lemma 1 is stated for nonnegative measures $dG(p,q,\cdot)$ on $\mathbb{R}^N$, integrated over $D$. The right-hand supremum may be infinite, so it is expressed through its real upper bounds.
• In § 8 the number of states is written both $N+1$ and $n+1$; the formalization uses $n+1$, with $M \ge 1$ transformations indexed by Fin M.

A trivializing formalization would state uniqueness among all solutions of the equation, which is false because constants solve it when $g = 0$ and $h = 1$. Equally trivializing would be to encode the supremum with a junk-valued sSup, so that unbounded return sets pass for solutions. Both are excluded: the class is part of each statement, and the equation is an IsLUB.

Theorem 6 of the chapter (the optimal inventory equation) is not part of this mission; it is treated in the inventory mission of the series. Welcome contributions include a reusable library for localized successive approximations and the equicontinuity lemmas that the continuity statements need.

Selected references

• R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010, Chapter IV. https://doi.org/10.2307/j.ctv1nxcw0f
• S. Karlin, "The structure of dynamic programming models", Naval Research Logistics Quarterly 2 (1955), 285–294. https://doi.org/10.1002/nav.3800020408
• D. P. Bertsekas and J. N. Tsitsiklis, "An analysis of stochastic shortest path problems", Mathematics of Operations Research 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580

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 extends the best possible constant for complex diagonal matrices from $p\ge256$ to every real $p\ge90$. The result is proved in Lean. The constant and its formula are unchanged from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. For each exponent, it works for every triple of diagonal matrices, whatever their size, and no smaller constant does.

The mission started from a supplied pen-and-paper proof. Lowering the cutoff took more than replacing 256 with 90: several estimates in the original argument had to be strengthened. The research note proves the bound for real entries first, then transfers it to complex entries and shows that the constant cannot be improved. The goal theorem below gives the exact formula and statement.

This is the second step of the sharp diagonal Hlawka campaign, and it reuses the foundation's definitions and supporting results. The campaign invites further improvements below 90, keeping the same formula.

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 ≥ 256.
• The accepted diagonal Schatten norm identity.

Motivation

Markov chain Monte Carlo (MCMC) estimates an expectation $\int f\,d\pi$ by the average of $f$ along a Markov chain whose invariant distribution is $\pi$. Many chains share the same $\pi$: every Metropolis–Hastings acceptance rule that satisfies detailed balance, every mixture of such kernels, every choice of proposal. Practitioners need a criterion for preferring one of them. The standard yardstick is the asymptotic variance of the ergodic average, the constant in the Markov chain central limit theorem. A smaller asymptotic variance means fewer iterations for the same Monte Carlo error.

Peskun (1973) compared chains on a finite state space through a partial order on transition matrices: if one reversible matrix moves off the diagonal at least as much as another, entry by entry, its asymptotic variances are no larger, for every function. That result justifies the Metropolis–Hastings acceptance probability as the best possible among reversible acceptance rules. It covers only finite state spaces, while MCMC is used almost exclusively on continuous or mixed ones.

Tierney (1998) extended Peskun's theorem to general state spaces, using the spectral approach of Kipnis and Varadhan (1986) for reversible chains. The theorem is the one usually cited when an MCMC paper argues that one sampler dominates another; Mira (2001) surveys orderings built on it.

Setting

Let $(E, \mathcal E)$ be a measurable space in which singletons are measurable, and let $\pi$ be a probability measure on $E$. A Markov kernel $H$ assigns to each $x \in E$ a probability measure $H(x, \cdot)$, measurably in $x$. It acts on functions by $(Hf)(x) = \int f(y)\,H(x,dy)$. The measure $\pi$ is invariant for $H$ if $\int H(x, A)\,\pi(dx) = \pi(A)$ for every $A \in \mathcal E$. The kernel $H$ is reversible with respect to $\pi$ (satisfies detailed balance) if

$$\pi(dx)\,H(x,dy) = \pi(dy)\,H(y,dx),$$

that is, $\int_A H(x,B)\,\pi(dx) = \int_B H(x,A)\,\pi(dx)$ for all $A, B \in \mathcal E$. Reversibility implies invariance.

Write $\langle f, g\rangle = \int fg\,d\pi$, $L^2(\pi)$ for the square-integrable functions and $L^2_0(\pi) = \{g \in L^2(\pi) : \int g\,d\pi = 0\}$.

Off-diagonal domination. For kernels $P_1, P_2$, $P_1 \succeq P_2$ (OffDiagDominates π P₁ P₂) if for $\pi$-almost every $x$,

$$P_1(x, A\setminus\{x\}) \ge P_2(x, A \setminus\{x\}) \quad\text{for all } A \in \mathcal E.$$

So from almost every state $P_1$ moves to every region at least as readily as $P_2$, and the kernels differ only in the probability of staying put.

The chain and its asymptotic variance. For a Markov kernel $H$, let $X_0, X_1, \dots$ be the Markov chain with initial distribution $\pi$ and transition kernel $H$ (chainMeasure π H, a measure on paths $\mathbb N \to E$). For $f \in L^2_0(\pi)$ put $S_n = \sum_{i=1}^n f(X_i)$ (pathSum f n) and

$$v(f, H) = \lim_{n \to \infty} \frac1n \operatorname{Var}_H(S_n) \in [0, \infty].$$

The lag inner products are $\langle f, H^k f\rangle = \int f(x) \int f(y)\,H^k(x,dy)\,\pi(dx)$ (lagInner π H f k), and for $0 \le \lambda < 1$ the regularized variance is $v_\lambda(f,H) = \langle f,f\rangle + 2 \sum_{k\ge1} \lambda^k \langle f, H^k f\rangle$ (vLam π H f lam).

Formalization targets

Goal: Theorem 4 (p. 5)

Let $P_1, P_2$ be Markov kernels reversible with respect to $\pi$, $f \in L^2_0(\pi)$, and $P_1 \succeq P_2$. Then both asymptotic variances exist in $[0,\infty]$ and

$$v(f, P_1) \le v(f, P_2).$$

No rate, constant or regularity of the kernels is fixed. The statement is the ordering itself, valid for every reversible pair and every $f \in L^2_0(\pi)$.

Milestones, in attack order

1. Lemma 3 (p. 5): if $P_1, P_2$ have invariant distribution $\pi$ and $P_1 \succeq P_2$, then $P_2 - P_1$ is a positive operator on $L^2(\pi)$:

$$\iint f(x)f(y)\,\bigl(P_2(x,dy) - P_1(x,dy)\bigr)\,\pi(dx) \ge 0 \qquad (f \in L^2(\pi)).$$

2. A reversible kernel is a self-adjoint contraction on $L^2_0(\pi)$ (p. 5): $\langle Hf, g\rangle = \langle f, Hg\rangle$ and $\|Hf\| \le \|f\|$.
3. Finite-$n$ variance identity (p. 5), for $n \ge 1$:

$$\frac1n \operatorname{Var}_H(S_n) = \langle f,f\rangle + 2\sum_{i=1}^n \frac{n-i}{n}\,\langle f, H^i f\rangle.$$

4. Existence of $v(f,H)$ in $[0,\infty]$ (p. 6).
5. $v_\lambda(f,H) \to v(f,H)$ as $\lambda \uparrow 1$, finite or infinite (p. 6).
6. $v_\lambda(f,P_1) \le v_\lambda(f,P_2)$ for $0 \le \lambda < 1$ when $P_1 \succeq P_2$ (p. 6).

Significance

The result. Theorem 4 turns a pointwise, one-step comparison of kernels, which is easy to check, into a comparison of the quantity that governs Monte Carlo error. Its main consequence, drawn in §3 of the paper, is that the Metropolis–Hastings acceptance probability $\alpha_{MH}(x,y) = \min\{1, r(y,x)\}$ gives the maximal kernel in the off-diagonal order among reversible Metropolis–Hastings kernels with a given proposal. It is therefore optimal in asymptotic variance, on arbitrary state spaces. Proposition 5 of the same paper (a separate mission in this series) combines with it to show that a single Metropolis–Hastings kernel built on a mixture proposal beats the mixture of the component kernels. Later orderings of samplers (Mira 2001; Andrieu and Livingstone 2021) take this theorem as their base case.

Formalizing it. The theorem has been proved since 1998. No machine-checked version exists for general state spaces, and none of its milestones is on the platform. The formalization produces reusable infrastructure: the asymptotic variance of a stationary chain as an extended-real limit on Mathlib's Ionescu–Tulcea path measure, the $L^2$ facts for reversible kernels (self-adjointness, contraction, the covariance formula for path sums), and the positivity of $P_2 - P_1$ under off-diagonal domination. Each of these is used again in any formal treatment of MCMC efficiency or the Markov chain central limit theorem.

Difficulty

The direct approach compares the two finite-$n$ variances. This fails, and not just technically: the paper exhibits two doubly stochastic, symmetric $4\times4$ matrices with $P_1 \succeq P_2$ for which the variance of $f(X_0)+f(X_1)+f(X_2)$ is 15.4 under $P_1$ and 14.8 under $P_2$ (p. 7). Off-diagonal domination orders the lag-one covariances, but higher-order correlations "need not be ordered" (p. 5). The ordering appears only in the limit, and only for reversible kernels. The comparison must pass through an object that sees all lags at once and is monotone along the segment $P_1 + \beta(P_2 - P_1)$, and that object involves resolvents of operators on $L^2_0(\pi)$. The limit may be infinite, so every comparison must be made in $[0,\infty]$. Mathlib has neither the spectral measure of a self-adjoint operator nor the Kipnis–Varadhan theory.

Formalization scope

The state space is {E : Type*} [MeasurableSpace E] with [MeasurableSingletonClass E] wherever off-diagonal domination appears. This is an assumption the paper leaves implicit: $A \setminus \{x\}$ must be an event. $\pi$ is a probability measure and all kernels are Markov kernels. Reversibility is Mathlib's Kernel.IsReversible, invariance is Kernel.Invariant. The function $f$ is measurable with MemLp f 2 π and, for $L^2_0$, ∫ f ∂π = 0; measurability picks a representative of the $L^2$ class and costs nothing. The chain is Kernel.trajMeasure started from $\pi$. The sum runs over $X_1,\dots,X_n$, not $X_0$. Variances are Mathlib's evariance in $[0,\infty]$, and $v(f,H)$ is a Tendsto limit in ℝ≥0∞, so an infinite asymptotic variance is represented. The goal asserts the existence of both limits rather than assuming it, so it cannot hold vacuously. Neither it nor any milestone specializes to finite $E$, to Metropolis–Hastings kernels, or to a chain started from a point. Lemma 3 assumes invariance only, and the theorem requires reversibility, as printed.

Two statements depart in form from the page. The finite-$n$ variance identity and $v_\lambda$ are written through the moments $\langle f, H^k f\rangle$ (a Neumann series) instead of through the spectral measure $e_{f,H}$ and the resolvent $(I-\lambda H)^{-1}$. The two forms agree for a self-adjoint contraction, and this is noted in each item. The paper's appeal to the spectral theorem and to Kipnis and Varadhan (1986) is not restated as an item: a complete development needs it, or an equivalent argument, as part of the proof. Proofs of any milestone, and reusable lemmas on the path measure (stationarity and the marginal laws of $(X_i, X_j)$), are welcome.

Selected references

• L. Tierney, A Note on Metropolis–Hastings Kernels for General State Spaces, Ann. Appl. Probab. 8(1), 1–9, 1998. https://doi.org/10.1214/aoap/1027961031
• P. H. Peskun, Optimum Monte-Carlo sampling using Markov chains, Biometrika 60(3), 607–612, 1973. https://doi.org/10.1093/biomet/60.3.607
• C. Kipnis and S. R. S. Varadhan, Central limit theorem for additive functionals of reversible Markov processes and applications to simple exclusions, Comm. Math. Phys. 104, 1–19, 1986. https://doi.org/10.1007/BF01210789
• A. Mira, Ordering and improving the performance of Monte Carlo Markov chains, Statist. Sci. 16(4), 340–350, 2001. https://doi.org/10.1214/ss/1015346318
• C. Andrieu and S. Livingstone, Peskun–Tierney ordering for Markovian Monte Carlo: beyond the reversible scenario, Ann. Statist. 49(4), 1958–1981, 2021. https://doi.org/10.1214/20-AOS2008