Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Appendix A: divergence under the conditioning integral

Proved
FlowMatchingT1.divergence_integral

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

analysiscontinuity-equationflow-matchingmeasure-theory

Let d∈Nd\in\mathbb Nd∈N, let QQQ be any Borel measure on E=RdE=\mathbb R^dE=Rd, and let F:E×E→EF:E\times E\to EF:E×E→E. At a position xxx, assume F(x,⋅)F(x,\cdot)F(x,⋅) is QQQ-integrable, nearby slices are almost-everywhere strongly measurable, and DxF(x,⋅)D_xF(x,\cdot)Dx​F(x,⋅) is almost-everywhere strongly measurable. Assume there exist a common neighborhood NNN of xxx and a QQQ-integrable real function bbb such that, for almost every zzz, the map F(⋅,z)F(\cdot,z)F(⋅,z) is differentiable throughout NNN and ∥DxF(y,z)∥≤b(z)\|D_xF(y,z)\|\leq b(z)∥Dx​F(y,z)∥≤b(z) for every y∈Ny\in Ny∈N. Then the averaged field is differentiable at xxx, the conditional divergence is QQQ-integrable, and

div⁡x(∫EF(x,z) dQ(z))=∫Ediv⁡xF(x,z) dQ(z).\operatorname{div}_x\left(\int_E F(x,z)\,dQ(z)\right)=\int_E\operatorname{div}_x F(x,z)\,dQ(z).divx​(∫E​F(x,z)dQ(z))=∫E​divx​F(x,z)dQ(z).

This isolates the third equality of Appendix A's proof as a local vector-calculus statement. The result allows arbitrary measures QQQ and includes the empty coordinate sum when d=0d=0d=0.

Preamble
import Definitions.Def_FlowMatchingT1
open MeasureTheory
open FlowMatchingT1

Formal statement
theorem FlowMatchingT1.divergence_integral
    {d : ℕ} (Q : Measure (Space d))
    (F : Space d → Space d → Space d) (x : Space d)
    (h : SpaceRegularAt Q F x) :
    DifferentiableAt ℝ (fun y => ∫ z, F y z ∂Q) x ∧
    Integrable (fun z => divergence (fun y => F y z) x) Q ∧
    divergence (fun y => ∫ z, F y z ∂Q) x =
      ∫ z, divergence (fun y => F y z) x ∂Q := 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 ddd, including d=0d=0d=0, let E=R{0,…,d−1}E=\mathbb{R}^{\{0,\ldots,d-1\}}E=R{0,…,d−1}, with its usual finite-product real normed-space structure (the maximum norm), let QQQ be any measure on the Borel measurable space EEE, let F:E×E→EF:E\times E\to EF:E×E→E be any function, and let x∈Ex\in Ex∈E. For a function g:E→Eg:E\to Eg:E→E, write Dg(y)Dg(y)Dg(y) for its real Fréchet derivative, regarded as a continuous linear map, with the convention that this map is zero when ggg is not differentiable at yyy, and define div⁡g(y)=∑i=0d−1(Dg(y)ei)i\operatorname{div}g(y)=\sum_{i=0}^{d-1}(Dg(y)e_i)_idivg(y)=∑i=0d−1​(Dg(y)ei​)i​, where eie_iei​ has coordinate 111 at iii and zero at all other coordinates. Assume that z↦F(x,z)z\mapsto F(x,z)z↦F(x,z) is Bochner integrable with respect to QQQ; that there is a neighborhood of xxx on which, for every yyy, the function z↦F(y,z)z\mapsto F(y,z)z↦F(y,z) is QQQ-almost everywhere strongly measurable; that z↦D(F(⋅,z))(x)z\mapsto D(F(\cdot,z))(x)z↦D(F(⋅,z))(x) is QQQ-almost everywhere strongly measurable as a function taking values in the space of continuous real linear maps E→EE\to EE→E; and that there exist a set N⊆EN\subseteq EN⊆E containing an open neighborhood of xxx and a real-valued QQQ-integrable function b:E→Rb:E\to\mathbb{R}b:E→R such that, for QQQ-almost every zzz, simultaneously for every y∈Ny\in Ny∈N, ∥D(F(⋅,z))(y)∥op≤b(z)\|D(F(\cdot,z))(y)\|_{\mathrm{op}}\le b(z)∥D(F(⋅,z))(y)∥op​≤b(z), and, for QQQ-almost every zzz, simultaneously for every y∈Ny\in Ny∈N, the function F(⋅,z)F(\cdot,z)F(⋅,z) is real Fréchet differentiable at yyy. The two almost-everywhere conditions may initially have different null exceptional sets, but neither exceptional set depends on yyy. Here almost-everywhere strong measurability means agreement outside a QQQ-null set with a strongly measurable function, and Bochner integrability means almost-everywhere strong measurability together with a finite integral of the norm. Then the function G:E→EG:E\to EG:E→E defined by G(y)=∫EF(y,z) dQ(z)G(y)=\int_E F(y,z)\,dQ(z)G(y)=∫E​F(y,z)dQ(z) is real Fréchet differentiable at xxx, the real-valued function z↦div⁡(F(⋅,z))(x)z\mapsto\operatorname{div}(F(\cdot,z))(x)z↦div(F(⋅,z))(x) is QQQ-integrable, and div⁡G(x)=∫Ediv⁡(F(⋅,z))(x) dQ(z)\operatorname{div}G(x)=\int_E\operatorname{div}(F(\cdot,z))(x)\,dQ(z)divG(x)=∫E​div(F(⋅,z))(x)dQ(z). The integral defining GGG uses the total Bochner-integral convention, which assigns zero to a nonintegrable integrand; the assumptions do not separately require integrability of F(y,⋅)F(y,\cdot)F(y,⋅) at every y∈Ey\in Ey∈E. There is no assumption that QQQ is a probability measure, finite, or sigma-finite, no joint measurability assumption on FFF, and no global nonnegativity assumption on bbb; its displayed bound forces b≥0b\ge0b≥0 almost everywhere because x∈Nx\in Nx∈N. The case Q=0Q=0Q=0 is included, in which the almost-everywhere conditions are vacuous and all the displayed integrals are zero. When d=0d=0d=0, EEE is the one-point zero vector space, the defining divergence sum is empty and equals zero, every EEE-valued function is the zero vector, and the asserted equality is 0=00=00=0 for every measure QQQ on this space. The neighborhood NNN cannot be empty because it contains xxx.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me