Equation (8): weighted velocity and marginal flux

Proved

FlowMatchingT1.marginal_velocity_identity

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

analysiscontinuity-equationflow-matchingmeasure-theory

Let $d\in\mathbb N$ , $E=\mathbb R^d$ , $Q$ any Borel measure on $E$ , $\rho:\mathbb R\times E\times E\to\mathbb R$ , and $v:\mathbb R\times E\times E\to E$ . At fixed $t\in\mathbb R$ and $x\in E$ , write $p=\int\rho(t,x,z)\,dQ(z)$ and $J=\int\rho(t,x,z)v(t,x,z)\,dQ(z)$ . Suppose $p>0$ and the conditional flux is $Q$ -integrable. The velocity $u=p^{-1}J$ satisfies both

u=\int_E\frac{\rho(t,x,z)}p v(t,x,z)\,dQ(z),\qquad pu=J.

The first identity matches equation (8) in measure notation; the second identifies the flux appearing in the continuity equation. This local algebraic result imposes no time interval, conditional normalization, or probability assumption on $Q$ .

Preamble

import Definitions.Def_FlowMatchingT1
open MeasureTheory
open FlowMatchingT1

Formal statement

theorem FlowMatchingT1.marginal_velocity_identity
    {d : ℕ} (Q : Measure (Space d))
    (ρ : ℝ → Space d → Space d → ℝ) (v : ℝ → Space d → Space d → Space d)
    (t : ℝ) (x : Space d) (hp : 0 < marginalDensity Q ρ t x)
    (hF : Integrable (fun z => conditionalFlux ρ v t x z) Q) :
    marginalVelocity Q ρ v t x =
      (∫ z, (ρ t x z / marginalDensity Q ρ t x) • v t x z ∂Q) ∧
    marginalDensity Q ρ t x • marginalVelocity Q ρ v t x =
      marginalFlux Q ρ v 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$ , let $E=\{0,\ldots,d-1\}\to\mathbb R$ , with its usual finite-dimensional real vector-space and Borel measurable structures. For every measure $Q$ on $E$ , every function $\rho:\mathbb R\times E\times E\to\mathbb R$ , every function $v:\mathbb R\times E\times E\to E$ , every real number $t$ , and every $x\in E$ , define $p=\int_E\rho(t,x,z)\,dQ(z)$ , $F=\int_E\rho(t,x,z)v(t,x,z)\,dQ(z)$ , and $u=p^{-1}F$ , where multiplication of a vector by a real number is scalar multiplication and the vector integral is the Bochner integral. If $p>0$ and the function $z\mapsto\rho(t,x,z)v(t,x,z)$ is Bochner integrable with respect to $Q$ (almost everywhere strongly measurable with integrable norm), then both identities hold:

u=\int_E\frac{\rho(t,x,z)}{p}v(t,x,z)\,dQ(z) \qquad\text{and}\qquad p u=F.

Here $Q$ need not be finite or a probability measure, $\rho$ need not be pointwise nonnegative or normalized, and no differentiability, continuity equation, or time-interval restriction is assumed; the integrability assumption concerns the product $\rho(t,x,\cdot)v(t,x,\cdot)$ , rather than $v(t,x,\cdot)$ separately. The integrals use the total Bochner-integral convention, which assigns zero to a nonintegrable function; consequently the strict inequality $p>0$ excludes a nonintegrable scalar density slice as well as a zero or negative scalar integral, and excludes the zero measure. Real inversion is total with $0^{-1}=0$ , but the assumption excludes that denominator case. The quantification includes $d=0$ , for which $E$ is the one-element zero-dimensional vector space and both vector identities are identities of its unique vector, provided the same hypotheses hold.

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