Equation (6): the marginal is a positive probability density

Proved

FlowMatchingT1.marginal_probability

by MiltMont · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscontinuity-equationflow-matchingmeasure-theory

Let $d$ be any natural number, $E=\mathbb R^d$ , and $Q$ a Borel probability measure on $E$ . Suppose that for every $t\in[0,1]$ , the real function $\rho(t,x,z)$ is jointly measurable in $(x,z)$ and strictly positive at every pair $(x,z)$ ; for each $z$ , its integral in $x$ is one and it is Lebesgue integrable; and for each $x$ , its integral in $z$ against $Q$ is integrable. Then the mixture $p(t,x)=\int\rho(t,x,z)\,dQ(z)$ satisfies

p(t,x)>0\quad\text{for all }x,\qquad \int_Ep(t,x)\,dx=1,

and is Lebesgue integrable, for every $t\in[0,1]$ . This establishes the probability-path meaning of equation (6), including positivity needed by the velocity formula. It requires no velocity field or derivative assumptions.

Preamble

import Definitions.Def_FlowMatchingT1
open MeasureTheory
open FlowMatchingT1

Formal statement

theorem FlowMatchingT1.marginal_probability
    {d : ℕ} (Q : Measure (Space d)) [IsProbabilityMeasure Q]
    (ρ : ℝ → Space d → Space d → ℝ) (hρ : DensityHypotheses Q ρ) :
    ∀ t ∈ Set.Icc (0 : ℝ) 1,
      ProbabilityDensity (marginalDensity Q ρ t) ∧
      ∀ x, 0 < marginalDensity Q ρ t x := by sorry

Source

Y. Lipman, R. T. Q. Chen, H. Ben-Hamu, M. Nickel, M. Le, Flow Matching for Generative Modeling, ICLR 2023; https://arxiv.org/abs/2210.02747v2; Section 2, Section 3.1, Theorem 1, equations (6), (8), (26), Appendix A proof of Theorem 1.

Read-back

What the Lean code literally says, in plain math · gpt-6-astra

For every natural number $d$ (including $d=0$ ), let $X=\mathbb R^d$ , represented as the real-valued functions on $\{0,\ldots,d-1\}$ , with its usual measurable structure and Lebesgue measure $dx$ . Let $Q$ be any probability measure on $X$ , so $Q(X)=1$ , and let $\rho:\mathbb R\times X\times X\to\mathbb R$ be any function satisfying all of the following: for every $t\in[0,1]$ and every $x,z\in X$ , $\rho(t,x,z)>0$ ; for every $t\in[0,1]$ , the function $(x,z)\mapsto\rho(t,x,z)$ is jointly measurable; for every $t\in[0,1]$ and every $z\in X$ , the function $x\mapsto\rho(t,x,z)$ is nonnegative at every $x$ , integrable with respect to $dx$ , and satisfies $\int_X\rho(t,x,z)\,dx=1$ ; and for every $t\in[0,1]$ and every $x\in X$ , the function $z\mapsto\rho(t,x,z)$ is integrable with respect to $Q$ . Define $p(t,x)=\int_X\rho(t,x,z)\,dQ(z)$ , using the real-valued Bochner integral. Then for every $t\in[0,1]$ , $p(t,x)\geq0$ for every $x\in X$ , $x\mapsto p(t,x)$ is integrable with respect to $dx$ , $\int_Xp(t,x)\,dx=1$ , and, additionally, $p(t,x)>0$ for every $x\in X$ . Both the hypotheses and the conclusion include the endpoint times $0$ and $1$ ; they impose no conditions or conclusion at other times. The pointwise positivity assertions hold everywhere, rather than merely almost everywhere. The case $d=0$ is included, in which $X$ consists of the single empty-coordinate vector; the spatial quantifiers still range over that singleton. No absolute continuity assumption on $Q$ is made.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by MiltMont · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph