Functional Analysis

Motivation

Many problems in optimization, game theory and partial differential equations reduce to a monotone inclusion: find $x$ in a real Hilbert space $H$ with $0\in(A+B)(x)$, where $A$ is a maximally monotone set-valued operator with an easily computed resolvent and $B$ is a single-valued monotone operator. Saddle-point problems, variational inequalities and composite convex minimization are all of this form. Splitting methods solve such inclusions by evaluating $B$ forward and $A$ backward (through its resolvent), never inverting $A+B$.

The classical forward-backward method requires $B$ to be cocoercive, which excludes the skew operators arising from saddle-point problems. Tseng's forward-backward-forward method (2000) removed that assumption at the price of a second evaluation of $B$ per iteration. Malitsky and Tam (arXiv:1808.04162, SIAM J. Optim. 2020) introduced the forward-reflected-backward method, which needs only monotonicity and Lipschitz continuity of $B$ and evaluates $B$ once per iteration. Its §4, the subject of this mission, adds inertia (extrapolation along $x_k-x_{k-1}$) and relaxation (averaging with the previous iterate). Inertial and relaxed variants are used in practice to accelerate convergence and to enlarge the range of admissible step sizes; the inertial proximal point algorithm goes back to Alvarez and Attouch (2001).

Setting

Let $H$ be a real Hilbert space. A set-valued operator $A:H\rightrightarrows H$ is monotone if $\langle x-y,u-v\rangle\ge0$ whenever $u\in A(x)$, $v\in A(y)$, and maximally monotone if its graph is not properly contained in the graph of another monotone operator. Its resolvent with step $\gamma>0$ is $J_{\gamma A}=(I+\gamma A)^{-1}$, a single-valued map on all of $H$ when $A$ is maximally monotone. A map $B:H\to H$ is $L$-Lipschitz if $\|B(x)-B(y)\|\le L\|x-y\|$ and $\tfrac1L$-cocoercive if $\tfrac1L\|B(x)-B(y)\|^2\le\langle B(x)-B(y),x-y\rangle$ for all $x,y$. The zero set is $(A+B)^{-1}(0)=\{x: -B(x)\in A(x)\}$.

Given parameters $\alpha\ge0$, $\beta,\lambda>0$ and starting points $x_0,x_{-1}\in H$, the relaxed inertial forward-reflected-backward scheme (34) is

$$z_{k+1}=J_{\lambda A}\Big(x_k-\lambda B(x_k)-\frac{\lambda}{\beta}\big(B(x_k)-B(x_{k-1})\big)+\frac{\alpha}{\beta}(x_k-x_{k-1})\Big),\qquad x_{k+1}=(1-\beta)x_k+\beta z_{k+1}.$$

With $B'=B-\frac\alpha\lambda I$ it is equivalently (35), in which the inertial term is absorbed into $B'$. The case $\alpha=0$, $\beta=1$ is the forward-reflected-backward method; $\beta=1$ alone gives the inertial method (45).

Formalization targets

Goal: Theorem 4.3

If $A$ is maximally monotone, $B$ monotone, $(A+B)^{-1}(0)\ne\varnothing$, $\alpha\in[0,1)$, $\beta\in(0,1]$, $\lambda>0$, and either (a) $B$ is $L$-Lipschitz and

$$\lambda<\min\Big\{\frac{2-\beta-\alpha\beta-2\alpha}{2L},\frac{1-\alpha-\alpha\beta}{\beta L}\Big\},$$

or (b) $B$ is $\tfrac1L$-cocoercive, $\alpha<\frac{2-\beta}{2+\beta}$ and

$$\lambda<\min\Big\{\frac{2-\beta-\alpha\beta+2\alpha}{2L},\frac{1-\alpha+\alpha\beta}{\beta L}\Big\},$$

then the sequence $(x_k)$ of (34) converges weakly to a point of $(A+B)^{-1}(0)$.

Milestones

1. Lemma 4.1: $B-\rho I$ is $(L+\rho)$-Lipschitz if $B$ is $L$-Lipschitz, and $(L-\rho)$- or $\rho$-Lipschitz if $B$ is $\tfrac1L$-cocoercive and $\rho\le L/2$ or $\rho>L/2$.
2. (37): the resolvent inequality of Proposition 2.3 in the form used in §4.
3. Lemma 4.2: the energy inequality for (35), with $b_k=2\lambda\langle B(x)-B(x_k),x-x_k\rangle\ge0$.
4. (40): the sharper energy inequality with $(1-\beta)b_k$, from the proof of Lemma 4.2.
5. (43): the step-size conditions give $\varepsilon=\min\{\frac{2-\beta(1+\alpha)}2,\frac{1-\alpha}\beta\}-\lambda L'>0$.
6. The telescoped bound $\beta\varepsilon\|x_{k+1}-x\|^2+\varepsilon\sum_{i=1}^k\|x_{i+1}-x_i\|^2\le C_0$, with $C_0$ depending only on $x_0,x_{-1}$.
7. $(x_k)$ is bounded and $\|x_k-x_{k+1}\|\to0$.

A companion item states Corollary 4.4, the case $\beta=1$, where the conditions become $\alpha<\tfrac13$ with $\lambda<\frac{1-3\alpha}{2L}$ (Lipschitz) or $\lambda<\frac{1+\alpha}{2L}$ (cocoercive).

Significance

Theorem 4.3 gives an explicit region of $(\alpha,\beta,\lambda L)$ for which a single-evaluation, inertial, relaxed splitting method converges for monotone Lipschitz $B$, with no cocoercivity. In the cocoercive case it shows that inertia enlarges the admissible step size beyond that of the plain method (Corollary 4.4(b) allows $\lambda L<\frac{1+\alpha}2$); in the Lipschitz case it quantifies the opposite effect. With $B=0$ it recovers the convergence of the inertial proximal point algorithm by an argument different from the classical one.

The theorem is proved in the paper; to our knowledge none of §4 has been machine-checked. The mission produces a formal proof of Theorem 4.3 and of the Lyapunov inequalities behind it. The proof in the paper ends with "the remainder of the proof follows a similar argument to Theorem 2.5"; making that remainder explicit, in particular the convergence of the energy terms $b_k$, which rests on the factor $1-\beta$ in (40) rather than on Lemma 4.2 as printed, is part of the work.

Difficulty

The natural energy $\|x_k-x\|^2$ is not monotone along the iteration: both the reflected term $B(x_k)-B(x_{k-1})$ and the inertial term $x_k-x_{k-1}$ make it increase at some steps, and the standard Fejér argument for forward-backward methods does not apply. The energy that does decrease couples three consecutive iterates through $\langle B'(x_{k+1})-B'(x_k),x-x_{k+1}\rangle$ and the residual $b_k$, and this cross term has no sign. Showing that the energy controls $\|x_{k+1}-x\|^2$ from below, and that the step-size conditions (41) and (42) make all the coefficients positive, is where the specific constants come from. Passing from boundedness to weak convergence then needs an Opial-type argument and the demiclosedness of the graph of the maximally monotone operator $A+B$, in an infinite-dimensional space where bounded sequences only have weakly convergent subsequences.

Formalization scope

The Lean development works in a real inner product space H, complete for the goal and the corollary; the intermediate inequalities need neither completeness nor maximality of $A$ and assume only monotonicity. Operator notions come from the published module ThreeOpSplitting.Accel.MonotoneOperators; "$\tfrac1L$-cocoercive" is IsCocoercive L⁻¹ B. The resolvent is supplied as a family J : ℝ → H → H with the hypothesis that J γ is the resolvent of $\gamma A$ for every $\gamma>0$; for maximally monotone $A$ such a family exists and is unique, so this loses nothing. Sequences are shifted by one index: Lean's x j is $x_{j-1}$ and z j is $z_{j-1}$; the values z 0, z 1 are never used. Weak convergence is $\langle x_k,v\rangle\to\langle\bar x,v\rangle$ for all $v$, not norm convergence.

Committed conventions: $L>0$ is assumed (the step-size bounds divide by $L$); $B$ is assumed monotone in both cases, as printed; the constants of (41), (42), (43) and Lemma 4.2 are copied exactly. The resolvent hypothesis is not vacuous (the identity is a resolvent family of $A\equiv\{0\}$), the step-size range is not shrunk, and the conclusion is weak convergence to a zero, not a weaker boundedness or cluster-point statement.

A complete development needs: the Lyapunov inequalities (milestones 2–6), Opial's lemma for sequential weak cluster points, weak sequential compactness of bounded sets in a Hilbert space, and weak–strong closedness of the graph of a maximally monotone operator. The last three are reusable well beyond this mission and contributions of them are welcome.

Selected references

• Y. Malitsky, M. K. Tam, A Forward-Backward Splitting Method for Monotone Inclusions Without Cocoercivity, SIAM J. Optim. 30(2), 2020. arXiv:1808.04162, doi:10.1137/18M1207260
• P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38(2), 2000. doi:10.1137/S0363012998338806
• F. Alvarez, H. Attouch, An inertial proximal method for maximal monotone operators via discretization of a nonlinear oscillator with damping, Set-Valued Anal. 9, 2001. doi:10.1023/A:1011253113155
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. doi:10.1007/978-3-319-48311-5

Monotone inclusions and the cost of splitting

Many problems in convex optimization, variational inequalities and saddle-point computation can be written as a monotone inclusion: find $x$ in a real Hilbert space $H$ with

$$0 \in (A+B)(x),$$

where $A$ is a set-valued maximally monotone operator (a subdifferential, a normal cone, a constraint) and $B$ is a single-valued monotone operator (a gradient, or the skew operator of a saddle-point problem). Splitting methods solve such problems using $A$ and $B$ separately: a backward step evaluates the resolvent $J_{\lambda A}=(I+\lambda A)^{-1}$, and a forward step evaluates $B$.

The classical forward-backward method $x_{k+1}=J_{\lambda A}(x_k-\lambda B(x_k))$ converges when $B$ is cocoercive, but can fail when $B$ is merely monotone and Lipschitz, which is the case for saddle-point operators such as $B(z_1,z_2)=(z_2,-z_1)$. Tseng's forward-backward-forward method (Tseng 2000) removes the cocoercivity assumption at the price of two evaluations of $B$ per iteration. Malitsky and Tam (arXiv:1808.04162; SIAM J. Optim. 30(2), 2020) propose the forward-reflected-backward method, which needs one evaluation of $B$ and one resolvent of $A$ per iteration, reusing the previous value of $B$.

Timeline of the relevant results:

• 1967: Opial's lemma on weak convergence of sequences in Hilbert space (Opial 1967).
• 1979: Lions and Mercier analyse forward-backward splitting with cocoercive $B$ (Lions–Mercier 1979).
• 1980: Popov's modified Arrow–Hurwicz method for saddle points, with one operator evaluation per step (Popov 1980).
• 2000: Tseng's forward-backward-forward method for monotone and Lipschitz $B$.
• 2015: Malitsky's projected reflected gradient method for variational inequalities (Malitsky 2015), the special case $A=N_C$, $B$ affine.
• 2018–2020: Malitsky and Tam, the forward-reflected-backward method, Theorem 2.5.

Setting

$H$ is a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$. A set-valued operator $A:H\rightrightarrows H$ is monotone if $\langle x-y,u-v\rangle\ge 0$ whenever $u\in A(x)$, $v\in A(y)$, and maximally monotone if its graph is not properly contained in the graph of another monotone operator. Its resolvent $J_{\lambda A}=(I+\lambda A)^{-1}$ is, for $\lambda>0$ and $A$ maximally monotone, an everywhere defined single-valued map, characterised by $\lambda^{-1}(w-J_{\lambda A}w)\in A(J_{\lambda A}w)$. A map $B:H\to H$ is $L$-Lipschitz if $\|B(x)-B(y)\|\le L\|x-y\|$, and monotone if $\langle x-y,B(x)-B(y)\rangle\ge0$.

The zero set is $(A+B)^{-1}(0)=\{x : -B(x)\in A(x)\}$. Given initial points $x_0,x_{-1}\in H$ and step sizes $(\lambda_k)_{k\ge-1}$, the forward-reflected-backward method is

$$x_{k+1}=J_{\lambda_k A}\big(x_k-\lambda_k B(x_k)-\lambda_{k-1}(B(x_k)-B(x_{k-1}))\big)\qquad\forall k\in\mathbb N. \tag{13}$$

A sequence $(x_k)$ converges weakly to $\bar x$ if $\langle x_k,v\rangle\to\langle\bar x,v\rangle$ for every $v\in H$; a sequential weak cluster point is the weak limit of a subsequence.

Formalization targets

Goal: Theorem 2.5 (p. 6)

If $A$ is maximally monotone, $B$ is monotone and $L$-Lipschitz, $(A+B)^{-1}(0)\ne\varnothing$, and $(\lambda_k)\subseteq[\varepsilon,\tfrac{1-2\varepsilon}{2L}]$ for some $\varepsilon>0$, then every sequence generated by (13) satisfies

$$x_k\rightharpoonup\bar x\quad\text{for some }\bar x\in(A+B)^{-1}(0).$$

Milestones

In attack order:

1. Proposition 2.3, the basic inequality (19) for one resolvent step.
2. Lemma 2.4, the energy inequality (20).
3. The telescoped bound after (24).
4. Boundedness of $(x_k)$ and $\|x_k-x_{k+1}\|\to0$.
5. Weak cluster points lie in the zero set.
6. Convergence of the energy (26).
7. Its limit equals $\lim\|x_k-\bar x\|^2$.
8. Lemma 2.2, an Opial-type criterion for weak convergence.

Corollary 2.6, the constant-step case $\lambda\in(0,\tfrac1{2L})$, is included as a companion theorem.

Significance

Theorem 2.5 shows that monotone inclusions with a Lipschitz, non-cocoercive single-valued part can be solved by a splitting method with the per-iteration cost of forward-backward splitting: one forward and one backward evaluation. For saddle-point problems, where each evaluation of $B$ is a pair of matrix–vector products, this halves the operator cost of Tseng's method. The method contains the projected reflected gradient method and, for $A=0$, Popov's method and the optimistic gradient method used in training generative adversarial networks (Remark 2.1). The analysis of this section is reused for the linear rate, the linesearch, the inertial variant and the three-operator variant of later sections (missions 2–5 of this series).

The theorem is proved in the paper. Formalizing it requires a machine-checked Opial-type lemma and a machine-checked demiclosedness argument for maximally monotone operators perturbed by a continuous monotone map, both reusable well beyond this mission. To our knowledge no machine-checked proof of convergence of the forward-reflected-backward method exists.

Difficulty

The energy inequality of Lemma 2.4 is algebra plus monotonicity and the Lipschitz estimate, and it yields boundedness and $\|x_{k+1}-x_k\|\to0$. The difficulty lies in passing from these facts to weak convergence of the whole sequence. Norm convergence is false in general, so a Cauchy-sequence argument is unavailable. The energy is not Fejér monotone in $\|x_k-x\|$ alone, because of the cross term $2\lambda_{k-1}\langle B(x_k)-B(x_{k-1}),x-x_k\rangle$, so the standard Fejér/Opial lemma does not apply directly. Identifying weak cluster points as zeros requires the weak-strong closedness of the graph of $A+B$, which in turn rests on maximal monotonicity of the sum: this is not a consequence of monotonicity of the two parts, and the inclusion (25) can be passed to the limit only because the step sizes stay above $\varepsilon$.

Formalization scope

The Lean development uses a real inner product space H (InnerProductSpace ℝ H), complete wherever the page needs it, and the published operator vocabulary ThreeOpSplitting.Accel.MonotoneOperators (monotone and maximally monotone set-valued operators, monotone and Lipschitz single-valued maps, resolvents). Conventions:

• Resolvents are hypotheses. The iteration is driven by a family $J:\mathbb R\to H\to H$ with $\gamma^{-1}(w-J(\gamma)w)\in A(J(\gamma)w)$ for all $\gamma>0$, $w\in H$; for maximally monotone $A$ such a family exists and is unique. The goal keeps maximal monotonicity of $A$ as a hypothesis as well.
• Index shift. Lean's x j is $x_{j-1}$ and lam j is $\lambda_{j-1}$; the initial points are arbitrary.
• Step range. Every $\lambda_j$, $j\ge-1$, lies in $[\varepsilon,(1-2\varepsilon)/(2L)]$, including $\lambda_{-1}$ as on p. 4. $L>0$ is assumed, since the range divides by $L$.
• Weak convergence is convergence of $\langle x_k,v\rangle$ for every $v$; cluster points are sequential weak cluster points (subsequences along strictly increasing index maps).
• Several milestones are stated in a stronger form than the page, with $A$ only monotone, $H$ not complete, or a conclusion for every zero rather than the cluster point. Each item's note says which.

Three formalizations would trivialize the goal and are excluded:

• an unconstrained resolvent map;
• norm convergence or convergence of a subsequence in place of weak convergence of the whole sequence;
• a step range shrunk or pinned to a constant.

A complete development needs the Opial-type Lemma 2.2, which in turn needs weak sequential compactness of bounded sets in Hilbert space, and maximal monotonicity of $A+B$ for continuous monotone $B$ (Bauschke–Combettes, Corollaries 20.25 and 24.4(i)) with its demiclosedness (Proposition 20.33). These are general results of monotone operator theory, and contributions of them as separate theorems are welcome.

Selected references

• Y. Malitsky and M. K. Tam, A Forward-Backward Splitting Method for Monotone Inclusions Without Cocoercivity, SIAM J. Optim. 30(2), 2020; arXiv:1808.04162v4. https://arxiv.org/abs/1808.04162v4 (DOI https://doi.org/10.1137/18M1207260)
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
• P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38(2), 2000. https://doi.org/10.1137/S0363012998338806
• Y. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM J. Optim. 25(1), 2015. https://doi.org/10.1137/14097238X
• L. D. Popov, A modification of the Arrow–Hurwicz method for search of saddle points, Math. Notes 28, 1980. https://doi.org/10.1007/BF01141092
• P.-L. Lions and B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM J. Numer. Anal. 16(6), 1979. https://doi.org/10.1137/0716071
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73, 1967. https://doi.org/10.1090/S0002-9904-1967-11761-0

Motivation

Distance covariance was introduced by Székely, Rizzo and Bakirov (2007) as a measure of dependence between random vectors in Euclidean spaces: it is zero exactly when the vectors are independent, and its empirical version gives a consistent test of independence that needs no moment beyond the first. Lyons (2013) asked for which metric spaces the same holds. His Theorem 3.11 shows that it holds whenever both spaces have strong negative type. This mission formalizes the complementary result, Proposition 3.15 of the same paper: the hypothesis on the space cannot be removed. Without negative type, distance covariance can even be negative; without strong negative type, it can vanish on a law that is not a product. Together with Theorem 3.11, the proposition locates the boundary of metric spaces on which distance covariance is a valid test of independence.

Timeline. 2007: Székely, Rizzo and Bakirov define distance covariance on $\mathbb R^p\times\mathbb R^q$ and prove the independence characterization there. 2013: Lyons extends the theory to metric spaces of negative type, characterizes the spaces where it remains a test of independence as those of strong negative type, and proves Proposition 3.15. 2018 and 2021: two errata by the author correct several statements of the paper; the first of them adds the standing assumption that all metric spaces are separable. Proposition 3.15 is not affected by the corrections.

Setting

Let $(\mathcal X,d)$ and $(\mathcal Y,d)$ be separable metric spaces, each with its Borel $\sigma$-field. A finite Borel measure $\mu$ on $\mathcal X$ has a finite first moment if $\int d(o,x)\,d\mu(x)<\infty$ for some point $o$. For such $\mu$ put

$$a_\mu(x):=\int d(x,x')\,d\mu(x'),\qquad D(\mu):=\int d(x,x')\,d\mu^2(x,x'),$$

and define the doubly centred distance $d_\mu(x,x'):=d(x,x')-a_\mu(x)-a_\mu(x')+D(\mu)$. For two probability measures $\mu_1,\mu_2$ with finite first moments, $D(\mu_1-\mu_2)$ is the energy of their difference,

$$D(\mu_1-\mu_2)=\iint d\,d\mu_1^2-2\iint d\,d(\mu_1\times\mu_2)+\iint d\,d\mu_2^2 .$$

Let $\theta$ be a Borel probability measure on $\mathcal X\times\mathcal Y$ whose marginals $\mu$ on $\mathcal X$ and $\nu$ on $\mathcal Y$ have finite first moments. Its distance covariance is

$$\operatorname{dcov}(\theta):=\int d_\mu(x,x')\,d_\nu(y,y')\,d\theta^2\big((x,y),(x',y')\big).$$

$\theta$ is a product measure if $\theta=\mu\times\nu$.

$\mathcal X$ has negative type if for every $n$, all points $x_1,\dots,x_n$ and all reals $\alpha_1,\dots,\alpha_n$ with $\sum_i\alpha_i=0$,

$$\sum_{i,j\le n}\alpha_i\alpha_j\,d(x_i,x_j)\le 0. \tag{3.1}$$

On such a space $D(\mu_1-\mu_2)\le 0$ for all probability measures with finite first moments, and $\mathcal X$ has strong negative type if moreover equality holds only when $\mu_1=\mu_2$. Write $\delta(y)$ for the point mass at $y$.

Formalization targets

Goal: Proposition 3.15

Let $\mathcal Y$ have at least two points.

1. If $\mathcal X$ is not of negative type, there is a probability measure $\theta$ on $\mathcal X\times\mathcal Y$ whose marginals have finite first moments and

$$\operatorname{dcov}(\theta)<0.$$

2. If $\mathcal X$ is not of strong negative type, there is a probability measure $\theta$ on $\mathcal X\times\mathcal Y$ whose marginals have finite first moments, with

$$\operatorname{dcov}(\theta)=0\quad\text{and}\quad \theta\neq\mu\times\nu .$$

The space $\mathcal Y$ is arbitrary apart from having two points, so the statement fixes nothing about it.

Milestones (all from the proof on p. 17)

1. For probability measures $\mu_1,\mu_2$ with finite first moments and $y_1\ne y_2$, the law $\theta=\big(\mu_1\times\delta(y_1)+\mu_2\times\delta(y_2)\big)/2$ has $\operatorname{dcov}(\theta)=-d(y_1,y_2)\,D(\mu_1-\mu_2)/8$.
2. If $\mathcal X$ is not of negative type, there are probability measures $\mu_1\neq\mu_2$ with finite first moments and $D(\mu_1-\mu_2)>0$.
3. If $x_1\neq x_2$ then $D(\delta(x_1)-\delta(x_2))<0$.
4. If $D(\mu_1-\mu_2)\ge 0$ and $x_1\ne x_2$, some $\gamma\in(0,1]$ makes $\tau_i:=\gamma\mu_i+(1-\gamma)\delta(x_i)$ satisfy $D(\tau_1-\tau_2)=0$.
5. For $\mu_1\ne\mu_2$ with $D(\mu_1-\mu_2)\ge0$, $x_1\ne x_2$, $\gamma\in(0,1]$ and $y_1\ne y_2$, the law $\big(\tau_1\times\delta(y_1)+\tau_2\times\delta(y_2)\big)/2$ is not a product measure.

Significance

The result. Theorem 3.11 of the paper shows that strong negative type of both spaces suffices for $\operatorname{dcov}(\theta)=0$ to characterize independence. Proposition 3.15 shows the hypothesis on each factor is necessary: a single failure of (3.1) already produces a law with negative distance covariance, so $\operatorname{dcov}$ is not even a nonnegative quantity there, and a single pair of distinct laws with $D(\mu_1-\mu_2)=0$ produces a dependent law that the test cannot detect. Consequently, any use of distance covariance on general metric data (graphs, $\ell^p$ spaces with $p>2$, spaces of distributions under Wasserstein metrics) has to verify strong negative type first. Since the two-point space $\mathcal Y$ is arbitrary, the failure is a property of $\mathcal X$ alone.

Formalizing it. The proposition is proved in the paper; no machine-checked proof of it, or of any result about distance covariance, is known to exist. The mission produces a formal definition of distance covariance on separable metric spaces, of negative and strong negative type in the paper's measure-theoretic form, and the computation of $\operatorname{dcov}$ on two-point mixtures. These are the same objects as in the sibling mission on Theorem 3.11, so the two together give a formal account of when distance covariance characterizes independence.

Difficulty

The step the paper calls "a little algebra" is the bulk of the work: $\operatorname{dcov}$ is a four-fold integral of a product of doubly centred distances, each of which is itself built from integrals against a marginal of $\theta$, and every manipulation of it happens inside Bochner integrals over product measures whose integrability has to be derived from first moments alone. In a formal setting nothing about these integrals is automatic. The passage from a violation of the finite-sum condition (3.1) to two probability measures with $D(\mu_1-\mu_2)>0$ is left implicit in the paper. The non-product claim also uses a fact the page does not state: that $\tau_1\neq\tau_2$, which follows from $D(\mu_1-\mu_2)\ge 0$ and is false without it.

Formalization scope

All metric spaces carry their Borel $\sigma$-field and are assumed second countable, which for metric spaces is separability; this is the author's own correction, Errata (i), which makes $d$ measurable on the product. Measures are Mathlib measures with values in $[0,\infty]$; mixture weights such as $\gamma$, $1-\gamma$ and $1/2$ enter as extended nonnegative reals, and $\gamma$ is always restricted to $(0,1]$. Because Mathlib's Bochner integral does not integrate against signed measures, $D(\mu_1-\mu_2)$ is defined as the bilinear energy expansion displayed above. "Not a product measure" means $\theta$ differs from the product of its own marginals, never from some other product.

Several formalizations of this statement would be trivially true and are excluded. A Bochner integral of a non-integrable function is $0$ in Lean, so every statement either assumes or concludes the finite first moments that make $\operatorname{dcov}$ and $D$ genuine integrals. Negative type is the finite-sum condition (3.1) and strong negative type the measure condition of p. 11, never an embedding property. The product condition is tested against $\theta$'s own marginals, not against free factors. $\mathcal Y$ is quantified before $\theta$ is chosen, and part 2's hypothesis is the full negation of strong negative type, which includes spaces of negative type.

A complete development needs integrability of $d_\mu\,d_\nu$ under $\theta^2$ from first moments (Lemma 2.1 of the paper), linearity of the energy in each measure, push-forwards of mixtures of product measures, and the intermediate value theorem. The integrability and energy-bilinearity lemmas are reusable for any work on energy distance or distance covariance. Contributions of these general lemmas, as well as of proofs of the individual milestones, are welcome.

Selected references

• R. Lyons, Distance covariance in metric spaces, Ann. Probab. 41 (2013), 3284–3305, https://doi.org/10.1214/12-AOP803; author's version arXiv:1106.5758 (version of 19 Dec. 2020, with errata). https://arxiv.org/abs/1106.5758
• R. Lyons, Errata to "Distance covariance in metric spaces", Ann. Probab. 46 (2018), 2400–2405; reproduced as pp. 24–29 of arXiv:1106.5758 (version of 19 Dec. 2020). https://arxiv.org/abs/1106.5758
• R. Lyons, Second errata to "Distance covariance in metric spaces", Ann. Probab. 49 (2021), 2668–2670; reproduced as pp. 30–32 of arXiv:1106.5758 (version of 19 Dec. 2020). https://arxiv.org/abs/1106.5758
• G. J. Székely, M. L. Rizzo, N. K. Bakirov, Measuring and testing dependence by correlation of distances, Ann. Statist. 35 (2007), 2769–2794. https://doi.org/10.1214/009053607000000505

Motivation

Distance covariance is a statistic for testing whether two random variables are independent. Székely, Rizzo and Bakirov introduced it for Euclidean spaces (Ann. Statist. 2007): the population distance covariance of a joint law $\theta$ is $0$ exactly when $\theta$ is a product measure, so a consistent test of independence follows. Lyons (arXiv:1106.5758) extended the statistic to arbitrary metric spaces and showed that the characterization of independence holds on a pair of metric spaces precisely when both have strong negative type (his Theorem 3.11 and Proposition 3.15). That makes strong negative type the property a statistician has to check before using distance covariance on a given space. Functional data, the main case in practice, live in Hilbert spaces.

This mission formalizes Lyons's Theorem 3.16: every separable Hilbert space is of strong negative type. Kosorok (2009, cited by Lyons) had asked whether the characterization of independence extends to Hilbert spaces.

Timeline.

• 1935–1938: Schoenberg shows that a metric space has negative type exactly when its distance is the squared distance of a subset of a Hilbert space (Trans. AMS 1938).
• 1982 and 1986: Koldobskiĭ (Theorem 1) and Linde (Theorem 6), as cited by Lyons, prove results on positive definite functions and stable measures in Banach spaces from which Theorem 3.16 follows, together with its analogue for separable $L^p$, $1<p<2$.
• 2007: Székely, Rizzo and Bakirov treat the Euclidean case.
• 2013: Lyons gives a direct proof of Theorem 3.16 through a Gaussian version of the Crofton embedding.
• 2018: the first Errata (Ann. Probab. 46) supply the justification of a continuity claim at the end of that proof (Errata (x)). They also note that Hilbert spaces were tacitly assumed real (Errata (viii)).

Setting

Let $(\mathscr X,d)$ be a separable metric space with its Borel $\sigma$-field. A Borel probability measure $\mu$ has a finite first moment if $\int d(o,x)\,d\mu(x)<\infty$ for some $o\in\mathscr X$. For two such measures write $E(\mu_1,\mu_2)=\iint d(x,x')\,d\mu_1(x)\,d\mu_2(x')$ and

$$D(\mu_1-\mu_2)=E(\mu_1,\mu_1)-2E(\mu_1,\mu_2)+E(\mu_2,\mu_2),$$

the integral of $d$ against the square of the signed measure $\mu_1-\mu_2$.

The space has negative type if, for all $n$, all $x_1,\dots,x_n\in\mathscr X$ and all real $\alpha_1,\dots,\alpha_n$ with $\sum_i\alpha_i=0$,

$$\sum_{i,j\le n}\alpha_i\alpha_j\,d(x_i,x_j)\le0. \tag{3.1}$$

By approximation, negative type gives $D(\mu_1-\mu_2)\le0$ for all probability measures with finite first moments. The space has strong negative type if it has negative type and $D(\mu_1-\mu_2)=0$ only when $\mu_1=\mu_2$. Strict negative type is the same condition restricted to finitely supported measures.

The proof works on $\ell^2(\mathbb Z^+)$ and uses the following objects. $\rho$ is the law on $\mathbb R^\infty$ of an IID standard normal sequence $Z_1,Z_2,\dots$; $\lambda$ is Lebesgue measure on $\mathbb R$; $c=\mathbf E|Z_1|$. For $w,u\in\mathbb R^\infty$ put $w(u)=\limsup_N\sum_{n\le N}u_nw_n$. The Gaussian Crofton embedding sends $u$ to the function

$$\phi(u)(w,s)=\mathbf 1_{[w(u)/c,\infty)}(s)-\mathbf 1_{[0,\infty)}(s)$$

on $\mathbb R^\infty\times\mathbb R$. For probability measures $\mu_1,\mu_2$ on $\ell^2$, its barycenter at $\mu=\mu_1-\mu_2$ is the function $\beta_\phi(\mu)(w,s)=\mu\{u\,;\,w(u)\le cs\}$.

Formalization targets

Goal: Theorem 3.16

$$H \text{ a separable real Hilbert space}\ \Longrightarrow\ H \text{ is of strong negative type.}$$

Milestones, in the order the proof uses them

1. $Z(u)=\sum u_nZ_n$ converges $\rho$-a.s., is centered normal with variance $\|u\|_2^2$, and $\mathbf E|Z(u)|=c\|u\|_2$ (p. 18).
2. The isometry $\|\phi(u)-\phi(u')\|_2^2=\|\phi(u)-\phi(u')\|_1=\|u-u'\|_2$ (p. 18).
3. Every Hilbert space has negative type, indeed strict negative type (p. 18).
4. $D(\mu_1-\mu_2)=-2\int\beta_\phi(\mu_1-\mu_2)^2\,d(\rho\times\lambda)$: identity (3.4) for the Gaussian embedding (pp. 11, 18).
5. The Cramér–Wold reduction: agreement of $\mu_i\{\langle u,v\rangle\le s\}$ for all finitely supported $v$ forces $\mu_1=\mu_2$ (p. 18).
6. If $\beta_\phi(\mu)=0$ holds $\rho\times\lambda$-a.e., then for $\rho$-a.e. $w$ it vanishes at $((v,w),s)$ for all $v\in\mathbb R^K$ and $s\in\mathbb R$ (p. 19; Errata (x)).
7. If the conclusion of 6 holds for every $K$, then $\mu_1[\langle u_{\le L},v\rangle\le s]=\mu_2[\langle u_{\le L},v\rangle\le s]$ for all $L$, $v$, $s$ (p. 19).

The goal has no constants. Each milestone states a claim of the paper in the paper's strength.

Significance

The result. With Theorem 3.11, Theorem 3.16 shows that for random elements of separable Hilbert spaces, zero distance covariance is equivalent to independence. Distance-covariance tests are therefore consistent for curves, images and other functional data. It also yields Corollary 3.18: if $(\mathscr X,d)$ is a separable metric space of negative type, then $(\mathscr X,d^{1/2})$ has strong negative type, so a test of independence is available on every separable space of negative type after a change of metric. Remark 3.17 shows that separability cannot simply be dropped: a non-separable Hilbert space is of strong negative type exactly when its dimension is a cardinal of measure zero.

The formalization. The theorem is proved, and to our knowledge no proof of it, or of negative type of Hilbert spaces, is machine-checked. A complete development needs four things:

• the Gaussian series on $\ell^2$, built from Mathlib's Measure.infinitePi and gaussianReal;
• an $L^1$/$L^2$ isometry for a Crofton-type embedding;
• the identity between the energy distance and a squared barycenter norm;
• the fact that a finite Borel measure on $\ell^2$ is determined by its one-dimensional projections.

Each of these is reusable outside distance covariance: the first in Gaussian measure theory, the last whenever laws on sequence spaces are compared.

Difficulty

The first idea is to approximate. Euclidean spaces have strict negative type, finite-dimensional projections of a Hilbert space are Euclidean, and probability measures are limits of finitely supported ones. Approximation preserves the inequality $D(\mu_1-\mu_2)\le0$, but it does not preserve the equality case. A limit of strictly negative quantities may be $0$ even though $\mu_1\neq\mu_2$. Remark 3.3 of the paper exhibits a space of strict but not strong negative type, so this gap is real.

The second idea is to transport the finite-dimensional Crofton embedding, in which $\|x-y\|$ is the measure of half-spaces separating $x$ and $y$. It fails because $\ell^2$ has no rotation-invariant Lebesgue measure on its half-spaces. The Gaussian measure $\rho$ replaces it. But $w(u)$ is defined only $\rho$-almost surely, and its exceptional set depends on $u$. As a result, "$\beta_\phi(\mu)=0$ almost everywhere" does not immediately give information for every direction $v$ and level $s$. That passage from almost every $(v,s)$ to every $(v,s)$ is the step the 2018 Errata had to justify.

Formalization scope

Lean conventions, all disclosed in the items:

• Spaces. A Hilbert space is a real InnerProductSpace ℝ H with CompleteSpace H, as Errata (viii) prescribes; a complex space has the distances of its realification. Separability is SecondCountableTopology, which matches the standing separability of Errata (i). $\ell^2(\mathbb Z^+)$ is lp (fun _ : ℕ => ℝ) 2 with the Borel $\sigma$-field, declared in the Setting file because Mathlib supplies none.
• Indices start at $0$.
• The energy term. $D(\mu_1-\mu_2)$ is the three-term energy expansion, since Mathlib does not integrate against signed measures. A signed measure $\mu_1-\mu_2$ is always handled through the pair $(\mu_1,\mu_2)$.
• Junk values. $\limsup$ is taken in $\mathbb R$, so its junk value on divergent sequences lives on a $\rho$-null set; statements about $w(u)$ are made $\rho$-a.e. or under integrals. $c$ is the integral $\int|z|\,dN(0,1)$. $\phi(u)$ is a plain function, and $L^p(\rho\times\lambda)$ norms are written as integrals, with integrability asserted alongside each one.

Trivializing encodings are ruled out:

• negative and strong negative type are defined by (3.1) and the equality case of (3.3), never through an embedding or the injectivity of a barycenter map;
• every item about $D$ carries finite-first-moment hypotheses, so no integral silently takes the junk value $0$.

Contributions are welcome on any milestone. The reduction of a general separable $H$ to $\ell^2(\mathbb Z^+)$ (by an isometry onto a closed subspace) is not posed separately and belongs to the goal's proof. Mathlib's Measure.ext_of_charFun, for finite measures on complete second-countable real inner product spaces, is a natural tool for milestone 5. Separability of lp is not yet an instance in Mathlib.

Selected references

• R. Lyons, Distance covariance in metric spaces, Ann. Probab. 41 (2013), 3284–3305; Errata, Ann. Probab. 46 (2018), 2400–2405; Second Errata, Ann. Probab. 49 (2021), 2668–2670. Author's version of 19 Dec. 2020, including both errata: https://arxiv.org/abs/1106.5758
• G. J. Székely, M. L. Rizzo, N. K. Bakirov, Measuring and testing dependence by correlation of distances, Ann. Statist. 35 (2007), 2769–2794. https://doi.org/10.1214/009053607000000505
• I. J. Schoenberg, Metric spaces and positive definite functions, Trans. Amer. Math. Soc. 44 (1938), 522–536. https://doi.org/10.1090/S0002-9947-1938-1501980-0

Motivation

Testing whether two random quantities are independent is one of the basic tasks of statistics. Classical correlation only detects linear dependence. Distance covariance, introduced by Székely, Rizzo and Bakirov (Ann. Statist. 2007) for random vectors in Euclidean spaces, is a dependence measure that vanishes exactly under independence. It only needs the distances between sample points, and its empirical version is a simple V-statistic. These properties made it a standard tool for nonparametric independence testing.

Lyons (Ann. Probab. 41 (2013), arXiv:1106.5758) asked in which metric spaces this characterization of independence survives. The answer is the class of metric spaces of strong negative type, which includes all separable Hilbert spaces. On such spaces, distance covariance gives a test of independence that is consistent against every alternative. This mission formalizes that result, Theorem 3.11 of the paper, together with the chain of results its proof rests on.

Timeline. Schoenberg (1937, 1938) characterized metric spaces of negative type by isometric embeddings of $(\mathcal X,d^{1/2})$ into Hilbert space. Székely, Rizzo and Bakirov (2007) defined distance covariance on $\mathbb R^p\times\mathbb R^q$ and proved that it vanishes only under independence. Lyons (2013) extended the theory to general metric spaces and identified strong negative type as the exact condition. The Errata (Ann. Probab. 46 (2018), 2400–2405; included in arXiv:1106.5758, pp. 24–29) added a standing separability assumption and repaired a gap in Lemma 3.8. The Second Errata appeared in Ann. Probab. 49 (2021).

Setting

Let $(\mathcal X,d)$ and $(\mathcal Y,d)$ be separable metric spaces with their Borel $\sigma$-fields. A finite measure $\mu$ on $\mathcal X$ has a finite first moment if $\int d(o,x)\,d\mu(x)<\infty$ for some (equivalently every) $o\in\mathcal X$. For such $\mu$ define

$$a_\mu(x)=\int d(x,x')\,d\mu(x'),\qquad D(\mu)=\int d(x,x')\,d\mu^2(x,x'),$$ $$d_\mu(x,x')=d(x,x')-a_\mu(x)-a_\mu(x')+D(\mu).$$

For a probability measure $\theta$ on $\mathcal X\times\mathcal Y$ whose marginals $\mu$ and $\nu$ have finite first moments, the distance covariance is

$$\operatorname{dcov}(\theta)=\int d_\mu(x,x')\,d_\nu(y,y')\,d\theta^2\big((x,y),(x',y')\big).$$

$\theta$ is a product measure if $\theta=\mu\times\nu$.

$(\mathcal X,d)$ has negative type if $\sum_{i,j\le n}\alpha_i\alpha_j d(x_i,x_j)\le0$ for all $n$, all points $x_1,\dots,x_n$ and all real weights with $\sum_i\alpha_i=0$. For finite measures $\mu_1,\mu_2$ with finite first moments, $D(\mu_1-\mu_2)$ is the integral of $d$ against $(\mu_1-\mu_2)^2$. On spaces of negative type $D(\mu_1-\mu_2)\le0$ for probability measures $\mu_1,\mu_2$. The space has strong negative type if, in addition, $D(\mu_1-\mu_2)=0$ only when $\mu_1=\mu_2$.

An embedding is a map $\phi:\mathcal X\to H$ into a real Hilbert space with $d(x,x')=\|\phi(x)-\phi(x')\|^2$. Its barycenter map is $\beta_\phi(\mu)=\int\phi\,d\mu$. The tensor embedding $(x,y)\mapsto\phi(x)\otimes\psi(y)$ takes values in the Hilbert tensor product $H\otimes K$. $M^1(\mathcal X)$ denotes the finite signed measures whose variation has finite first moment. $M^{1,1}(\mathcal X\times\mathcal Y)$ denotes those on the product whose variation has marginals of finite first moment.

Formalization targets

Goal: Theorem 3.11

If $\mathcal X$ and $\mathcal Y$ have strong negative type and the marginals $\mu,\nu$ of the probability measure $\theta$ have finite first moments, then

$$\operatorname{dcov}(\theta)=0\ \Longrightarrow\ \theta=\mu\times\nu .$$

Milestones

1. Lemma 2.1: $d_\mu\in L^2(\mu\times\mu)$. The integrability of $d_\mu(x,x')d_\nu(y,y')$ against $\theta^2$ (p. 4) follows, so $\operatorname{dcov}(\theta)$ is a genuine integral.
2. Schoenberg's theorem (p. 9): a separable space has negative type if and only if it has an embedding into $\ell^2(\mathbb N)$.
3. Identity (3.4): $D(\mu)=-2\|\beta_\phi(\mu)\|^2$ when $\mu(\mathcal X)=0$. Proposition 3.1: strong negative type holds iff $\beta_\phi$ is injective on probability measures with finite first moment.
4. Proposition 3.5: $d_\mu(x,x')=-2\langle\phi(x)-\beta_\phi(\mu),\phi(x')-\beta_\phi(\mu)\rangle$, together with $a_\mu(x)=\|\phi(x)-\beta_\phi(\mu)\|^2+D(\mu)/2$ and $D(\mu)=2\operatorname{Var}(\phi(X))$.
5. Proposition 3.7: $\operatorname{dcov}(\theta)=4\|\beta_{\phi\otimes\psi}(\theta-\mu\times\nu)\|^2$.
6. Lemma 3.9 (injectivity of $\beta_\phi$ on $M^1(\mathcal X)$) and Lemma 3.8 in its errata form (injectivity of $\beta_{\phi\otimes\psi}$ on $M^{1,1}(\mathcal X\times\mathcal Y)$).

The converse, that a product measure has $\operatorname{dcov}(\theta)=0$ (p. 5), is included as a companion statement.

Significance

The result. Theorem 3.11 makes the empirical distance covariance a consistent test of independence against all alternatives on any pair of separable metric spaces of strong negative type. Examples are separable Hilbert spaces and their subsets, and every space of negative type after replacing $d$ by $d^r$, $0<r<1$. Its companion, Proposition 3.15 (a separate mission of this series), shows that strong negative type is exactly the right hypothesis. Proposition 3.7 also identifies distance covariance with Brownian covariance and with the original Euclidean definition, through specific choices of embedding.

Formalizing it. The result is proved, with the gap in Lemma 3.8 closed by the Errata (2018). No part of it has a machine-checked proof that we know of. A formalization needs barycenters of Hilbert-space-valued maps against measures, the Hilbert tensor product of two real Hilbert spaces, and Schoenberg's embedding theorem. None of these is in Mathlib in this form, and all are reusable well beyond distance covariance.

Difficulty

The obvious route reads $\operatorname{dcov}(\theta)=0$ as "the barycenters of $\theta$ and of $\mu\times\nu$ coincide in $H\otimes K$" and concludes by injectivity. Strong negative type only gives injectivity of $\beta_\phi$ on probability measures, while $\theta-\mu\times\nu$ is a signed measure on a product space. Getting from injectivity on single factors to injectivity on $M^{1,1}$ of the product is where the original proof had a gap: an auxiliary signed measure built from $\theta$ was not shown to have a finite first moment. The errata version changes the embeddings so that this can be done. Two smaller obstacles are integrability (the definition of $\operatorname{dcov}$ is meaningful only by Lemma 2.1) and the construction of the Hilbert space in Schoenberg's theorem.

Formalization scope

All spaces are Lean metric spaces with their Borel $\sigma$-fields and SecondCountableTopology. This is the separability the author adds in Errata (i), which makes $d$ measurable on the product. Measures are Mathlib Measures. A probability $\theta$ on $\mathcal X\times\mathcal Y$ has marginals θ.map Prod.fst and θ.map Prod.snd. "Product measure" means $\theta$ equals the product of these marginals. Hilbert spaces are real (Errata (viii)). Existential embeddings land in $\ell^2(\mathbb N)$, which suffices for separable spaces. The Hilbert tensor product is the completion of the algebraic tensor product with its inner product. $D(\mu_1-\mu_2)$ is defined by its bilinear expansion. Injectivity on $M^1$ and $M^{1,1}$ is stated for pairs of finite measures, which is equivalent to injectivity on signed measures via the Jordan decomposition.

Every integral here is a Bochner integral, which is $0$ for a non-integrable integrand. Each statement therefore carries the finite-first-moment hypotheses of the paper, and integrability itself is a milestone. Negative type and strong negative type are defined by (3.1) and by the condition on $D(\mu_1-\mu_2)$, not through an embedding or a barycenter map, so Schoenberg's theorem and Proposition 3.1 are not definitional. A statement with a "product measure" whose factors are free, or with dcov defined without the moment hypotheses, would be a different and trivializable theorem.

Welcome contributions: barycenter calculus for Hilbert-valued integrals, tensor-product integrals, Schoenberg's theorem, and proofs of any milestone.

Selected references

• R. Lyons, Distance covariance in metric spaces, Ann. Probab. 41 (2013), 3284–3305. https://doi.org/10.1214/12-AOP803 ; author's version with both errata: https://arxiv.org/abs/1106.5758
• R. Lyons, Errata to "Distance covariance in metric spaces", Ann. Probab. 46 (2018), 2400–2405; reproduced in https://arxiv.org/abs/1106.5758 (version of 19 Dec. 2020), pp. 24–29
• G. J. Székely, M. L. Rizzo, N. K. Bakirov, Measuring and testing dependence by correlation of distances, Ann. Statist. 35 (2007), 2769–2794. https://doi.org/10.1214/009053607000000505
• I. J. Schoenberg, Metric spaces and positive definite functions, Trans. Amer. Math. Soc. 44 (1938), 522–536. https://doi.org/10.1090/S0002-9947-1938-1501980-0