Formalizing De Giorgi-Nash-Moser theory in Lean
Julia Kempe and I have just completed a Lean 4 formalization of De Giorgi–Nash–Moser theory. We formalized the full slate of interior regularity statements for weak solutions of divergence-form elliptic equations with merely bounded measurable (and not necessarily symmetric) coefficients, including local boundedness, the weak Harnack and Harnack inequalities, and finally interior Hölder regularity. The […]
Formalizing De Giorgi-Nash-Moser theory in Lean Read More »