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 0df444a (Lean v4.33.1)

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

View graph