{"id":"palomar/PALOMAR-2026-10-11-000003","url":"https://github.com/scottnarmstrong/CoarseDeGiorgi/tree/200c40c9c55a5e19188739d27466ddffcb2660c4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-11-000003-v1.json","repo":"https://github.com/scottnarmstrong/CoarseDeGiorgi","tags":["math.AP","msc:35J70","msc:35B65","msc:35J15","msc:35B45","elliptic-pde","de-giorgi","degenerate-coefficients","lean"],"score":0,"title":"De Giorgi–Nash–Moser theory under coarse ellipticity","trust":"high","domain":"math.AP","source":"palomar","authors":["Scott Armstrong","Benny Avelin","Tuomo Kuusi","Aatu Turpeinen"],"reviews":0,"subject":"math.AP","summary":"A Lean 4 formalization of the paper \"Coarse ellipticity and De Giorgi–Nash–Moser theory in the optimal range\" by S. Armstrong, B. Avelin, T. Kuusi and A. Turpeinen (arXiv:2610.11879). The paper extends the theory of De Giorgi–Nash–Moser to elliptic equations with symmetric coefficients a(x) which are possibly degenerate and unbounded but satisfy a coarse ellipticity condition: spatial moments of coarse-grained matrices, suitably discounted and summed across scales, are finite. Under this condition it proves local upper bounds for weak subsolutions, a weak Harnack inequality for nonnegative…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-11","reactions":{},"formalized":true,"formalizes":[{"title":"Coarse ellipticity and De Giorgi–Nash–Moser theory in the optimal range","identifier":"arxiv:2610.11879","relationship":"formalizes"}]}