Coarse ellipticity and De Giorgi-Nash-Moser theory in the optimal range
Scott Armstrong, Benny Avelin, Tuomo Kuusi, Aatu Turpeinen
math.AP
Oct 8, 2026 · v1
TL;DR
The paper's main results are formalized in Lean 4 with Mathlib-only restatements of key theorems; the Lean code was produced by AI agents.
Abstract
We extend the theory of De Giorgi-Nash-Moser to elliptic equations with symmetric coefficients $\mathbf{a}(x)$ which are possibly degenerate and unbounded but satisfy a coarse ellipticity condition. We prove local upper bounds for weak subsolutions, a weak Harnack inequality for nonnegative supersolutions, and a Harnack inequality for nonnegative solutions. The coarse ellipticity hypothesis requires spatial moments of coarse-grained matrices, suitably discounted and summed across scales, to be finite. In particular, it holds if, for some $α,β\geq0$ and $1<p,q<\infty$, $$\mathbf{a}\in W^{-α,p}\cap L^1, \quad \mathbf{a}^{-1}\in W^{-β,q}\cap L^1 \quad\text{and}\quad \frac{α+β}{2}+\frac{d-1}{2}\Big(\frac1p+\frac1q\Big)<1.$$ We show that the coefficient range is sharp, including its boundary, in every dimension $d\geq3$, for $α=β=0$ and for the corresponding Besov-type quasi-norms of negative order when $α,β>0$. For $α=β=0$, it corresponds to the results of Bella and Schäffner [8].
Problem
De Giorgi-Nash-Moser theory, which gives local boundedness and Harnack inequalities, is extended to elliptic equations with symmetric coefficients. These coefficients may be degenerate and unbounded but satisfy a coarse ellipticity condition based on multiscale coarse-grained matrices.
Approach
The method uses weighted energy spaces, coarse-grained matrices on triadic triangulations, and fractional Sobolev embeddings. It builds a piecewise harmonic extension at good radii and combines it with Caccioppoli inequalities and De Giorgi iteration. The full development is formalized in Lean 4, with main statements restated using only Mathlib definitions. The formalization was orchestrated by Claude agents, with code written by GPT subagents.
Results
The paper proves local upper bounds for subsolutions, a weak Harnack inequality for supersolutions, and a Harnack inequality for solutions. These hold under the condition (α+β)/2 + (d-1)/2 (1/p+1/q) < 1. A construction shows this range is sharp, including the endpoint, in every dimension d≥3.
