LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

One-step stability of frozen-slow Euler with fast microsteps

Statement

Let $r, s \geq 1$ , let $Ω \subseteq R^{r + s}$ be open, and let $F = (f, g) : Ω \to R^{r} \times R^{s}$ . Suppose $K \geq 0$ and $F$ is jointly $K$ -Lipschitz in the product Euclidean norm on a set $S \subseteq Ω$ . Fix $T > 0$ and $0 < H \leq T$ , and let $m \geq 1$ , $h = H / m$ . For any two input states $(x, z)$ and $(\overset{ˉ}{x}, \overset{ˉ}{z})$ for which both algorithm runs return success and all inputs and fast microstates lie in $S$ , the outputs of Frozen-slow explicit Euler with fast microsteps satisfy $∥ Ψ_{H, m} (x, z) - Ψ_{H, m} (\overset{ˉ}{x}, \overset{ˉ}{z}) ∥_{2} \leq (1 + L_{T} H) ∥ (x, z) - (\overset{ˉ}{x}, \overset{ˉ}{z}) ∥_{2}, L_{T} : = K \sqrt{2 (1 + \exp (2 K T))} .$ The constant is independent of $m$ .

Facts & Assumptions

Given: The jointly $K$ -Lipschitz fields, the two admissible inputs and their fast microstates, and $0 < H \leq T$ in the Statement.

[F1]

The slow update is $x^{+} = x + H f (x, z)$ and the fast recurrence is $z_{j + 1} = z_{j} + h g (x, z_{j})$ (Frozen-slow explicit Euler with fast microsteps).

[F2]

For $u \geq 0$ , $1 + u \leq \exp (u)$ ; integer powers preserve order on nonnegative inputs; and $\exp (u + v) = \exp (u) \exp (v)$ ( $1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ , Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , Integer powers $a^{m}$ , The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , The real exponential function and the number $e$ by a power series).

[F3]

The exponential is strictly increasing and $\exp^{'} = \exp$ ; the real mean-value theorem therefore bounds its increments on a compact interval (The exponential function is strictly increasing, The exponential function is smooth and $(\exp)^{'} = \exp$ , The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[F4]

The product Euclidean norm is $∥ (x, z) ∥_{2} = (∥ x ∥_{2}^{2} + ∥ z ∥_{2}^{2})^{1 / 2}$ ; Cauchy–Schwarz implies the Frobenius norm bounds the Euclidean operator norm of a real matrix (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[A1]

Every input and microstate used in the two successful executions lies in $S$ , and $∥ F (u) - F (v) ∥_{2} \leq K ∥ u - v ∥_{2}$ for all $u, v \in S$ .

Proof

1.1F1F4A1algebra

Put $d_{x} = ∥ x - \overset{ˉ}{x} ∥_{2}$ and $d_{j} = ∥ z_{j} - {\overset{ˉ}{z}}_{j} ∥_{2}$ . By [F1] and the joint Lipschitz inequality [A1], $∥ x^{+} - {\overset{ˉ}{x}}^{+} ∥_{2} \leq (1 + K H) d_{x} + K H d_{0}$ , and $d_{j + 1} \leq (1 + h K) d_{j} + h K d_{x}$ . The second inequality uses $∥ (x, z_{j}) - (\overset{ˉ}{x}, {\overset{ˉ}{z}}_{j}) ∥_{2} \leq d_{x} + d_{j}$ .

2.1F1F2step 1.1inductionalgebra

Iterating the fast recurrence in step 1.1 gives $d_{m} \leq (1 + h K)^{m} d_{0} + ((1 + h K)^{m} - 1) d_{x}$ when $K > 0$ . For $K = 0$ it gives $d_{m} \leq d_{0}$ , the same formula at $K = 0$ . By [F2], $1 + h K \leq \exp (h K)$ ; raising nonnegative terms to the integer power $m$ and using repeated exponential addition yields $(1 + h K)^{m} \leq \exp (K H)$ . Hence $d_{m} \leq \exp (K H) d_{0} + (\exp (K H) - 1) d_{x}$ .

3.1F2F3step 1.1step 2.1algebra

If $K > 0$ , [F3] applied to $\exp$ on $[0, K H]$ gives $0 \leq η_{H} : = (\exp (K H) - 1) / H \leq K \exp (K T)$ , since its intermediate point $c$ satisfies $0 < c < K H \leq K T$ and $\exp (c) \leq \exp (K T)$ . If $K = 0$ , set $η_{H} = 0$ , and the same bound holds. Put $d = (d_{x}, d_{0})^{T}$ and $d^{+} : = (∥ x^{+} - {\overset{ˉ}{x}}^{+} ∥_{2}, ∥ z_{m} - {\overset{ˉ}{z}}_{m} ∥_{2})^{T}$ . Steps 1.1–2.1 give $d^{+} \leq (I + H B_{H}) d$ componentwise, where $B_{H} : = (\begin{array}{cc} K & K \\ η_{H} & η_{H} \end{array}), ∥ B_{H} ∥_{F} \leq \sqrt{2 K^{2} + 2 K^{2} \exp (2 K T)} = L_{T} .$

4.1F4step 3.1algebra∎

All entries of $I + H B_{H}$ are nonnegative, so componentwise domination implies $∥ d^{+} ∥_{2} \leq ∥ (I + H B_{H}) d ∥_{2}$ . By [F4], $∥ (I + H B_{H}) d ∥_{2} \leq ∥ d ∥_{2} + H ∥ B_{H} ∥_{F} ∥ d ∥_{2} \leq (1 + L_{T} H) ∥ d ∥_{2}$ . Under the product norm, $∥ d ∥_{2} = ∥ (x, z) - (\overset{ˉ}{x}, \overset{ˉ}{z}) ∥_{2}$ and $∥ d^{+} ∥_{2}$ is the output difference, proving the claim.

Depends on

Used by

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

Dependency tree · two levels

64 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)