Completed graph, crossings, and paired routes for $F_\sigma = F_\mu - F_\nu$

Definition

excursion_coupling

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

measure-theoryoptimal-transportreal-analysis

Basic objects of Juillet's excursion-coupling construction on the real line.

For finite Borel measures $\mu,\nu$ on $\mathbf{R}$ , the signed cumulative distribution function is $F_\sigma(x) = \mu((-\infty,x]) - \nu((-\infty,x])$ , a càdlàg function of bounded variation. Its completed graph $\mathrm{Graph}^*(F_\sigma)$ adds at every discontinuity point $x$ the vertical segment joining $(x,F_\sigma(x^-))$ to $(x,F_\sigma(x))$ ; for $(x,h)\in\mathrm{Graph}^*(F_\sigma)$ one calls $x$ a generalized solution of $F_\sigma=h$ , and the set of generalized solutions at level $h$ is the level set of $h$ .

A point $(x,h)$ of the completed graph is increasing (a positive crossing, $\mathrm{Graph}^{*,+}$ ) if on a punctured neighborhood of $x$ every point $(x',h')$ of the completed graph satisfies $(h'-h)(x'-x)>0$ , and decreasing ( $\mathrm{Graph}^{*,-}$ ) in the symmetric case. A level $h$ is regular when its generalized solutions form a finite set of even cardinality, each is an increasing or decreasing point, and, enumerated in increasing order, they strictly alternate, starting with an increasing point when $h>0$ and with a decreasing one when $h<0$ . The paired routes $\Gamma$ (eq. (14) of the source) pair each increasing point with the adjacent decreasing point at the same regular level $h\neq 0$ - the one immediately to its right when $h>0$ , immediately to its left when $h<0$ .

Finally, a set $S\subset\mathbf{R}\times\mathbf{R}$ of transport routes, seen as arches over the real line, is monotone when its arches are non-crossing (any two intervals $[x,y]$ , $[x',y']$ with unordered endpoints are disjoint, meet in exactly one point, or are nested), non-connecting (the arrival point of a non-degenerate route is never the departure point of another non-degenerate route), and consistently oriented (nested arches point in the same direction).

Formalization Note The completed graph is defined through Mathlib's Function.leftLim; for the càdlàg functions $F_\sigma$ used throughout the mission the left limits exist, so the definition agrees with the source. Unordered intervals $[x,y]$ are Set.uIcc.

Definition code

/- Draft statements for Mission 1: Juillet (2019), arXiv:1907.00681v1
   "On a solution to the Monge transport problem on the real line arising
    from the strictly concave case"
   Definitions layer + Theorem statements (all `by sorry`), single-file first pass. -/
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.MeasureTheory.Measure.MutuallySingular
import Mathlib.Topology.Order.LeftRightLim
import Mathlib.Topology.EMetricSpace.BoundedVariation
import Mathlib.Data.Real.ENatENNReal
import Mathlib.Data.Set.Card
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

namespace ExcursionCoupling

open MeasureTheory Set Function

/-- Cumulative distribution function of the signed measure `σ = μ - ν`:
`F_σ(x) = F_μ(x) - F_ν(x)` (Juillet 2019, eq. (1)). -/
noncomputable def Fsigma (μ ν : Measure ℝ) (x : ℝ) : ℝ :=
  (μ (Iic x)).toReal - (ν (Iic x)).toReal

/-- The completed graph `Graph*(F)` of a real function: the graph completed at
discontinuity points by the vertical segments joining `(x, F(x⁻))` to `(x, F(x))`
(Juillet 2019, Section 1). -/
def completedGraph (F : ℝ → ℝ) : Set (ℝ × ℝ) :=
  {p | p.2 ∈ uIcc (leftLim F p.1) (F p.1)}

/-- The set of generalized solutions of `F = h` (Juillet 2019, Section 1). -/
def levelSet (F : ℝ → ℝ) (h : ℝ) : Set ℝ :=
  {x | (x, h) ∈ completedGraph F}

/-- `Graph^{*,+}(F)`: increasing (positive-crossing) points of the completed graph.
`(x,h)` is increasing if in a punctured neighborhood of `x`, every point `(x',h')` of the
completed graph satisfies `(h'-h)(x'-x) > 0` (Juillet 2019, Section 1). -/
def posPoints (F : ℝ → ℝ) : Set (ℝ × ℝ) :=
  {p | p ∈ completedGraph F ∧ ∃ ε > 0, ∀ q ∈ completedGraph F,
    |q.1 - p.1| < ε → q.1 ≠ p.1 → 0 < (q.2 - p.2) * (q.1 - p.1)}

/-- `Graph^{*,-}(F)`: decreasing (negative-crossing) points of the completed graph
(Juillet 2019, Section 1). -/
def negPoints (F : ℝ → ℝ) : Set (ℝ × ℝ) :=
  {p | p ∈ completedGraph F ∧ ∃ ε > 0, ∀ q ∈ completedGraph F,
    |q.1 - p.1| < ε → q.1 ≠ p.1 → (q.2 - p.2) * (q.1 - p.1) < 0}

/-- A level `h` is regular for `F` when the set of generalized solutions of `F = h`
is finite of even cardinality, each solution is an increasing or decreasing point, and,
enumerated in increasing order, solutions strictly alternate between increasing and
decreasing, starting with an increasing point if `h > 0` and a decreasing one if `h < 0`
(the conclusion of Juillet 2019, Proposition 3.2). -/
def regularLevel (F : ℝ → ℝ) (h : ℝ) : Prop :=
  ∃ n : ℕ, ∃ x : Fin (2 * n) → ℝ, StrictMono x ∧ levelSet F h = range x ∧
    (∀ i : Fin (2 * n), (x i, h) ∈ posPoints F ∪ negPoints F) ∧
    (∀ i : Fin (2 * n), ((x i, h) ∈ posPoints F ↔ (0 < h ↔ Even (i : ℕ))))

/-- The set `Γ` of paired routes (Juillet 2019, eq. (14)): pairs of consecutive
generalized solutions at a regular level `h ≠ 0`, the increasing point paired with the
decreasing point immediately to its right when `h > 0`, and with the decreasing point
immediately to its left when `h < 0`. -/
def pairedRoutes (F : ℝ → ℝ) : Set (ℝ × ℝ) :=
  {r | ∃ h : ℝ, h ≠ 0 ∧ regularLevel F h ∧
    (r.1, h) ∈ posPoints F ∧ (r.2, h) ∈ negPoints F ∧
    ((0 < h ∧ r.1 < r.2 ∧ ∀ z ∈ Ioo r.1 r.2, z ∉ levelSet F h) ∨
     (h < 0 ∧ r.2 < r.1 ∧ ∀ z ∈ Ioo r.2 r.1, z ∉ levelSet F h))}

/-- Routes of `S` are non-crossing arches: any two closed intervals `[x,y]`, `[x',y']`
(unordered endpoints) are disjoint, meet in exactly one point, or are nested
(Juillet 2019, Definition 0.3). -/
def NonCrossing (S : Set (ℝ × ℝ)) : Prop :=
  ∀ p ∈ S, ∀ q ∈ S,
    uIcc p.1 p.2 ∩ uIcc q.1 q.2 = ∅ ∨ (∃ z : ℝ, uIcc p.1 p.2 ∩ uIcc q.1 q.2 = {z}) ∨
    uIcc p.1 p.2 ⊆ uIcc q.1 q.2 ∨ uIcc q.1 q.2 ⊆ uIcc p.1 p.2

/-- Arches of `S` do not connect: an arrival point of a non-degenerate route is never the
starting point of another non-degenerate route (Juillet 2019, Definition 0.3). -/
def NonConnecting (S : Set (ℝ × ℝ)) : Prop :=
  ∀ p ∈ S, ∀ q ∈ S, 0 < min |p.2 - p.1| |q.2 - q.1| → p.2 ≠ q.1

/-- Nested arches of `S` have the same orientation (Juillet 2019, Definition 0.3). -/
def SameOrientation (S : Set (ℝ × ℝ)) : Prop :=
  ∀ p ∈ S, ∀ q ∈ S, uIcc q.1 q.2 ⊆ Ioo (p.1 ⊓ p.2) (p.1 ⊔ p.2) →
    0 ≤ (p.2 - p.1) * (q.2 - q.1)

/-- A monotone set of arches: non-crossing, non-connecting, and consistently oriented
(Juillet 2019, Definition 0.3 and Section 3.2). -/
def IsMonotoneArchSet (S : Set (ℝ × ℝ)) : Prop :=
  NonCrossing S ∧ NonConnecting S ∧ SameOrientation S

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), https://arxiv.org/abs/1907.00681; eq. (1) and Section 1 (pp. 4-5) for the completed graph and Graph^{*,+/-}; Definition 0.3 (pp. 3-4) for monotone sets of arches; Proposition 3.2 (p. 14) for regular levels; eq. (14) (p. 16) for the paired routes

Read-back

What the Lean code literally says, in plain math · claude-fable-5

All notions live on $\mathbb{R}$ with its Borel $\sigma$ -algebra and standard order topology; pairs $(a,b)\in\mathbb{R}^2$ are used both as points of a graph and as "routes/arches".

1. $F_\sigma$ (Fsigma). For two Borel measures $\mu,\nu$ on $\mathbb{R}$ (arbitrary — no finiteness is assumed in the definition itself) and $x\in\mathbb{R}$ , $F_\sigma(x)$ is the real number

F_\sigma(x)\;=\;\overline{\mu\big((-\infty,x]\big)}-\overline{\nu\big((-\infty,x]\big)},

where $\overline{\,\cdot\,}$ converts a value of $[0,\infty]$ to a real number by the total map that sends $\infty$ to $0$ . Thus if either measure gives infinite mass to $(-\infty,x]$ , that term silently contributes $0$ .

2. completedGraph. For a function $F:\mathbb{R}\to\mathbb{R}$ , the set of pairs $(x,y)$ such that

y\in\big[\min(F^-(x),F(x)),\;\max(F^-(x),F(x))\big],

where $F^-(x)$ is the left limit of $F$ at $x$ . $F^-$ is a total function: at a point where $F$ has no limit from the left, $F^-(x)$ is an arbitrary unspecified (junk) value, and the "vertical segment" at $x$ then joins $F(x)$ to that junk value. For every $x$ the graph contains at least $(x,F(x))$ .

3. levelSet. $L_F(h)$ is the set of $x\in\mathbb{R}$ with $(x,h)$ in the completed graph of $F$ , i.e. $h$ lies (inclusively) between $F^-(x)$ and $F(x)$ .

4. posPoints. The set of points $p=(x,h)$ of the completed graph of $F$ for which there exists $\varepsilon>0$ such that every point $q=(x',h')$ of the completed graph with $x'\neq x$ and $|x'-x|<\varepsilon$ (no restriction whatsoever on $h'$ ) satisfies

(h'-h)(x'-x)>0 \quad\text{strictly.}

5. negPoints. The same with the strict inequality reversed: every completed-graph point $(x',h')$ with $x'\neq x$ , $|x'-x|<\varepsilon$ satisfies

(h'-h)(x'-x)<0.

6. regularLevel $F$ , $h$ . There exist $n\in\mathbb{N}$ (possibly $n=0$ ) and a strictly increasing list of reals $x_0<x_1<\dots<x_{2n-1}$ such that:

(i) $L_F(h)=\{x_0,\dots,x_{2n-1}\}$ exactly (for $n=0$ this says $L_F(h)=\varnothing$ , and then all remaining conditions are vacuous);
(ii) each $(x_i,h)$ lies in posPoints $\cup$ negPoints;
(iii) for every index $i\in\{0,\dots,2n-1\}$ , $(x_i,h)\in$ posPoints holds if and only if the biconditional

(h>0)\iff(i\text{ is even})

holds.

So for $h>0$ the increasing points are exactly the even-indexed ones $x_0,x_2,\dots$ , while for $h\le 0$ (including $h=0$ ; the definition itself does not require $h\neq 0$ ) they are exactly the odd-indexed ones. Membership in negPoints is constrained only through (ii): where posPoints fails, negPoints must hold; where posPoints holds, simultaneous negPoints membership is not excluded by the definition.

7. pairedRoutes $\Gamma_F$ . The set of pairs $(a,b)\in\mathbb{R}^2$ such that there exists $h\in\mathbb{R}$ with $h\neq 0$ , $h$ a regular level of $F$ (in the exact sense above), $(a,h)\in$ posPoints $F$ , $(b,h)\in$ negPoints $F$ , and either

$h>0$ , $a<b$ , and no point of the open interval $(a,b)$ belongs to $L_F(h)$ ; or
$h<0$ , $b<a$ , and no point of the open interval $(b,a)$ belongs to $L_F(h)$ .

8. NonCrossing $S$ . For all $p,q\in S$ (including $p=q$ ), writing $I_p$ for the closed interval with endpoints $p_1,p_2$ taken in either order (a single point if $p_1=p_2$ ), at least one of:

$I_p\cap I_q=\varnothing$ ;
$I_p\cap I_q$ is a singleton $\{z\}$ for some $z$ ;
$I_p\subseteq I_q$ ;
$I_q\subseteq I_p$ .

(The case $p=q$ is trivially satisfied by the inclusion disjuncts.)

9. NonConnecting $S$ . For all $p,q\in S$ , if $\min(|p_2-p_1|,|q_2-q_1|)>0$ (i.e. both routes are non-degenerate) then $p_2\neq q_1$ . Degenerate routes ( $p_1=p_2$ ) are entirely unconstrained.

10. SameOrientation $S$ . For all $p,q\in S$ , if the closed interval $I_q$ is contained in the open interval $\big(\min(p_1,p_2),\max(p_1,p_2)\big)$ , then

(p_2-p_1)(q_2-q_1)\ge 0 \quad\text{(non-strict).}

If $p$ is degenerate the open interval is empty, so the hypothesis is unsatisfiable and such $p$ impose nothing; if $q$ is degenerate the conclusion holds trivially (product $=0$ ).

11. IsMonotoneArchSet $S$ . The conjunction of the three conditions

\texttt{NonCrossing}\,S\;\wedge\;\texttt{NonConnecting}\,S\;\wedge\;\texttt{SameOrientation}\,S.

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

Completed graph, crossings, and paired routes for Fσ=Fμ−FνF_\sigma = F_\mu - F_\nuFσ​=Fμ​−Fν​

Completed graph, crossings, and paired routes for $F_\sigma = F_\mu - F_\nu$