Sullivan无游荡域定理在Lean中的形式化
Formalization of Sullivan's No Wandering Domains Theorem in Lean
浏览论文内容
中文总结 AI 辅助
本文报告了在Lean 4中形式化Sullivan无游荡域定理的工作，该定理断言黎曼球面上次数至少为二的有理自映射的每个Fatou分量最终周期，并描述了相关数学背景的形式化与证明架构。
中文摘要 AI 辅助
我们报告了Sullivan无游荡域定理在Lean 4中的形式化：黎曼球面上次数至少为二的有理自映射的每个Fatou分量最终都是周期的。该项目形式化了相关背景，包括正规族、Montel-Carathéodory定理、Julia集和Fatou集、局部Sobolev正则性和Wirtinger导数、Cauchy变换和Beurling变换、解析与几何拟共形性的等价性，以及可测黎曼映射定理。本文描述了将这些数学内容转化为Lean的过程、证明架构、可复用组件以及自动形式化工作流。
英文摘要
We report on a Lean 4 formalization of Sullivan's No Wandering Domains theorem: every Fatou component of a rational self-map of the Riemann sphere of degree at least two is eventually periodic. The project formalizes the relevant background in normal families, the Montel-Carathéodory theorem, Julia and Fatou sets, local Sobolev regularity and Wirtinger derivatives, the Cauchy and Beurling transforms, the equivalence of analytic and geometric quasiconformality, and the measurable Riemann mapping theorem. This paper describes the translation of this mathematics into Lean, the proof architecture, the reusable components, and the autoformalization workflow.
