{"id":"palomar/PALOMAR-2026-10-03-000006","url":"https://github.com/scottnarmstrong/EscauriazaSereginSverak/tree/ae1a0e46086b9b16179dea76b41da10b01845151","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-03-000006-v1.json","repo":"https://github.com/scottnarmstrong/EscauriazaSereginSverak","tags":["math.AP","msc:35Q30","msc:76D05","msc:35B65","msc:35D30","msc:35B60","navier-stokes","pde-regularity","fluid-dynamics","lean-formalization"],"score":0,"title":"Escauriaza–Seregin–Šverák and Ladyzhenskaya–Prodi–Serrin regularity","trust":"high","domain":"math.AP","source":"palomar","authors":["Scott Armstrong"],"reviews":0,"subject":"math.AP","summary":"A Lean formalization of two classical regularity theorems for the three-dimensional incompressible Navier–Stokes equations. The Escauriaza–Seregin–Šverák theorem states that a Leray–Hopf solution whose spatial L³ norm remains bounded in time is smooth at positive times and unique among Leray–Hopf solutions with the same initial data. The Ladyzhenskaya–Prodi–Serrin theorem gives the corresponding conclusion under a family of mixed space-time integrability conditions. The development includes the local regularity theorem, L⁵ space-time integrability under the endpoint L³ condition, and the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-03","reactions":{},"formalized":true,"formalizes":[{"title":"The Escauriaza--Seregin--Šverák theorem: version for the Lean formalization","identifier":"paper/ess.tex","relationship":"formalizes"},{"title":"The Three-Dimensional Navier-Stokes Equations: Classical Theory","identifier":"doi:10.1017/CBO9781139095143","relationship":"formalizes"}]}