TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Variable-step BDF2 is second-order convergent under a uniform ratio bound

Statement

Let $y^{'} = f (t, y)$ on $[0, T]$ , with $y : [0, T] \to R^{d}$ having three continuous derivatives. Let $K \subset R^{d}$ be compact with $y ([0, T]) \subset int K$ , and suppose $f$ is defined on $[0, T] \times K$ and Lipschitz in its state variable there with constant $L$ in the max norm. Let $h_{n} = t_{n + 1} - t_{n} > 0$ , $t_{0} = 0$ , $t_{N} = T$ , $H = \max_{n} h_{n} \to 0$ , and suppose

$0 < r_{\min} \leq r_{n} : = \frac{h_{n}}{h_{n - 1}} \leq r_{*} < 1 + \sqrt{2} (1 \leq n < N) .$

Assume $∥ Y_{0} - y (t_{0}) ∥_{\infty} + ∥ Y_{1} - y (t_{1}) ∥_{\infty} = O (H^{2})$ . For each step prescribe a closed branch ball $B_{n + 1} \subset K$ as in Variable-step BDF2 with an explicit local implicit-branch rule. Assume there are radii $η, ε > 0$ , independent of the grid and step index, such that for every sufficiently small $H$ and each $1 \leq n < N$ , whenever

$\max {∥ Y_{n} - y (t_{n}) ∥_{\infty}, ∥ Y_{n - 1} - y (t_{n - 1}) ∥_{\infty}} \leq η,$

the step equation has exactly one root in $\overline{B} (y (t_{n + 1}), ε) \subset K$ , and $B_{n + 1}$ contains exactly one root, which is this same local root selected by the algorithm. Then for sufficiently small $H$ all computed states remain in $K$ and

$\max_{0 \leq n \leq N} ∥ Y_{n} - y (t_{n}) ∥_{\infty} = O (H^{2}) .$

The lower ratio bound controls the local residual constant; the upper bound controls the parasitic increment. This is a separate variable-grid theorem and does not follow from the constant-step root condition alone.

Facts & Assumptions

Given: A solution in the sense of First-order systems, initial value problems, and solutions on intervals, a grid, the variable-step BDF2 recurrence, and the ratio, smoothness, Lipschitz, starter, tube, and branch hypotheses in the statement.

[F1]

Variable-step BDF2 with an explicit local implicit-branch rule defines the step equation and specifies that the unique root in the prescribed ball is the output.

[F2]

Quadratic interpolation gives the variable-step BDF2 formula and cubic residual gives the exact BDF2 coefficients and bounds the exact unscaled residual by $C h_{n}^{3}$ when adjacent ratios stay in a compact subinterval of $(0, \infty)$ .

[F3]

The variable-step BDF2 parasitic increment contracts below the sharp ratio threshold gives $q (r_{n}) = r_{n}^{2} / (1 + 2 r_{n}) \leq q_{*} < 1$ under the stated upper ratio bound.

[F4]

$1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ gives $1 + x \leq \exp (x)$ , and The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ gives $\exp (x + y) = \exp (x) \exp (y)$ .

[A1]

For every $t \in [0, T]$ and $u, v \in K$ , $∥ f (t, u) - f (t, v) ∥_{\infty} \leq L ∥ u - v ∥_{\infty}$ .

[A2]

There are fixed radii $η, ε > 0$ such that, for each sufficiently small grid and every step, each preceding pair within $η$ of its exact history gives exactly one root in $\overline{B} (y (t_{n + 1}), ε) \subset K$ ; the prescribed ball $B_{n + 1}$ also contains exactly one root, and it is this local root.

Proof

1.1F1F2algebra

Put $e_{n} = Y_{n} - y (t_{n})$ and $d_{n} = e_{n} - e_{n - 1}$ . Subtracting the exact residual in [F2] from the numerical equation in [F1], then using the BDF2 coefficients, gives $(1 + 2 r_{n}) d_{n + 1} - r_{n}^{2} d_{n} = h_{n} (1 + r_{n}) (f (t_{n + 1}, Y_{n + 1}) - f (t_{n + 1}, y (t_{n + 1}))) - τ_{n}$ .

2.1A1F2F3step 1.1algebra

Divide by $1 + 2 r_{n}$ and use [F3], [A1], $∥ e_{n + 1} ∥_{\infty} \leq ∥ e_{n} ∥_{\infty} + ∥ d_{n + 1} ∥_{\infty}$ , $(1 + r_{n}) / (1 + 2 r_{n}) \leq 1$ , and $1 + 2 r_{n} \geq 1$ . This gives $∥ d_{n + 1} ∥_{\infty} \leq q_{*} ∥ d_{n} ∥_{\infty} + L h_{n} (∥ e_{n} ∥_{\infty} + ∥ d_{n + 1} ∥_{\infty}) + C h_{n}^{3}$ . Move the last increment term left; since $L h_{n} \leq 1 / 2$ , $(1 - L h_{n})^{- 1} \leq 1 + 2 L h_{n}$ and $(1 - L h_{n})^{- 1} \leq 2$ . Using $∥ τ_{n} ∥_{\infty} \leq C h_{n}^{3}$ from [F2] yields $∥ d_{n + 1} ∥_{\infty} \leq (q_{*} + 2 L q_{*} h_{n}) ∥ d_{n} ∥_{\infty} + 2 L h_{n} ∥ e_{n} ∥_{\infty} + 2 C h_{n}^{3}$ .

3.1step 2.1constructalgebra

Choose $A > \max {1, q_{*} / (1 - q_{*})}$ , so $(1 + A) q_{*} < A$ , and set $E_{n} = ∥ e_{n} ∥_{\infty} + A ∥ d_{n} ∥_{\infty}$ . For sufficiently small $H$ , $(1 + A) (q_{*} + 2 L q_{*} H) \leq A$ . Using $e_{n + 1} = e_{n} + d_{n + 1}$ in step 2.1 gives a coefficient at most $1 + 2 L (1 + A) h_{n}$ on $∥ e_{n} ∥_{\infty}$ and at most $A$ on $∥ d_{n} ∥_{\infty}$ ; hence $E_{n + 1} \leq (1 + C_{1} h_{n}) E_{n} + C_{2} h_{n}^{3}$ for constants independent of the grid.

4.1A2F4step 3.1algebra∎

The starter hypothesis gives $E_{1} = O (H^{2})$ . Iterate step 3.1 only while the preceding pair is in the local neighborhood of [A2]. The coefficients $C_{1} = 2 L (1 + A)$ and $C_{2}$ in step 3.1 can be taken nonnegative. For every subproduct, [F4] gives $\prod_{j = r}^{s} (1 + C_{1} h_{j}) \leq \prod_{j = r}^{s} \exp (C_{1} h_{j}) = \exp (C_{1} \sum_{j = r}^{s} h_{j}) \leq e^{C_{1} T}$ : the unused time $T - \sum_{j = r}^{s} h_{j}$ is nonnegative, and [F4] gives $\exp (C_{1} (T - \sum_{j = r}^{s} h_{j})) \geq 1$ , which with the addition law proves the last comparison. Expanding the finite recurrence by induction therefore gives $E_{n} \leq e^{C_{1} T} (E_{1} + C_{2} \sum_{j = 1}^{n - 1} h_{j}^{3})$ ; here $\sum_{j} h_{j}^{3} \leq H^{2} \sum_{j} h_{j} \leq T H^{2}$ . These bounds give $\max_{n} E_{n} \leq C H^{2}$ up to any first exit, with $C$ independent of the grid. Since $A \geq 1$ , $∥ e_{n} ∥_{\infty} \leq E_{n}$ and $∥ e_{n - 1} ∥_{\infty} \leq ∥ e_{n} ∥_{\infty} + ∥ d_{n} ∥_{\infty} \leq (1 + 1 / A) E_{n}$ . For sufficiently small $H$ , this bound is strictly below $η$ , so no first exit occurs. At each step [A2] therefore supplies the selected root in $K$ , and induction continues through $N$ . Finally $∥ e_{n} ∥_{\infty} \leq E_{n}$ proves the claimed maximum error.

Depends on

Used by

Dependency tree · two levels

26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

G. Söderlind, I. Fekete, and I. Faragó, On the zero-stability of multistep methods on smooth nonuniform grids, §4 (standard reference, not scraped)
Ernst Hairer, Syvert P. Nørsett, and Gerhard Wanner, Solving Ordinary Differential Equations I: Nonstiff Problems, 2nd ed., Chapter III.5, Stability and Convergence, pp. 402–409 (standard reference, not scraped)