Formal verification of iterative convergence of numerical algorithms

Physical systems are usually modeled by differential equations, but solving these differential equations analytically is often intractable. Instead, the differential equations can be solved numerically by discretization in a finite computational domain. The discretized equation 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_m. The iterative algorithm is said to converge to the exact solution x of the linear system if and only if x_m converges to x. It is important that we formally guarantee the convergence of iterative algorithm, since these algorithms are used in simulations for design of safety critical systems such as airplanes, cars, or nuclear power plants. In this paper, we first formalize the necessary and sufficient conditions for iterative convergence in the Coq proof assistant. We then extend this result to two classical iterative methods: Gauss-Seidel iteration and Jacobi iteration. We formalize conditions for the convergence of the Gauss--Seidel classical iterative method, based on positive definiteness of the iterative matrix. We then use these conditions and the main proof of iterative convergence to prove convergence of the Gauss-Seidel method. We also apply the main theorem of iterative convergence on an example of the Jacobi classical iterative method to prove its convergence. We leverage recent developments of the Coq linear algebra, Coquelicot's real analysis library and the mathcomp library for our formalization