KAM 理论的严格计算机辅助应用：一种现代方法

本文提出并阐释一种基于{\em 后验}方法将 KAM 理论应用于特定问题的一般方法论。我们关注辛映射的实解析拟周期拉格朗日不变环面的存在性。目的在于以后验格式验证 KAM 定理的假设：给定近似不变环面的一个参数化，我们必须检验非共振（丢番图）条件、非退化条件以及某些不等式成立。为检验此类不等式，我们需要控制依赖于映射、环境结构和参数化的某些函数的解析范数。为此，我们提出一种高效的计算机辅助方法论，使用快速傅里叶变换，其渐近代价与用于获得不变环面数值近似的参数化方法相同。我们通过证明标准映射（直至 $\eps=0.9716$）的不变曲线、非扭曲标准映射的蜿蜒曲线以及 Froeschlé 映射的二维环面的存在性来阐释我们的方法论。