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

A continuous flow changes log density by minus its divergence

Statement

Assume the Axiom of Countable Choice. Let $d \geq 1$ , $U_{0} \subseteq R^{d}$ be open, $T > 0$ , and let $f$ be jointly $C^{1}$ on an open time-state domain. Suppose the ODE $x^{'} (t) = f (t, x (t))$ has a common flow $Φ : [0, T] \times U_{0} \to R^{d}, x (t) = Φ_{t} (x_{0}),$ whose time slices $Φ_{t} : U_{0} \to U_{t}$ are $C^{1}$ diffeomorphisms onto open sets $U_{t}$ , with $Φ_{0} = {id}_{U_{0}}$ . Let $p_{0} : U_{0} \to (0, \infty)$ be a continuous probability density with respect to Lebesgue measure, let $μ_{t}$ be the pushforward of $p_{0} (x) d x$ under $Φ_{t}$ , and define $p_{t} (y) : = {\begin{cases} \frac{p_{0} (Φ_{t}^{- 1} (y))}{∣ \det D Φ_{t} (Φ_{t}^{- 1} (y)) ∣}, & y \in U_{t}, \\ 0, & y \notin U_{t} . \end{cases}$ Then $p_{t}$ is a density of $μ_{t}$ on $R^{d}$ , the flow Jacobian has positive determinant, and $p_{t} (Φ_{t} (x_{0})) = \frac{p_{0} (x_{0})}{\det D Φ_{t} (x_{0})} > 0,$ and, for $0 < t < T$ , $\frac{d}{d t} \log p_{t} (x (t)) = - {div}_{x} f (t, x (t)), {div}_{x} f : = tr D_{x} f = \sum_{i = 1}^{d} \partial_{x_{i}} f_{i} .$ The derivative at $0$ or $T$ is understood one-sided.

Facts & Assumptions

Given: The Countable Choice axiom, the stated common C¹ flow of diffeomorphisms, and the positive continuous initial probability density.

[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 through the change-of-variables supplier [F3].

[F1]

A solution of a first-order system satisfies $x (t_{0}) = x_{0}$ and $x^{'} (t) = F (t, x (t))$ on its interval (First-order systems, initial value problems, and solutions on intervals).

[F2]

A measure with density $p_{0}$ relative to Lebesgue measure is defined by $μ_{0} (E) = \int_{E} p_{0} d λ_{d}$ (The measure with density $f$ relative to $μ$ ).

[F3]

For a C¹ diffeomorphism $S : U \to V$ between open subsets of $R^{d}$ , Countable Choice and the nonnegative change-of-variables theorem give $\int_{V} g (y) d λ_{d} (y) = \int_{U} g (S (x)) ∣ \det D S (x) ∣ d λ_{d} (x)$ for every nonnegative Lebesgue-measurable $g$ (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions).

[F4]

If a vector field is continuous and C¹ in the state variable and the solutions through nearby initial states exist on a common compact interval $I = [s - a, s + a]$ for some $a > 0$ , then the solution map is C¹ in the initial state and its derivative $V_{t}$ solves $V^{'} (t) = D_{x} f (t, x (t)) V_{t}$ with $V_{s} = I_{d}$ ; endpoint derivatives are one-sided ( $C^{1}$ dependence of solutions on initial data, First-order systems, initial value problems, and solutions on intervals).

[F5]

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

[F6]

A continuous real function on a closed interval takes every value between its endpoint values (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ ).

[F7]

For $z > 0$ , $\log z$ is defined as the inverse of the real exponential and $\log^{'} (z) = 1 / z$ (The natural logarithm as the inverse of the exponential function, The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[F8]

The determinant of a square matrix is the finite Leibniz sum over permutations (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[F9]

A real square matrix is invertible if and only if its determinant is nonzero (A finite square real matrix is invertible if and only if its determinant is nonzero).

[F10]

The determinant is a polynomial in its matrix entries, and polynomial functions are continuous (For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries, Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function).

[F11]

The Leibniz determinant is column-multilinear and alternating (The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring).

[F12]

Sums and products of differentiable real functions obey the binary sum and product rules; repeated application over finitely many factors follows by induction (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$ ).

Proof

1.1A1F2F3F5F9given

For fixed $t$ , the inverse-flow chain rule [F5] gives $D Φ_{t}^{- 1} (Φ_{t} (x_{0})) D Φ_{t} (x_{0}) = I$ , so $D Φ_{t} (x_{0})$ is invertible and [F9] gives $\det D Φ_{t} (x_{0}) \neq 0$ . Thus the formula for $p_{t}$ is continuous and positive on $U_{t}$ and zero outside, hence Borel measurable on $R^{d}$ . For any Borel $E \subseteq R^{d}$ , apply [F3] to $g = 1_{E \cap U_{t}} p_{t} ∣_{U_{t}}$ . Change of variables gives $\int_{E} p_{t} (y) d y = \int_{E \cap U_{t}} p_{t} (y) d y = \int_{Φ_{t}^{- 1} (E \cap U_{t})} p_{0} (x) d x = μ_{0} (Φ_{t}^{- 1} (E)) = μ_{t} (E)$ because $Φ_{t} (U_{0}) = U_{t}$ . Thus $p_{t}$ is a density of $μ_{t}$ on all of $R^{d}$ .

2.1F1F4F5F6F9F10F11step 1.1algebra

Put $s : = T / 2$ . For $z \in U_{s}$ define $Ψ_{t} (z) : = Φ_{t} (Φ_{s}^{- 1} (z))$ for $0 \leq t \leq T$ . Each $Ψ_{t} (z)$ is a solution of the same ODE on the common interval $[0, T] = [s - s, s + s]$ , and $Ψ_{s} (z) = z$ . Apply [F4] to this family at the initial state $x (s) = Φ_{s} (x_{0})$ and initial time $s$ : its derivative $V_{t} : = D_{z} Ψ_{t} (x (s))$ satisfies $V_{t}^{'} = A_{t} V_{t}$ , where $A_{t} : = D_{x} f (t, Φ_{t} (x_{0}))$ , and $V_{s} = I_{d}$ , with one-sided derivatives at $0, T$ . Since $Φ_{t} = Ψ_{t} \circ Φ_{s}$ , the chain rule [F5] gives $J_{t} : = D Φ_{t} (x_{0}) = V_{t} J_{s}$ , so $J_{t}^{'} = A_{t} J_{t}$ on $[0, T]$ and $J_{0} = I_{d}$ , again with one-sided endpoint derivatives. Thus $J_{t}$ is continuous. Separately, the inverse-flow chain rule [F5] and [F9] give $\det J_{t} \neq 0$ for each $t$ ; [F10] and continuity of $J_{t}$ give continuity of $t \mapsto \det J_{t}$ . If this determinant were negative at any $t > 0$ , [F6] on $[0, t]$ with target $0$ would give a zero, contradicting nonsingularity; since $\det J_{0} = 1$ by [F11], it is positive throughout. The density formula in step 1.1 therefore becomes $p_{t} (Φ_{t} (x_{0})) = p_{0} (x_{0}) / \det J_{t}$ .

3.1F4F5F7F8F11F12step 2.1algebrainduction

Fix an interior time, write $A : = D_{x} f (t, Φ_{t} (x_{0}))$ and $C : = J_{t}^{- 1} J_{t}^{'}$ , and denote the columns of $J_{t}$ by $v_{1}, \dots, v_{d}$ . By the Leibniz formula [F8], differentiating each $d$ -factor monomial with repeated binary product rules (induction on the number of factors) and distributing the finite sum gives $(\det J_{t})^{'} = \sum_{σ \in S_{d}} sgn (σ) \sum_{j = 1}^{d} (v_{j}^{'})_{σ (j)} \prod_{i \neq j} (v_{i})_{σ (i)} = \sum_{j = 1}^{d} \det [v_{1}, \dots, v_{j - 1}, v_{j}^{'}, v_{j + 1}, \dots, v_{d}]$ . Since $J_{t}^{'} = J_{t} C$ , if $C_{j}$ is column $j$ of $C$ then $v_{j}^{'} = \sum_{k = 1}^{d} C_{k j} v_{k}$ . Multilinearity [F11] expands the $j$ th determinant into $\sum_{k} C_{k j} \det [v_{1}, \dots, v_{j - 1}, v_{k}, v_{j + 1}, \dots, v_{d}]$ ; for $k \neq j$ the repeated columns make the determinant zero by alternation [F11], while $k = j$ gives $C_{j j} \det J_{t}$ . Hence $(\det J_{t})^{'} = \det J_{t} tr (C)$ and [F7] gives $(\log \det J_{t})^{'} = tr (C)$ . Since $C = J_{t}^{- 1} A J_{t}$ , $tr (C) = \sum_{i, j, k} (J_{t}^{- 1})_{i j} A_{j k} (J_{t})_{k i} = \sum_{j, k} A_{j k} (J_{t} J_{t}^{- 1})_{k j} = \sum_{j} A_{j j} = tr (A)$ . The density formula in step 2.1 has constant numerator $p_{0} (x_{0})$ , so [F7] and the chain rule [F5] give $(\log p_{t} (Φ_{t} (x_{0})))^{'} = - (\det J_{t})^{'} / \det J_{t} = - tr (D_{x} f (t, Φ_{t} (x_{0})))$ . This proves the identity for $0 < t < T$ .

4.1F1F4F7F8step 2.1step 3.1algebra∎

At the endpoints, step 2.1 gives the variational equation for $J_{t}$ on $[0, T]$ , and [F1] makes its endpoint equations one-sided: $J_{0 +}^{'} = A_{0} J_{0}$ and $J_{T -}^{'} = A_{T} J_{T}$ , where $A_{r} : = D_{x} f (r, Φ_{r} (x_{0}))$ . To differentiate the determinant there, use its finite Leibniz polynomial [F8]: as $t ↓ 0$ , each matrix entry has expansion $J_{i j} (t) = J_{i j} (0) + t (J_{0 +}^{'})_{i j} + o (t)$ , and as $t ↑ T$ it has expansion $J_{i j} (t) = J_{i j} (T) + (t - T) (J_{T -}^{'})_{i j} + o (∣ t - T ∣)$ . Expanding each finite product in that polynomial, the terms linear in the increment are exactly the binary product-rule terms and all terms with at least two increments are little-oh of the increment. Thus the same finite expansion as in step 3.1 gives $(\det J)_{0 +}^{'} = \det J_{0} tr (J_{0}^{- 1} A_{0} J_{0}) = \det J_{0} tr (A_{0})$ and $(\det J)_{T -}^{'} = \det J_{T} tr (J_{T}^{- 1} A_{T} J_{T}) = \det J_{T} tr (A_{T})$ . The determinants are positive by step 2.1, so one-sided differentiation of their logarithms [F7] gives $(\log \det J)_{0 +}^{'} = tr (A_{0})$ and $(\log \det J)_{T -}^{'} = tr (A_{T})$ . Using the density identity in step 2.1, $\log p_{t} (Φ_{t} (x_{0})) = \log p_{0} (x_{0}) - \log \det J_{t}$ , therefore its right derivative at $0$ and left derivative at $T$ are respectively $- tr (A_{0})$ and $- tr (A_{T})$ . These are exactly the stated endpoint identities.

Depends on

Used by

Dependency tree · two levels

95 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)