Theorem 1.1 (mutually singular case): the excursion-coupling definition is well-defined

Proved

ExcursionCoupling.excursion_coupling_well_defined

by ykanoria · Aug 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

couplingmeasure-theoryoptimal-transport

Let $\mu\perp\nu$ be mutually singular Borel probability measures on $\mathbb R$ , let $F_\sigma=F_\mu-F_\nu$ , and let

N(h)= \#\bigl((\mathbb R\times\{h\})\cap\operatorname{Graph}^{*,+}(F_\sigma)\bigr) + \#\bigl((\mathbb R\times\{h\})\cap\operatorname{Graph}^{*,-}(F_\sigma)\bigr).

Then the measure $\theta/2$ with density $N(h)/2$ relative to Lebesgue measure is a probability measure. For $\theta/2$ -almost every sampled level $h$ , the level is nonzero, its completed-graph section is nonempty and finite of even cardinality, every intersection is an increasing or decreasing crossing, and the crossings alternate in order, starting with an increasing crossing for $h>0$ and a decreasing crossing for $h<0$ .

Pair adjacent crossings as in Juillet's construction and, conditionally on the sampled level, choose uniformly among those pairs. The resulting joint law $\gamma_{\mathrm{EC}}$ is Juillet's excursion coupling in the exact formal sense: it is the completed-graph occupation measure

\gamma_{\mathrm{EC}} = \int_{\mathbb R} \sum_{\text{paired }(x,y)\text{ at }h}\delta_{(x,y)}\,dh,

it is a probability measure, and its coordinate laws are respectively $\mu$ and $\nu$ .

This is the mutually singular case of the well-definedness assertion in Theorem 1.1, with every implicit claim listed in Remark 1.2 made explicit.

Formalization Note The named predicate IsJuilletExcursionCoupling requires equality with the occupation measure, not only concentration on the paired-route set.

Preamble

import Definitions.Def_JuilletExcursionCoupling

open MeasureTheory Set Function

Formal statement

namespace ExcursionCoupling

theorem excursion_coupling_well_defined
    (mu nu : Measure Real)
    [IsProbabilityMeasure mu] [IsProbabilityMeasure nu]
    (hsing : mu ⟂ₘ nu) :
    IsProbabilityMeasure (excursionLevelLaw mu nu) ∧
      (∀ᵐ h ∂excursionLevelLaw mu nu,
        h ≠ 0 ∧
          (levelSet (Fsigma mu nu) h).Nonempty ∧
          regularLevel (Fsigma mu nu) h) ∧
      ∃ gamma : Measure (Real × Real),
        IsJuilletExcursionCoupling mu nu gamma := by sorry

end ExcursionCoupling

Source

Nicolas Juillet, On a solution to the Monge transport problem on the real line arising from the strictly concave case, arXiv:1907.00681v1 (2019), Theorem 1.1, mutually singular case, and Remark 1.2, p. 5; construction in Section 3.1, pp. 12-16

Read-back

What the Lean code literally says, in plain math · openai-codex

For every pair of probability measures $\mu,\nu$ on $\mathbb R$ that are mutually singular, define $F(x)=\operatorname{toReal}(\mu((-\infty,x]))-\operatorname{toReal}(\nu((-\infty,x]))$ . For any $G:\mathbb R\to\mathbb R$ , let $C_G=\{(x,y):y\in[\min(\operatorname{leftLim}G(x),G(x)),\max(\operatorname{leftLim}G(x),G(x))]\}$ , $L_G(h)=\{x:(x,h)\in C_G\}$ , and let $P_G$ consist of those $p\in C_G$ for which there exists $\varepsilon>0$ such that every $q\in C_G$ with $|q_1-p_1|<\varepsilon$ and $q_1\ne p_1$ satisfies $0<(q_2-p_2)(q_1-p_1)$ ; define $N_G$ identically except that the required inequality is $(q_2-p_2)(q_1-p_1)<0$ . Say that $h$ is regular for $G$ when there exist $n\in\mathbb N$ and a strictly increasing map $x:\operatorname{Fin}(2n)\to\mathbb R$ such that $L_G(h)=\{x_i:i\in\operatorname{Fin}(2n)\}$ , every $(x_i,h)$ lies in $P_G\cup N_G$ , and, for every $i$ , $(x_i,h)\in P_G\iff(0<h\iff i\text{ is even})$ ; here $n=0$ is allowed. Let $m_F(h)$ be the sum, in $\mathbb R_{\ge0}\cup\{\infty\}$ , of the extended cardinalities of $\{x:(x,h)\in P_F\}$ and $\{x:(x,h)\in N_F\}$ , and let $\lambda=(2:\mathbb R_{\ge0}\cup\{\infty\})^{-1}\!\cdot(\operatorname{Leb}\text{ with density }m_F)$ . Then $\lambda$ is a probability measure; for $\lambda$ -almost every $h$ , one has $h\ne0$ , $L_F(h)\ne\varnothing$ , and $h$ is regular for $F$ ; and there exists a probability measure $\gamma$ on $\mathbb R^2$ whose first and second coordinate pushforwards are respectively $\mu$ and $\nu$ , together with functions $s_i,t_i:\mathbb R\to\mathbb R$ and Borel sets $A_i\subseteq\mathbb R$ for every $i\in\mathbb N$ , such that every $s_i$ and $t_i$ is measurable, every $A_i$ excludes $0$ , and the following hold: for Lebesgue-almost every $h$ , $h\ne0$ implies that $h$ is regular for $F$ ; for Lebesgue-almost every $h$ , every $i$ with $h\in A_i$ satisfies $(s_i(h),h)\in P_F$ , $(t_i(h),h)\in N_F$ , and either $0<h$ , $s_i(h)<t_i(h)$ , and no $z\in(s_i(h),t_i(h))$ belongs to $L_F(h)$ , or $h<0$ , $t_i(h)<s_i(h)$ , and no $z\in(t_i(h),s_i(h))$ belongs to $L_F(h)$ ; for Lebesgue-almost every $h$ , every $x$ satisfying $h\ne0$ , regularity of $h$ , and $(x,h)\in P_F$ has a unique $i\in\mathbb N$ with $h\in A_i$ and $s_i(h)=x$ ; for Lebesgue-almost every $h$ , every $y$ satisfying $h\ne0$ , regularity of $h$ , and $(y,h)\in N_F$ has a unique $i\in\mathbb N$ with $h\in A_i$ and $t_i(h)=y$ ; for Lebesgue-almost every $h$ , the set $\{i:h\in A_i\}$ is finite; and $\gamma=\sum_{i\in\mathbb N}(h\mapsto(s_i(h),t_i(h)))_{\#}(\operatorname{Leb}|_{A_i})$ .

Human review

Endorsed by Community (Bot) · Aug 6, 2026
Endorsed by ykanoria · Aug 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph