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

Euler global state and log-density error on a bounded C² tube

Statement

Assume Countable Choice and the flow-density hypotheses of A continuous flow changes log density by minus its divergence. Let $T > 0$ , $h = T / N$ , $N \geq 1$ , and $t_{n} = n h$ . Let $K \subset R^{d}$ be compact and convex, and let $U \subset R^{1 + d}$ be a bounded convex open subset of the ODE domain containing $[0, T] \times K$ . Suppose $f \in C^{2} (U, R^{d})$ , all partial derivatives of $f$ through order two are bounded on $U$ , and the exact path and every Euler node lie in $K$ . Thus $[0, T] \times K$ is a compact tube with positive margin inside $U$ . Put $q (t, x) : = - {div}_{x} f (t, x)$ and define $B_{f} : = \sup_{U} ∥ f ∥_{2}, L_{f} : = \sup_{U} ∥ D_{x} f ∥, M_{f} : = \sup_{U} ∥ \partial_{t} f ∥_{2}, L_{q} : = \sup_{U} ∥ D_{x} q ∥, M_{q} : = \sup_{U} ∣ \partial_{t} q ∣,$ where matrix and linear-functional norms are induced by Euclidean norms. These constants are finite by the hypotheses. Apply forward Euler to the state and to the continuous-flow log-density equation: $x_{n + 1} = x_{n} + h f (t_{n}, x_{n}), {\hat{ℓ}}_{n + 1} = {\hat{ℓ}}_{n} + h q (t_{n}, x_{n}) .$ If $∥ x_{0} - x (0) ∥_{2} \leq C_{x, 0} h$ and $∣ {\hat{ℓ}}_{0} - \log p_{0} (x (0)) ∣ \leq C_{ℓ, 0} h$ , define $C_{x} : = \frac{M_{f} + L_{f} B_{f}}{2}, D_{q} : = \frac{M_{q} + L_{q} B_{f}}{2},$ and $K_{x} : = {\begin{cases} C_{x, 0} \exp (L_{f} T) + C_{x} \frac{\exp (L_{f} T) - 1}{L_{f}}, & L_{f} > 0, \\ C_{x, 0} + C_{x} T, & L_{f} = 0. \end{cases}$ Then, for every $0 \leq n \leq N$ , $∥ x_{n} - x (t_{n}) ∥_{2} \leq K_{x} h,$ and $∣ {\hat{ℓ}}_{n} - \log p_{t_{n}} (x (t_{n})) ∣ \leq (C_{ℓ, 0} + T L_{q} K_{x} + D_{q} T) h .$ This is a first-order Euler result; it asserts no adjoint-gradient error bound.

Facts & Assumptions

Given: Countable Choice, a positive initial density and C¹ diffeomorphic flow, $f \in C^{2}$ with the stated bounded derivatives on a common convex tube, and the displayed Euler state and scalar updates.

[A1]

The state and log-density initial errors are at most $C_{x, 0} h$ and $C_{ℓ, 0} h$ , respectively; exact, numerical, and local flow segments stay in the stated tube.

[A2]

Countable Choice is used only to identify the continuous flow's pushforward density (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

A solution of $x^{'} = f (t, x)$ satisfies $x (t) = x (t_{0}) + \int_{t_{0}}^{t} f (s, x (s)) d s$ (A first-order initial value problem is equivalent to its Volterra integral equation).

[F2]

The derivative of a composite is the composite of the derivatives (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F3]

On a convex open set, a uniform derivative bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies a Lipschitz bound $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ (On a convex open set, a uniform bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ ).

[F4]

A differentiable vector-valued curve with derivative norm bounded by $M$ is Lipschitz with constant $M$ ; for an integrable vector function, $∥ \int g ∥_{2} \leq \int ∥ g ∥_{2}$ (If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz, 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).

[F5]

A uniform one-step defect $C h^{p + 1}$ and stability factor $1 + L h$ give the stated fixed-time global error bound, including the $L = 0$ case (Global error from uniform one-step defect and stability).

[F6]

If the divergence update has state sensitivity $h K_{q}$ and local quadrature defect $D h^{m + 1}$ , then its global error is the sum of the initial, state, and quadrature contributions (Global continuous-flow log-density error from state and quadrature bounds).

[F7]

$\exp$ is the real exponential defined by its factorial power series, with $e : = \exp (1)$ (The real exponential function and the number $e$ by a power series).

Proof

1.1A1F3algebra

For fixed $t_{n}$ , the open convex fiber $U_{t_{n}}$ contains $K$ . Applying [F3] there gives $∥ f (t_{n}, u) - f (t_{n}, v) ∥_{2} \leq L_{f} ∥ u - v ∥_{2}$ for $u, v \in K$ . Hence the Euler state map satisfies $∥ u + h f (t_{n}, u) - v - h f (t_{n}, v) ∥_{2} \leq (1 + L_{f} h) ∥ u - v ∥_{2}$ .

1.2A1F1F2F4algebra

Let $r (s) : = f (t_{n} + s, x (t_{n} + s))$ for $0 \leq s \leq h$ . By [F2], $r^{'} (s) = \partial_{t} f (t_{n} + s, x (t_{n} + s)) + D_{x} f (t_{n} + s, x (t_{n} + s)) f (t_{n} + s, x (t_{n} + s))$ , whose norm is at most $M_{f} + L_{f} B_{f}$ . By [F4], $∥ r (s) - r (0) ∥_{2} \leq (M_{f} + L_{f} B_{f}) s$ . Using [F1] and the integral norm bound in [F4], the exact-start Euler defect is ${∥ x (t_{n + 1}) - x (t_{n}) - h f (t_{n}, x (t_{n})) ∥}_{2} = {∥ \int_{0}^{h} (r (s) - r (0)) d s ∥}_{2} \leq C_{x} h^{2}$ .

1.3A1F2F3F4algebra

Since $f \in C^{2} (U)$ , $q = - {div}_{x} f$ is $C^{1}$ on $U$ . The open convex fiber $U_{t_{n}}$ contains $K$ , so [F3] gives $∣ h q (t_{n}, u) - h q (t_{n}, v) ∣ \leq h L_{q} ∥ u - v ∥_{2}$ for $u, v \in K$ . Along the exact trajectory, [F2] gives $\frac{d}{d s} q (t_{n} + s, x (t_{n} + s)) = \partial_{t} q + D_{x} q f$ , with absolute value at most $M_{q} + L_{q} B_{f}$ , hence $∣ q (t_{n} + s, x (t_{n} + s)) - q (t_{n}, x (t_{n})) ∣ \leq (M_{q} + L_{q} B_{f}) s$ by [F4]. The left-Euler exact-start defect is $∣ \int_{0}^{h} (q (t_{n} + s, x (t_{n} + s)) - q (t_{n}, x (t_{n}))) d s ∣$ , which [F4] bounds by $(M_{q} + L_{q} B_{f}) h^{2} / 2 = D_{q} h^{2}$ .

2.1A1F5F7step 1.1step 1.2

The Euler state map from step 1.1 and defect from step 1.2 satisfy Global error from uniform one-step defect and stability with order $p = 1$ , $C = C_{x}$ , $L = L_{f}$ , and initial constant $C_{x, 0}$ . Therefore $\max_{n} ∥ x_{n} - x (t_{n}) ∥_{2} \leq K_{x} h$ , with the stated formula when $L_{f} > 0$ and its separate zero branch when $L_{f} = 0$ .

3.1A2F6step 2.1step 1.3∎

Apply [F6] with state order $p = 1$ , quadrature order $m = 1$ , state constant $K_{x}$ from step 2.1, sensitivity $K_{q} = L_{q}$ , defect constant $D = D_{q}$ , and initial log-density error $C_{ℓ, 0} h$ . This yields $∣ {\hat{ℓ}}_{n} - \log p_{t_{n}} (x (t_{n})) ∣ \leq (C_{ℓ, 0} + T L_{q} K_{x} + D_{q} T) h$ for every grid index.

Depends on

Used by

Dependency tree · two levels

79 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)
Ricky T. Q. Chen, Yulia Rubanova, Jesse Bettencourt, and David Duvenaud, Neural Ordinary Differential Equations (standard reference, not scraped)
George Papamakarios, Eric Nalisnick, Danilo Jimenez Rezende, Shakir Mohamed, and Balaji Lakshminarayanan, Normalizing Flows for Probabilistic Modeling and Inference (standard reference, not scraped)