Formalization of Landau damping in the Vlasov--Poisson equations in Lean

Abstract

We present a formalization in Lean 4 of Mouhot and Villani's theorem on nonlinear Landau damping in ${\mathbb{T}}^d$ in all Gevrey regularity indices $s>1/3$ for small backgrounds.