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.


翻译:物理系统通常以差异方程式为模型, 但分析解决这些差异方程式往往难以解决。 相反, 差异方程式可以通过在有限计算域中的离散化以数字方式解决。 离散方程式被降为大型线性系统, 其解决方案通常使用迭代求解器。 我们从最初的猜测开始, $_ 0 美元, 并循环算法以获得解析矢量序列, x_ m 。 迭代算法据说会趋同于线性系统的确切解决方案 x, 前提是 x_ m 和 x 。 重要的是, 我们正式保证迭代算法的趋同性, 因为这些算法用于模拟设计安全关键系统, 如飞机、汽车或核电厂等。 在本文中, 我们首先正式设定必要和足够的条件, 用于调合调调调调。 然后将这一结果推广到两种经典的迭代方法: 高音- Seidel Exliverationation 和 Jacoberationration 。 我们正式确定调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调,,, 的调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调调, 。

0
下载
关闭预览

相关内容

Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
零样本文本分类,Zero-Shot Learning for Text Classification
专知会员服务
95+阅读 · 2020年5月31日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
AIART 2022 Call for Papers
CCF多媒体专委会
1+阅读 · 2022年2月13日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium9
中国图象图形学学会CSIG
0+阅读 · 2021年12月17日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium8
中国图象图形学学会CSIG
0+阅读 · 2021年11月16日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium7
中国图象图形学学会CSIG
0+阅读 · 2021年11月15日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium5
中国图象图形学学会CSIG
1+阅读 · 2021年11月11日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium2
中国图象图形学学会CSIG
0+阅读 · 2021年11月8日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium1
中国图象图形学学会CSIG
0+阅读 · 2021年11月3日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2022年8月3日
Arxiv
0+阅读 · 2022年7月29日
VIP会员
相关VIP内容
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
零样本文本分类,Zero-Shot Learning for Text Classification
专知会员服务
95+阅读 · 2020年5月31日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
相关资讯
AIART 2022 Call for Papers
CCF多媒体专委会
1+阅读 · 2022年2月13日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium9
中国图象图形学学会CSIG
0+阅读 · 2021年12月17日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium8
中国图象图形学学会CSIG
0+阅读 · 2021年11月16日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium7
中国图象图形学学会CSIG
0+阅读 · 2021年11月15日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium5
中国图象图形学学会CSIG
1+阅读 · 2021年11月11日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium2
中国图象图形学学会CSIG
0+阅读 · 2021年11月8日
【ICIG2021】Check out the hot new trailer of ICIG2021 Symposium1
中国图象图形学学会CSIG
0+阅读 · 2021年11月3日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
相关基金
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员