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 mixture of straight Gaussian paths has a nonlinear marginal velocity
Example
Assume the Axiom of Choice and fix and . Let the endpoint law assign probability to each endpoint and . For each endpoint, use the one-dimensional Gaussian path with For either endpoint and each fixed , the conditional particle trajectory is a straight line. The marginal density is and its marginal velocity field, defined by averaging the conditional velocity against the endpoint density at fixed , is The denominator in the definition of is positive for every real input. The density is strictly positive, and on . For every , is nonlinear.
Example references
Facts & Assumptions
Given: AC, , , the two-point endpoint law, and the Gaussian conditional path in the Example.
The Axiom of Choice is the assertion that every family of nonempty sets has a choice function (The Axiom of Choice); it is required by the Gaussian-law and density suppliers used by [F1].
The Gaussian conditional affine map is quadratic-cost optimal: under AC, for each fixed endpoint the mean-linear Gaussian path has the displayed density and affine conditional velocity, and its density and flux satisfy the conditional continuity equation.
Probability paths and velocity fields: the marginal density is and its velocity, where and the flux is finite, is .
A conditional mixture is a probability path: the endpoint mixture of normalized conditional densities is a probability density at each time.
A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value: a continuous real-valued function on a compact metric space is bounded.
Conditional continuity equations pass to the marginal path: if the conditional PDE derivatives admit the stated local integrable endpoint majorant, then the marginal density and flux satisfy the continuity equation.
The real exponential function and the number by a power series: the real exponential is defined on every real input by its convergent power series.
The exponential addition formula : for all real .
The exponential is positive and satisfies : and for every real .
Verification
Given: The hypotheses in the Example.
Apply [F1] to the two endpoints and . Their conditional densities are positive and continuous in , as are their time derivatives, fluxes, and spatial flux derivatives; throughout . Hence for each compact the finitely many such functions are bounded on by [F4]. Taking a common bound as the constant function gives an element of because has total mass one. Thus [F5] applies. The mixture density is normalized by [F3] and is strictly positive because it is a sum of two positive Gaussian densities.
Put The common Gaussian normalizing factor cancels in the endpoint-weighted mean, so [F2] gives Expanding the two squares gives by [F7] and [F9]. Multiplying numerator and denominator by therefore yields .
For endpoint , [F1] gives Taking the endpoint-weighted mean and using step 1.2 gives . Since , we have and hence . Substitution gives the marginal velocity formula in the Example.
Fix and put and . The formula for , the addition formula [F7], and the reciprocal identity [F9] give , so is odd. For , [F7] gives , and positivity [F9] therefore gives ; strict increase [F8] now yields . Put . Rewriting and using [F7, F9] gives Thus for every , step 2.1 gives An odd affine function must be linear through the origin, and every such function has . Hence is not affine and is nonlinear.
Source notes
The cited sources give the straight conditional Gaussian paths and the conditional-to-marginal velocity formula. The explicit two-endpoint mixture calculation is local. Its conclusion concerns nonlinearity of the marginal velocity; it makes no claim that the marginal field is a globally optimal transport field.
Depends on
- Probability paths and velocity fields
- A conditional mixture is a probability path
- Conditional continuity equations pass to the marginal path
- The Gaussian conditional affine map is quadratic-cost optimal
- The Axiom of Choice
- A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value
- The real exponential function and the number $e$ by a power series
- The exponential addition formula $\exp(x+y)=\exp(x)\exp(y)$
- The exponential function is strictly increasing
- The exponential is positive and satisfies $\exp(-x)=1/\exp(x)$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
63 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
- Yaron Lipman et al., Flow Matching for Generative Modeling, §4.1 Example II and the note on marginal optimal transport (standard reference, not scraped)
- Peter Holderrieth and Ezra Erives, Introduction to Flow Matching and Diffusion Models, §§3.2–3.3 (standard reference, not scraped)