Stat.Coupling.Product­Loss­Monotone­Coupling

The signed tail representation of a real number

The elementary identity behind Hoeffding's covariance formula is that every real number is the Lebesgue integral of a signed tail indicator:

a = ∫ s, (𝟙{s < a} - 𝟙{s < 0}) ds.

Indeed the integrand vanishes outside the interval between 0 and a, where it equals +1 (if a ≥ 0) or -1 (if a < 0), so the integral is the signed length a.

This file packages that identity, its integrability, and the corresponding statements for the product signedTail x s * signedTail y t on ℝ × ℝ, which represents the product x * y as a two-dimensional Lebesgue integral:

x * y = ∫∫ (𝟙{s < x} - 𝟙{s < 0})(𝟙{t < y} - 𝟙{t < 0}) ds dt.

Together with the L¹ bound ∫∫ |·| = |x| * |y| (which is what makes the downstream Fubini swap legitimate for L² marginals, via Cauchy–Schwarz), this is the entire analytic input to hoeffding_cov_identity.

Probability integral transform (PIT) for the quantile function

This file proves the probability-integral-transform: if μ is a Borel probability measure on ℝ, then pushing the uniform measure on (0,1) through the (lower) quantile function Causalean.Stat.quantile μ recovers μ:

(volume.restrict (Ioo 0 1)).map (quantile μ) = μ.

The proof rests on the Galois characterisation quantile_le_iff from Causalean.Stat.Quantile:

quantile μ τ ≤ x ↔ τ ≤ cdf μ x (for interior 0 < τ < 1),

so that, writing U for a Unif(0,1) variable, P(quantile μ U ≤ x) = P(U ≤ cdf μ x) = cdf μ x, i.e. the pushforward and μ have the same values on every left-ray Iic x, hence are equal by Measure.ext_of_Iic.

These are the reusable primitives feeding the comonotone / countermonotone optimal couplings in Coupling.lean.

Couplings and the explicit monotone couplings

A coupling of two real probability measures μ, ν is a probability measure π on ℝ × ℝ whose two marginals are μ and ν. This file:

* defines IsCoupling π μ ν (probability measure with π.map Prod.fst = μ, π.map Prod.snd = ν), the Fréchet class Π(μ,ν); * defines the two extremal couplings built from the quantile transform: * comonotoneCoupling μ ν — pushforward of Unif(0,1) under u ↦ (quantile μ u, quantile ν u) (the comonotone / quantile coupling); * countermonotoneCoupling μ ν — pushforward under u ↦ (quantile μ u, quantile ν (1 - u)) (the countermonotone coupling); * proves each is genuinely a coupling of (μ, ν) (marginals via the PIT quantile_map_uniform, plus that u ↦ 1 - u preserves Unif(0,1)).

These are the optimizers whose optimality is established downstream.

Fréchet–Hoeffding bounds on the joint cdf

For a coupling π ∈ Π(μ, ν) with marginal cdfs F = cdf μ, G = cdf ν, the joint cdf H_π x y = π (Iic x ×ˢ Iic y) obeys the pointwise Fréchet–Hoeffding bounds

max (F x + G y - 1) 0 ≤ H_π x y ≤ min (F x) (G y).

The upper bound is H ≤ F and H ≤ G (monotonicity of measure under the two projections onto the marginals); the lower bound is inclusion–exclusion on the complement. Both bounds are attained:

• the comonotone coupling attains the upper bound H = min (F, G);
• the countermonotone coupling attains the lower bound H = max (F+G-1, 0).

This is the pointwise ordering that, integrated against the Hoeffding covariance identity, yields the optimality of the monotone couplings.

Survival functions of a coupling, and the survival-to-cdf bridge

For a coupling π ∈ Π(μ, ν) we record the two marginal survival functions and the joint survival function

SX s = π{p | s < p.1}, SY t = π{p | t < p.2}, S s t = π{p | s < p.1 ∧ t < p.2}.

Since π is a probability measure, complementation gives SX = 1 - F and SY = 1 - G, and inclusion–exclusion on the two half-planes gives S = 1 - F - G + H_π. The point of this file is the resulting survival gap = cdf gap identity

S s t - SX s * SY t = H_π s t - F s * G t,

which is what converts the Fubini computation of Cov_π (which naturally produces survival functions, because the tail indicator 𝟙{s < x} is a survival indicator) into the Fréchet-gap form used by the optimality theorem.

Sharp Fréchet-Hoeffding attainability for monotone quantile couplings

This file proves that the quantile couplings attain the Fréchet-Hoeffding bounds on the joint distribution function. The comonotone coupling realizes the upper envelope, and the countermonotone coupling realizes the lower envelope.

The resulting pointwise comparisons are the cdf-order inputs used by the product-expectation optimality theorem.

Hoeffding's covariance identity

For a coupling π ∈ Π(μ, ν) of two L² real measures, with marginal cdfs F = cdf μ, G = cdf ν and joint cdf H_π, Hoeffding's identity expresses the covariance as a double integral of the gap between the joint cdf and the product of the marginals:

Cov_π(X, Y) = ∫∫ (H_π x y - F x · G y) dx dy,

where Cov_π(X,Y) = E_π[XY] - E[X] E[Y].

Proof structure

Everything is assembled from HoeffdingFubini.lean and Survival.lean:

1. integral_prod_eq_integral_fiber : E_π[XY] = ∫ q, (∫ Φ q p ∂π) dq, where Φ q p = signedTail p.1 q.1 * signedTail p.2 q.2 is the product tail representation of p.1 * p.2. 2. fiber_integral_pi : the inner integral is S - 𝟙{t<0}·SX - 𝟙{s<0}·SY + 𝟙{s<0}·𝟙{t<0} in terms of survival functions. 3. mean_fst_tail, mean_snd_tail and integral_prod_mul : the product of the means is ∫ q, (SX q.1 - 𝟙{q.1<0})·(SY q.2 - 𝟙{q.2<0}) dq. 4. Subtracting (2) and (3) pointwise, the three inhomogeneous terms cancel and what remains is the survival gap S - SX·SY. 5. surv_gap_eq : the survival gap equals the Fréchet gap H_π - F·G.

The MemLp 2 hypotheses on the marginals enter exactly once, through Cauchy–Schwarz, to give E|XY| < ∞ and hence the Fubini domination.

The Fubini step in Hoeffding's covariance identity

Fix a coupling π ∈ Π(μ, ν) with L² marginals. Writing Φ q p = signedTail p.1 q.1 * signedTail p.2 q.2 for the product tail representation of p.1 * p.2 (see TailIntegral.lean), this file performs the two Fubini swaps that turn the moments of π into Lebesgue integrals of survival functions:

* integral_prod_eq_integral_fiber : E_π[XY] = ∫∫ (∫ Φ q p ∂π) dq; * mean_fst_tail / mean_snd_tail : E[X] = ∫ (SX s - 𝟙{s<0}) ds, likewise E[Y]; * fiber_integral_pi : the inner π-integral evaluates, by linearity of the expectation of a product of tail indicators, to S s t - 𝟙{t<0}·SX s - 𝟙{s<0}·SY t + 𝟙{s<0}·𝟙{t<0}.

The domination that legitimises both swaps is ∫∫ |Φ q p| dq = |p.1| * |p.2| (integral_norm_signedTail_prod), whose π-integral is finite by Cauchy–Schwarz on the L² marginals. Subtracting E[X]·E[Y] (rewritten as a double integral via integral_prod_mul) cancels the three inhomogeneous terms and leaves the survival gap S - SX·SY, which is the Fréchet gap by surv_gap_eq.

Orientation convention: all product measures are taken as (volume.prod volume).prod π, i.e. tail variables first, so that MeasureTheory.Integrable.integral_prod_left directly yields integrability of the fibre q ↦ ∫ Φ q p ∂π against Lebesgue×Lebesgue.

Integrability and Fubini swaps for Hoeffding's identity

This file proves the integrability bounds and Fubini swaps that turn the signed tail representation of the product into Lebesgue integrals of fibre expectations and marginal tail means.

The output supplies the integrable fibre and mean-tail formulas consumed by the final Hoeffding covariance identity.

Optimality of the monotone couplings (capstone)

Over the Fréchet class Π(μ, ν) of couplings of two L² real probability measures, the product expectation E_π[XY] = ∫ p, p.1 * p.2 ∂π is:

• maximised by the comonotone (quantile) coupling, and
• minimised by the countermonotone coupling.

The argument: by Hoeffding's identity E_π[XY] = E[X]E[Y] + ∫∫ (H_π - F·G). The term E[X]E[Y] depends only on the marginals μ, ν, hence is constant across Π(μ, ν); so extremising E_π[XY] is the same as extremising ∫∫ H_π. The Fréchet–Hoeffding bounds give this pointwise: H_π ≤ H_comonotone and H_countermonotone ≤ H_π, and monotonicity of the double integral lifts the pointwise ordering to the integrals.

A closed form for the optimum is also recorded: E[XY] under the comonotone coupling equals ∫_(0,1) quantile μ · quantile ν.