# Population rank dependence coefficients For jointly attainable values, see the [pairwise rank regions](rank-regions.md) guide: all ten exact regions, including sharp boundaries and interior attainment. Import `Copula.Rank` (or `Copula`) for the six bivariate coefficients. These are population functionals of a copula, not finite-sample rank statistics or numerical integration routines. Every definition applies to any `Copula 2`, including singular copulas. Write `C(u,v)` for the CDF, `dC` for the copula probability measure, and `K(u,[0,t])` for the conditional probability of the second coordinate being at most `t`, given that the first is `u`. Unspecified integrals below are with respect to uniform volume on the unit interval or square. | Lean accessor | Definition | Proved range | | --- | --- | --- | | `C.spearmanRho` | `12 ∫ uv dC(u,v) − 3`, also `12 ∫ C(u,v) du dv − 3` | `[-1,1]` | | `C.kendallTau` | `4 ∫ C(u,v) dC(u,v) − 1` | `[-1,1]` | | `C.spearmanFootrule` | `6 ∫ C(t,t) dt − 2` | `[-1/2,1]` | | `C.giniGamma` | `4 ∫ [C(t,t) + C(t,1−t)] dt − 2` | `[-1,1]` | | `C.blomqvistBeta` | `4 C(1/2,1/2) − 1` | `[-1,1]` | | `C.chatterjeeXi` | `6 ∫∫ K(u,[0,t])² du dt − 2` | `[0,1]` | The footrule normalization is the population copula convention in [Kokol Bukovšek and colleagues' treatment of footrule, gamma and beta](https://arxiv.org/abs/2009.06221). It is distinct from the unnormalized sum of absolute differences of sample ranks. In particular, its countermonotonic value is `−1/2`. ## Conditional CDFs and classical derivatives `Rank.ConditionalDerivative` proves that the conditional CDF equals the first partial derivative of the copula CDF almost everywhere in the conditioning coordinate, for every fixed threshold. `cdfSection C v` extends the section constantly outside the unit interval; its derivative agrees with the ordinary partial derivative in the interior, and endpoints have zero measure. `chatterjeeXi_eq_integral_deriv` therefore identifies the conditional-distribution definition of xi with the classical double integral of the squared derivative. The proof uses disintegration and the almost-everywhere fundamental theorem of calculus. It applies to singular copulas and requires no density assumption. `Rank.ChatterjeeCrossMixture` proves `chatterjeeCross_mix_right`, the affine mixture identity for the polarized xi functional. Together with the existing squared-distance and comonotonic cross-term identities, this supports sharp coefficient bounds by comparison with mixtures of independence and M. ## Checked benchmark values All entries in this table are proved and registered as simplification lemmas. They also establish that the stated range bounds are sharp. | Copula | rho | tau | footrule | gamma | beta | xi | | --- | ---: | ---: | ---: | ---: | ---: | ---: | | Independence `Π` | 0 | 0 | 0 | 0 | 0 | 0 | | Comonotonicity `M` | 1 | 1 | 1 | 1 | 1 | 1 | | Countermonotonicity `W` | −1 | −1 | −1/2 | −1 | −1 | 1 | For example: ```lean import Copula.Rank open ProbabilityTheory example (C : Copula 2) : C.chatterjeeXi ∈ Set.Icc 0 1 := C.chatterjeeXi_mem_Icc example : Copula.countermonotonic.chatterjeeXi = 1 := by simp ``` ## Equality cases and independence detection `Rank.Extrema` and `Rank.MedianExtrema` prove the equality cases: | Equality | Equivalent condition | | --- | --- | | `rho = 1`, `tau = 1`, `gamma = 1`, or `footrule = 1` | `C = M` | | `rho = −1`, `tau = −1`, or `gamma = −1` | `C = W` | | `beta = 1` | `C(1/2,1/2) = 1/2` | | `beta = −1` | `C(1/2,1/2) = 0` | | `footrule = −1/2` | `beta = −1`, also `δ(t) = max(0,2t−1)` for every t | The corresponding strict-bound lemmas are available, for example `spearmanRho_lt_one_iff` and `neg_one_lt_kendallTau_iff`. `Copula.Support` identifies M with almost-sure equality of the uniform coordinates and W with their sum being one almost surely. No density assumptions occur in these characterizations. The beta conditions do not determine the whole copula. Every ordinal sum with split `1/2` has beta 1; reflecting its second coordinate gives beta −1 and footrule −1/2. Choosing independent copulas as both components gives explicit witnesses different from M and W. Thus minimal footrule, unlike maximal footrule, does not determine a unique copula. `OrdinalSum.CutConsequences` supplies the converses: beta 1 characterizes ordinal sums with split `1/2`, with a unique component pair at that split; beta −1 characterizes their second-coordinate reflections. It follows that beta 1 forces `rho≥1/2`, `tau≥0`, and `footrule≥1/4`, whereas beta −1 forces `rho≤−1/2` and `tau≤0`. The equal-split W/W copula and its reflection attain these bounds. See the [decomposition API](ordinal-sums.md#converse-decomposition-and-unique-components). `Order.StrictSpearman` proves that distinct copulas comparable in lower orthant or concordance order have strictly different rho. Within either the PQD or NQD class, rho vanishes exactly at independence. The same equivalence holds for tau, using `rho ≤ 3 tau` for PQD and `3 tau ≤ rho` for NQD. These are conditional independence criteria: zero rho or tau alone is insufficient, as the equal M/W mixture already demonstrates. ## Concordance probabilities and Kendall's tau `C.concordanceQ D = 4 ∫ C dD − 1` is the bivariate concordance function Q. It is symmetric, belongs to `[-1,1]`, increases under lower orthant order in either argument, and equals Kendall's tau when both arguments are `C`. For independent observations `X ~ C` and `Y ~ D`, `concordantPairs` is the event `(X₀−Y₀)(X₁−Y₁)>0`; `discordantPairs` uses `<0`. In Lean their joint law is `C.toMeasure.prod D.toMeasure`. `Rank.ConcordanceProbability` proves ```text P(concordance) = (1+Q(C,D))/2 P(discordance) = (1−Q(C,D))/2 Q(C,D) = P(concordance) − P(discordance). ``` The probabilities sum to one. Uniform marginals imply that each coordinate has probability zero of a tie across these independent observations; no density is needed. Taking `D=C` gives Kendall's interpretation. Tau is `1` exactly when almost every pair is concordant, `−1` exactly when almost every pair is discordant, and zero exactly when those probabilities are equal. Zero tau does not in general imply independence. Pairing Q with the benchmarks links the classical coefficients: ```text Q(C,Π) = rho(C)/3 Q(C,M) = (2 footrule(C)+1)/3 Q(C,W) = gamma(C) − (2 footrule(C)+1)/3. ``` In particular `gamma(C)=Q(C,M)+Q(C,W)` and `Q(M,W)=0`. ## Chatterjee's direction and conditional distributions `C.chatterjeeXi` measures dependence of **coordinate 1 given coordinate 0**. To ask about the opposite direction, first swap the coordinates using `C.reindex ![1,0]`. The API does not symmetrize xi. `C.conditionalKernel` uses mathlib's regular conditional distribution; `C.conditionalCDF u t` is its real-valued mass on `Set.Iic t`. The library proves joint measurability, integrability, bounds between zero and one, and the identity `∫ K(u,[0,t]) du = t`. It also proves ```text xi(C) = 6 ∫∫ (K(u,[0,t]) − t)² du dt. ``` `chatterjeeXi_eq_of_kernel_ae` permits replacement by any almost-everywhere equal kernel version. `chatterjeeXi_eq_one_of_function` proves xi equals one when the second coordinate is almost surely a measurable function of the first. This includes both increasing and decreasing deterministic dependence. The conditional-distribution definition follows the population coefficient introduced in [Chatterjee, A new coefficient of correlation](https://arxiv.org/abs/1909.10140). Using a kernel avoids assuming a density or choosing pointwise derivatives of a singular copula. `chatterjeeXi_eq_zero_iff` now proves that xi is zero exactly at independence, and `chatterjeeXi_pos_iff` gives strict positivity for every other copula. Equivalence to a partial-derivative formula and the converse functional-dependence characterization at xi=1 are not yet formalized. The proof uses `conditionalCDFDistanceSq C D = ∫∫ (K_C−K_D)²`. This quantity is symmetric, nonnegative, and zero exactly when `C=D`; xi equals six times the squared distance to independence. `ext_conditionalCDF_ae` identifies copulas from nested almost-everywhere equality of their conditional CDFs. Continuity of the copula CDF handles exceptional threshold sets without assuming a jointly continuous conditional kernel. ## Algebra and family formulas `spearmanRho_eq_one_sub` and `spearmanRho_eq_neg_one_add` give the two square-distance identities `rho = 1 − 6 E[(U−V)²] = −1 + 6 E[(U+V−1)²]`. `spearmanRho_eq_integral_cdf` connects the moment and CDF definitions via Fubini. Rho, footrule, gamma and beta are proved monotone under pointwise CDF ordering. `Copula.Order.Rank` adds Kendall's tau using symmetry of the cross-concordance integral. `Copula.Order.Schur` proves monotonicity of xi in directional Schur order. See [comparison orders](orders.md) for the precise conventions. The `*_mix` theorems for rho, footrule, gamma and beta prove affine behavior under `Copula.mix C D a`, where `a` is the weight on `C`. Tau and xi have quadratic mixture identities. `Rank.KendallMixture` proves ```text tau(a C + (1−a) D) = a² tau(C) + (1−a)² tau(D) + 2a(1−a) Q(C,D) tau(∑ᵢ wᵢ Cᵢ) = ∑ᵢ ∑ⱼ wᵢ wⱼ Q(Cᵢ,Cⱼ). ``` The finite weights are nonnegative and sum to one. Q is affine in each argument separately. Mixing with independence gives `tau(a C+(1−a)Π)=a² tau(C)+(2/3)a(1−a)rho(C)`; mixing with M or W gives formulas involving footrule and gamma. In particular the equal mixture of M and Π has tau `5/12`, and `kendallTau_not_affine` formally rules out a general affine identity. The M/W segment has tau `2a−1`. `conditionalCDF_finiteMixture` and `conditionalCDF_mix` give almost-everywhere conditional CDF identities for finite and binary mixtures. The weights remain constant because the conditioning marginals are uniform. `Rank.ChatterjeeMixture` proves the exact quadratic identity ```text xi(a C + (1−a) D) = a xi(C) + (1−a) xi(D) − 6a(1−a) conditionalCDFDistanceSq(C,D). ``` Consequently xi is convex, and the inequality is strict when `C≠D` and `0