Appendix A: time differentiation under the conditioning integral

Proved

FlowMatchingT1.time_derivative_integral

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

analysiscontinuity-equationflow-matchingmeasure-theory

Let $d\in\mathbb N$ , let $Q$ be any Borel measure on $E=\mathbb R^d$ , and let $f:\mathbb R\times E\to\mathbb R$ . At a real time $t$ , assume $f(t,\cdot)$ is $Q$ -integrable, the nearby slices are almost-everywhere strongly measurable, and the time derivative at $t$ is almost-everywhere strongly measurable in $z$ . Assume there exist a common neighborhood $N$ of $t$ and a $Q$ -integrable real function $b$ such that, for almost every $z$ , $f(\cdot,z)$ is differentiable throughout $N$ and its derivative has norm at most $b(z)$ there. Then that derivative is integrable at $t$ , and

\frac{d}{ds}\bigg|_{s=t}\int_E f(s,z)\,dQ(z)=\int_E\partial_t f(t,z)\,dQ(z).

The conclusion includes existence of the derivative. This is the time-differentiation operation used in the first equality of Appendix A's proof. No finiteness or probability assumption on $Q$ is needed.

Preamble

import Definitions.Def_FlowMatchingT1
open MeasureTheory
open FlowMatchingT1

Formal statement

theorem FlowMatchingT1.time_derivative_integral
    {d : ℕ} (Q : Measure (Space d)) (f : ℝ → Space d → ℝ) (t : ℝ)
    (h : TimeRegularAt Q f t) :
    Integrable (fun z => deriv (fun s => f s z) t) Q ∧
    HasDerivAt (fun s => ∫ z, f s z ∂Q)
      (∫ z, deriv (fun s => f s z) t ∂Q) t := 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 $X=\{0,\ldots,d-1\}\to\mathbb R$ , with its usual finite-dimensional real vector-space topology and Borel measurable structure. For every measure $Q$ on $X$ , every function $f:\mathbb R\times X\to\mathbb R$ , and every $t\in\mathbb R$ , suppose all of the following hold: the function $z\mapsto f(t,z)$ is $Q$ -integrable; for all $s$ in some neighborhood of $t$ , the function $z\mapsto f(s,z)$ is $Q$ -almost everywhere strongly measurable (that is, it agrees $Q$ -almost everywhere with a strongly measurable function); the function $z\mapsto \partial_s f(t,z)$ is $Q$ -almost everywhere strongly measurable; and there exist a neighborhood $N\subseteq\mathbb R$ of $t$ and a $Q$ -integrable function $b:X\to\mathbb R$ such that, for $Q$ -almost every $z$ , the bound $|\partial_s f(s,z)|\le b(z)$ holds for every $s\in N$ , and, for $Q$ -almost every $z$ , the function $r\mapsto f(r,z)$ is differentiable at every $s\in N$ . Here $\partial_s f(s,z)$ denotes the ordinary real derivative of $r\mapsto f(r,z)$ at $s$ , with the total-function convention that its value is zero where this function is not differentiable. A neighborhood $N$ need not itself be open but contains an open set containing $t$ ; the exceptional null sets in the two assertions quantified over $N$ are independent of $s$ , though they may differ between the assertions. Then $z\mapsto\partial_s f(t,z)$ is $Q$ -integrable, and the function $s\mapsto\int_X f(s,z)\,dQ(z)$ has an ordinary two-sided derivative at $t$ equal to $\int_X\partial_s f(t,z)\,dQ(z)$ , namely $\displaystyle \left.\frac{d}{ds}\int_X f(s,z)\,dQ(z)\right|_{s=t}=\int_X\partial_s f(t,z)\,dQ(z)$ . Integrability here includes almost everywhere strong measurability and finiteness of the integral of the absolute value; integrals are the total Bochner integrals, assigned zero for nonintegrable inputs. There is no restriction of $t$ to a time interval, no positivity or normalization assumption on $f$ , and no finiteness or probability assumption on $Q$ . The quantification includes $d=0$ , when $X$ is a singleton, and the zero measure $Q$ , for which the almost everywhere conditions are vacuous and both integrals in the conclusion are zero. The majorant $b$ is not separately required to be nonnegative everywhere, but the bound at $s=t\in N$ forces it to be nonnegative $Q$ -almost everywhere.

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