finite difference格式的Lax等价定理的形式证明
A formal proof of the Lax equivalence theorem for finite difference schemes
摘要：
物理系统的行为通常使用微分方程来建模，这些微分方程太复杂而无法解析求解。在实际问题中，这些方程在计算域上离散，并计算数值解。如果在无穷小的离散极限内，离散误差的离散化误差的界也是无穷小的，则称一个数值格式是收敛的。在此极限下，近似解收敛于“真解”。Lax等价定理使收敛性证明的一致性和稳定性的方法。在这项工作中，我们使用Coq Proof Assistant正式证明了Lax等价定理。我们假设完备赋范空间之间的连续线性微分算子，并在离散化空间中定义一个等价映射。假定数值方法是一致的（即，当离散化步长趋于零时离散化误差趋于零），并且该方法是稳定的（即，误差是一致有界的），形式上证明了该近似解收敛于真解.然后，我们证明了收敛的差分格式的一个例子的问题，证明其一致性和稳定性，然后应用Lax等价定理。为了证明一致性，我们使用泰勒-拉格朗日定理，正式表明，离散化误差是有界以上的离散化步骤的n次幂，其中n是截断泰勒多项式的顺序。
英文摘要：
The behavior of physical systems is typically modeled using differential equations which are too complex to solve analytically. In practical problems, these equations are discretized on a computational domain, and numerical solutions are computed. A numerical scheme is called convergent, if in the limit of infinitesimal discretization, the bounds on the discretization error is also infinitesimally small. The approximate solution converges to the "true solution" in this limit. The Lax equivalence theorem enables a proof of convergence given consistency and stability of the method. In this work, we formally prove the Lax equivalence theorem using the Coq Proof Assistant. We assume a continuous linear differential operator between complete normed spaces, and define an equivalent mapping in the discretized space. Given that the numerical method is consistent (i.e., the discretization error tends to zero as the discretization step tends to zero), and the method is stable (i.e., the error is uniformly bounded), we formally prove that the approximate solution converges to the true solution. We then demonstrate convergence of the difference scheme on an example problem by proving both its consistency and stability, and then applying the Lax equivalence theorem. In order to prove consistency, we use the Taylor-Lagrange theorem by formally showing that the discretization error is bounded above by the nth power of the discretization step, where n is the order of the truncated Taylor polynomial.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
