Formalising Linear Elliptic PDE Theory in Lean 4 NBT0ZCHBB6

URI	`m2://res/NBT0ZCHBB6`
Kind	preprint
Creators	Alejandro José Soto Franco, Kobe Marshall-Stevens
Date	2026-09-26
MSC	35-XX
Subjects	arxiv math.AP, arxiv cs.LO
Scope	in

Expressions

The mentions of the inventory that name this resource. Each name links to the card of its inventory row.

Item	Kind	Where	Source
One-dimensional Poincar\'e inequality	statement	lemma 2	arxiv
Classical solvability in the interior, [\S 6.3.1, Theorem 3]{evans-2010-par-dif-equ	statement	corollary 3	arxiv
G{\aa}rding inequality	statement	theorem 3	arxiv
Sobolev embedding	statement	theorem 10	arxiv
Spectrum of a compact operator	statement	theorem 8	arxiv
Variational principle for the principal eigenvalue	statement	theorem 7	arxiv
Existence II	statement	theorem 6	arxiv
Completeness of the eigenspaces	statement	corollary 2	arxiv
Lax--Milgram theorem	statement	theorem 2	arxiv
Weak solvability of the Poisson equation	statement	corollary 1	arxiv
Existence I	statement	theorem 4	arxiv
Existence III	statement	theorem 9	arxiv
Existence II	statement	theorem 5	arxiv
Infinite differentiability in the interior	statement	theorem 13	arxiv
Interior $H^2$ regularity	statement	theorem 11	arxiv
Higher interior regularity	statement	theorem 12	arxiv
Poincar\'e inequality	statement	theorem 1	arxiv
One-dimensional Cauchy--Schwarz inequality	statement	lemma 1	arxiv