PreprintarXiv licencearXiv
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 ๐d in all Gevrey regularity indices s > 1/3 for small backgrounds.
Related
- Nonlinear Landau damping for the unconfined Vlasov-Poisson system in 2D
- Galaxy dynamics, gravitational VlasovโPoisson system, Landau damping, and scattering theory *
- Large-Box Transition in Nonlinear Landau Damping for the Vlasov--Yukawa Equation
- Pointwise Wave--Damping for Linearized Vlasov--Poisson: Compactly Supported Radial Equilibria and Relativistic Applications
- A model of a multiphase medium based on the closure of moment chains for the Vlasov-Poisson equations
BibTeX
@misc{bedrossian2026formalization,
title = {{Formalization of Landau damping in the Vlasov--Poisson equations in Lean}},
author = {Jacob Bedrossian},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.16801},
eprint = {2609.16801},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.16801},
}
RIS
TY - UNPB
TI - Formalization of Landau damping in the Vlasov--Poisson equations in Lean
AU - Jacob Bedrossian
PY - 2026
DA - 2026/09/15
PB - arXiv
DO - 10.48550/arxiv.2609.16801
UR - https://arxiv.org/abs/2609.16801
AB - We present a formalization in Lean 4 of Mouhot and Villani's theorem on nonlinear Landau damping in ๐^d in all Gevrey regularity indices s > 1/3 for small backgrounds.
ER -