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

Global divergence-integral error separates state and quadrature error

Statement

Let $T > 0$ , $N \in N$ with $N \geq 1$ , $h = T / N > 0$ , and $t_{n} = n h$ . Let $K \subseteq R^{d}$ be compact, let $x : [0, T] \to K$ be an exact path, and suppose every numerical state $x_{n}$ also belongs to $K$ . Let $q : [0, T] \times K \to R$ be a continuous scalar integrand. Define $I_{n} : = \int_{t_{n}}^{t_{n + 1}} q (s, x (s)) d s, ℓ_{n} : = ℓ_{0} + \sum_{j = 0}^{n - 1} I_{j} .$ Suppose the one-step state method satisfies the hypotheses of Global error from uniform one-step defect and stability at its positive integer order $p$ , and write $K_{x}$ for its resulting constant, so $\max_{n} ∥ x_{n} - x (t_{n}) ∥_{2} \leq K_{x} h^{p}$ . Let $Q_{h} (t_{n}, \cdot) : K \to R$ be the increment map in the numerical scalar update ${\hat{ℓ}}_{n + 1} = {\hat{ℓ}}_{n} + Q_{h} (t_{n}, x_{n})$ , with $∣ {\hat{ℓ}}_{0} - ℓ_{0} ∣ \leq C_{ℓ, 0} h^{r}$ for $r \in R$ with $r \geq 0$ , using the real powers of Real powers for positive bases, with the zero-base positive-exponent convention. If constants $K_{q}, D \geq 0$ and an integer $m \geq 1$ satisfy, uniformly for $n < N$ and $u, v \in K$ , $∣ Q_{h} (t_{n}, u) - Q_{h} (t_{n}, v) ∣ \leq h K_{q} ∥ u - v ∥_{2}, ∣ Q_{h} (t_{n}, x (t_{n})) - I_{n} ∣ \leq D h^{m + 1},$ then $\max_{0 \leq n \leq N} ∣ {\hat{ℓ}}_{n} - ℓ_{n} ∣ \leq C_{ℓ, 0} h^{r} + T K_{q} K_{x} h^{p} + D T h^{m} .$

Facts & Assumptions

Given: The exact path, continuous integrand, numerical state and scalar updates, and the uniform state-solver, sensitivity, and quadrature-defect hypotheses in the Statement.

[F1]

Under the full hypotheses of Global error from uniform one-step defect and stability, the state method has a fixed-time bound $K_{x} h^{p}$ with the explicit $L > 0$ and $L = 0$ constants. These hypotheses require a common compact time-state tube with positive margin in the open ODE domain, containing the entire exact path, all numerical grid states, and every method stage; the one-step map is defined on each grid-time fiber, with local-defect bound $C h^{p + 1}$ , fiberwise stability factor $1 + L h$ , and initial error bound $C_{0} h^{p}$ , for constants independent of $N$ and $n$ .

[A1]

For each step, the scalar update is Lipschitz in its starting state with constant $h K_{q}$ and has exact-start quadrature defect at most $D h^{m + 1}$ ; the initial scalar error is at most $C_{ℓ, 0} h^{r}$ .

[F3]

For $h > 0$ and $r \in R$ , $h^{r}$ is the real power defined by $h^{r} = \exp (r \log h)$ (Real powers for positive bases, with the zero-base positive-exponent convention).

Proof

1.1F1A1algebra

Let $e_{n} : = ∣ {\hat{ℓ}}_{n} - ℓ_{n} ∣$ . By [F1], $∥ x_{n} - x (t_{n}) ∥_{2} \leq K_{x} h^{p}$ . The exact and numerical scalar updates, the triangle inequality, and [A1] give $e_{n + 1} \leq e_{n} + ∣ Q_{h} (t_{n}, x_{n}) - Q_{h} (t_{n}, x (t_{n})) ∣ + ∣ Q_{h} (t_{n}, x (t_{n})) - I_{n} ∣ \leq e_{n} + h K_{q} K_{x} h^{p} + D h^{m + 1}$ .

2.1A1F3step 1.1algebra∎

Iterating the recurrence from step 1.1 for $n$ steps yields $e_{n} \leq e_{0} + n (h K_{q} K_{x} h^{p} + D h^{m + 1})$ . Since $n \leq N = T / h$ and $e_{0} \leq C_{ℓ, 0} h^{r}$ , this is at most $C_{ℓ, 0} h^{r} + T K_{q} K_{x} h^{p} + D T h^{m}$ . Taking the maximum proves the claim.

Remarks

For a continuous normalizing flow, $q (t, x) = - {div}_{x} f (t, x)$ . This theorem bounds that divergence integral without identifying it as a probability log density; the separate identification is proved in A continuous flow changes log density by minus its divergence. The bound makes a higher-order state solver insufficient by itself: the chosen divergence quadrature must also have the required order $m$ and state sensitivity bound.

Depends on

Used by

Global continuous-flow log-density error from state and quadrature bounds Corollary

Dependency tree · two levels

9 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 and Gerhard Wanner, Introduction à l’Analyse Numérique, Chapter III: Équations Différentielles Ordinaires (standard reference, not scraped)
Mark Embree, Lecture Notes on Numerical Analysis (standard reference, not scraped)