Lax-Milgram 定理：待在 Coq 中形式化的详细证明
计算机科学中的逻辑
2016-10-05 v2 数值分析
摘要
为了对实现有限元方法的数值模拟程序的正确性获得最高置信度，必须对能够确立该方法可靠性的数学概念和结果进行形式化。Lax-Milgram 定理可被视为这些理论基石之一：在一定的完备性和强制性假设下，它表明某些边值问题的弱形式解的存在性与唯一性。本文档旨在为形式化证明社区提供一份关于 Lax-Milgram 定理的非常详细的纸笔证明。
引用
@article{arxiv.1607.03618,
title = {The Lax-Milgram Theorem. A detailed proof to be formalized in Coq},
author = {François Clément and Vincent Martin},
journal= {arXiv preprint arXiv:1607.03618},
year = {2016}
}