在 Lean 中形式化 Vlasov--Poisson 方程中的朗道阻尼
Formalization of Landau damping in the Vlasov--Poisson equations in Lean
首次发表
浏览论文内容
中文总结 AI 辅助
本文在 Lean 4 中形式化了 Mouhot 和 Villani 关于非线性朗道阻尼的定理，覆盖所有 Gevrey 指标 $s>1/3$ 的小背景情况。
中文摘要 AI 辅助
我们在 Lean 4 中形式化了 Mouhot 和 Villani 关于在 $\u211d^d$ 中所有 Gevrey 正则性指标 $s > 1/3$ 的小背景下非线性朗道阻尼的定理。
英文摘要
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.
发表机构
- University of California, Los Angeles（加州大学洛杉矶分校）
机构由 AI 辅助整理，请以论文原文为准。
