Documentation

LeanPool.EllipticPDE

Linear elliptic PDE: solvability, regularity and spectral theory #

Source: arxiv:2609.32561, url:https://github.com/alejandro-soto-franco/EllipticPDE Authors: Alejandro José Soto Franco, Kobe Marshall-Stevens Status: verified Main declarations: EllipticPdes.Regularity.higher_interior_regularity Tags: elliptic-pde, sobolev-spaces, regularity, fredholm-theory, spectral-theory MSC: 35J15, 35J25, 35B65, 46E35

EllipticPdes #

Solvability and interior regularity for the linear second-order elliptic Dirichlet problem in divergence form on a bounded domain, with bounded measurable coefficients and a drift term, so the bilinear form is in general non-symmetric.

For zero drift and a nonnegative zeroth-order term, existence and uniqueness run from the one-dimensional Poincaré inequality through the domain inequality, continuity and coercivity of the form, and Lax-Milgram. The same operator then supports the Gårding inequality, the Fredholm alternative with its index and solvability clauses, the resolvent bound and spectral compactness, the interior H² estimate with its higher-order and smooth refinements, and interior Hölder continuity in dimensions one to three through Morrey's inequality and Campanato's characterisation.

The imported closure contains completed results; boundary H² regularity is outside its scope.