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.