Skip to content

Pairwise rank regions

Import Copula.Rank.Region, Copula.Rank, or Copula. The namespace ProbabilityTheory.Copula.RankRegion provides a common API for all ten pairs among Spearman's rho, Kendall's tau, Blomqvist's beta, Spearman's footrule, and Gini's gamma. It also exposes the exact xi–beta, xi–rho and xi–Blest regions.

All ten pairs have complete exact-region theorems. An exact-region theorem proves both that every copula satisfies the bounds and that every point satisfying them is attained by an actual Copula 2. All statements include singular copulas.

Coverage

Pair Status Public theorem or development
Footrule–tau Exact attainable_footrule_tau_iff
Gamma–tau Exact attainable_gamma_tau_iff
Footrule–gamma Exact attainable_footrule_gamma_iff
Beta–rho Exact attainable_beta_rho_iff
Beta–tau Exact attainable_beta_tau_iff
Beta–footrule Exact attainable_beta_footrule_iff
Beta–gamma Exact attainable_beta_gamma_iff
Rho–tau Exact attainable_rho_tau_iff
Rho–footrule Exact attainable_footrule_rho_iff
Rho–gamma Exact attainable_gamma_rho_iff
Xi–beta Exact attainable_xi_beta_iff
Xi–rho Exact attainable_xi_rho_iff
Xi–Blest Exact attainable_xi_blest_iff
Tau–footrule–beta Exact triple attainable_tau_footrule_beta_iff
Mean absolute distance–variance Exact attainable_mean_distance_variance_iff

For Chatterjee's directional coefficient \(x=\xi\) and Blomqvist's \(b=\beta\), attainable_xi_beta_iff proves the complete region \(0\le x\le1,\ -1\le b\le1,\ |b|^3\le2x\). The proof includes the sharp lower boundary, the upper fibre endpoint, and every point between them. Xi is directional: it is coordinate 1 given coordinate 0.

For the directional xi–rho pair, attainable_xi_rho_iff states \(0\le x\le1\) and \(|r|\le M_x\). The function XiRho.upperRhoAtXi defines the sharp \(M_x\) by the paper's explicit trigonometric/radical inverse, with \(M_0=0\) and \(M_1=1\).

For directional xi and Blest's weighted coefficient nu, attainable_xi_blest_iff gives the full parametric region. The fibre at \(x=1\) is \([-1,1]\); for the remaining fibres, an extremal parameter \(b\ge0\) gives \(x=\operatorname{xiFormula}(b)\) and \(|\nu|\le\operatorname{nuFormula}(b)\). Both boundary branches and all interior points have copula witnesses.

The three-coordinate tau–footrule–beta theorem additionally characterizes all triples \((t,p,b)\): beta lies in \([-1,1]\), footrule lies between \(3(1+b)^2/16-1/2\) and \(1-3(1-b)^2/8\), and tau lies between \(4p/3-1/3\) and \(2p/3+1/3\). Every such triple is attained by a copula.

The rho–footrule result also gives the full region of the mean absolute coordinate distance and its variance. The theorem attainable_mean_distance_variance_iff includes \(0\le m\le1/2\), the sharp lower variance MeanVariance.minimumVariance m, and the sharp upper variance MeanVariance.maximumVariance m, with witnesses for every intermediate value.

The exact statements are collected in Copula.Rank.Region.

Conventions and exact formulas

Write \(b=\beta\), \(p=\phi\) (footrule), \(g=\gamma\), \(t=\tau\), and \(r=\rho\). Footrule has range \([-1/2,1]\); the other four coefficients have range \([-1,1]\). This is the population footrule normalization in the rank coefficient guide.

Each row below is an if and only if characterization. The interval restriction in the second column is part of the theorem.

Coordinates First coordinate Bounds on the second coordinate
\((p,t)\) \(-1/2\le p\le1\) \(4p/3-1/3\le t\le2p/3+1/3\)
\((g,t)\) \(-1\le g\le1\) \(\max(2g/3-1/3,2g-1)\le t\le\min(2g/3+1/3,2g+1)\)
\((p,g)\) \(-1/2\le p\le1\) \(4p/3-1/3\le g\le\min(4p/3+1/6,2p/3+1/3)\)
\((b,r)\) \(-1\le b\le1\) \(3(1+b)^3/16-1\le r\le1-3(1-b)^3/16\)
\((b,t)\) \(-1\le b\le1\) \((1+b)^2/4-1\le t\le1-(1-b)^2/4\)
\((b,p)\) \(-1\le b\le1\) \(3(1+b)^2/16-1/2\le p\le1-3(1-b)^2/8\)
\((b,g)\) \(-1\le b\le1\) \(3(1+b)^2/8-1\le g\le1-3(1-b)^2/8\) 
import Copula.Rank.Region

open ProbabilityTheory.Copula.RankRegion

example : (0, 13 / 16) ∈ attainable .beta .rho := by
  rw [attainable_beta_rho_iff]
  norm_num

example : (13 / 16, 0) ∈ attainable .rho .beta := by
  rw [mem_attainable_swap, attainable_beta_rho_iff]
  norm_num

example : (-1 / 2, 0) ∉ attainable .footrule .gamma := by
  rw [attainable_footrule_gamma_iff]
  norm_num

attainable a b is the image of actual copulas in the stated coordinate order. mem_attainable_iff exposes the existential copula witness. mem_attainable_swap reverses the coordinates. Merely defining this set does not establish its boundary.

Proofs and witnesses

TauFootrule formalizes the diagonal argument of Kokol Bukovšek–Stopar, applying it directly to copula measures. TauGamma uses their reflection reduction and ordinal-sum boundary families. FootruleGamma proves the quadrilateral bounds with absolute moments and fills its boundary with mixtures.

BetaBounds proves the quadratic fixed-median bounds using diagonal envelopes and tent integrals. RhoBeta proves the cubic bounds with a squared-displacement certificate and median quadrant probabilities. Centered supplies ordinal sums with equal comonotonic edge blocks. In Beta, a centered half-turn simultaneously attains all four upper boundaries, and its reflection supplies the lower boundaries.

Mixtures preserve rho, beta, footrule, and gamma affinely. Tau varies continuously, but is generally quadratic in the mixture weight. fixed_coefficient_intermediate therefore uses the intermediate value theorem to fill each fixed-coordinate interval, including intervals of tau values. It does not assume tau is affine or its regions are convex.

The proofs use only this package and its existing mathlib dependency. CopulaTest.RankRegion checks boundary points, an interior point, exclusions, coordinate reversal, and imported contact points. Transitive axiom reports for all ten exact theorems use only propext, Classical.choice, and Quot.sound.

The exact rho–footrule boundary

For \(-1/2\le p\le1\), the sharp lower boundary is [ r_{\min}(p)=-1+2\left(\sqrt{\frac{1+2p}{3}}\right)^3. ] The upper boundary consists of the endpoint \((1,1)\) and the following polynomial arcs. For each integer \(N\ge1\), let \(L=1/(2N)\), \(R=1/(2(N+1))\), and \(0\le v\le L-R\).

  • Right half: \(m=R+N(N+1)v^2\) and \(q=R^2+2N(N+1)Rv^2+\frac23N(N+1)v^3\).
  • Left half: \(m=L-N(N+1)v^2\) and \(q=L^2-2N(N+1)Lv^2+\frac23N(N+1)v^3\).

In both cases \((p,r_{\max})=(1-3m,1-6q)\). The theorem attainable_footrule_rho_iff uses this parametrization through RhoFootrule.UpperParameter. Its definitions are arithmetic; they do not quantify over copulas or a variational optimum. The proof establishes coverage of every \(p\), uniqueness at junctions, global optimality, boundary attainment, and every intermediate rho value.

UpperSpline supplies the globally feasible periodic potential. UpperRightOptimal and UpperLeftOptimal verify the finite path mixtures, their uniform marginals, their moments, and equality in the dual bound. Lower supplies the complementary sharp inequality and its centered copula witnesses.

The exact rho–gamma boundary

The upper boundary is parametrized by auxiliary displacement certificates. For their parameters \(s,c,m,q\), set [ A=\frac{s+\sqrt{s^2+2c}}2,\qquad a=\frac A{1+A},\qquad z=\frac1{1+A}. ] The coordinates are [ g=1-2a^2-z^2m,\qquad r_{\max}=1-2a^3-\frac32z^3q. ] RhoGamma.UpperParameter includes the two endpoints, the half-shift branch \(s\ge1,\ c=3/8-s/2,\ m=1/2,\ q=1/4\), and the left and right auxiliary families used for rho–footrule. All coordinates are explicit arithmetic expressions. Reflection gives the lower boundary.

The theorem attainable_gamma_rho_iff proves membership exactly when gamma is in \([-1,1]\) and rho lies between the corresponding boundary values. Coverage proves every gamma coordinate is covered, including the limiting endpoints. GluedCertificate proves global dual feasibility and equality for actual copula measures; GluedMoments computes their coefficients. The proof fills all intermediate points by mixtures.

The exact rho–tau boundary

The Schreyer–Paulin–Trutschnig lower boundary consists of \((-1,-1)\) and the arcs below, with coordinates ordered as \((t,r)=(\tau,\rho)\). For every integer \(n\ge0\) and \(s\in[0,1]\), [ t_n(s)=-1+\frac2{n+2}+\frac{2s^2}{(n+1)(n+2)}, ] [ r_n(s)=-1+\frac2{(n+2)^2} +\frac{6s^2}{(n+1)(n+2)^2} -\frac{2ns^3}{(n+1)^2(n+2)^2}. ] The upper boundary is its reflection through the origin. attainable_rho_tau_iff characterizes membership using these arithmetic parameters (RhoTau.LowerParameter). Equivalently, if \(\Phi(t_n(s))=r_n(s)\) and \(\Phi(-1)=-1\), then [ -1\le t\le1,\qquad \Phi(t)\le r\le-\Phi(-t). ]

The proof follows the finite permutation reduction in Section 4 of Schreyer–Paulin–Trutschnig. PowerSums proves the symmetric minimum; SparseVariations and FourVariations eliminate the forbidden patterns; AdjacentSwap handles the remaining nonendpoint case. The swap argument redistributes the two swapped weights to preserve the inversion statistic exactly. FiniteReduction.finite_sharp_bound then proves the sharp inequality for every finite weighted permutation.

Quantization and GridMoments transfer this inequality to every copula using finite grid distributions and dominated convergence. Uniform marginals exclude coordinate ties; GridCollisions proves that the diagonal correction terms vanish. BoundaryFunction proves continuity and ordering across all arc junctions and at the limiting endpoint. Universal proves the sharp bound for arbitrary copulas. Finally, Exact uses reflection and continuity of tau along mixtures at fixed rho to attain every interior point. The proof includes singular copulas and does not assume a density.

Imported developments

The rho–footrule and rho–gamma proofs were adapted from Corrram/lean-verifications at commit 9e144da5e0d8e2b59dadf9cef090947cb2220313 (Apache 2.0). Each ported file records its original module. Imports and namespaces were adapted, and unused helpers were omitted; no dependency on that repository is required. These are the checked portions of the two developments listed on the source papers page.

Mathematical references

Library revision: fe53ea2f · Lean 4.34.0