TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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 diffeomorphic flow has the inverse-Jacobian density

Statement

Assume the Axiom of Countable Choice. Let $d \geq 1$ , let $U, V \subseteq R^{d}$ be nonempty open sets, and let $T : U \to V$ be a bijection such that $T$ and $T^{- 1}$ are both $C^{1}$ . Let $p_{U} : U \to [0, \infty]$ be Lebesgue measurable with $\int_{U} p_{U} d λ_{d} = 1$ , and define $μ_{U} (A) = \int_{A} p_{U} d λ_{d}$ for Lebesgue-measurable $A \subseteq U$ and $μ_{X} (B) = μ_{U} (T^{- 1} (B))$ for Borel $B \subseteq V$ . Then

$q (x) = p_{U} (T^{- 1} (x)) ∣ \det D (T^{- 1}) (x) ∣$

is Lebesgue measurable and satisfies $μ_{X} (B) = \int_{B} q d λ_{d}$ for every Borel $B \subseteq V$ . Thus $q$ is a version of the density of the transformed measure.

Let $K \geq 1$ , let $U_{0}, \dots, U_{K}$ be nonempty open subsets of $R^{d}$ , and let $T_{j} : U_{j - 1} \to U_{j}$ be a $C^{1}$ diffeomorphism for $j = 1, \dots, K$ . For $T = T_{K} \circ \dots \circ T_{1}$ , $u \in U_{0}$ , and $z_{0} = u$ , $z_{j} = T_{j} (z_{j - 1})$ , the log-Jacobian terms add:

$\log ∣ \det D T (u) ∣ = \sum_{j = 1}^{K} \log ∣ \det D T_{j} (z_{j - 1}) ∣ .$

Equivalently, for $z_{K} = x \in U_{K}$ and $z_{j - 1} = T_{j}^{- 1} (z_{j})$ ,

$\log ∣ \det D T^{- 1} (x) ∣ = \sum_{j = 1}^{K} \log ∣ \det D T_{j}^{- 1} (z_{j}) ∣ .$

Statement references

The Axiom of Countable Choice ( ${A C}_{ω}$ ) — Countable Choice is the axiom used by the measurable change-of-variables supplier.

Papamakarios et al., §2.1, PDF pp. 2–4; §2.2, PDF pp. 4–5

Sheldon, COMPSCI 688 Lecture 23, PDF pp. 2–5

Facts & Assumptions

Given: Countable Choice, a flow $T : U \to V$ , and a Lebesgue probability density $p_{U}$ as in the Statement.

[A1]

The Axiom of Countable Choice, written ${A C}_{ω}$ , asserts that every sequence of nonempty sets has a choice function. The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

A normalizing flow is a finite composition of bijections between open equal-dimensional Euclidean domains whose maps and inverses are $C^{1}$ ; a base density $p_{U}$ defines $μ_{U} (A) = \int_{A} p_{U} d λ_{d}$ , and the transformed measure is $μ_{X} (B) = μ_{U} (T^{- 1} (B))$ . A normalizing flow and its base density

[F2]

For a nonnegative measurable function $f$ , the measure with density $f$ relative to $λ_{d}$ assigns $A$ the value $\int_{A} f d λ_{d}$ . The measure with density $f$ relative to $μ$

[F3]

If $S : U_{0} \to V_{0}$ is a $C^{1}$ diffeomorphism and $f : V_{0} \to [0, \infty]$ is Lebesgue measurable, then under Countable Choice $\int_{V_{0}} f (y) d λ_{d} (y) = \int_{U_{0}} f (S (x)) ∣ \det D S (x) ∣ d λ_{d} (x)$ . A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions

[F4]

Under Countable Choice, Borel sets are Lebesgue measurable, and a $C^{1}$ diffeomorphism maps every Lebesgue-measurable subset of its domain to a Lebesgue-measurable subset of its range. Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable, A C^1 diffeomorphism maps Lebesgue measurable sets to Lebesgue measurable sets

[F5]

For totally differentiable maps, $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ . The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$

[F6]

For same-sized square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ . For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$

[F7]

The Jacobian matrix is the matrix of the total derivative in standard bases, and its Jacobian determinant is the determinant of that matrix. The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, The Jacobian determinant of a square-dimensional $C^{1}$ map is the determinant of its Jacobian matrix

[F8]

The determinant is the finite Leibniz polynomial in the entries of a real square matrix; in particular, $\det (I_{d}) = 1$ . For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries

[F9]

Products of extended-real measurable functions are measurable whenever defined, including the nonnegative density and determinant factors here. Arithmetic and lattice operations preserve measurability whenever they are defined

Proof

technique · direct

1.1A1F1F4F7F8F9

For every $a \in R$ , the superlevel set $E_{a} = {u \in U : p_{U} (u) > a}$ is Lebesgue measurable, and ${x \in V : p_{U} (T^{- 1} (x)) > a} = T (E_{a})$ is Lebesgue measurable by [F4]. Thus $p_{U} \circ T^{- 1}$ is measurable. The entries of $D (T^{- 1})$ are continuous by the $C^{1}$ hypothesis, and [F8] makes its determinant continuous. Thus [F9] shows that $q$ is nonnegative measurable.

1.2givenF1F5F7

For $z_{0} = u$ and $z_{j} = T_{j} (z_{j - 1})$ , repeated use of [F5] gives $D T (u) = D T_{K} (z_{K - 1}) \dots D T_{1} (z_{0})$ . For $x = z_{K}$ , applying the chain rule to $T^{- 1} = T_{1}^{- 1} \circ \dots \circ T_{K}^{- 1}$ gives $D (T^{- 1}) (x) = D T_{1}^{- 1} (z_{1}) \dots D T_{K}^{- 1} (z_{K})$ .

2.1A1F1F2F3F4F9step 1.1

Fix a Borel set $B \subseteq V$ and put $E = T^{- 1} (B)$ . By [F4], $E$ is Lebesgue measurable. The function $h (u) = p_{U} (u) 1_{E} (u)$ is nonnegative measurable by [F9]. Apply [F3] to $S = T^{- 1} : V \to U$ and $h$ to obtain $μ_{X} (B) = \int_{E} p_{U} (u) d λ_{d} (u) = \int_{V} p_{U} (T^{- 1} (x)) 1_{B} (x) ∣ \det D (T^{- 1}) (x) ∣ d λ_{d} (x) = \int_{B} q (x) d λ_{d} (x) .$ Therefore $q$ is a density version of $μ_{X}$ .

3.1F5F6F8step 1.2algebra∎

By [F6], determinants of each derivative composition are the products of the stage determinants. Each factor is nonzero: differentiating $T_{j}^{- 1} \circ T_{j} = id$ by [F5] gives a product equal to the identity matrix, whose determinant is $1$ by [F8]. Taking absolute values and then real logarithms yields both displayed additive formulas.

Depends on

Used by

Dependency tree · two levels

66 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

George Papamakarios, Eric Nalisnick, Danilo Jimenez Rezende, Shakir Mohamed, and Balaji Lakshminarayanan, Normalizing Flows for Probabilistic Modeling and Inference, arXiv:1912.02762v1 (standard reference, not scraped)
Dan Sheldon, COMPSCI 688: Probabilistic Graphical Models, Lecture 23: Normalizing Flows (annotated course notes) (standard reference, not scraped)