Functional Analysis

Motivation

The log-Sobolev constant $\alpha$ of a finite Markov chain controls how fast the chain forgets its starting point in relative entropy and in $\ell^2$, and it gives sharper mixing-time bounds than the spectral gap $\lambda$ when the stationary distribution has very small atoms. Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996)) made this constant a standard tool for finite chains. A practical obstacle runs through their paper: $\alpha$ is defined by a nonlinear variational problem, and exact values are known for very few chains. Lower bounds on $\alpha$ for a complicated chain are usually obtained by comparison with a simple chain whose constant is known exactly.

The Appendix of that paper computes such a reference value. For the chain that forgets its state in one step, $K(x,y)=\pi(y)$, it determines $\alpha$ in closed form for every positive $\pi$, and with it the log-Sobolev constant of every chain on two points and of the random walk on the complete graph.

Timeline. Rothaus's work on log-Sobolev inequalities (references [38–40] of the paper) studied the constant through its minimizers, the approach the Appendix follows. Diaconis and Saloff-Coste (1996) give the formula $\alpha=(1-2\pi_*)/\log(1/\pi_*-1)$, and note that Higuchi and Yoshida independently found the asymmetric two-point value.

Setting

Let $\mathcal X$ be a finite set and $K$ a Markov kernel on it: $K(x,y)\ge0$ and $\sum_y K(x,y)=1$. Let $\pi$ be an invariant probability, $\sum_x\pi(x)K(x,y)=\pi(y)$, with $\pi(x)>0$ for every $x$. Functions on $\mathcal X$ are real. Write $Kf(x)=\sum_yK(x,y)f(y)$, $\langle f,g\rangle=\sum_x f(x)g(x)\pi(x)$, $\|f\|_2^2=\langle f,f\rangle$, $E_\pi f=\sum_x f(x)\pi(x)$ and $\mathrm{Var}_\pi(f)=\|f-E_\pi f\|_2^2$.

The Dirichlet form is $\mathcal E(f,g)=\langle (I-K)f,g\rangle$. The entropy functional is

$$\mathcal L(f)=\sum_{x\in\mathcal X}|f(x)|^2\log\frac{|f(x)|^2}{\|f\|_2^2}\,\pi(x),$$

which is nonnegative and vanishes exactly when $|f|$ is constant. The spectral gap and the log-Sobolev constant are

$$\lambda=\inf\Big\{\frac{\mathcal E(f,f)}{\mathrm{Var}_\pi(f)}:\mathrm{Var}_\pi(f)\ne0\Big\},\qquad \alpha=\inf\Big\{\frac{\mathcal E(f,f)}{\mathcal L(f)}:\mathcal L(f)\ne0\Big\}.$$

Equivalently, $1/\alpha$ is the best constant $C$ in $\mathcal L(f)\le C\,\mathcal E(f,f)$.

The chain of the mission is $K(x,y)=\pi(y)$: at each step it draws a fresh point from $\pi$, ignoring its current state. Its invariant measure is $\pi$, and $\pi_*=\min_{\mathcal X}\pi$ is its smallest atom. In Lean the objects are dirichlet, entL, gap, logSobolev, indepChain and piMin in the namespace LogSobolevMC.TwoPoint.

Formalization targets

Goal: Theorem A.1

For a positive probability $\pi$ on $\mathcal X$ with $\pi_*<1/2$, the chain $K(x,y)=\pi(y)$ has

$$\alpha=\frac{1-2\pi_*}{\log(1/\pi_*-1)},$$

and in particular, for $\pi\equiv1/|\mathcal X|$ with $|\mathcal X|\ge3$, $\alpha=(1-2/|\mathcal X|)/\log(|\mathcal X|-1)$. The goal is an equality, so it contains both a log-Sobolev inequality with this constant and the existence of functions that make it sharp.

Milestones

1. Lemma 3.1: $2\alpha\le\lambda$ for every chain.
2. $\mathcal E(|f|,|f|)\le\mathcal E(f,f)$ (proof of Theorem A.1).
3. Either $\alpha=\lambda/2$, or the infimum is attained at a nonconstant nonnegative function (proof of Theorem A.1).
4. (A.3): a positive minimizer $u$ of a reversible chain satisfies $2u\log u-2u\log\|u\|_2-\alpha^{-1}(I-K)u=0$.
5. (A.1): the explicit pair $a=\log[(1-\theta)/\theta]/(1-2\theta)$, $s=(1-2\theta)/(2\theta(1-\theta))$ solves the two-equation system of the proof of Theorem A.2.
6. Theorem A.2: the two-point chain with both rows $(\theta,1-\theta)$, $0<\theta\le1/2$, has $\alpha(\theta)=(1-2\theta)/\log[(1-\theta)/\theta]$, with the limit value $1/2$ at $\theta=1/2$.

Consequences

Corollary A.3 (every two-point chain), Corollary A.4 ($\alpha(K)\ge(1-2\pi_*)\lambda(K)/\log[1/\pi_*-1]$ for every finite chain) and Corollary A.5 (the complete graph, $\alpha=(|\mathcal X|-2)/((|\mathcal X|-1)\log(|\mathcal X|-1))$, and $\alpha=1/(2\log2)$ on $\mathbb Z_3$).

Significance

The result. Theorem A.1 is one of the few exact log-Sobolev constants known for a whole family of chains. Since this chain has $\lambda=1$, the formula shows that $\alpha$ can be smaller than $\lambda/2$ by a factor of order $\log(1/\pi_*)$, which answers the question on p. 715 of how far $2\alpha$ and $\lambda$ can be apart. Corollary A.4 turns this into a general tool: any spectral gap bound gives a log-Sobolev bound, losing only a factor $\log(1/\pi_*-1)/(1-2\pi_*)$. Corollary A.3 settles every chain on two points, and Corollary A.5 gives the complete graph, a frequent reference chain for comparison arguments.

Formalizing it. These results are proved in the paper. To our knowledge none of them, nor the log-Sobolev constant of a finite Markov chain itself, has a machine-checked formalization. The mission produces the definitions of $\mathcal E$, $\mathcal L$, $\lambda$ and $\alpha$ for finite chains, and exact values that later comparison arguments can cite.

Difficulty

The upper bound $\alpha\le(1-2\pi_*)/\log(1/\pi_*-1)$ needs only a good test function. The lower bound is the hard part: it is a statement about every function on $\mathcal X$, and $\mathcal L$ is neither quadratic nor convex. The obvious route, comparing with the spectral gap, loses exactly the logarithmic factor the theorem is about. Reducing to two-valued functions requires the infimum to be attained and analysed through its minimizers. The two-point problem that remains is a one-parameter inequality $l(s)\le a\,e(s)$ on an interval. The authors describe its solution as a calculus exercise that depended on numerical guessing, and it has removable singularities at $\theta=1/2$.

Formalization scope

$\mathcal X$ is a Fintype with decidable equality. $K$ is a Matrix V V ℝ and $\pi$ a function V → ℝ. Stochasticity, invariance, distributions and reversibility are the published MarkovMixing predicates (IsStochastic, IsStationary, IsDist, DetailedBalance) from mm_basic, and $\mathrm{Var}_\pi$ is MarkovMixing.distVar from mm_lower. Positivity of $\pi$ is a hypothesis throughout, as in §2.1. The infima $\lambda$ and $\alpha$ are Lean sInfs over exactly the sets of (2.4) and (3.1). $\mathcal E$ is the bilinear form $\langle (I-K)f,g\rangle$. $\lambda$ is the variational gap, not the eigenvalue-based MarkovMixing.spectralGap, which agrees with it only for reversible chains.

Disclosed additions, all at removable singularities of the printed formulas: $\pi_*<1/2$ in Theorem A.1 (and $|\mathcal X|\ge3$ in its uniform case); the explicit limit value $1/2$ at $\theta=1/2$ in Theorem A.2; strict $\pi(0)<\pi(1)$ in Corollary A.3; and $|\mathcal X|\ge3$ in Corollary A.5. In (A.3), reversibility, positivity of $u$ and $\alpha>0$ are added. Irreducibility is not assumed anywhere.

Trivializing formalizations are ruled out. A closed form evaluated at $0/0$ would be Lean's value $0$, so each such case is excluded or replaced by its limit. Real.log of a nonpositive number and an sInf over an empty or unbounded set do not occur under the stated hypotheses. Dropping the positivity or invariance of $\pi$, or replacing $\lambda$ by the eigenvalue gap, would change the statements. Stating the goal for two points only, or assuming the minimizer is two-valued, would state a step of the proof.

Contributions welcome: the general facts $\mathcal L\ge0$, $\mathcal E(f,f)=\tfrac12\sum_{x,y}(f(x)-f(y))^2K(x,y)\pi(x)$ and the existence of minimizers are reusable for every log-Sobolev development on finite spaces. The two-point calculus of Theorem A.2 is self-contained real analysis.

Selected references

• P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Ann. Appl. Probab. 6(3):695–750, 1996. https://doi.org/10.1214/aoap/1034968224
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, AMS, 2009 (source of the MarkovMixing definitions used here). https://doi.org/10.1090/mbk/058

Motivation

The Metropolis algorithm turns a simple random walk into a Markov chain with a prescribed stationary distribution, by accepting or rejecting the walk's proposals. It is the basic tool of Markov chain Monte Carlo, and the practical question it raises is quantitative: how many steps are needed before the chain's distribution is close to the target? For most chains used in practice there is no rigorous answer.

Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996) 695–750) developed logarithmic Sobolev inequalities for finite Markov chains as a tool for exactly this question. Their first illustration, stated as Theorem 1.1 in the introduction, is the Metropolis chain for the binomial distribution: a one-dimensional chain for which the spectral gap gives a bound of order $n^2$ steps, while the log-Sobolev constant gives the correct order $n\log n$. This mission formalizes that theorem and the chain of results the paper uses to prove it: the log-Sobolev constant of a product chain, of the hypercube walk, of the Ehrenfest chain, a comparison principle, and a discrete-time convergence bound.

Setting

Let $\mathcal X$ be a finite set. A Markov kernel $K$ on $\mathcal X$ is a matrix with $K(x,y)\ge 0$ and $\sum_y K(x,y)=1$; $K^l(x,\cdot)$, written $K^l_x$, is the law of the chain after $l$ steps from $x$. A probability $\pi$ on $\mathcal X$ is invariant if $\sum_x\pi(x)K(x,y)=\pi(y)$; throughout, $\pi$ charges every point. $(K,\pi)$ is reversible if $\pi(x)K(x,y)=\pi(y)K(y,x)$.

For real functions $f,g$ on $\mathcal X$ write $\langle f,g\rangle=\sum_x f(x)g(x)\pi(x)$, $\|f\|_2=\langle f,f\rangle^{1/2}$, $Ef=\sum_x f(x)\pi(x)$ and $\operatorname{Var}(f)=\|f-Ef\|_2^2$. The Dirichlet form is $\mathcal E(f,g)=\langle (I-K)f,g\rangle$, and

$$\mathcal L(f)=\sum_x |f(x)|^2\log\frac{|f(x)|^2}{\|f\|_2^2}\,\pi(x).$$

The spectral gap and the log-Sobolev constant are

$$\lambda=\inf\Big\{\frac{\mathcal E(f,f)}{\operatorname{Var}(f)}:\operatorname{Var}(f)\neq0\Big\},\qquad \alpha=\inf\Big\{\frac{\mathcal E(f,f)}{\mathcal L(f)}:\mathcal L(f)\neq0\Big\}.$$

For reversible $K$, $\beta_{\min}$ is the smallest eigenvalue of $K$. The total variation distance is $\|\mu-\nu\|_{TV}=\max_{A\subseteq\mathcal X}|\mu(A)-\nu(A)|$.

The chain of the goal lives on $\mathcal X=\{0,1,\dots,n\}$, $n\ge1$, with the binomial distribution $\pi(x)=2^{-n}\binom nx$. The base chain is the nearest-neighbour walk $K(x,x\pm1)=1/2$ for $1\le x\le n-1$, holding with probability $1/2$ at $0$ and at $n$. The Metropolis chain $M$ accepts a proposed move $x\to y\neq x$ with probability $\min\{1,\pi(y)/\pi(x)\}$, so $M(x,y)=K(x,y)\min\{1,\pi(y)/\pi(x)\}$ for $y\ne x$, and $M(x,x)=1-\sum_{y\ne x}M(x,y)$. Explicitly, $M(x,x+1)=\frac12$ for $x\le (n-1)/2$ and $M(x,x+1)=\frac{n-x}{2(x+1)}$ above, symmetrically for $x-1$; this is the kernel (1.9) of the paper.

Two auxiliary chains appear in the proof: the hypercube walk on $\{-1,1\}^n$, which flips a uniformly chosen coordinate, and the Ehrenfest chain $P(x,x+1)=(n-x)/n$, $P(x,x-1)=x/n$ on $\{0,\dots,n\}$, which records the number of coordinates equal to $1$.

Formalization targets

Goal: Theorem 1.1 (upper bound)

For every $n\ge1$, every starting point $x$, every $c>0$ and every integer $l$,

$$\|M^l_x-\pi\|_{TV}\le e^{1-c}\qquad\text{whenever } l\ge\frac n2(\log n+2c).$$

The goal is stated about the explicit chain (1.9) only; it fixes the constants as printed.

Milestones

1. Example 1.1, (1.9). The Metropolis construction gives the six-case kernel (1.9), and $\pi(x)M(x,y)=\pi(y)M(y,x)$.
2. Example 3.1. The two-point chain on $\{-1,1\}$ has $\pi\equiv1/2$, $\lambda=2$ and $\alpha=\lambda/2=1$.
3. Lemma 3.2. The product chain (2.9) of $d$ chains, with the product measure (2.10), has $\lambda=\frac1d\min_i\lambda_i$ and $\alpha=\frac1d\min_i\alpha_i$.
4. Example 3.2. The hypercube walk is that product of two-point chains and has $\alpha=\lambda/2=1/n$.
5. Lemma 3.1. $2\alpha\le\lambda$ for every chain.
6. Lemma 3.3. If $\mathcal E'\le A\mathcal E$ and $a\pi\le\pi'$ with $A,a>0$, then $\lambda'\le\frac Aa\lambda$ and $\alpha'\le\frac Aa\alpha$.
7. Example 3.3. The Ehrenfest chain is the projection of the hypercube walk, with $\lambda=2/n$ and $\alpha(P)=1/n$; $\frac12P(x,y)\le M(x,y)\le P(x,y)$ for $x\ne y$, so $\mathcal E_M\le\mathcal E_P\le2\mathcal E_M$; hence $\frac1n\le\lambda(M)\le\frac2n$ and $\frac1{2n}\le\alpha(M)\le\frac1n$.
8. Corollary 3.8. For reversible $(K,\pi)$ and $\pi(x)\le1/e$, with $\lambda_*=\min\{\lambda,1+\beta_{\min}\}$, $\|K^m_x/\pi-1\|_2\le(1+2e^2)^{1/2}e^{-c}$ for $m\ge\frac1{4\alpha}\log\log\frac1{\pi(x)}+\frac c{\lambda_*}+1$.
9. Example 3.4. $M(x,x)\ge2/(n+3)$, $\beta_{\min}\ge-1+4/(n+3)$, and $\|M^l_x/\pi-1\|_2\le(1+2e^2)^{1/2}e^{-c}$ for $l\ge\frac n2(\log n+2c)+1$.

Significance

The theorem shows that the Metropolis chain for the binomial distribution mixes in $\frac n2\log n+O(n)$ steps, matching the lower bound of order $n\log n$ quoted in the paper's converse. The spectral gap $\lambda(M)\asymp1/n$ together with $\pi_*=2^{-n}$ only yields order $n^2$; the improvement comes from replacing $\log(1/\pi_*)$ by $\log\log(1/\pi_*)$, which is what the log-Sobolev constant buys. The intermediate results are reusable on their own: the tensorization of $\lambda$ and $\alpha$ (Lemma 3.2), the comparison principle (Lemma 3.3) and the discrete-time bound (Corollary 3.8) apply to any finite chain, and the exact log-Sobolev constants of the two-point chain, the hypercube and the Ehrenfest chain are standard inputs elsewhere.

All results are proved in the paper (the gap $\lambda=2/n$ of the Ehrenfest chain is quoted there as known). To our knowledge none of them is machine-checked: there is no log-Sobolev constant of a Markov chain in Mathlib or on the platform. The work is to formalize the known proofs.

Difficulty

The natural first idea is to bound the distance to stationarity by the spectral gap: $\|K^l_x/\pi-1\|_2^2\le\pi(x)^{-1}\beta^{2l}$. With $\pi(x)$ as small as $2^{-n}$ and $1-\beta\asymp 1/n$, this needs $l$ of order $n^2$, so no amount of care with this argument reaches the theorem. The proof instead goes through the log-Sobolev constant, which is hard to compute even for simple chains: the paper obtains $\alpha(M)$ only through a sequence of exact computations (two points, products, a projection) followed by a comparison. Each step involves the nonlinear functional $\mathcal L$, whose tensorization and behaviour under comparison of measures are less elementary than those of the variance. The passage from continuous to discrete time also needs control of $\beta_{\min}$, since a chain with eigenvalue near $-1$ does not converge.

Formalization scope

The state space $\{0,\dots,n\}$ is Fin (n + 1), $\{-1,1\}$ is Fin 2 ($0\mapsto-1$, $1\mapsto1$), and $\{-1,1\}^n$ is Fin n → Fin 2. Kernels are real matrices Matrix V V ℝ; stochasticity, invariance, irreducibility, reversibility (detailed balance), total variation, the rows $K^l_x$, the product chain (2.9) and the generic Metropolis rule are the published MarkovMixing definitions (mm_basic, mm_mixing, mm_continuous, mm_mcmc). Functions are real valued. Time $l$ is a natural number and thresholds are compared in $\mathbb R$.

$\lambda$, $\alpha$ and $\beta_{\min}$ are defined variationally as real infima (sInf). $\beta_{\min}$ is the minimum of the Rayleigh quotient $\langle Kf,f\rangle/\langle f,f\rangle$, which is the smallest eigenvalue for reversible chains. The eigenvalue-based MarkovMixing.spectralGap is not used, since it equals $\lambda$ only for reversible chains. Two hypotheses are added where Lean's conventions would otherwise falsify a statement: Lemma 3.2 assumes every factor has at least two points (Lean evaluates the infimum over an empty set as $0$, the paper as $+\infty$), and Corollary 3.8 assumes $1+\beta_{\min}>0$ (Lean evaluates $c/0$ as $0$, the paper as $+\infty$). Lemmas 3.1 and 3.3 are stated without the section's irreducibility assumption, which they do not need.

A trivializing formalization is ruled out: the goal mentions only the explicit chain $M$, the binomial distribution, $M^l_x$ and total variation, not a chain assumed to have $\alpha\ge1/(2n)$; positivity and invariance of $\pi$ are never dropped; and no statement relies on a junk value of sInf, Real.log or division. The converse half of Theorem 1.1, $\max_x\|M^l_x-\pi\|_{TV}\ge\frac14+o(1)$ for $l\le\frac n8\log n$, is asymptotic and proved in the paper only by citation; it is not part of the mission. The second statement of Corollary 3.8 (the uniform bound on $|k^{2n}(x,y)-1|$) is also left out.

A complete development needs the semigroup $H_t=e^{-t(I-K)}$ and the hypercontractivity theorem of the paper (Theorem 3.5) on the way to Corollary 3.8, a spectral decomposition of reversible kernels, and the entropy inequalities behind Lemmas 3.2 and 3.3. The general results (Lemmas 3.1–3.3, Corollary 3.8) are reusable beyond this mission. Contributions to any milestone, and alternative routes to the goal, are welcome.

Selected references

• P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Ann. Appl. Probab. 6(3) (1996), 695–750. https://doi.org/10.1214/aoap/1034968224
• P. Diaconis and L. Saloff-Coste, What do we know about the Metropolis algorithm?, J. Comput. System Sci. 57 (1998), 20–36 (reference [18] of the paper, in its preprint form). https://doi.org/10.1006/jcss.1998.1576
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, AMS, 2009 (source of the published MarkovMixing definitions). https://doi.org/10.1090/mbk/058

Motivation

Existence theory for elliptic, parabolic and nonlinear PDEs mostly runs through one argument: build approximate solutions, bound them in a Sobolev norm, extract a convergent subsequence, and pass to the limit. The extraction step needs a compact embedding: a bound on derivatives must buy convergence of the functions themselves in a weaker norm. On a bounded domain this is the Rellich–Kondrachov theorem. It is what makes the resolvent of the Dirichlet Laplacian compact, and so gives the Fredholm alternative and the discrete spectrum of elliptic operators on bounded domains. The companion topics of the same section, extension and trace, are how Sobolev functions are moved between a domain and all of space, and how they are given boundary values.

This mission follows Chapter 3 (§3.9–3.10) and Theorem 1.15 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014).

Timeline. Rellich proved the compactness of $H^1_0 \hookrightarrow L^2$ on bounded domains in 1930. Kondrachov extended it to $W^{1,p}$ and exponents below the Sobolev exponent in 1945. The $L^p$ compactness criterion used in the notes goes back to Kolmogorov (1931) and M. Riesz (1933); a modern account with a history is Hanche-Olsen and Holden 2010. Gagliardo characterized the traces of $W^{1,p}$ in 1957.

Setting

Throughout, $\mathbb{R}^n$ carries Lebesgue measure, and functions are real-valued. For an open set $\Omega \subseteq \mathbb{R}^n$, a test function $\phi \in C_c^\infty(\Omega)$ is smooth with compact support inside $\Omega$. A locally integrable $g$ is the weak derivative $\partial^\alpha f$ of a locally integrable $f$ if $\int_\Omega g\phi = (-1)^{|\alpha|}\int_\Omega f\,\partial^\alpha\phi$ for every test function $\phi$. Here $\alpha \in \mathbb{N}_0^n$ is a multi-index of order $|\alpha| = \sum_i \alpha_i$.

For $k \in \mathbb{N}$ and $1 \le p \le \infty$, the Sobolev space $W^{k,p}(\Omega)$ consists of the $f$ whose weak derivatives $\partial^\alpha f$, $|\alpha| \le k$, exist and lie in $L^p(\Omega)$. For $p < \infty$ its norm is

$$\|f\|_{W^{k,p}(\Omega)} = \Big(\sum_{|\alpha|\le k} \int_\Omega |\partial^\alpha f|^p\,dx\Big)^{1/p},$$

and for $p = \infty$ it is the maximum of the essential suprema. The space $W^{k,p}_0(\Omega)$ is the closure of $C_c^\infty(\Omega)$ in this norm. For $1 \le p < n$ the Sobolev conjugate is $p^* = np/(n-p)$.

The upper half-space is $\mathbb{R}^n_+ = \{x = (x', x_n) : x_n > 0\}$, with closure $\overline{\mathbb{R}}^n_+$ and boundary $\partial\mathbb{R}^n_+ = \{(x', 0)\} \cong \mathbb{R}^{n-1}$. The space $C_c^\infty(\overline{\mathbb{R}}^n_+)$ consists of the functions that are smooth up to the boundary and vanish outside a compact set. Unlike $C_c^\infty(\mathbb{R}^n_+)$, they need not vanish on $\partial\mathbb{R}^n_+$.

A subset of a metric space is precompact if its closure is compact. $C_0(\mathbb{R}^n)$ is the space of continuous functions vanishing at infinity, with the sup norm.

In Lean the weak derivative is HasWeakDeriv (with weakDeriv and weakGradNorm) in the series' shared namespace HunterPDE.Shared; the other objects are MemW k p Ω f, sobolevNorm k p Ω f, MemW0 k p Ω f, sobolevConjugate, upperHalfSpace m, IsSmoothCompactClosedHalfSpace and boundaryPoint, in the namespace HunterPDE.Compactness.

Formalization targets

Goal: Rellich–Kondrachov (Theorem 3.45)

Let $\Omega$ be a bounded open set in $\mathbb{R}^n$, $1 \le p < n$ and $1 \le q < p^*$. If $\mathcal{F} \subseteq W^{1,p}_0(\Omega)$ satisfies $\|f\|_{W^{1,p}(\Omega)} \le M$ for all $f \in \mathcal{F}$, then

$$\{\, f\mathbf{1}_\Omega : f \in \mathcal{F} \,\} \ \text{is precompact in } L^q(\mathbb{R}^n).$$

Milestones

• Theorem 1.15 (Kolmogorov–Riesz). For $1 \le p < \infty$, a set $\mathcal{F} \subseteq L^p(\mathbb{R}^n)$ is precompact if and only if it is bounded, tight ($\sup_{f}\|f\|_{L^p(|x|>R)} \to 0$ as $R \to \infty$), and $L^p$-equicontinuous:

$$\forall \varepsilon > 0\ \exists \delta > 0:\ |h| < \delta \implies \|f(\cdot + h) - f\|_{L^p(\mathbb{R}^n)} < \varepsilon \quad \forall f \in \mathcal{F}.$$

• Theorem 3.41 (extension). There is a bounded linear $E : W^{1,p}(\mathbb{R}^n_+) \to W^{1,p}(\mathbb{R}^n)$ with $Ef = f$ a.e. on $\mathbb{R}^n_+$ and $\|Ef\|_{W^{1,p}(\mathbb{R}^n)} \le C(n,p)\,\|f\|_{W^{1,p}(\mathbb{R}^n_+)}$.
• Theorem 3.42 (density). $C_c^\infty(\overline{\mathbb{R}}^n_+)$ is dense in $W^{k,p}(\mathbb{R}^n_+)$ for $1 \le p < \infty$.
• Theorem 3.44 (trace). For $1 \le p < \infty$ there is a bounded linear $T : W^{1,p}(\mathbb{R}^n_+) \to L^p(\mathbb{R}^{n-1})$ with $(Tf)(x') = f(x', 0)$ on $C_c^\infty(\overline{\mathbb{R}}^n_+)$ and $\|Tf\|_{L^p} \le C(p)\,\|f\|_{W^{1,p}(\mathbb{R}^n_+)}$, whose kernel is exactly $W^{1,p}_0(\mathbb{R}^n_+)$.
• Theorem 3.48 ($p > n$). For $\Omega$ bounded and $n < p < \infty$, a family with $\operatorname{supp} f \Subset \Omega$ and $\|Df\|_{L^p} \le C$ is precompact in $C_0(\mathbb{R}^n)$.

The goal is stated qualitatively (precompactness), with no constants, so it does not depend on any particular form of the Sobolev inequality.

Significance

The result itself. Rellich–Kondrachov is the source of compactness in the $L^2$ theory of elliptic equations. With it, the solution operator of a coercive elliptic problem on a bounded domain is compact. That yields the Fredholm alternative, the discreteness of the Dirichlet spectrum, and existence results for semilinear problems via compactness and fixed-point arguments. The trace theorem makes the boundary condition "$u = 0$ on $\partial\Omega$" meaningful for Sobolev functions, and identifies $W^{1,p}_0$ as the space in which Dirichlet problems are posed. The extension theorem transfers whole-space results to domains. Theorem 3.48 gives the uniform-norm counterpart above the critical exponent.

Formalizing it. All results here are classical and proved. The notes prove 3.45, 3.48 and the forward direction of 3.44. They describe 3.41 and 3.42 in a sentence each, and cite 1.15 without proof. Mathlib has the Lebesgue spaces Lp, Arzelà–Ascoli for bounded continuous functions, and mollification. It has no weak derivatives, no Sobolev spaces on domains, no trace, no extension operators and no Kolmogorov–Riesz criterion. A complete development would supply the first machine-checked versions of these in the notes' form, and a formal $W^{1,p}_0$ compactness theorem usable by the elliptic chapters of the same series.

Difficulty

The obvious route to the goal is: approximate by test functions, extend by zero, and verify the three Kolmogorov–Riesz conditions. The first two follow from the Sobolev inequality and the boundedness of $\Omega$. The hard parts are elsewhere. First, the Kolmogorov–Riesz criterion is not in Mathlib, and its "if" direction needs a mollification and total-boundedness argument in $L^p(\mathbb{R}^n)$. Second, the $L^q$-equicontinuity for $q$ above $p$ needs an interpolation between an $L^1$ translation estimate and the critical Sobolev embedding into $L^{p^*}$, so the Gagliardo–Nirenberg–Sobolev inequality must be available for $W^{1,p}_0(\Omega)$, not only for smooth compactly supported functions. Third, weak derivatives are defined by integration against test functions, and every density step has to be carried through that definition. The exponent restriction $q < p^*$ is sharp (Example 3.47 in the notes), so no argument that ignores it can succeed.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with volume. Open sets are Ω : Set _ with IsOpen Ω, and bounded means Bornology.IsBounded Ω. Coordinates are 0-based (i : Fin n), and multi-indices are α : Fin n → ℕ.
• Functions are ℝⁿ → ℝ, and only their values on the relevant set matter. weakDeriv is a chosen representative, used only where a weak derivative is assumed to exist. sobolevNorm takes values in ℝ≥0∞.
• $W^{1,p}_0(\Omega)$ is the norm closure of $C_c^\infty(\Omega)$, not "zero trace". "Bounded in $W^{1,p}_0(\Omega)$" is a uniform bound on sobolevNorm 1 p Ω.
• In the goal, $\mathcal{F}$ is placed in $L^q(\mathbb{R}^n)$ by extension by zero (Ω.indicator f). The conclusion asserts both that each extension lies in $L^q$ and that the set of their classes in Mathlib's Lp ℝ q volume has compact closure. The hypothesis $q < p^*$ rules out $q = \infty$.
• Half-space results use dimension $n = m+1$ and the last coordinate Fin.last m. The boundary is $\mathbb{R}^m$ via $x' \mapsto (x',0)$. Extension and trace operators are maps on functions that are linear up to a.e. equality on $W^{1,p}(\mathbb{R}^n_+)$.
• Conventions read off the page: in Theorem 3.44 the trace constant is quantified before the dimension ("depending only on $p$"), and its final clause is taken with $k = 1$ (the printed "$W^{k,p}_0$" cannot mean $k \ge 2$, as the notes remark after the proof). Theorem 3.42 is stated for $1 \le p < \infty$, and Theorem 3.41 for $1 \le p \le \infty$. Theorem 3.48 assumes $n \ge 1$.
• A trivializing reading is ruled out: the goal's conclusion is compactness of the closure in $L^q(\mathbb{R}^n)$ of the zero extensions themselves, not of some other representative. The norm bound is on the genuine weak derivatives, which the hypotheses guarantee exist, not on a junk value.
• Reusable infrastructure: weak derivatives and Sobolev spaces on open sets, the Kolmogorov–Riesz criterion, and the half-space extension and trace operators. Contributions of any of these as standalone lemmas are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §1.5 and §3.9–3.10. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• H. Hanche-Olsen and H. Holden, The Kolmogorov–Riesz compactness theorem, Expositiones Mathematicae 28 (2010) 385–394. https://arxiv.org/abs/0906.4883
• L. C. Evans, Partial Differential Equations, 2nd ed., AMS Graduate Studies in Mathematics 19, 2010, §5.5–5.7. https://doi.org/10.1090/gsm/019

Motivation

Second-order elliptic equations in divergence form, such as $-\nabla\cdot(A\nabla u) + b\cdot\nabla u + cu = f$, model steady diffusion, electrostatics in inhomogeneous media and linear elasticity. They are also the stationary part of every parabolic and hyperbolic problem studied later in the same notes. When the coefficients are only bounded and measurable, classical solutions need not exist. The modern theory replaces them by weak solutions in the Sobolev space $H^1_0(\Omega)$ and settles existence, uniqueness and solvability by Hilbert-space methods. This mission formalizes that theory as presented in Chapter 4 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014). The chapter follows the standard development of Evans, Partial Differential Equations, Chapter 6, and of Gilbarg–Trudinger, Chapter 8.

Timeline. Riesz (1907) and Fréchet represented bounded functionals on Hilbert spaces. Fredholm (1903) proved the alternative for integral equations of the second kind, and Riesz (1918) extended it to compact operators. Lax and Milgram (1954) removed the symmetry assumption from the Riesz approach, and Gårding (1953) proved the coercivity estimate for elliptic forms. Together these give the existence and Fredholm theory for the Dirichlet problem stated here.

Setting

Let $\Omega \subseteq \mathbb{R}^n$ be open. A test function is a smooth $\phi$ with compact support in $\Omega$. The space $H^1_0(\Omega)$ is the closure of the test functions in the norm $\|u\|_{H^1_0}^2 = \int_\Omega (u^2 + |Du|^2)\,dx$; each element carries a function $u$ and a weak gradient $Du$, both square-integrable. $H^{-1}(\Omega)$ is the space of bounded linear functionals on $H^1_0(\Omega)$, and $f \in L^2(\Omega)$ acts on it by $\langle f, \phi\rangle = \int_\Omega f\phi\,dx$.

Given coefficients $a_{ij}, b_i, c \in L^\infty(\Omega)$ with $a_{ij} = a_{ji}$, the operator is

$$Lu = -\sum_{i,j=1}^n \partial_i(a_{ij}\partial_j u) + \sum_{i=1}^n \partial_i(b_i u) + cu .$$

It is uniformly elliptic if $\sum_{i,j} a_{ij}(x)\xi_i\xi_j \ge \theta|\xi|^2$ for some $\theta > 0$, almost every $x$ and every $\xi$. Its bilinear form on $H^1_0(\Omega)$ is

$$a(u,v) = \int_\Omega \Big(\sum_{i,j} a_{ij}\,\partial_i u\,\partial_j v - \sum_i b_i\,u\,\partial_i v + c\,uv\Big)dx ,$$

and the formal adjoint $L^*u = -\sum\partial_i(a_{ij}\partial_j u) - \sum b_i\partial_i u + cu$ has the form $a^*(u,v) = a(v,u)$. For $\mu \in \mathbb{R}$, $u$ is a weak solution of $Lu + \mu u = f$ with $u = 0$ on $\partial\Omega$ if $u \in H^1_0(\Omega)$ and $a(u,\phi) + \mu\int_\Omega u\phi = \langle f,\phi\rangle$ for all $\phi \in H^1_0(\Omega)$. The resolvent $K = (L+\mu I)^{-1}$ maps $f \in L^2(\Omega)$ to that solution.

A bounded operator $T$ on a Hilbert space is Fredholm if its kernel is finite-dimensional and its range is closed with finite-dimensional orthogonal complement. Its index is $\dim\ker T - \dim(\operatorname{ran}T)^\perp$.

Formalization targets

Goal: the Fredholm alternative (Theorem 4.24)

For $\Omega$ bounded, $L$ uniformly elliptic and $\lambda \in \mathbb{R}$, exactly one of the following holds:

$$\text{(1)}\quad \ker(L^*-\lambda) = 0 \ \text{ and } \ \forall f \in L^2(\Omega)\ \exists!\,u \in H^1_0(\Omega):\ Lu - \lambda u = f;$$ $$\text{(2)}\quad 0 < \dim\ker(L-\lambda) = \dim\ker(L^*-\lambda) < \infty,\quad Lu - \lambda u = f \text{ solvable} \iff f \perp_{L^2} \ker(L^*-\lambda),$$

with non-unique solutions in case (2). Every kernel and equation is meant in the weak sense on $H^1_0(\Omega)$.

Milestones

• Poincaré inequality (Theorem 4.9): $\int_\Omega u^2 \le C\int_\Omega |Du|^2$ on $H^1_0(\Omega)$ when $\Omega$ lies between two parallel hyperplanes. Unique solvability of $-\Delta u = f \in H^{-1}(\Omega)$ (Theorem 4.11).
• The Lax–Milgram theorem (Theorem 4.20).
• Energy estimates (Theorem 4.21): $C_1\|u\|_{H^1_0}^2 \le a(u,u) + \gamma\|u\|_{L^2}^2$ and $|a(u,v)| \le C_2\|u\|_{H^1_0}\|v\|_{H^1_0}$, with the explicit $\gamma = \theta - c_0$ if $b = 0$ and $\gamma = \tfrac{1}{2\theta}\sum\|b_i\|_{L^\infty}^2 + \tfrac\theta2 - c_0$ otherwise.
• Unique weak solvability of $Lu + \mu u = f$ for $\mu \ge \gamma$ (Theorem 4.22). The resolvent $K$ is bounded on $L^2(\Omega)$ with adjoint $(L^*+\mu I)^{-1}$, and it is compact when $\Omega$ is bounded (Theorem 4.23).
• The abstract Fredholm alternative for Fredholm operators of index zero (Theorem 4.50).
• The spectral theorem for symmetric $L$ (Theorem 4.25): eigenvalues $\lambda_1 \le \lambda_2 \le \dots \to \infty$ of finite multiplicity, with an orthonormal eigenbasis of $L^2(\Omega)$.

Significance

The Fredholm alternative is the complete linear solvability theory of the Dirichlet problem for general elliptic operators on bounded domains. Uniqueness for the homogeneous problem is equivalent to existence for all data. When uniqueness fails, the obstruction is a finite set of orthogonality conditions given by the adjoint problem. This feeds directly into the spectral theory of Theorem 4.25, into eigenfunction expansions, and into the existence theory for parabolic and hyperbolic equations (Galerkin approximation in later chapters). Nonlinear elliptic problems are routinely reduced to it through linearization and the implicit function theorem.

Mathlib has Lax–Milgram for continuous coercive forms, compact operators, the Riesz representation theorem and the spectral theorem for compact self-adjoint operators. It does not have Sobolev spaces with zero boundary values as used here, elliptic bilinear forms, Fredholm operators or their index. As far as a search of the platform shows, none of these results has a machine-checked statement for elliptic operators with $L^\infty$ coefficients. The mission would give formal statements, and eventually proofs, of textbook results that are fully proved on paper.

Difficulty

The abstract functional analysis is close to the library. The difficulty lies in connecting it to the PDE objects. Gårding's inequality needs pointwise uniform ellipticity turned into an integral bound on the weak gradient, with the non-symmetric first-order term controlled explicitly enough to reach the stated $\gamma$. Compactness of the resolvent needs the Rellich–Kondrachov theorem: $H^1_0(\Omega)$ embeds compactly in $L^2(\Omega)$ for bounded $\Omega$, which is not in Mathlib in this form. The goal then relates the weak problem on $H^1_0(\Omega)$ to operator statements on $L^2(\Omega)$ in both directions, including the solution spaces and the adjoint's kernel. A proof that argues only on $L^2(\Omega)$, without tracking that the solutions lie in $H^1_0(\Omega)$ and satisfy the weak identity for every $H^1_0$ test function, does not reach the stated result.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure. Coordinates are 0-based.
• $H^1_0(\Omega)$ (H10 n Ω) is modelled by jets. It is the closure, in $L^2(\Omega;\mathbb{R}\times\mathbb{R}^n)$, of the pairs $(\phi,\nabla\phi)$ for smooth compactly supported $\phi$ with support in $\Omega$. Its norm is exactly the standard $H^1$ norm, and it is a Hilbert space. $H^{-1}(\Omega)$ is StrongDual ℝ (H10 n Ω).
• Coefficients are bundled in Coeffs n. Admissible is $L^\infty(\Omega)$ membership plus a.e. symmetry. Uniform ellipticity carries $\theta > 0$.
• Weak solutions are tested against every $\phi \in H^1_0(\Omega)$, not only test functions. $f \in L^2(\Omega)$ is an element of Lp ℝ 2 on $\Omega$.
• The printed display (4.21) of the adjoint form has $+\sum b_i(\partial_i u)v$. That contradicts both $a^*(u,v) = a(v,u)$ and the stated $L^*$. The formalization uses $a^*(u,v) = a(v,u)$.
• Theorem 4.22's printed equation "$Lu + \mu f = 0$" is read as $Lu + \mu u = f$, as in Definition 4.19 and the proof.
• Theorem 4.25's printed $\lambda_1 < \lambda_2$ is stated as $\lambda_1 \le \lambda_2$, since the strict inequality fails for disconnected $\Omega$. $\Omega \neq \emptyset$ and $n \ge 1$ are assumed there.
• In Theorem 4.21 the explicit $\gamma$ is asserted for every a.e. lower bound $c_0$ of $c$, which is equivalent to the book's $c_0 = \inf c$.
• The Fredholm index is an integer computed from Module.finrank and is only used for Fredholm operators.
• Solution spaces are subspaces of $H^1_0(\Omega)$. Their finite-dimensionality is asserted separately from the equality of dimensions, so a finrank equality between two infinite-dimensional spaces (both $0$ in Lean) cannot stand in for the book's claim.
• A resolvent defined by an arbitrary choice with junk value $0$ is only used for $\mu \ge \gamma$, where the weak solution exists and is unique. The theorem asserts that this function is a continuous linear map, so it cannot be satisfied vacuously.

Needed infrastructure, reusable beyond this mission: the jet model of $H^1_0$ and its Poincaré inequality, Gårding-type estimates, a Rellich–Kondrachov compactness theorem for $H^1_0(\Omega) \hookrightarrow L^2(\Omega)$, and Fredholm operators with index on Hilbert spaces. Contributions of any of these as separate lemmas are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, Chapter 4. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• L. C. Evans, Partial Differential Equations, 2nd ed., AMS Graduate Studies in Mathematics 19, 2010, Chapter 6. https://doi.org/10.1090/gsm/019
• P. D. Lax and A. N. Milgram, "Parabolic equations", Contributions to the Theory of Partial Differential Equations, Annals of Mathematics Studies 33, 1954, 167–190. https://doi.org/10.1515/9781400882182-010
• L. Gårding, "Dirichlet's problem for linear elliptic partial differential equations", Mathematica Scandinavica 1 (1953), 55–72. https://doi.org/10.7146/math.scand.a-10364
• D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Springer Classics in Mathematics, 2001, Chapter 8. https://doi.org/10.1007/978-3-642-61798-0

Motivation

Metric absorption asks whether adjoining a null-sequence component changes a space up to controlled distances. Linear absorption imposes a different requirement. The pinned manuscript supplies the research context.

Setting

The space Z is a separable real Banach space. The product Z×c0 uses the product metric, and equivalent metrics are compared through positive bi-Lipschitz constants.

Formalization target

The selected goal is OAI.C0Absorption.main_result. Its central assertion is

$$Z\times c_0\simeq_{\rm biLip}Z,\qquad c_0\not\hookrightarrow_{\rm linear}Z.$$

The theorem states that there exists a real normed space Z, in a fixed universe, with the following properties, where C₀ denotes the real Banach space of sequences ℝ-valued on ℕ that tend to zero at infinity, and a map f between metric spaces is bi-Lipschitz if there are constants 0<c≤C with c·d(x,y) ≤ d(f x,f y) ≤ C·d(x,y) for all x,y. First, Z is complete and separable. Second, Z contains no linear copy of C₀: every continuous linear map T from C₀ to Z fails to satisfy ‖Tx‖ ≥ c‖x‖ for all x for any c>0. Third, there is a surjective bi-Lipschitz map F from the product metric space Z × C₀ onto Z. Fourth, there is a bi-Lipschitz map from C₀ into Z. Fifth, Z is metrically universal for separable metric spaces: every separable metric space M, in the base universe, admits a bi-Lipschitz map into Z. Sixth, Z × C₀ is not linearly homeomorphic to Z, that is, there is no continuous linear equivalence, with continuous inverse, between Z × C₀ and Z.

Significance and status

The target also includes a bi-Lipschitz embedding of c0, universality for base-universe separable metric spaces, and failure of linear homeomorphism between the product and Z. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The metric universality and absorption maps must not produce a bounded-below linear embedding of c0.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Bi-Lipschitz Absorption of c0 Without a Linear Copy of c0, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

How well can a graph be drawn inside a Banach space without stretching some distances much more than others? The distortion of the best such drawing measures the mismatch between the graph's metric and the geometry of the space. Diamond graphs are a standard test family: each edge is repeatedly replaced by parallel two-edge paths, so the graph contains many "midpoints" between the same two endpoints at every scale. For binary diamonds, bounded distortion in a space is tied to the failure of super-reflexivity (Johnson–Schechtman 2009). For countably branching diamonds, where each edge is replaced by infinitely many paths, the relevant property is asymptotic midpoint uniform convexity (AMUC): an equivalent AMUC norm prevents uniform embeddings (Baudier et al. 2017).

This mission asks for an explicit, quantitative lower bound on the distortion of countably branching diamonds in two specific James-type tree spaces, deduced from a midpoint "lens" estimate for those spaces.

Timeline

• 1974. James introduces the square-sum norm over disjoint tree segments (doi:10.1090/S0002-9904-1974-13580-9).
• 2001. Girardi proves asymptotic uniform convexity of the coordinate predual and dual of the binary James tree space (doi:10.4064/sm147-2-2).
• 2004. Lee and Naor give quantitative lower bounds for binary diamonds in $L_p$, $1<p\le2$, by summing a convexity inequality over levels (doi:10.1007/s00039-004-0473-8).
• 2009. Johnson and Schechtman characterize super-reflexivity by non-embeddability of binary diamonds (doi:10.1142/S1793525309000114).
• 2016. Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov introduce AMUC and characterize it via lenses (doi:10.1016/j.jmaa.2015.11.061).
• 2017. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang prove that an AMUC renorming with power-type modulus $t^p$ forces distortion $\gtrsim k^{1/p}$ for depth-$k$ countably branching diamonds, and prove a converse under unconditional asymptotic structure (arXiv:1612.01984).
• 2018, 2021. Swift and Perreau extend the converse to bundle graphs and dual settings under additional structure (arXiv:1710.00877, arXiv:2104.10494).
• 2025. Malthaner gives a coloring-based proof of the power-type lower bound (arXiv:2310.03257).

The source of this mission is an OpenAI preprint dated September 27, 2026; its lens input comes from the companion OpenAI preprint Midpoint lenses in segment spaces of the same date.

Setting

Diamonds. The normalized diamond $\mathcal D_0$ is one edge of length $1$. $\mathcal D_{k+1}$ replaces every edge of $\mathcal D_k$ by countably many internally disjoint two-edge paths with the same endpoints, each new edge having half the length of its parent. Let $d_k$ be the shortest-path metric. A map $f:\mathcal D_k\to Y$ has distortion at most $D$ if for some scale $s>0$

$$s\,d_k(u,v)\le\|f(u)-f(v)\|\le D\,s\,d_k(u,v)\qquad(u,v\in\mathcal D_k).$$

Tree spaces. Let $\mathcal T=\coprod_{h\ge1}\mathbb N^{\le h}$ (one rooted tree of each finite height, prefix order inside each tree). A segment is the set of vertices between two comparable nodes. For a finitely supported array $a$,

$$\rho(a)=\sup\Bigl\{\Bigl(\sum_{j=1}^m\Bigl|\sum_{s\in S_j}a_s\Bigr|^2\Bigr)^{1/2}:\ S_1,\dots,S_m\ \text{pairwise disjoint segments}\Bigr\}.$$

$J$ is the completion and $X=J^*$ with the dual norm. On $T_\infty=\mathbb N^{<\omega}$ (root included) the same formula defines $J_\infty$, and $B_\infty=\overline{\operatorname{span}}\{e_t^*\}\subset J_\infty^*$ is the closed span of the coordinate functionals.

Formalization targets

Goal: Theorem 1.1

For every $k\ge0$ and every distortion-$D$ embedding of $\mathcal D_k$ into $Y\in\{X,\ B_\infty\}$,

$$D^2\ \ge\ 1+\frac k4.$$

The Lean statement OAI.DiamondDistortion.headline_all_pairs is the conjunction of the two cases. It is open on the platform.

Significance

The bound shows that the countably branching diamonds do not embed with uniformly bounded distortion into either space, with an explicit square-root growth rate. Combined with the companion results that neither space admits an equivalent asymptotically uniformly convex norm, and that the forest dual $X$ is reflexive, it shows that the diamond obstruction can hold in reflexive spaces without AUC renormability, so the unconditional-structure hypotheses in the known converses are doing real work. The constant $1/4$ is obtained by retaining the full quadratic budget of the lens inequality. The paper also gives direct energy proofs (Theorem 5.1, Propositions 4.2–4.3) with weaker constants, and general transfer theorems (Section 7) from lens inequalities to distortion bounds.

The theorem is proved in the OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formalization would certify both the metric deduction and, through its input, the tree-space lens estimate.

Difficulty

The input lens inequality bounds only the tail of a displacement outside a finite head. Turning it into a loss of squared edge stretch at every replacement level requires selecting, among infinitely many middle vertices, two whose head projections nearly coincide, so that their half-difference is a tail vector that still lies in the lens. Doing this simultaneously along a descending chain of edges, with the head growing at each step, and summing the losses without wasting the quadratic budget is where the constant is decided. A binary diamond argument does not transfer, because finitely many midpoints give no near-coincident projections.

Formalization scope

• Diamond.Vertex k and Diamond.Edge k are defined by recursion on the stage, each parent edge receiving new vertices indexed by $\mathbb N$; Diamond.graph k is the undirected replacement graph and Diamond.distance k u v is SimpleGraph.dist divided by $2^k$. Since distortion is scale invariant, the normalization does not affect the statement.
• ForestDual is the full continuous dual of the completion of the finite-height forest James space; InfinitePredual is the norm-closed span of coordinate functionals in the dual of the infinite-tree space, with the subspace norm.
• Segments are nonempty finite intervals of an ancestral partial order; test families are finite and pairwise disjoint.
• The conclusion is stated as $1+k/4\le D^2$, with $s>0$ given and the two-sided bound holding for all pairs $u,v$.

A complete development needs the James segment norm and its dual, coordinate projections onto finite ancestral sets, the companion lens estimate, and graph distances on the countably branching diamonds. This infrastructure is shared with the other missions of this family. Formal proofs of Theorem 7.2 (lens-to-distortion transfer) and Theorem 7.12 (AMUC prevents uniform embeddings) are welcome as reusable components.

Selected references

• OpenAI, Distortion of countably branching diamonds from midpoint and tree energies, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Diamond-distortion-from-midpoint-and-tree-energies-September-27-2026/manuscript.pdf
• OpenAI, Midpoint lenses in segment spaces, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Midpoint-lenses-in-segment-spaces-September-27-2026/manuscript.pdf
• F. Baudier, R. Causey, S. Dilworth, D. Kutzarova, N. L. Randrianarivony, T. Schlumprecht, S. Zhang, On the geometry of the countably branching diamond graphs, J. Funct. Anal., 2017. https://arxiv.org/abs/1612.01984
• S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
• J. R. Lee, A. Naor, Embedding the diamond graph in $L_p$ and dimension reduction in $L_1$, Geom. Funct. Anal., 2004. https://doi.org/10.1007/s00039-004-0473-8
• W. B. Johnson, G. Schechtman, Diamond graphs and super-reflexivity, J. Topol. Anal., 2009. https://doi.org/10.1142/S1793525309000114
• R. Malthaner, On Matoušek-like embedding obstructions of countably branching graphs, J. Math. Anal. Appl., 2025. https://arxiv.org/abs/2310.03257
• R. C. James, A separable somewhat reflexive Banach space with nonseparable dual, Bull. Amer. Math. Soc., 1974. https://doi.org/10.1090/S0002-9904-1974-13580-9
• M. Girardi, The dual of the James tree space is asymptotically uniformly convex, Studia Math., 2001. https://doi.org/10.4064/sm147-2-2

Motivation

A finite Markov chain repeatedly applies a transition rule to move among a finite set of states. Its stationary distribution is a probability law that the transition rule leaves unchanged. For algorithms that sample from a target distribution, and for random walks used to model a system, a central question is how long a chain started from one state takes to resemble its stationary law. Diaconis and Saloff-Coste study how a logarithmic Sobolev inequality controls this approach to equilibrium. Their paper develops finite-chain functional inequalities and applies them to mixing bounds, product chains, and concrete walks. Diaconis and Saloff-Coste, 1996.

Theorem 3.7 gives a starting-state bound in a weighted quadratic distance. Its dependence on the initial state's stationary mass is a double logarithm, while the final convergence term is governed by the spectral gap. This separates two effects: reaching a distribution that is no longer sharply concentrated, and then reducing its remaining deviation from stationarity. The paper also distinguishes general chains from reversible ones, with different constants in the first time scale. Diaconis and Saloff-Coste, 1996, pp. 719 and 723–724.

Setting

Let $V$ be a finite state space. A transition matrix $K$ assigns nonnegative numbers $K(x,y)$ whose sum over $y$ is one for every $x$. A probability vector $\pi$ is stationary when $\sum_x\pi(x)K(x,y)=\pi(y)$ for every $y$; here every $\pi(y)$ is strictly positive. The chain is irreducible when every state can reach every other state in some finite number of steps. It is reversible when $\pi(x)K(x,y)=\pi(y)K(y,x)$ for all states $x,y$. These conditions are the paper's standing finite-chain setting. Diaconis and Saloff-Coste, 1996, pp. 700–702 and 714.

For a real function $f$ on $V$, write $E_\pi f=\sum_x f(x)\pi(x)$ and $\operatorname{Var}_\pi(f)=\sum_x(f(x)-E_\pi f)^2\pi(x)$. Its weighted $p$-norm is $\|f\|_p=(\sum_x|f(x)|^p\pi(x))^{1/p}$. The Dirichlet form used here is the ordered bilinear expression $\mathcal E(f,g)=\sum_x(f(x)-(Kf)(x))g(x)\pi(x)$. It is generally not symmetric for a nonreversible chain. The spectral gap is the variational quantity $\lambda=\inf_{\operatorname{Var}_\pi(f)\ne0}\mathcal E(f,f)/\operatorname{Var}_\pi(f)$. The log-Sobolev constant is $\alpha=\inf_{\mathcal L(f)\ne0}\mathcal E(f,f)/\mathcal L(f)$, where $\mathcal L(f)=\sum_x |f(x)|^2\log(|f(x)|^2/\|f\|_2^2)\pi(x)$. Diaconis and Saloff-Coste, 1996, pp. 701, 705–706, 714.

The continuous-time heat kernel $H_t=e^{-t(I-K)}$ averages all discrete step counts with Poisson weights. If the chain starts at $x$, then $H_t(x,y)$ is the probability of being at $y$ at time $t$. Its density relative to stationarity is $h_t^x(y)=H_t(x,y)/\pi(y)$. Thus $\|h_t^x-1\|_2$ measures the weighted quadratic deviation of the time-$t$ law from $\pi$. Diaconis and Saloff-Coste, 1996, p. 702.

Formalization targets

Spectral decay and hypercontractivity

The milestones include the $L^2$ spectral-gap decay of Lemma 2.4, the heat-flow moment identity of Lemma 2.5, the power inequalities of Lemma 2.6, and the derivative formula (3.2). The two hypercontractivity clauses of Theorem 3.5 state that $\|H_t f\|_q\le\|f\|_2$ when $q-1\le e^{2\alpha t}$ for a general chain, or when $q-1\le e^{4\alpha t}$ for a reversible chain, with $q\ge2$ and $t>0$. These are separate source statements and remain separate milestones. Diaconis and Saloff-Coste, 1996, pp. 706–707, 719–721.

Chi-square convergence

The goal is Theorem 3.7. For a state $x$ with $\pi(x)\le e^{-1}$ and any $c>0$, it asserts

$$\|h_t^x-1\|_2\le e^{1-c} \quad\text{at}\quad t=\frac{1}{2\alpha}\log\log\frac1{\pi(x)}+\frac c\lambda.$$

For a reversible chain, the same bound holds with $1/(4\alpha)$ in place of $1/(2\alpha)$. The theorem specifies these times exactly; no broader range of times is built into the goal. Diaconis and Saloff-Coste, 1996, p. 723, Theorem 3.7.

Significance

The goal turns two chain constants into an explicit convergence estimate for every eligible starting state. It provides a way to assess a chain whose initial law is a point mass, where the initial density can be large when $\pi(x)$ is small. The reversible clause records the paper's stronger time bound under detailed balance. The preceding milestones expose the general spectral and hypercontractive results as reusable statements for other mixing questions. Diaconis and Saloff-Coste, 1996, pp. 719 and 723–724.

These statements are proved in the 1996 paper; this mission asks for machine-checked proofs of the specified formal statements. Published finite-chain definitions for stochasticity, stationarity, irreducibility, detailed balance, weighted expectation and variance, and the heat kernel are already available. The variational gap, log-Sobolev constant, entropy functionals, and this theorem family are the remaining local formalization work. Their individual proof status on the platform can evolve independently after the proposal is launched.

Difficulty

The immediate spectral-gap estimate reduces the $L^2$ deviation exponentially, but by itself retains a factor tied to the size of the initial point-mass density. That gives a dependence on $\log(1/\pi(x))$, rather than the double logarithm in Theorem 3.7. The stronger bound requires control of how the heat operator changes norms, including the distinction between reversible and nonreversible chains. A formal proof must keep the bilinear Dirichlet arguments in their printed order and handle a real exponent that varies with time. Diaconis and Saloff-Coste, 1996, pp. 706–707, 719–724.

Formalization scope

The Lean state space is a finite type, $K$ is a real matrix, and $\pi$ is a real-valued stationary probability vector positive at every state. Irreducibility is explicit in the Section 3 statements; reversibility is an additional premise only for the corresponding clauses. The heat kernel is the published Poissonized semigroup. The local $\lambda$ and $\alpha$ are variational real infima, and operator norm claims are expressed as inequalities for every function. Discrete eigenvalue-based gap definitions are not substituted for the paper's $\lambda$.

The goal's condition $\pi(x)\le e^{-1}$ gives a meaningful double logarithm, and irreducibility in this finite setting gives positive gap and log-Sobolev constants on every state space where the goal is applicable. The positive stationary mass makes the density quotient meaningful. Nonnegative or positive function premises follow the source's power and derivative statements; no arbitrary sign-changing real powers are used. The Lean conventions for zero logarithm terms and for real infima are documented with the definitions. This excludes trivial conclusions from totalized logarithms, division by zero, or empty variational sets.

The development invites proofs of the seven target theorems and reusable finite-state lemmas about the semigroup, weighted norms, entropy, and variational constants. The definitions remain local to this paper's mission series because the published Markov-chain substrate provides the general finite-chain model, while the variational quantities and normalization here are tied to these source statements.

Selected references

• Persi Diaconis and Laurent Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Annals of Applied Probability 6(3):695–750, 1996. DOI: 10.1214/aoap/1034968224.