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

crossingMultiplicity

For every function $F:\mathbb R\to\mathbb R$ and level $h\in\mathbb R$, let

$$G_F=\{(x,t):\min(\operatorname{leftLim}F(x),F(x))\le t\le\max(\operatorname{leftLim}F(x),F(x))\}.$$

A point $(x,t)\in G_F$ is positive when some $\varepsilon>0$ satisfies, for every $(y,s)\in G_F$,

$$|y-x|<\varepsilon\ \land\ y\ne x\quad\Longrightarrow\quad 0<(s-t)(y-x),$$

and is negative when the same condition instead implies $(s-t)(y-x)<0$. Then crossingMultiplicity F h is the extended-nonnegative-real sum of the cardinalities of the sets of $x$ for which $(x,h)$ is respectively positive and negative. A finite set contributes its ordinary cardinality and an infinite set contributes $+\infty$. No regularity or existence of an ordinary left limit is assumed: leftLim is used as a total operator even when $F$ has no ordinary left limit.

excursionLevelLaw

For arbitrary measures $\mu,\nu$ on $\mathbb R$, define

$$F_{\mu,\nu}(x)=\bigl(\mu((-\infty,x])\bigr)_{\mathbb R} -\bigl(\nu((-\infty,x])\bigr)_{\mathbb R},$$

where $(\cdot)_{\mathbb R}$ is extended-nonnegative-real conversion to a real number; in particular, $+\infty$ converts to $0$. At each $h$, form the sum $\theta(h)\in[0,\infty]$ of the extended cardinalities of the positive and negative completed-graph points at height $h$, where the completed graph and its positive and negative points are exactly those described under crossingMultiplicity, with $F=F_{\mu,\nu}$. Then excursionLevelLaw mu nu is

$$\frac12\cdot\bigl(\lambda\mathbin{\mathrm{withDensity}}\theta\bigr),$$

where $\lambda$ is Lebesgue measure. The declaration imposes no finiteness, probability, mutual-singularity, or measurability hypothesis on $\mu,\nu$ or on $\theta$.

pairedAtLevel

For $F:\mathbb R\to\mathbb R$ and $h\in\mathbb R$, use $G_F$ and its positive and negative points as expanded under crossingMultiplicity, and set $L_F(h)=\{x:(x,h)\in G_F\}$. Call $h$ regular precisely when there are $n\in\mathbb N$ and a strictly increasing family $x_i\in\mathbb R$, indexed by $i=0,\ldots,2n-1$, such that $L_F(h)=\{x_i:0\le i<2n\}$, every $(x_i,h)$ is positive or negative, and, for every $i$,

$$\bigl((x_i,h)\text{ is positive}\bigr) \quad\Longleftrightarrow\quad \bigl(h>0\Longleftrightarrow i\text{ is even}\bigr).$$

Then pairedAtLevel F h consists exactly of pairs $(a,b)$ such that $h\ne0$, $h$ is regular, $(a,h)$ is positive, $(b,h)$ is negative, and either

$$h>0,\quad a<b,\quad L_F(h)\cap(a,b)=\varnothing,$$

or

$$h<0,\quad b<a,\quad L_F(h)\cap(b,a)=\varnothing.$$

The natural number $n$ may be $0$, in which case regularity requires $L_F(h)=\varnothing$ and all indexed conditions are vacuous; such a level cannot nevertheless produce a pair because a pair also requires positive and negative points.

JuilletPairingData

For arbitrary measures $\mu,\nu$ on $\mathbb R$, a JuilletPairingData mu nu value is a package of functions $s_i,t_i:\mathbb R\to\mathbb R$ and sets $A_i\subseteq\mathbb R$, indexed by every $i\in\mathbb N$, satisfying all of the following. Each $s_i$ and $t_i$ is measurable, each $A_i$ is measurable, and $0\notin A_i$. Put $F(x)=(\mu((-\infty,x]))_{\mathbb R}-(\nu((-\infty,x]))_{\mathbb R}$, with $+\infty$ converting to $0$, and define its completed graph, positive points, negative points, regular levels, and paired points by the fully expanded conditions above. For Lebesgue-almost every $h$, $h\ne0$ implies that $h$ is regular. For Lebesgue-almost every $h$, simultaneously for every $i$, membership $h\in A_i$ implies that $(s_i(h),t_i(h))$ is paired at $h$, including all the nonzero, regularity, sign, ordering, and no-intermediate-level-point conditions in pairedAtLevel. For Lebesgue-almost every $h$, every positive completed-graph point $(x,h)$ at a nonzero regular level has exactly one index $i$ satisfying $h\in A_i$ and $s_i(h)=x$. Likewise, for Lebesgue-almost every $h$, every negative point $(y,h)$ at a nonzero regular level has exactly one index $i$ satisfying $h\in A_i$ and $t_i(h)=y$. Finally, for Lebesgue-almost every $h$, the set $\{i:h\in A_i\}$ is finite. These almost-everywhere fields may have different exceptional null sets. At $h=0$, the regular-level implication is vacuous and every $A_i$ is nevertheless required to exclude $0$; outside the asserted full-measure sets, the pairing, exhaustion, uniqueness, and finiteness conditions impose nothing.

excursionCouplingMeasure

For arbitrary implicit measures $\mu,\nu$ and any package $(s_i,t_i,A_i)_{i\in\mathbb N}$ satisfying every measurability, zero-exclusion, almost-everywhere regularity, expanded pairing, unique positive-source exhaustion, unique negative-target exhaustion, and finite-active-index condition stated in JuilletPairingData, excursionCouplingMeasure data is the measure on $\mathbb R^2$

$$\sum_{i\in\mathbb N}(h\mapsto(s_i(h),t_i(h)))_\# \bigl(\lambda|_{A_i}\bigr).$$

Equivalently, for every measurable $B\subseteq\mathbb R^2$, its value is

$$\sum_{i\in\mathbb N} \lambda\bigl(\{h\in A_i:(s_i(h),t_i(h))\in B\}\bigr).$$

Every active index contributes one full restricted-Lebesgue pushforward; the definition contains no normalization or division by the number of active indices. Null-set exceptional behavior does not affect these restricted measures.

IsJuilletExcursionCoupling

For arbitrary measures $\mu,\nu$ on $\mathbb R$ and an arbitrary measure $\gamma$ on $\mathbb R^2$, IsJuilletExcursionCoupling mu nu gamma asserts the conjunction of four requirements: $\gamma(\mathbb R^2)=1$; the pushforward of $\gamma$ by $(x,y)\mapsto x$ equals $\mu$; the pushforward by $(x,y)\mapsto y$ equals $\nu$; and there exist measurable functions $s_i,t_i:\mathbb R\to\mathbb R$ and measurable sets $A_i\subseteq\mathbb R$, indexed by $i\in\mathbb N$, satisfying all of the expanded JuilletPairingData conditions above for $F(x)=(\mu((-\infty,x]))_{\mathbb R}-(\nu((-\infty,x]))_{\mathbb R}$, such that

$$\gamma= \sum_{i\in\mathbb N}(h\mapsto(s_i(h),t_i(h)))_\# \bigl(\lambda|_{A_i}\bigr).$$

Thus the existential data must exclude $0$ from every $A_i$, satisfy regularity almost everywhere away from $0$, pair every active source and target almost everywhere by the fully expanded adjacent-crossing condition, uniquely enumerate all positive and negative crossings at almost every nonzero regular level, and have only finitely many active indices almost everywhere. No assumptions on $\mu$ or $\nu$ are premises; if the conjunction holds, their equality to the marginals of the probability measure $\gamma$ is part of what is asserted.