← Copula mathematical handbook

Spearman's rho of the Raftery family

For the Raftery copula C_θ (0 ≤ θ < 1, exponent p = 1/(1-θ)) Spearman's rho is

ρ(C_θ) = θ(4 - 3θ)/(2 - θ)² (spearmanRho_raftery; Nelsen 2006, exercises of Ch. 5).

The double integral ∫∫ C_θ splits along the diagonal. Below the diagonal (u ≤ v) the inner integral in u is elementary; above it, the integrand v + v^p (u^p - u^{1-p})/(2p-1) is integrated in v after exchanging the order of integration (Fubini), so that no integral of u^{1-p} (logarithmic at p = 2) is needed. Both triangles contribute ∫₀¹ (x²/2 + (x^{2p+1} - x²)/((2p-1)(p+1))) dx, which gives ρ = 1 - 4/(p+1)².

theorem ProbabilityTheory.Copula.RafterySpearman.integral_branch {p : ℝ} (hp : 1 ≤ p) (c x : ℝ) : ∫ (t : ℝ) in 0..x, t + c * t ^ p = x ^ 2 / 2 + c * x ^ (p + 1) / (p + 1)

noncomputable def ProbabilityTheory.Copula.RafterySpearman.G (p x : ℝ) : ℝ

The common value of the two triangle integrals, in closed form.

Equations

• ProbabilityTheory.Copula.RafterySpearman.G p x = x ^ 2 / 2 + (x ^ (2 * p + 1) - x ^ 2) / ((2 * p - 1) * (p + 1))

theorem ProbabilityTheory.Copula.RafterySpearman.branch_value {p : ℝ} (hp : 1 ≤ p) {x : ℝ} (hx : 0 ≤ x) : x ^ 2 / 2 + (x ^ p - x ^ (1 - p)) / (2 * p - 1) * x ^ (p + 1) / (p + 1) = G p x

noncomputable def ProbabilityTheory.Copula.RafterySpearman.lower (p : ℝ) (v u : ↑unitInterval) : ℝ

The part of the Raftery CDF below the diagonal, as a function of (v, u).

Equations

• ProbabilityTheory.Copula.RafterySpearman.lower p v u = if ↑u ≤ ↑v then ↑u + ↑u ^ p * (↑v ^ p - ↑v ^ (1 - p)) / (2 * p - 1) else 0

noncomputable def ProbabilityTheory.Copula.RafterySpearman.upper (p : ℝ) (v u : ↑unitInterval) : ℝ

The part of the Raftery CDF above the diagonal, as a function of (v, u).

Equations

• ProbabilityTheory.Copula.RafterySpearman.upper p v u = if ↑u ≤ ↑v then 0 else ↑v + ↑v ^ p * (↑u ^ p - ↑u ^ (1 - p)) / (2 * p - 1)

theorem ProbabilityTheory.Copula.RafterySpearman.core_eq {p : ℝ} (v u : ↑unitInterval) : Raftery.core p ↑u ↑v = lower p v u + upper p v u

theorem ProbabilityTheory.Copula.RafterySpearman.measurable_lower (p : ℝ) : Measurable (Function.uncurry (lower p))

theorem ProbabilityTheory.Copula.RafterySpearman.measurable_upper (p : ℝ) : Measurable (Function.uncurry (upper p))

theorem ProbabilityTheory.Copula.RafterySpearman.abs_core_le {p : ℝ} (hp : 1 ≤ p) (u v : ↑unitInterval) : |Raftery.core p ↑u ↑v| ≤ 1

theorem ProbabilityTheory.Copula.RafterySpearman.abs_lower_le {p : ℝ} (hp : 1 ≤ p) (v u : ↑unitInterval) : |lower p v u| ≤ 1

theorem ProbabilityTheory.Copula.RafterySpearman.abs_upper_le {p : ℝ} (hp : 1 ≤ p) (v u : ↑unitInterval) : |upper p v u| ≤ 1

theorem ProbabilityTheory.Copula.RafterySpearman.integrable_upper {p : ℝ} (hp : 1 ≤ p) : MeasureTheory.Integrable (Function.uncurry (upper p)) (MeasureTheory.volume.prod MeasureTheory.volume)

theorem ProbabilityTheory.Copula.RafterySpearman.integrable_lower_section {p : ℝ} (hp : 1 ≤ p) (v : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => lower p v u) MeasureTheory.volume

theorem ProbabilityTheory.Copula.RafterySpearman.integrable_upper_section {p : ℝ} (hp : 1 ≤ p) (v : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => upper p v u) MeasureTheory.volume

theorem ProbabilityTheory.Copula.RafterySpearman.integral_lower {p : ℝ} (hp : 1 ≤ p) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), lower p v u = G p ↑v

The inner integral below the diagonal.

theorem ProbabilityTheory.Copula.RafterySpearman.integral_upper {p : ℝ} (hp : 1 ≤ p) (u : ↑unitInterval) : ∫ (v : ↑unitInterval), upper p v u = G p ↑u

The inner integral above the diagonal, after exchanging the order of integration.

theorem ProbabilityTheory.Copula.RafterySpearman.integral_G {p : ℝ} (hp : 1 ≤ p) : ∫ (x : ↑unitInterval), G p ↑x = 1 / 6 + (1 / (2 * p + 2) - 1 / 3) / ((2 * p - 1) * (p + 1))

theorem ProbabilityTheory.Copula.spearmanRho_raftery {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) : (raftery θ h0 h1).spearmanRho = θ * (4 - 3 * θ) / (2 - θ) ^ 2

Spearman's rho of the Raftery copula: ρ(C_θ) = θ(4 - 3θ)/(2 - θ)².