验证 Taylor 步与全步包围

形式陈述

普通时间步返回一个近似点；验证Taylor步返回一只包含所有允许初值之真实终值的盒。先证明轨道在整步内有界，再用这个界认证余项，是算法的两个不同阶段。

考虑实系统 $x'=f(t,x)$ ，状态维数 $d\ge1$ 。输入为时刻 $t$ 、步长 $h>0$ 、非空紧初值盒 $X$ 、整数阶数 $p\ge1$ ，以及在开定义域中具有 $p$ 阶连续导数的 $f$ 。所有盒运算均采用可靠的区间包含运算；有理精确端点也是一种实现。记 $I=[t,t+h]$ 。

第一阶段：认证整步存在

提出一个紧盒 $B$ ，检查 $I\times B$ 位于定义域内，并取得 $f$ 在其上的包含扩张 $[f](I,B)$ 。若

\boxed{X+[0,h]\,[f](I,B)\subset\operatorname{int}B,} \tag{1}

则每个 $\xi\in X$ 的解都存在到 $t+h$ ，且整个时间段内留在 $B$ 。式(1)是逐坐标严格包含；不是只检查候选终点在 $B$ 里。

这是一项充分条件。失败时可以改变 $B$ 或 $h$ ，也可以返回未认证；不能因此断言原问题无解。盒 $B$ 可宽于最终希望交付的端点盒。

第二阶段：认证有限Taylor余项

定义向量函数

F_0(s,y)=y,\qquad F_{k+1}(s,y)=\frac1{k+1} \left(\partial_sF_k(s,y)+D_yF_k(s,y)f(s,y)\right), \quad0\le k\le p. \tag{2}

取得包含盒

C_k\supseteq\{F_k(t,\xi):\xi\in X\},\quad0\le k\le p, \qquad E\supseteq\{F_{p+1}(s,y):(s,y)\in I\times B\}.

其中 $C_0=X$ 。返回

\boxed{Y=B\cap\left(\sum_{k=0}^{p}h^k C_k+h^{p+1}E\right).} \tag{3}

于是精确流映射满足

\Phi_{t,h}(X)\subseteq Y. \tag{4}

式(2)中显含时间的导数不能漏掉。 $F_k$ 已除以 $k!$ ，式(3)不应再除一次阶乘。

直觉

Taylor系数描述从起点怎样出发，余项却依赖这一步中途经过的状态。若直接用一个尚未证明有效的小盒估计余项，就可能用错误的余项“证明”自己选的盒。第一阶段提供独立的全步范围，第二阶段才有可靠的余项输入。

整步盒与端点盒也不一样。轨道可能在中途达到一个大值，终点却很小；只包住终点不能控制途中导数。反过来，第一阶段的盒可以很粗，有限Taylor式仍可能给出窄得多的终点包围。

严格包含为何给整步存在

局部存在唯一性先对每个初值成立，因为 $f$ 至少为 $C^1$ 。式(1)含 $X\subset\operatorname{int}B$ 。若解首次在时刻 $s\le t+h$ 触及 $\partial B$ ，此前的积分式给

x(s)=\xi+\int_t^s f(\tau,x(\tau))\,d\tau \in X+[0,h]\,[f](I,B)\subset\operatorname{int}B,

矛盾。积分平均留在向量盒内，这里没有让不同分量共用某个中间时间点。

若最大解在本步内停止而尚未触边，紧集 $I\times B$ 上的速度有界，所以有限端点处有状态极限；该点在开定义域内，可以再次局部延拓。于是每个初值的解确实覆盖整步。这个证明不要求额外检查 $hL<1$ ：短时局部定理和首次出盒已经完成了延拓逻辑。

归一化导数与正权余项

沿一条真实轨道应用链式法则，由式(2)归纳得

x^{(k)}(s)=k!F_k(s,x(s)),\qquad0\le k\le p+1.

积分型Taylor余项于是给

x(t+h)=\sum_{k=0}^p h^kF_k(t,\xi) +(p+1)\int_0^h(h-s)^pF_{p+1}(t+s,x(t+s))\,ds. \tag{5}

最后积分的权重非负，总质量为 $h^{p+1}$ ，且轨道已被证明在 $B$ 内。因此积分项属于 $h^{p+1}E$ ，得到式(3)。对向量值函数，各分量的积分余项都属于对应的盒分量，不需要存在一个共用的Lagrange中值点。

例子与边界

一步有理证书

取 $x'=x^2$ 、 $t=0$ 、 $X=[1,101/100]$ 、 $h=1/8$ ，提出

B=[9/10,6/5].

$[f](I,B)=[81/100,36/25]$ ，所以

X+[0,1/8][f](I,B)=[1,119/100] \subset(9/10,6/5).

整步认证通过。递推式(2)给 $F_k(x)=x^{k+1}$ 。取 $p=4$ ，式(3)的未交集部分为

Y_*=\sum_{k=0}^4\frac{X^{k+1}}{8^k}+\frac{B^6}{8^5}.

这里所有区间端点为正，幂的真实值域由端点给出；精确有理计算得到

Y_*= \left[\frac{37448531441}{32768000000}, \frac{47349395541301}{40960000000000}\right] \subset \left[\frac{1142838}{10^6},\frac{1155992}{10^6}\right]. \tag{6}

$Y_*\subset B$ ，故 $Y=Y_*$ 。这次认证没有使用精确解；事后用 $x(s;\xi)=\xi/(1-s\xi)$ 交叉检查，真实终值范围是 $[8/7,808/699]$ ，确实包含于式(6)的精确区间。

若错误地提出 $B=[1,11/10]$ ，式(1)不仅下端没有严格余量，上端也越过 $11/10$ ，必须拒绝。这不会使已经存在的真实解消失，只说明该盒不适合作为当前步的证书。

非自治项不能用自治递推替代

对 $x'=t+x$ ， $F_1=t+x$ ，而

F_2=\tfrac12(1+t+x).

若只算 $D_xF_1\,f/2$ ，会漏掉常数 $1/2$ 。将时间并入扩展状态 $s'=1$ 可以统一实现，但输出和余项仍要按原时间区间解释。

区间相加可能抹掉真实收缩

对 $x'=-x$ ，若只用一阶区间式 $X-hX$ ，两个 $X$ 被当作独立取值，宽度变为 $(1+h)\operatorname{wid}X$ ；真实流却将宽度乘 $e^{-h}$ 。更高阶展开仍可能遇到重复出现初值的依赖损失。可靠性与紧致度是两项不同任务，保留坐标关系的流集合传播专门处理后者。

光滑性与爆破

本页使用有限阶导数，不要求 $f$ 解析，也不要求无穷Taylor级数收敛。对不光滑右端，应选择与其解概念相符的方法，不能继续调用不存在的 $F_{p+1}$ 。

$x'=x^2$ 的解会在有限时间爆破。认证程序若在接近爆破时反复缩步而不能覆盖指定终点，应返回实际认证到的时间。无穷多步逼近一个较早时间不是“完成到 $T$ ”。

推论与应用

完整推进与可复核输入

一份有限网格证书保存

t_0<t_1<\cdots<t_N=T,\qquad X_0,B_0,X_1,B_1,\ldots,B_{N-1},X_N.

每步的起点盒为 $X_n$ ，通过式(1)及式(3)后，要求实际保存的 $X_{n+1}$ 包含得到的 $Y_n$ 。归纳不变量是：每个原始初值的解存在到当前时刻，并且 $x(t_n)\in X_n$ 。第二阶段也可在 $0\le s\le h_n$ 上评估式(5)，给密集时间包围，不能把端点插值自动称为严格流管。

复核器应重新计算向量场、系数和余项的区间包含，而不是信任证书声称的一个小数字。对多项式右端，可保存精确系数与运算树，用有理区间重放；对超越函数则需要已验证的基础函数外包络。每步还要检查盒非空、域条件、步长正、时刻相接和最后时刻恰为目标 $T$ 。

被拒绝的步不改变当前认证状态。候选生成器可以缩步或增大工作盒，但需要限制尝试次数和最小步长，并保留失败原因。预算耗尽返回“未决”，不能强行接受没有通过式(1)的步。后验残差流管是另一种认证路径，可检查外部求解器已有的连续轨道，并不要求候选本身来自Taylor方法。

计算量按实际表达式计算

若直接符号递推式(2)，表达式可能迅速膨胀，不能只按 $p$ 报线性成本。对由 $L$ 个加、减、乘运算组成的多项式求值图，可用归一化时间系数的截断级数传播：加法逐系数相加，乘法取卷积

(uv)_k=\sum_{j=0}^k u_jv_{k-j},\qquad x_{k+1}=f_k/(k+1).

朴素卷积得到前 $p+1$ 阶需 $O(L(p+1)^2)$ 次标量区间运算，保存各节点系数需 $O(L(p+1))$ 空间。对起点盒和整步盒分别重放，量级相同；盒检查与端点组合另需 $O(dp)$ 。这里 $L$ 必须包含所用非自治时间输入与全部分量的运算，稠密耦合的成本不会凭空消失。

有理实现还要计入分子分母的位数增长；浮点区间实现要计入端点精度与向外舍入。跨越多步时，实际接受步和拒绝尝试都消耗计算。以上是给定表达式图的算术成本，不是任意ODE达到指定精度的统一复杂度保证。

参考资料

N. S. Nedialkov、K. R. Jackson、G. F. Corliss，“Validated Solutions of Initial Value Problems for Ordinary Differential Equations”，Applied Mathematics and Computation 105 (1999), pp.21–68。作者技术报告目录，1997报告 vsode.97.ps.gz：§2.5 pp.7–8，§§4–5.1 pp.8–10，§7 pp.17–18，分别给系数传播、全步存在包围和端点细化。本页采用严格包含加首次出盒的证明。

形式陈述 ​

第一阶段：认证整步存在 ​

第二阶段：认证有限Taylor余项 ​

严格包含为何给整步存在 ​

归一化导数与正权余项 ​

一步有理证书 ​

非自治项不能用自治递推替代 ​

区间相加可能抹掉真实收缩 ​

光滑性与爆破 ​

完整推进与可复核输入 ​

计算量按实际表达式计算 ​

反向链接