Solvability of divergence-form elliptic equations (Evans §6.2)
A Lean 4 formalisation of the solvability theory of linear second-order elliptic operators in divergence form on a bounded domain, -div(A grad u) + b · grad u + c u = f in Ω, u = 0 on ∂Ω, with A uniformly elliptic and every coefficient bounded and measurable. The drift b is unrestricted and the bilinear form is in general non-symmetric. The six compared statements are the results of Evans §6.2: the Gårding inequality, existence and uniqueness of the weak solution with no drift and a nonnegative zeroth-order coefficient, the Fredholm alternative, solvability against the transpose problem, the…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-15-000012
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-15-000012/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-15-000012/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'