Formalization of De Giorgi--Nash--Moser Theory in Lean

Scott Armstrong, Julia Kempe

We present a formalization in Lean of the core interior De Giorgi--Nash--Moser theory for uniformly elliptic divergence-form equations with bounded measurable coefficients. The for…