arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2202.05587math.NAcs.NA
收藏

平稳迭代方法渐近收敛的形式化

Formalization of Asymptotic Convergence for Stationary Iterative Methods

Mohit Tekriwal, Joshua Miller, Jean-Baptiste Jeannin

AI总结:

本文在 Coq 定理证明器中形式化证明了平稳迭代方法的渐近收敛性,给出了收敛的充要条件,并应用于 Gauss-Seidel 和 Jacobi 方法及一维热方程模型问题。

摘要:

用于模拟物理系统的微分方程的解,是通过求解一组离散化方程来数值计算的。这组离散化方程被化简为一个大型线性系统,其解通常使用迭代求解器来求得。我们从初始猜测 $x_0$ 开始,迭代该算法以获得解向量序列 $x_k$,这些向量是线性系统精确解 $x$ 的近似。在实数域中,当且仅当 $x_k$ 在 $k \to \infty$ 的极限下收敛于 $x$ 时,称该迭代算法收敛于 $x$。\n 在本文中,我们在 Coq 定理证明器中正式证明了被称为平稳迭代方法的一类特定迭代方法的渐近收敛性。我们形式化了迭代收敛所需的必要且充分条件,并将此结果扩展到两种经典迭代方法:Gauss-Seidel 方法和 Jacobi 方法。对于 Gauss-Seidel 方法,我们还针对特定的矩阵结构形式化了一组易于检验的迭代收敛条件,称为 Reich 定理,并将其应用于一维热方程的模型问题。我们还应用迭代收敛的主定理来证明 Jacobi 方法在该模型问题上的收敛性。

英文摘要:

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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑