{"id":"palomar/PALOMAR-2026-09-07-000015","url":"https://github.com/Arthur742Ramos/lean-poincare-formalization-plan/tree/d9f4c4deaea269a1ab1f5f8874697da798cc3db2/almost-schur","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-07-000015-v1.json","repo":"https://github.com/Arthur742Ramos/lean-poincare-formalization-plan","tags":["math.DG","math.LO","msc:53C21","msc:53C25","msc:03B35","riemannian-geometry","scalar-curvature","lean","formalization"],"score":0,"title":"De Lellis--Topping almost-Schur inequality","trust":"high","domain":"math.DG","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"math.DG","summary":"Formalizes the quantitative almost-Schur lemma on nonempty connected closed smooth Riemannian manifolds of dimension at least three with nonnegative Ricci curvature: scalar-curvature variance is bounded by 4*n*(n-1)/(n-2)^2 times the squared L2 norm of trace-free Ricci, with the Einstein equality characterization. The development constructs normalized Riemannian volume, solves the mean-zero Poisson problem variationally and upgrades it to a smooth representative, proves the actual integrated Bochner and contracted-Bianchi identities, and closes the sharp algebra.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-07","reactions":{},"formalized":true,"formalizes":[{"title":"Almost-Schur lemma","identifier":"10.1007/s00526-011-0413-z","relationship":"formalizes"}]}