Escauriaza–Seregin–Šverák and Ladyzhenskaya–Prodi–Serrin regularity
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-03-000006
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-03-000006/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-03-000006/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'