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

Explicit Euler gives a second-order local backward-foot defect

Statement

Let $b \in C^{1} ([0, T] \times R^{d}; R^{d})$ be periodic in space, and set $M : = \sup ∥ b ∥_{2}, L_{x} : = \sup ∥ D_{x} b ∥, L_{t} : = \sup ∥ \partial_{t} b ∥_{2},$ where the suprema are over one full periodic time-space cylinder. For $0 \leq t_{n} < t_{n + 1} \leq T$ , $Δ t = t_{n + 1} - t_{n}$ , and an arrival lift $x$ , let $X (t_{n}; t_{n + 1}, x)$ be the exact backward characteristic foot. The explicit Euler foot $x - Δ t b (t_{n + 1}, x)$ satisfies $∥ X (t_{n}; t_{n + 1}, x) - (x - Δ t b (t_{n + 1}, x)) ∥_{2} \leq \frac{1}{2} (L_{x} M + L_{t}) (Δ t)^{2} .$ The estimate is local for every positive $Δ t$ ; it requires no relation between displacement and grid width.

Facts & Assumptions

Given: The periodic $C^{1}$ field, its finite derivative bounds, a time interval $[t_{n}, t_{n + 1}]$ , and an arrival point $x$ .

[F1]

Explicit Euler characteristic backtracking with multilinear interpolation: the algorithm uses the lifted explicit backward foot $x - Δ t b (t_{n + 1}, x)$ .

[F2]

A periodic C1 velocity has a global characteristic flow on a finite horizon: the exact characteristic exists on the whole interval, and $∥ b ∥_{2} \leq M$ on its periodic tube.

[F3]

A first-order initial value problem is equivalent to its Volterra integral equation: the exact characteristic increment is the oriented integral of $b (s, X (s))$ .

[F4]

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: the norm of a vector integral is at most the integral of its norm.

Proof

1.1givenF2F3F4

By [F2] and [F3], for $s \in [t_{n}, t_{n + 1}]$ the backward characteristic satisfies $X (s) = x - \int_{s}^{t_{n + 1}} b (r, X (r)) d r$ . Applying [F4] and the velocity bound gives $∥ X (s) - x ∥_{2} \leq M (t_{n + 1} - s)$ .

2.1givenF1F3F4step 1.1algebra∎

Subtracting the explicit Euler foot from the exact foot and using [F3] writes the difference as the integral from t_n to t_{n+1} of b(t_{n+1},x)-b(s,X(s)). The derivative bounds make its integrand norm at most L_x times the state difference plus L_t times (t_{n+1}-s); by step 1.1 the state difference is at most M(t_{n+1}-s). Integrating the resulting bound (L_x M+L_t)(t_{n+1}-s) gives one half (L_x M+L_t)(Delta t)^2.

Depends on

Used by

Periodic semi-Lagrangian error is controlled by local foot and interpolation defects Theorem

Dependency tree · two levels

37 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

European Centre for Medium-Range Weather Forecasts, Numerical Methods, Meteorological Training Course Lecture Series, 2002 (standard reference, not scraped)
Lukas Einkemmer and Alexander Ostermann, On the error propagation of semi-Lagrange and Fourier methods for advection problems, Computers & Mathematics with Applications 69 (2015), 170–179 (standard reference, not scraped)