椭圆问题解存在性数值证明的一种新形式化

无限维牛顿方法可有效用于推导偏微分方程(PDEs)解存在性的数值证明。在PDE的计算机辅助证明中，原问题被转化为无限牛顿型不动点方程 $w = - {\mathcal L}^{-1} {\mathcal F}(\hat{u}) + {\mathcal L}^{-1} {\mathcal G}(w)$，其中 ${\mathcal L}$ 是线性化算子，${\mathcal F}(\hat{u})$ 是残差，${\mathcal G}(w)$ 是局部Lipschitz项。因此，$\| {\mathcal L}^{-1} {\mathcal F}(\hat{u}) \|$ 和 $\| {\mathcal L}^{-1}{\mathcal G}(w) \|$ 的估计在验证过程中起主要作用。本文利用类似于矩阵问题中的“Schur补”概念，将逆算子 ${\mathcal L}^{-1}$ 表示为可分解为有限维和无限维两部分的无限维算子矩阵。该算子矩阵给出了无限维牛顿方法的一种新的有效实现，与现有椭圆PDE解的方法相比，实现了更高效的验证过程。我们给出了一些确认所提方法有用性的数值例子。附录中给出了由算子矩阵表示为 ${\mathcal L}^{-1}$ 得到的相关结果。