{"id":"palomar/PALOMAR-2026-10-15-000012","url":"https://github.com/alejandro-soto-franco/EllipticPDE/tree/ec784093f30308ef770ff855ce624725adf6f870/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000012-v2.json","repo":"https://github.com/alejandro-soto-franco/EllipticPDE","tags":["math.AP","msc:35J25","msc:47A53","msc:35A01","msc:35A02","elliptic-pdes","functional-analysis","formal-verification"],"score":0,"title":"Solvability of divergence-form elliptic equations (Evans §6.2)","trust":"high","domain":"math.AP","source":"palomar","authors":["Alejandro Soto Franco","Kobe Marshall-Stevens"],"reviews":0,"subject":"math.AP","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"Partial Differential Equations (2nd edition), Graduate Studies in Mathematics 19","identifier":"American Mathematical Society, 2010","relationship":"formalizes"}]}