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.

翻译：微分方程用于建模物理系统，其数值解需通过求解一组离散化方程获得。这组离散化方程可归结为大型线性系统，其解通常采用迭代求解器计算。我们以初始猜测 $x_0$ 出发，通过算法迭代生成解向量序列 $x_k$，这些向量逐步逼近线性系统的精确解 $x$。在实数域中，当且仅当 $x_k$ 在 $k \to \infty$ 极限下收敛于 $x$ 时，称该迭代算法收敛。本文在 Coq 定理证明器中形式化证明了一类特定迭代方法——定常迭代法的渐近收敛性。我们建立了迭代收敛的充要条件，并将该结果推广至两种经典迭代法：高斯-赛德尔法与雅可比法。针对高斯-赛德尔法，进一步形式化了一组易于检验的收敛条件（即 Reich 定理），该条件适用于特定矩阵结构，并将其应用于一维热传导方程模型问题的求解。同时，我们运用迭代收敛主定理，证明了模型问题中雅可比法的收敛性。