TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge 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.

Positive densities with smooth conditional CDFs admit an exact triangular-flow representation

Statement

Assume the Axiom of Countable Choice. Let $d \geq 1$ and let $p : R^{d} \to (0, \infty)$ be a Lebesgue probability density. For $i = 1, \dots, d$ , write $x_{< i} = (x_{1}, \dots, x_{i - 1})$ , with $x_{< 1}$ the unique element of $R^{0}$ . For each $i$ , let $q_{i} : R \times R^{i - 1} \to (0, \infty)$ be a positive continuous function, written $q_{i} (t ∣ x_{< i})$ , and suppose $p (x) = \prod_{i = 1}^{d} q_{i} (x_{i} ∣ x_{< i}), \int_{R} q_{i} (t ∣ x_{< i}) d t = 1$ for every $x \in R^{d}$ and every preceding-coordinate vector $x_{< i}$ . Define the conditional cumulative distribution functions $F_{i} (t ∣ x_{< i}) = \int_{- \infty}^{t} q_{i} (s ∣ x_{< i}) d s .$ Assume each $F_{i}$ is jointly $C^{1}$ in $(t, x_{< i})$ , satisfies $\partial_{t} F_{i} (t ∣ x_{< i}) = q_{i} (t ∣ x_{< i})$ , and, for every fixed $x_{< i}$ , the slice $t \mapsto F_{i} (t ∣ x_{< i})$ is a strictly increasing bijection from $R$ onto $(0, 1)$ . In each inverse below, $F_{i}^{- 1}$ means the inverse in its first argument with the preceding coordinates held fixed.

Then there is a global $C^{1}$ diffeomorphism $T : (0, 1)^{d} \to R^{d}$ whose $i$ th output coordinate depends only on the first $i$ input coordinates and which maps the uniform density $1$ on $(0, 1)^{d}$ to the density $p$ . Its inverse is $S_{i} (x) = F_{i} (x_{i} ∣ x_{< i}),$ and $T = S^{- 1}$ is determined recursively by $x_{1} = F_{1}^{- 1} (u_{1}), x_{i} = F_{i}^{- 1} (u_{i} ∣ x_{< i}) (i = 2, \dots, d) .$ This is an exact representational existence result; it makes no claim about finite-network approximation, trainability, or numerical performance.

Statement references

The Axiom of Countable Choice ( ${A C}_{ω}$ ) — Countable Choice is used by the change-of-variables and box-volume suppliers.

Papamakarios et al., §2.2, PDF pp. 4–5; §3.1, PDF pp. 10–16

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

Facts & Assumptions

Given: Countable Choice, the density $p$ , the factorization by the positive conditional density factors $q_{i}$ , and the stated smoothness and bijectivity of each $F_{i}$ .

[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 global $C^{1}$ diffeomorphisms between open equal-dimensional Euclidean domains; its base density defines a measure by integration. A normalizing flow and its base density

[F2]

A nonnegative measurable density $f$ defines the measure $A \mapsto \int_{A} f d λ_{d}$ . The measure with density $f$ relative to $μ$

[F3]

The determinant of a triangular matrix is the product of its diagonal entries. The determinant of a triangular matrix is the product of its diagonal entries

[F4]

If $f : U \to R^{d}$ is $C^{1}$ and $D f (a)$ is invertible, then $f$ has a $C^{1}$ local inverse near $a$ . The Euclidean inverse function theorem

[F5]

Under Countable Choice, a $C^{1}$ diffeomorphism transforms a nonnegative Lebesgue density $r$ by the formula $r \circ T^{- 1} ∣ \det D (T^{- 1}) ∣$ . A diffeomorphic flow has the inverse-Jacobian density

[F6]

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

[F7]

The open box $(0, 1)^{d}$ is Lebesgue measurable and has measure $\prod_{i = 1}^{d} (1 - 0) = 1$ under Countable Choice. A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included

Proof

technique · direct

1.1givenF3F6

Define $S : R^{d} \to (0, 1)^{d}$ by $S_{i} (x) = F_{i} (x_{i} ∣ x_{< i})$ . Joint $C^{1}$ regularity makes $S$ $C^{1}$ . Each $S_{i}$ depends only on $x_{1}, \dots, x_{i}$ , so $D S (x)$ is lower triangular; its $i$ th diagonal entry is $\partial_{x_{i}} F_{i} (x_{i} ∣ x_{< i}) = q_{i} (x_{i} ∣ x_{< i}) > 0$ . By [F3] and the factorization hypothesis, $\det D S (x) = \prod_{i = 1}^{d} q_{i} (x_{i} ∣ x_{< i}) = p (x) > 0$ .

1.2givenconstruct

For any $u \in (0, 1)^{d}$ , choose $x_{1} = F_{1}^{- 1} (u_{1})$ , then recursively choose the unique $x_{i} = F_{i}^{- 1} (u_{i} ∣ x_{< i})$ . The slice bijections make every coordinate exist and be unique, and construction gives $S (x) = u$ . Conversely, any $x$ with $S (x) = u$ must have these same coordinates by induction. Hence $S$ is bijective, and the recursive formula shows that $T = S^{- 1}$ is triangular.

2.1F4step 1.1step 1.2

By step 1.1, $D S (x)$ is invertible at every $x$ . Applying [F4] at each point gives a $C^{1}$ local inverse; because $S$ is globally bijective, each local inverse agrees with the same set-theoretic map $S^{- 1}$ . Therefore $S^{- 1}$ is globally $C^{1}$ , so $T$ is a global $C^{1}$ diffeomorphism.

3.1A1F1F2F5F7step 1.1step 2.1∎

By [F7], density $1$ on $(0, 1)^{d}$ is a probability density. Apply [F5] to $T = S^{- 1}$ : the output density at $x$ is $1 \cdot ∣ \det D S (x) ∣ = p (x)$ by step 1.1. Thus the uniform base pushes forward to the target density $p$ , as claimed. Countable Choice is used here through [F5] and [F7]; the recursive inverse construction uses only uniqueness of each conditional quantile.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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