Hörmander's hypoellipticity theorem and the Rothschild–Stein theory
A Lean 4 / Mathlib formalization of the regularity theory of Hörmander operators: second-order operators built from smooth vector fields X_1, ..., X_q (and possibly a drift X_0) whose iterated commutators span the tangent space at every point. It proves Hörmander's 1967 theorem that such operators are hypoelliptic: every locally integrable weak solution of X_0 u + sum X_i^2 u + c u = g with smooth data is smooth. It then develops the Rothschild–Stein theory (Acta Math. 1976), following Bramanti and Brandolini's "Hörmander Operators" (2023): lifting and approximation of the fields by the…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-09-000014
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-09-000014/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-09-000014/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'