ExampleConstruction: AI-generatedVerification: 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.

Euler has state error but exact log-density quadrature for a linear flow

Example

Assume Countable Choice. Let $f (t, x) = x$ on $[0, 1] \times R$ , start at $x (0) = 1$ , take $h = 1 / N$ , and use any strictly positive continuous probability density $p_{0}$ on $R$ . Initialize ${\hat{ℓ}}_{0} = \log p_{0} (1)$ . The exact state is $x (t) = e^{t}$ , while Euler gives $x_{n} = (1 + h)^{n}$ , so its final state error is $e - (1 + 1 / N)^{N} > 0$ . The exact continuous-flow log-density change is $- 1$ , and the Euler divergence accumulator also gives exactly $- 1$ .

Facts & Assumptions

Given: Countable Choice, $T = 1$ , $N \geq 1$ , $h = 1 / N$ , $f (t, x) = x$ on $[0, 1] \times R$ , $x (0) = 1$ , a positive continuous probability density $p_{0}$ on $R$ , and the Euler state and divergence updates initialized by ${\hat{ℓ}}_{0} = \log p_{0} (1)$ .

[A1]

Countable Choice is the assertion that every countable family of nonempty sets has a choice function (The Axiom of Countable Choice ( ${A C}_{ω}$ )); it is used only for the density interpretation inherited from [F1].

[F1]

For a C¹ diffeomorphic flow, $p_{t} (Φ_{t} (x_{0})) = p_{0} (x_{0}) / \det D Φ_{t} (x_{0})$ and the log-density derivative is $- div f$ (A continuous flow changes log density by minus its divergence).

[F2]

Under the stated C² tube and flow hypotheses, Euler state updates and the divergence accumulator have the fixed-time error bounds proved in Euler global state and log-density error on a bounded C² tube.

[F3]

The real exponential is defined by its power series, is differentiable with derivative $\exp$ , and satisfies $\exp (0) = 1$ (The real exponential function and the number $e$ by a power series, The exponential function is smooth and $(\exp)^{'} = \exp$ ).

[F4]

$\exp (t) > 0$ and $1 / \exp (t) = \exp (- t)$ (The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

[F5]

The mean value theorem gives $\exp (h) - \exp (0) = \exp^{'} (c) h$ for some $c \in (0, h)$ (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)$ ).

[F6]

$\exp$ is strictly increasing (The exponential function is strictly increasing).

[F7]

$\exp (u + v) = \exp (u) \exp (v)$ (The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ ).

[F8]

Natural powers preserve order on nonnegative bases for exponent $N \geq 1$ (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ); they satisfy the recursive natural-power definition (Integer powers $a^{m}$ ).

[F9]

A scalar multiple of a differentiable function is differentiable with derivative the same scalar multiple (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[F10]

For positive $u, v$ , $\log (u / v) = \log u - \log v$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F11]

The natural logarithm is the inverse of $\exp$ on positive reals, so $\log (\exp u) = u$ (The natural logarithm as the inverse of the exponential function).

Verification

1.1givenF2F3F4F5F6F7F8F9inductionalgebra

Extend the given field to the open domain $R^{2}$ by the same formula $f (t, x) = x$ ; its restriction to $[0, 1] \times R$ is unchanged. Define $Φ_{t} (x_{0}) : = \exp (t) x_{0}$ for $t \in [0, 1]$ . By [F3] and [F9], $\partial_{t} Φ_{t} (x_{0}) = \exp (t) x_{0} = f (t, Φ_{t} (x_{0}))$ and $Φ_{0} (x_{0}) = x_{0}$ ; [F4] makes every slice a C¹ diffeomorphism $R \to R$ with inverse $y \mapsto y / \exp (t)$ . Thus $x (t) = Φ_{t} (1) = \exp (t)$ is the exact path. Euler satisfies $x_{n + 1} = (1 + h) x_{n}$ , so induction gives $x_{n} = (1 + h)^{n}$ . Since $h > 0$ , [F5] gives $\exp (h) - 1 = \exp (c) h$ for some $c \in (0, h)$ , and [F6] with $\exp (0) = 1$ gives $\exp (c) > 1$ , hence $1 + h < \exp (h)$ . By [F8], $(1 + h)^{N} < \exp (h)^{N}$ ; [F7] gives $\exp (h)^{N} = \exp (N h) = \exp (1)$ , so $∣ x_{N} - x (1) ∣ = \exp (1) - (1 + h)^{N} > 0$ . For $1 \leq n \leq N$ , [F8] and [F7] give $1 \leq x_{n} \leq \exp (n h) \leq \exp (1)$ , while $x_{0} = 1$ ; exact states lie in $[1, \exp (1)]$ by [F6]. Therefore $K = [0, \exp (1)]$ contains the exact path and Euler nodes. The bounded convex open set $U = (- 1, 2) \times (- 1, \exp (1) + 1)$ contains $[0, 1] \times K$ , and $f (t, x) = x$ is C² with bounded derivatives there, so [F2] applies.

2.1givenA1F1F4F10F11step 1.1algebra∎

Here $D Φ_{1} (1) = \exp (1)$ , so [F1] gives $p_{1} (\exp (1)) / p_{0} (1) = 1 / \exp (1) = \exp (- 1)$ by [F4]. Since $p_{0} (1) > 0$ , [F10] and [F11] show that the exact log-density change is $\log (p_{1} (\exp (1))) - \log p_{0} (1) = - 1$ . Euler subtracts $h {div}_{x} f = h$ on each of the $N$ steps, so its computed change is $- N h = - 1$ ; with the given exact initialization, the log-density error is zero despite the positive state error from step 1.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

80 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

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)