Juillet's excursion coupling as a completed-graph occupation measure

Definition

JuilletExcursionCoupling

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

measure-theoryoptimal-transportprobability

This definition formalizes Juillet's excursion coupling for mutually singular probability measures on the real line as the literal occupation measure of the completed-graph pairing construction.

For $F_\sigma=F_\mu-F_\nu$ , 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).

The level law $\theta/2$ has density $N(h)/2$ with respect to Lebesgue measure. Measurable branch data enumerate every increasing and decreasing crossing exactly once at almost every nonzero regular level and pair each increasing crossing with the adjacent decreasing crossing prescribed by the sign of the level. If $s_i(h)$ and $t_i(h)$ are these paired branches on their measurable active level sets $A_i$ , the resulting occupation measure is

\gamma_{\mathrm{EC}} = \sum_{i\in\mathbb N} \bigl(h\mapsto(s_i(h),t_i(h))\bigr)_\# \bigl(\mathcal L^1\!\restriction A_i\bigr).

A measure is a Juillet excursion coupling precisely when it is a probability measure with marginals $\mu,\nu$ and is exactly this occupation measure. Thus the definition records the completed-graph construction itself, rather than merely requiring concentration on the set of admissible paired routes.

Formalization Note Countably many measurable branches are used only to represent the finite collection of pairs at almost every level. The exhaustive-uniqueness fields make the resulting sum independent of unused branch values and of null exceptional levels.

Definition code

import Definitions.Def_excursion_coupling
import Mathlib.MeasureTheory.Measure.WithDensity

namespace ExcursionCoupling

open MeasureTheory Set Function

/-- The total number of increasing and decreasing completed-graph crossings
at a level, viewed as an extended nonnegative real number. -/
noncomputable def crossingMultiplicity (F : Real -> Real) (h : Real) : ENNReal :=
  ({x | (x, h) ∈ posPoints F}.encard.toENNReal) +
    ({x | (x, h) ∈ negPoints F}.encard.toENNReal)

/-- Juillet's law `theta / 2` for the randomly sampled completed-graph level. -/
noncomputable def excursionLevelLaw
    (mu nu : Measure Real) : Measure Real :=
  (2 : ENNReal)⁻¹ •
    (volume.withDensity (crossingMultiplicity (Fsigma mu nu)))

/-- The increasing crossing and its adjacent decreasing crossing at one
nonzero regular level, with the orientation prescribed by the sign. -/
def pairedAtLevel
    (F : Real -> Real) (h : Real) : Set (Real × Real) :=
  {r |
    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))}

/-- Measurable branch data for Juillet's completed-graph construction.
At almost every nonzero level, the active indices enumerate every increasing
and every decreasing crossing exactly once and pair adjacent crossings. -/
structure JuilletPairingData (mu nu : Measure Real) where
  source : Nat -> Real -> Real
  target : Nat -> Real -> Real
  active : Nat -> Set Real
  source_measurable : ∀ i, Measurable (source i)
  target_measurable : ∀ i, Measurable (target i)
  active_measurable : ∀ i, MeasurableSet (active i)
  active_nonzero : ∀ i, active i ⊆ {0}ᶜ
  regular_levels :
    ∀ᵐ h ∂(volume : Measure Real),
      h ≠ 0 -> regularLevel (Fsigma mu nu) h
  paired_ae :
    ∀ᵐ h ∂(volume : Measure Real),
      ∀ i, h ∈ active i ->
        (source i h, target i h) ∈ pairedAtLevel (Fsigma mu nu) h
  sources_exhaustive_unique_ae :
    ∀ᵐ h ∂(volume : Measure Real),
      ∀ x, h ≠ 0 -> regularLevel (Fsigma mu nu) h ->
        (x, h) ∈ posPoints (Fsigma mu nu) ->
          ∃! i : Nat, h ∈ active i ∧ source i h = x
  targets_exhaustive_unique_ae :
    ∀ᵐ h ∂(volume : Measure Real),
      ∀ y, h ≠ 0 -> regularLevel (Fsigma mu nu) h ->
        (y, h) ∈ negPoints (Fsigma mu nu) ->
          ∃! i : Nat, h ∈ active i ∧ target i h = y
  finite_active_ae :
    ∀ᵐ h ∂(volume : Measure Real), {i | h ∈ active i}.Finite

/-- The joint law obtained by integrating one atom at every adjacent
increasing/decreasing crossing pair over the completed-graph levels. This is
equivalent to sampling `H` with law `theta / 2` and then choosing uniformly
among the pairs at level `H`. -/
noncomputable def excursionCouplingMeasure
    {mu nu : Measure Real} (data : JuilletPairingData mu nu) :
    Measure (Real × Real) :=
  Measure.sum fun i =>
    Measure.map (fun h => (data.source i h, data.target i h))
      ((volume : Measure Real).restrict (data.active i))

/-- A measure is Juillet's excursion coupling when it has the prescribed
marginals and is exactly the completed-graph occupation measure. -/
def IsJuilletExcursionCoupling
    (mu nu : Measure Real) (gamma : Measure (Real × Real)) : Prop :=
  IsProbabilityMeasure gamma ∧
    gamma.map Prod.fst = mu ∧
      gamma.map Prod.snd = nu ∧
        ∃ data : JuilletPairingData mu nu,
          gamma = excursionCouplingMeasure data

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), Section 1, pp. 4-5, Theorem 1.1 and Remark 1.2; Section 3.1, eq. (14), p. 16

View graph