论文标题
用于固定迭代方法的渐近收敛的形式化
Formalization of Asymptotic Convergence for Stationary Iterative Methods
论文作者
论文摘要
用于建模物理系统的微分方程的解决方案是通过求解一组离散方程来数值计算的。这组离散的方程式被简化为大型线性系统，通常使用迭代求解器找到该解决方案。我们从初始猜测（$ x_0 $）开始，然后迭代算法以获得一系列解决方案向量，$ x_k $，这是线性系统的精确解决方案$ x $的近似值。据说，当$ x_k $收敛到$ k \ of $ k \ to \ infty $时，迭代算法被认为在皇家领域收敛到$ x $。 在本文中，我们正式证明了在COQ定理供体中，特定类别的迭代方法称为固定迭代方法的渐近收敛性。我们将迭代收敛性所需的必要条件正式化，并将此结果扩展到两种经典的迭代方法：高斯 - Seidel方法和Jacobi方法。对于Gauss-seidel方法，我们还为迭代收敛的一组易于测试条件（称为帝国定理，特定的矩阵结构）形式化，并将其应用于一维热方程的模型问题上。我们还将迭代收敛的主要定理应用于模型问题上证明雅各比方法的收敛性。
Solutions to differential equations, which are used to model physical systems, are computed numerically by solving a set of discretized equations. This set of discretized equations is reduced to a large linear system, whose solution is typically found using an iterative solver. We start with an initial guess, $x_0$, and iterate the algorithm to obtain a sequence of solution vectors, $x_k$, which are approximations to the exact solution of the linear system, $x$. The iterative algorithm is said to converge to $x$, in the field of reals, if and only if $x_k$ converges to $x$ in the limit of $k \to \infty$. In this paper, we formally prove the asymptotic convergence of a particular class of iterative methods called the stationary iterative methods, in the Coq theorem prover. We formalize the necessary and sufficient conditions required for the iterative convergence, and extend this result to two classical iterative methods: the Gauss--Seidel method and the Jacobi method. For the Gauss--Seidel method, we also formalize a set of easily testable conditions for iterative convergence, called the Reich theorem, for a particular matrix structure, and apply this on a model problem of the one-dimensional heat equation. We also apply the main theorem of iterative convergence to prove convergence of the Jacobi method on the model problem.
