Theorem 4.32 — integrating against a marginal

Proved

MongeKantorovichYao.integral_fst_eq_of_mem_transferencePlans

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

measure-theoryoptimal-transport

Let $X,Y$ be measurable spaces and let $\pi$ be a probability measure on $X\times Y$ with marginals $\mu$ and $\nu$ on $X$ and $Y$ respectively. Then for every $\mu$ -integrable $f : X\to\mathbb R$ ,

\int_X f(x)\,d\mu(x)=\int_{X\times Y}f(x)\,d\pi(x,y).

This identity converts the dual objective $\int\psi\,d\mu+\int\varphi\,d\nu$ into a single integral against a plan.

Formalization Note The function $(x,y)\mapsto f(x)$ is the extension $\tilde f$ mentioned in the source; the analogous statement for the second marginal is symmetric.

Preamble

import Mathlib
import Definitions.Def_MongeKantorovichYao_Defs

open MeasureTheory

Formal statement

namespace MongeKantorovichYao

theorem integral_fst_eq_of_mem_transferencePlans {X Y : Type*}
    [MeasurableSpace X] [MeasurableSpace Y]
    (μ : Measure X) (ν : Measure Y) (π : Measure (X × Y)) (hπ : π ∈ transferencePlans μ ν)
    (f : X → ℝ) (hf : Integrable f μ) :
    ∫ x, f x ∂μ = ∫ p, f p.1 ∂π := by sorry

end MongeKantorovichYao

Source

Colin Yao, *Monge–Kantorovich and Transportation Theory* (paper dated September 10, 2023), p. 16, Theorem 4.32

Read-back

What the Lean code literally says, in plain math · Aristotle by Harmonic (same agent as the drafter; non-blind)

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source paper and of the intended meaning. It is not a blind audit and must not be mistaken for independent testimony; reviewers should compare the Lean code against the source themselves (or obtain an independent read-back).

Data and hypotheses. Types $X,Y$ with σ-algebras (no topology); measures $\mu$ on $X$ , $\nu$ on $Y$ , $\pi$ on $X\times Y$ with $\pi\in\Pi(\mu,\nu)$ (probability measure, first marginal $=\mu$ , second marginal $=\nu$ ); a real function $f$ on $X$ that is Bochner-integrable with respect to $\mu$ .

Conclusion. $\int_X f\,d\mu=\int_{X\times Y}f(p_1)\,d\pi(p)$ , where $p_1$ is the first coordinate of $p$ (both ordinary real-valued Bochner integrals). Only the first marginal is treated; $\nu$ plays no role beyond membership of $\pi$ in $\Pi(\mu,\nu)$ .

Human review

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

View graph