← Copula mathematical handbook

Spearman's rho of the Plackett family

For the Plackett copula C_θ (θ > 0, θ ≠ 1) the inner integral is elementary: writing disc(u,v) = x² + 4θv(1-v) with x = (θ-1)u + 1 - (θ+1)v, a primitive of √disc in u is (x √disc + 4θv(1-v) log(x + √disc)) / (2(θ-1)), and the logarithmic boundary terms combine to log θ. This gives

∫₀¹ C_θ(u,v) du = v/2 + v(1-v) (θ² - 1 - 2θ log θ) / (2(θ-1)²)

(PlackettSpearman.integral_plackettCDF) and hence Mardia's formula (K. V. Mardia, Some contributions to contingency-type bivariate distributions, Biometrika 54 (1967); see Nelsen 2006, §3.3.1):

ρ(C_θ) = (θ + 1)/(θ - 1) - 2θ log θ/(θ - 1)² (spearmanRho_plackett), with ρ(C_1) = 0.

theorem ProbabilityTheory.Copula.PlackettSpearman.plackettDisc_eq_sq_add (θ u v : ℝ) : plackettDisc θ u v = ((θ - 1) * u + 1 - (θ + 1) * v) ^ 2 + 4 * θ * v * (1 - v)

noncomputable def ProbabilityTheory.Copula.PlackettSpearman.sqrtPrimitive (θ v u : ℝ) : ℝ

A primitive of u ↦ √disc(u,v) for 0 < v < 1.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.PlackettSpearman.hasDerivAt_sqrtPrimitive {θ v : ℝ} (hθ : 0 < θ) (hθ1 : θ ≠ 1) (hv0 : 0 < v) (hv1 : v < 1) (u : ℝ) : HasDerivAt (sqrtPrimitive θ v) (√(plackettDisc θ u v)) u

noncomputable def ProbabilityTheory.Copula.PlackettSpearman.innerIntegral (θ v : ℝ) : ℝ

The closed form of the inner integral ∫₀¹ C_θ(u,v) du.

Equations

• ProbabilityTheory.Copula.PlackettSpearman.innerIntegral θ v = v / 2 + v * (1 - v) * (θ ^ 2 - 1 - 2 * θ * Real.log θ) / (2 * (θ - 1) ^ 2)

noncomputable def ProbabilityTheory.Copula.PlackettSpearman.cdfPrimitive (θ v u : ℝ) : ℝ

A primitive of u ↦ C_θ(u,v).

Equations

• ProbabilityTheory.Copula.PlackettSpearman.cdfPrimitive θ v u = (u + (θ - 1) * (u ^ 2 / 2 + v * u) - ProbabilityTheory.Copula.PlackettSpearman.sqrtPrimitive θ v u) / (2 * (θ - 1))

theorem ProbabilityTheory.Copula.PlackettSpearman.hasDerivAt_cdfPrimitive {θ v : ℝ} (hθ : 0 < θ) (hθ1 : θ ≠ 1) (hv0 : 0 < v) (hv1 : v < 1) (u : ℝ) : HasDerivAt (cdfPrimitive θ v) (plackettCDF θ u v) u

theorem ProbabilityTheory.Copula.PlackettSpearman.sqrt_plackettDisc_zero_left {θ v : ℝ} (hθ : 0 < θ) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : √(plackettDisc θ 0 v) = 1 + (θ - 1) * v

theorem ProbabilityTheory.Copula.PlackettSpearman.sqrt_plackettDisc_one_left {θ v : ℝ} (hθ : 0 < θ) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : √(plackettDisc θ 1 v) = θ - (θ - 1) * v

theorem ProbabilityTheory.Copula.PlackettSpearman.integral_plackettCDF {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≠ 1) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), plackettCDF θ ↑u ↑v = innerIntegral θ ↑v

The inner integral of the Plackett copula, for every v ∈ [0,1] and θ ≠ 1.

theorem ProbabilityTheory.Copula.spearmanRho_plackett {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≠ 1) : (plackett θ hθ).spearmanRho = (θ + 1) / (θ - 1) - 2 * θ * Real.log θ / (θ - 1) ^ 2

Spearman's rho of the Plackett copula (Mardia 1967; Nelsen 2006, §3.3.1): ρ(C_θ) = (θ + 1)/(θ - 1) - 2θ log θ/(θ - 1)² for θ ≠ 1.

theorem ProbabilityTheory.Copula.spearmanRho_plackett_one : (plackett 1 ⋯).spearmanRho = 0

ρ(C_1) = ρ(Π) = 0.