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

Definition

excursion_coupling

by ykanoria · Aug 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

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

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$