← Mathematical handbook

Population rank coefficients of bivariate copulas

These are population functionals, not finite-sample rank estimators. Spearman's footrule uses the convention with range [-1/2,1]. The conditional-distribution coefficient of Chatterjee is in Rank.Chatterjee.

noncomputable def ProbabilityTheory.Copula.spearmanRho (C : Copula 2) : ℝ

Spearman's rho: the Pearson correlation of the two uniform coordinates.

Equations

• C.spearmanRho = 12 * ∫ (x : Fin 2 → ↑unitInterval), ↑(x 0) * ↑(x 1) ∂C.toMeasure - 3

noncomputable def ProbabilityTheory.Copula.kendallTau (C : Copula 2) : ℝ

Kendall's tau, expressed as the self-concordance integral.

Equations

• C.kendallTau = 4 * ∫ (x : Fin 2 → ↑unitInterval), C.cdf x ∂C.toMeasure - 1

noncomputable def ProbabilityTheory.Copula.spearmanFootrule (C : Copula 2) : ℝ

Spearman's population footrule coefficient, normalized to [-1/2,1].

Equations

• C.spearmanFootrule = (6 * ∫ (t : ↑unitInterval), C.cdf ![t, t]) - 2

noncomputable def ProbabilityTheory.Copula.giniGamma (C : Copula 2) : ℝ

Gini's gamma, using the diagonal and antidiagonal sections of the copula.

Equations

• C.giniGamma = 4 * ((∫ (t : ↑unitInterval), C.cdf ![t, t]) + ∫ (t : ↑unitInterval), C.cdf ![t, unitInterval.symm t]) - 2

noncomputable def ProbabilityTheory.Copula.unitHalf : ↑unitInterval

The midpoint of the closed unit interval.

Equations

• ProbabilityTheory.Copula.unitHalf = ⟨1 / 2, ProbabilityTheory.Copula.unitHalf._proof_1⟩

noncomputable def ProbabilityTheory.Copula.blomqvistBeta (C : Copula 2) : ℝ

Blomqvist's beta, the population median concordance coefficient.

Equations

• C.blomqvistBeta = 4 * C.cdf ![ProbabilityTheory.Copula.unitHalf, ProbabilityTheory.Copula.unitHalf] - 1

theorem ProbabilityTheory.Copula.integrable_diagonal_cdf (C : Copula 2) : MeasureTheory.Integrable (fun (t : ↑unitInterval) => C.cdf ![t, t]) MeasureTheory.volume

theorem ProbabilityTheory.Copula.integrable_antidiagonal_cdf (C : Copula 2) : MeasureTheory.Integrable (fun (t : ↑unitInterval) => C.cdf ![t, unitInterval.symm t]) MeasureTheory.volume

theorem ProbabilityTheory.Copula.blomqvistBeta_mem_Icc (C : Copula 2) : C.blomqvistBeta ∈ Set.Icc (-1) 1

theorem ProbabilityTheory.Copula.kendallTau_mem_Icc (C : Copula 2) : C.kendallTau ∈ Set.Icc (-1) 1

theorem ProbabilityTheory.Copula.blomqvistBeta_mono {C D : Copula 2} (h : ∀ (u : Fin 2 → ↑unitInterval), C.cdf u ≤ D.cdf u) : C.blomqvistBeta ≤ D.blomqvistBeta

theorem ProbabilityTheory.Copula.spearmanFootrule_mono {C D : Copula 2} (h : ∀ (u : Fin 2 → ↑unitInterval), C.cdf u ≤ D.cdf u) : C.spearmanFootrule ≤ D.spearmanFootrule

theorem ProbabilityTheory.Copula.giniGamma_mono {C D : Copula 2} (h : ∀ (u : Fin 2 → ↑unitInterval), C.cdf u ≤ D.cdf u) : C.giniGamma ≤ D.giniGamma