LemmaStatement: Literature-sourcedProof: 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.

Lie and Strang splitting errors have commutator expansions

Statement

Let $a, b \in C^{3} (U, R^{d})$ on an open set and let $K_{0} \subset K \subset U$ , where $K_{0}$ is compact and $K$ is compact and convex. Assume the exact $a$ - and $b$ -subflows, their Lie and Strang compositions, and the exact flow $Φ_{a + b}^{h}$ from $K_{0}$ are defined and remain in $K$ for all sufficiently small $h > 0$ , and the fields and derivatives through order three are bounded on $K$ . Uniformly for $y \in K_{0}$ , $L_{h} (y) - Φ_{a + b}^{h} (y) = \frac{h^{2}}{2} [a, b] (y) + O (h^{3}),$ and the Strang expansion, pointwise in $y$ , is $S_{h} (y) - Φ_{a + b}^{h} (y) = - \frac{h^{3}}{24} [a, [a, b]] (y) - \frac{h^{3}}{12} [b, [a, b]] (y) + o (h^{3}) .$ The Strang defect is also uniformly $O (h^{3})$ on $K_{0}$ . The maps and bracket use Lie and Strang compositions of exact split flows; the claim is finite-dimensional.

Facts & Assumptions

Given: The fields, exact subflows, compact tube, and bounded derivatives in the Statement.

[F1]

Lie and Strang compositions of exact split flows: $L_{h} = Φ_{b}^{h} \circ Φ_{a}^{h}$ , $S_{h} = Φ_{a}^{h / 2} \circ Φ_{b}^{h} \circ Φ_{a}^{h / 2}$ , and $[a, b] = D b a - D a b$ .

[F2]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : differentiating a composition gives $D (g \circ f) = D g (f) \circ D f$ .

[F3]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : an integrable derivative satisfies $\int_{α}^{β} g^{'} = g (β) - g (α)$ .

[F4]

Continuous mixed partials of order $k$ are invariant under permutations: for a $C^{2}$ scalar function, the two Hessian arguments are symmetric.

[A1]

Each flow is defined on the stated tube, and its time derivatives through order three are bounded there; these follow from the $C^{3}$ fields and the compact-tube hypotheses.

Proof

1.1A1F2F3algebra

For a $C^{3}$ field $c$ and a smooth scalar coordinate function $q (y) = y_{j}$ , define $L_{c} q : = D q c$ . By [F2], differentiating $q (Φ_{c}^{t} (y))$ successively in $t$ gives $L_{c} q$ , $L_{c}^{2} q$ , and $L_{c}^{3} q$ , evaluated along the flow. Three uses of [F3] give the expansion through degree two with integral remainder $\frac{1}{2} \int_{0}^{h} (h - s)^{2} (L_{c}^{3} q) (Φ_{c}^{s} (y)) d s$ ; [A1] bounds this remainder uniformly by $C h^{3}$ and continuity at $s = 0$ gives cubic coefficient $\frac{1}{6} L_{c}^{3} q (y)$ with pointwise remainder $o (h^{3})$ . The same reasoning applies successively to the finite flow compositions.

2.1F1step 1.1algebra

For a map $M$ , define its pullback by $M^{*} q : = q \circ M$ , and for a vector field $c$ put $L_{c} q : = D q c$ . Set $X = L_{a}$ and $Y = L_{b}$ . The pullback of a composition reverses composition order, so [F1] and step 1.1 give, through degree two, $L_{h}^{*} q = q + h (X + Y) q + h^{2} (\frac{1}{2} X^{2} + X Y + \frac{1}{2} Y^{2}) q + O (h^{3}) .$ The exact total-flow pullback is $q + h (X + Y) q + \frac{1}{2} h^{2} (X + Y)^{2} q + O (h^{3})$ . Subtracting leaves $\frac{1}{2} h^{2} (X Y - Y X) q + O (h^{3})$ .

3.1F1F4step 2.1algebra

For any $C^{2}$ scalar $q$ , the chain rule gives $[L_{a}, L_{b}] q = D^{2} q (a, b) + D q D b a - D^{2} q (b, a) - D q D a b = D q (D b a - D a b),$ where [F4] cancels the Hessian terms. Thus $[X, Y] q = L_{[a, b]} q$ . Applying this to each coordinate function in step 2.1 gives the stated Lie map expansion.

3.2F1step 1.1step 2.1algebra

Pullback reversal and [F1] give $S_{h}^{*} = Φ_{a}^{h / 2 *} Φ_{b}^{h *} Φ_{a}^{h / 2 *}$ . Expanding its three factors by step 1.1 gives the cubic part $\frac{1}{6} X^{3} + \frac{1}{6} Y^{3} + \frac{1}{8} X^{2} Y + \frac{1}{4} X Y X + \frac{1}{8} Y X^{2} + \frac{1}{4} X Y^{2} + \frac{1}{4} Y^{2} X .$ Multiplying the three degree-three Taylor polynomials gives these coefficients: the $X^{3}$ term is $1 / 48 + 1 / 48 + 1 / 16 + 1 / 16 = 1 / 6$ , and the $Y^{3}$ term is $1 / 6$ . The mixed coefficients are $X^{2} Y : (1 / 8) (1) = 1 / 8$ , $X Y X : (1 / 2) (1) (1 / 2) = 1 / 4$ , $Y X^{2} : (1) (1 / 8) = 1 / 8$ , $X Y^{2} : (1 / 2) (1 / 2) = 1 / 4$ , and $Y^{2} X : (1 / 2) (1 / 2) = 1 / 4$ ; $Y X Y$ is absent because neither outer factor contains $Y$ . The exact total-flow cubic part is $\frac{1}{6} (X + Y)^{3}$ , whose eight words each have coefficient $1 / 6$ . Degrees zero through two agree, so subtraction gives $- \frac{1}{24} (X^{2} Y - 2 X Y X + Y X^{2}) - \frac{1}{12} (2 Y X Y - Y^{2} X - X Y^{2}) + o (h^{3}) .$

4.1F1step 1.1step 3.1step 3.2algebra∎

Step 3.1 also applies with the second field equal to $[a, b]$ , which is $C^{2}$ under the $C^{3}$ hypotheses. Hence $[X, [X, Y]] = L_{[a, [a, b]]}$ and $[Y, [X, Y]] = L_{[b, [a, b]]}$ . Applying step 3.2 to each coordinate yields the stated Strang coefficient and pointwise $o (h^{3})$ remainder. The uniform $O (h^{3})$ defect follows already from the uniform degree-two remainder in step 1.1 and the equality of all coefficients through degree two.

Depends on

Used by

Dependency tree · two levels

25 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

Ernst Hairer, Geometric Numerical Integration, Lecture 2: Symplectic Integrators (standard reference, not scraped)
Gilbert Strang, On the Construction and Comparison of Difference Schemes (standard reference, not scraped)