TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Rosenbrock–Euler has a first-order global error bound on a common tube

Statement

Let $f : D \to R^{d}$ be $C^{2}$ on an open time-state domain, and let $y (t)$ be an exact solution on $[t_{0}, t_{0} + T]$ . Fix $γ > 0$ and a compact convex tube $Q \subset D$ containing the solution, all numerical states, and all state segments used below. Assume the bounds of Rosenbrock–Euler has an explicit one-step defect and solve-residual allowance hold uniformly on $Q$ : $F, L, M_{1}$ , an exact-J inverse bound $κ_{0}$ , an approximate-J inverse bound $κ_{1}$ , and $∥ \tilde{J} - D_{y} f ∥_{2} \leq δ$ . Assume $∥ \tilde{J} (t, u) - \tilde{J} (t, v) ∥_{2} \leq L_{J} ∥ u - v ∥_{2}$ on each state slice of $Q$ , and $∥ (I - γ h \tilde{J} (t, y))^{- 1} ∥_{2} \leq κ_{1}$ for all $0 < h \leq h_{0}$ and all relevant $(t, y) \in Q$ . Fix the step size used below with $0 < h \leq h_{0}$ .

At each step $t_{n} = t_{0} + n h$ , use the one-stage algorithm of Finite-precision one-stage Rosenbrock step with residual status with a certified stage residual upper bound $ρ_{n} \leq R h$ , for a fixed $R \geq 0$ , and assume each call returns success, including its field evaluation, factorization, residual certification, and exact-storage checks. Starting from $y_{0} = y (t_{0})$ , suppose the computed states and comparison segments remain in $Q$ and $N h \leq T$ . Then, with $C_{E} = γ κ_{0} L F + \frac{M_{1}}{2} + γ κ_{0} κ_{1} δ F, C_{s} = κ_{1} L + γ κ_{1}^{2} L_{J} F h_{0} .$ the global error obeys

∥ y_{n} - y (t_{n}) ∥_{2} \leq (C_{E} + κ_{1} R) T e^{C_{s} T} h (0 \leq n \leq N) .

Thus the method is first order on this common tube when the linear solve residuals are $O (h)$ . The theorem is conditional on the stated tube and inverse bounds; it does not prove that computed states stay in the tube.

Facts & Assumptions

Given: The exact solution, common tube, derivative and inverse bounds, Lipschitz Jacobian approximation, residual bounds, and exact starting value in the Statement.

[F1]

Finite-precision one-stage Rosenbrock step with residual status: the stage system is $A (t, y) k = f (t, y)$ with $A (t, y) = I - γ h \tilde{J} (t, y)$ and output $y + h k$ .

[F2]

Rosenbrock–Euler has an explicit one-step defect and solve-residual allowance: at an exact state, the step defect is at most $C_{E} h^{2} + κ_{1} h ρ$ .

[F3]

Perturbing a shifted Jacobian perturbs its inverse explicitly: for two invertible shifted matrices, the inverse difference is bounded by $γ h$ times the two inverse norms and the Jacobian difference.

[F4]

Induced matrix norms are compatible with matrix-vector multiplication, submultiplicative, and satisfy ||I|| = 1: the induced Euclidean matrix norm bounds matrix action on vectors.

[F5]

If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz: a derivative bound on a convex segment gives the corresponding Lipschitz bound between its endpoints.

[F6]

$1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ : $1 + x \leq e^{x}$ for $x \geq 0$ .

[F7]

A computed shifted-system residual has a certified upper bound: a successful stage solve supplies a certified upper bound $ρ_{n}$ for the exact residual vector norm.

[F8]

If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative: the componentwise $C^{2}$ assumption makes $f$ totally differentiable at each point of $Q$ .

[F9]

A total derivative computes every directional derivative, and its matrix is the Jacobian: in the joint variable $(t, y)$ , the nonzero standard time and state basis directions identify the derivative blocks with $f_{t}$ and $D_{y} f$ .

[F10]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : composing $f$ with a differentiable segment gives derivative $D f$ applied to the segment direction.

Proof

Given: The data in the Statement.

1.1givenF1F4F5F8F9F10algebra

Fix $t$ and $u, v$ in the state slice of $Q$ , and set $x (s) = u + s (v - u)$ for $0 \leq s \leq 1$ . By [F8], [F10], and [F9], the curve $s \mapsto f (t, x (s))$ has derivative $D_{y} f (t, x (s)) (v - u)$ , whose norm is at most $L ∥ u - v ∥_{2}$ ; [F5] therefore gives $∥ f (t, u) - f (t, v) ∥_{2} \leq L ∥ u - v ∥_{2}$ . From [F1], subtract the two exact stage maps and add and subtract $A (t, u)^{- 1} f (t, v)$ . The triangle inequality and [F4] now give $∥ Φ (t, u) - Φ (t, v) ∥_{2} \leq ∥ u - v ∥_{2} + h κ_{1} L ∥ u - v ∥_{2} + h F ∥ A (t, u)^{- 1} - A (t, v)^{- 1} ∥_{2}$ .

1.2givenF1F4F7algebra

At the numerical input $y_{n}$ , let $k_{n}$ be the exact solution of the shifted stage equation, let ${\hat{k}}_{n}$ be the computed stage, and define $r_{n} = A (t_{n}, y_{n}) {\hat{k}}_{n} - f (t_{n}, y_{n})$ . Then ${\hat{k}}_{n} - k_{n} = A (t_{n}, y_{n})^{- 1} r_{n}$ , so [F4] and [F7] bound the output perturbation by $κ_{1} h ρ_{n} \leq κ_{1} R h^{2}$ .

2.1givenF3step 1.1algebra

The shifted matrices use the same $γ h$ . Their Jacobian difference is at most $L_{J} ∥ u - v ∥_{2}$ . Apply [F3] and both inverse bounds to get $∥ A (t, u)^{- 1} - A (t, v)^{- 1} ∥_{2} \leq γ h κ_{1}^{2} L_{J} ∥ u - v ∥_{2}$ . Since $h \leq h_{0}$ , step 1.1 implies $∥ Φ (t, u) - Φ (t, v) ∥_{2} \leq (1 + C_{s} h) ∥ u - v ∥_{2}$ .

3.1givenF1step 2.1algebra

Let $e_{n} = ∥ y_{n} - y (t_{n}) ∥_{2}$ . Insert $Φ (t_{n}, y_{n})$ and $Φ (t_{n}, y (t_{n}))$ between the computed value and exact solution value. Step 2.1 bounds the middle map difference by $(1 + C_{s} h) e_{n}$ .

4.1givenF2F8F9step 1.2step 3.1algebra

At the exact state $y (t_{n})$ , [F2] with zero stage residual bounds the exact map's local defect by $C_{E} h^{2}$ ; the componentwise $C^{2}$ premise in [F2] supplies the required total differentiability by [F8], and [F9] identifies its time and state derivative blocks. Combining this with steps 1.2 and 3.1 gives $e_{n + 1} \leq (1 + C_{s} h) e_{n} + (C_{E} + κ_{1} R) h^{2}$ .

5.1step 4.1givenF6algebra∎

Iterating step 4.1 from $e_{0} = 0$ gives $e_{n} \leq (C_{E} + κ_{1} R) h^{2} \sum_{j = 0}^{n - 1} (1 + C_{s} h)^{j}$ . Each summand is at most $e^{C_{s} n h} \leq e^{C_{s} T}$ by [F6]; also $n \leq T / h$ . Hence $e_{n} \leq (C_{E} + κ_{1} R) T e^{C_{s} T} h$ , as claimed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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

WIAS Berlin, Numerical Methods for Stiff Ordinary Differential Equations, §2.4 Rosenbrock Methods (standard reference, not scraped)
Daniel Kressner, Advanced Numerical Analysis, §3.5 Rosenbrock methods (standard reference, not scraped)