LemmaStatement: AI-adaptedProof: AI-generatedPipeline-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.

Local defect bound for frozen-slow Euler with fast microsteps

Statement

Let $Ω \subseteq R^{r + s}$ be open, let $r, s \geq 1$ , and let $F = (f, g) : Ω \to R^{r} \times R^{s}$ be continuous. Assume $K, M \geq 0$ , and that $F$ is jointly $K$ -Lipschitz and bounded by $M$ on a common set containing the exact solution $U (t) = (x (t), z (t))$ , $0 \leq t \leq H$ , and every microstate $(x_{0}, z_{j})$ of Frozen-slow explicit Euler with fast microsteps started at $U (0) = (x_{0}, z_{0})$ . Assume the exact path and those microstates lie in the domain where these bounds hold, $H > 0$ , $m \geq 1$ , and $h = H / m$ . Then the successful macro output $(x^{+}, z_{m})$ satisfies $∥ (x^{+}, z_{m}) - U (H) ∥_{2} \leq 4 K M H^{2} .$

Facts & Assumptions

Given: The exact IVP solution, jointly Lipschitz and bounded field, positive macro step, positive integer microstep count, and the common-domain conditions in the Statement.

[F1]

View the autonomous field as $\hat{F} (t, u) : = F (u)$ on $R \times Ω$ . An exact first-order IVP solution then satisfies the componentwise Volterra integral equation on every subinterval (First-order systems, initial value problems, and solutions on intervals, A first-order initial value problem is equivalent to its Volterra integral equation, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[F2]

The vector integral obeys $∥ \int_{a}^{b} V (t) d t ∥_{2} \leq \int_{a}^{b} ∥ V (t) ∥_{2} d t$ (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable).

[F3]

A successful step uses $x^{+} = x_{0} + H f (x_{0}, z_{0})$ and $z_{m} = z_{0} + \sum_{j = 0}^{m - 1} h g (x_{0}, z_{j})$ (Frozen-slow explicit Euler with fast microsteps).

[F4]

Along the exact path, $∥ U (s) - U (0) ∥_{2} \leq M s$ ; for every microstate, $∥ z_{j} - z_{0} ∥_{2} \leq j h M$ (Block variation bounds for a frozen-slow Euler step).

[F5]

A coordinate projection does not increase the Euclidean norm, and $∥ (a, b) ∥_{2} \leq ∥ a ∥_{2} + ∥ b ∥_{2}$ (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[F6]

If an integrable real-valued function $w$ satisfies $0 \leq w \leq C$ on $[a, b]$ , then $\int_{a}^{b} w \leq C (b - a)$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , claim 3).

[F7]

A continuous vector-valued function on a compact interval has continuous components, hence is componentwise integrable (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[A1]

On all points compared below, $∥ F (u) - F (v) ∥_{2} \leq K ∥ u - v ∥_{2}$ and $∥ F (u) ∥_{2} \leq M$ .

Proof

1.1F1F2F3F4F5F6F7A1algebra

By [F1] and [F3], the slow coordinate defect is the integral of the continuous vector-valued integrand $f (x_{0}, z_{0}) - f (x (s), z (s))$ , integrable by [F7]. The projection bound [F5], Lipschitz condition [A1], and [F4] show its pointwise norm is at most $K M H$ . Applying [F2] and [F6] to this integrand gives $∥ x^{+} - x (H) ∥_{2} \leq K M H^{2}$ .

1.2F1F3F4F5F7algebra

By [F1] and [F3], the fast-coordinate defect is the sum over $j$ of integrals of the continuous vector-valued functions $g (x_{0}, z_{j}) - g (x (s), z (s))$ on $[j h, (j + 1) h]$ , integrable by [F7]. For such an $s$ , [F4] gives $∥ x (s) - x_{0} ∥_{2} \leq M s \leq M H$ and $∥ z (s) - z_{j} ∥_{2} \leq ∥ z (s) - z_{0} ∥_{2} + ∥ z_{j} - z_{0} ∥_{2} \leq M s + j h M \leq 2 M H$ . By [F5], the product-state distance is at most the sum of these coordinate distances, hence at most $3 M H$ .

2.1F2F5F6F7A1step 1.2algebra

The projection bound [F5] and [A1] therefore bound each fast integrand norm by $3 K M H$ . Applying [F2] and [F6] on each interval, then summing the $m$ interval norms, gives $∥ z_{m} - z (H) ∥_{2} \leq m h (3 K M H) = 3 K M H^{2}$ .

3.1F5step 1.1step 2.1algebra∎

By [F5], the product output error is at most the sum of the coordinate errors from steps 1.1 and 2.1. Thus it is at most $(1 + 3) K M H^{2} = 4 K M H^{2}$ , as claimed.

Depends on

Used by

Fixed-time first-order error bound for frozen-slow Euler Theorem

Dependency tree · two levels

78 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

Michael Günther and Adrian Sandu, Multirate Methods for Ordinary Differential Equations, CSL-TR-25-5 (2025) (standard reference, not scraped)
Michael Günther, Numerical Analysis and Simulation I — Ordinary Differential Equations, Chapter 4: Multirate Schemes (lecture notes, 2017/18) (standard reference, not scraped)