有限差分格式Lax等价定理的形式化证明
数值分析
2021-03-26 v1 形式语言与自动机理论
数值分析
摘要
物理系统的行为通常用微分方程建模，这些方程过于复杂而无法解析求解。在实际问题中，这些方程在计算域上被离散化，并计算数值解。若在小离散化极限下离散化误差的界也无穷小，则称数值格式收敛。在此极限下近似解收敛到“真解”。Lax等价定理在方法一致且稳定的前提下可证明收敛性。本文中，我们使用Coq证明助手形式化证明了Lax等价定理。我们假设完备赋范空间之间的连续线性微分算子，并定义离散化空间中的等价映射。给定数值方法一致（即离散化误差随离散化步长趋于零而趋于零）且稳定（即误差一致有界），我们形式化证明近似解收敛到真解。然后我们通过证明某示例问题差分格式的一致性与稳定性并应用Lax等价定理，演示了该差分格式的收敛性。为证明一致性，我们利用Taylor-Lagrange定理，通过形式化表明离散化误差由上界为离散化步长的n次幂所界定，其中n为截断Taylor多项式的阶数。
引用
@article{arxiv.2103.13534,
title = {A formal proof of the Lax equivalence theorem for finite difference schemes},
author = {Mohit Tekriwal and Karthik Duraisamy and Jean-Baptiste Jeannin},
journal= {arXiv preprint arXiv:2103.13534},
year = {2021}
}