← Copula mathematical handbook

Scarsini's axioms for measures of concordance

Following Scarsini (1984) and Nelsen, An Introduction to Copulas, 2nd ed., Definition 5.1.7, a numerical measure κ of association, expressed through the copula of a continuous pair (X, Y), is a measure of concordance if

1. it is defined for every copula (automatic for a function Copula 2 → ℝ);
2. -1 ≤ κ(C) ≤ 1, κ(M) = 1 and κ(W) = -1;
3. κ(Cᵀ) = κ(C) (symmetry, κ_{Y,X} = κ_{X,Y});
4. κ(Π) = 0 (independence);
5. reflecting either coordinate changes the sign: κ_{-X,Y} = κ_{X,-Y} = -κ_{X,Y};
6. coherence: C ≤ D pointwise implies κ(C) ≤ κ(D);
7. continuity: if Cₙ → C pointwise then κ(Cₙ) → κ(C).

Pointwise convergence of copulas is equivalent to uniform convergence (tendstoUniformly_cdf_iff); IsMeasureOfConcordance.tendsto_of_tendstoUniformly restates property 7 in uniform form.

We prove that Spearman's rho, Kendall's tau, Blomqvist's beta and Gini's gamma are measures of concordance (Nelsen, §5.1), derive the standard consequences (Nelsen, §5.1: perfect positive/negative dependence gives ±1; invariance under the survival transformation; vanishing for copulas invariant under one reflection; signs under quadrant dependence), and show that Chatterjee's xi, the Schweizer–Wolff sigma, Hoeffding's Φ² and Spearman's footrule are not measures of concordance: the first three take the value 1 at both Fréchet bounds, which contradicts the reflection axiom, and the footrule takes the value -1/2 at W.

structure ProbabilityTheory.Copula.IsMeasureOfConcordance (κ : Copula 2 → ℝ) : Prop

Scarsini's axioms for a measure of concordance (Nelsen, Definition 5.1.7). Property 1 (definedness for every pair of continuous random variables) is built into the type.

• mem_Icc (C : Copula 2) : κ C ∈ Set.Icc (-1) 1

  Property 2: values in [-1, 1].

• comonotonic : κ (Copula.comonotonic 2) = 1

  Property 2: κ(M) = 1.

• countermonotonic : κ Copula.countermonotonic = -1

  Property 2: κ(W) = -1.

• transpose (C : Copula 2) : κ C.transpose = κ C

  Property 3: symmetry in the two coordinates.

• independence : κ (Copula.independence 2) = 0

  Property 4: independence has concordance zero.

• reflect_first (C : Copula 2) : κ (C.reflect {0}) = -κ C

  Property 5: reflecting the first coordinate changes the sign.

• reflect_second (C : Copula 2) : κ (C.reflect {1}) = -κ C

  Property 5: reflecting the second coordinate changes the sign.

• mono (C D : Copula 2) : C.LowerOrthantLE D → κ C ≤ κ D

  Property 6: coherence with the pointwise (concordance) order.

• tendsto (C : ℕ → Copula 2) (D : Copula 2) : (∀ (u : Fin 2 → ↑unitInterval), Filter.Tendsto (fun (n : ℕ) => (C n).cdf u) Filter.atTop (nhds (D.cdf u))) → Filter.Tendsto (fun (n : ℕ) => κ (C n)) Filter.atTop (nhds (κ D))

  Property 7: continuity under pointwise convergence of copulas.

theorem ProbabilityTheory.Copula.IsMeasureOfConcordance.tendsto_of_tendstoUniformly {κ : Copula 2 → ℝ} (h : IsMeasureOfConcordance κ) (C : ℕ → Copula 2) (D : Copula 2) (hC : TendstoUniformly (fun (n : ℕ) => (C n).cdf) D.cdf Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => κ (C n)) Filter.atTop (nhds (κ D))

Property 7 in the equivalent form of uniform convergence of the CDFs.

theorem ProbabilityTheory.Copula.IsMeasureOfConcordance.survivalCopula {κ : Copula 2 → ℝ} (h : IsMeasureOfConcordance κ) (C : Copula 2) : κ C.survivalCopula = κ C

Measures of concordance are invariant under the survival transformation C ↦ Ĉ (reflection of both coordinates, κ_{-X,-Y} = κ_{X,Y}).

theorem ProbabilityTheory.Copula.IsMeasureOfConcordance.eq_zero_of_reflect_first_eq {κ : Copula 2 → ℝ} (h : IsMeasureOfConcordance κ) {C : Copula 2} (hC : C.reflect {0} = C) : κ C = 0

A copula invariant under reflection of the first coordinate has concordance zero.

theorem ProbabilityTheory.Copula.IsMeasureOfConcordance.eq_zero_of_reflect_second_eq {κ : Copula 2 → ℝ} (h : IsMeasureOfConcordance κ) {C : Copula 2} (hC : C.reflect {1} = C) : κ C = 0

A copula invariant under reflection of the second coordinate has concordance zero.

theorem ProbabilityTheory.Copula.IsMeasureOfConcordance.eq_one_of_ae_eq {κ : Copula 2 → ℝ} (h : IsMeasureOfConcordance κ) {C : Copula 2} (hC : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 0 = x 1) : κ C = 1

Nelsen, §5.1: if Y is almost surely an increasing function of X (the copula is M), the concordance is 1.

theorem ProbabilityTheory.Copula.IsMeasureOfConcordance.eq_neg_one_of_ae_eq_symm {κ : Copula 2 → ℝ} (h : IsMeasureOfConcordance κ) {C : Copula 2} (hC : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 1 = unitInterval.symm (x 0)) : κ C = -1

Nelsen, §5.1: if Y is almost surely a decreasing function of X (the copula is W), the concordance is -1.

theorem ProbabilityTheory.Copula.IsMeasureOfConcordance.nonneg_of_isPQD {κ : Copula 2 → ℝ} (h : IsMeasureOfConcordance κ) {C : Copula 2} (hC : C.IsPQD) : 0 ≤ κ C

Positive quadrant dependence forces a nonnegative concordance.

theorem ProbabilityTheory.Copula.IsMeasureOfConcordance.nonpos_of_isNQD {κ : Copula 2 → ℝ} (h : IsMeasureOfConcordance κ) {C : Copula 2} (hC : C.IsNQD) : κ C ≤ 0

Negative quadrant dependence forces a nonpositive concordance.

theorem ProbabilityTheory.Copula.IsMeasureOfConcordance.mono_concordanceLE {κ : Copula 2 → ℝ} (h : IsMeasureOfConcordance κ) {C D : Copula 2} (hCD : C.ConcordanceLE D) : κ C ≤ κ D

A measure of concordance is nondecreasing along the concordance order.

theorem ProbabilityTheory.Copula.IsMeasureOfConcordance.convexComb {κ κ' : Copula 2 → ℝ} (h : IsMeasureOfConcordance κ) (h' : IsMeasureOfConcordance κ') {a : ℝ} (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) : IsMeasureOfConcordance fun (C : Copula 2) => a * κ C + (1 - a) * κ' C

Convex combinations of measures of concordance are measures of concordance.

theorem ProbabilityTheory.Copula.IsMeasureOfConcordance.comonotonic_ne_countermonotonic {κ : Copula 2 → ℝ} (h : IsMeasureOfConcordance κ) : κ (Copula.comonotonic 2) ≠ κ Copula.countermonotonic

A functional taking the same value at both Fréchet bounds violates the axioms.

The four classical measures of concordance

theorem ProbabilityTheory.Copula.isMeasureOfConcordance_spearmanRho : IsMeasureOfConcordance spearmanRho

Spearman's rho is a measure of concordance.

theorem ProbabilityTheory.Copula.isMeasureOfConcordance_kendallTau : IsMeasureOfConcordance kendallTau

Kendall's tau is a measure of concordance.

theorem ProbabilityTheory.Copula.isMeasureOfConcordance_blomqvistBeta : IsMeasureOfConcordance blomqvistBeta

Blomqvist's beta is a measure of concordance.

theorem ProbabilityTheory.Copula.isMeasureOfConcordance_giniGamma : IsMeasureOfConcordance giniGamma

Gini's gamma is a measure of concordance.

Coefficients that are not measures of concordance

theorem ProbabilityTheory.Copula.chatterjeeXi_reflect_second_comonotonic : ((comonotonic 2).reflect {1}).chatterjeeXi ≠ -(comonotonic 2).chatterjeeXi

Chatterjee's xi violates the reflection axiom: reflecting M gives W, but ξ(W) = ξ(M) = 1.

theorem ProbabilityTheory.Copula.not_isMeasureOfConcordance_chatterjeeXi : ¬IsMeasureOfConcordance chatterjeeXi

Chatterjee's xi is not a measure of concordance.

theorem ProbabilityTheory.Copula.schweizerWolff_reflect_second_comonotonic : ((comonotonic 2).reflect {1}).schweizerWolff ≠ -(comonotonic 2).schweizerWolff

The Schweizer–Wolff sigma violates the reflection axiom.

theorem ProbabilityTheory.Copula.not_isMeasureOfConcordance_schweizerWolff : ¬IsMeasureOfConcordance schweizerWolff

The Schweizer–Wolff sigma is not a measure of concordance.

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_reflect_second_comonotonic : ((comonotonic 2).reflect {1}).hoeffdingPhiSq ≠ -(comonotonic 2).hoeffdingPhiSq

Hoeffding's Φ² violates the reflection axiom.

theorem ProbabilityTheory.Copula.not_isMeasureOfConcordance_hoeffdingPhiSq : ¬IsMeasureOfConcordance hoeffdingPhiSq

Hoeffding's Φ² is not a measure of concordance.

theorem ProbabilityTheory.Copula.not_isMeasureOfConcordance_spearmanFootrule : ¬IsMeasureOfConcordance spearmanFootrule

Spearman's footrule takes the value -1/2 at W, so it is not a measure of concordance (it also violates the reflection axiom at M).