← Copula mathematical handbook

Spearman's rho of extreme-value copulas

For a Pickands dependence function A,

ρ(C_A) = 12 ∫₀¹ (A(t) + 1)⁻² dt - 3 (spearmanRho_pickandsCopula),

and hence ρ(C) = 12 ∫₀¹ (A_C(t) + 1)⁻² dt - 3 for every bivariate extreme-value copula (IsExtremeValue.spearmanRho_eq).

Proof. With ρ = 12 ∬ C_A - 3, substitute, for fixed v ∈ (0,1), u = v^{1/t - 1} (t = log v / log(uv) ∈ (0,1)), so that C_A(u,v) = v^{A(t)/t} and du = (-log v) t⁻² v^{1/t - 1} dt. After exchanging the order of integration (Tonelli), the inner integral is ∫₀¹ (-log v) v^{(A(t)+1)/t - 1} dv = t² / (A(t) + 1)², a Gamma integral (substitute v = e^{-s}). All integrals are computed as lower Lebesgue integrals of nonnegative functions, so no integrability bookkeeping is needed for the exchange.

References: G. Gudendorf and J. Segers, Extreme-value copulas (2010); W. Hürlimann, Hutchinson–Lai's conjecture for bivariate extreme value copulas (2003); P. Capéraà, A.-L. Fougères and C. Genest, A nonparametric estimation procedure for bivariate extreme value copulas (1997).

noncomputable def ProbabilityTheory.Copula.PickandsSpearman.extend (A : ℝ → ℝ) : ℝ → ℝ

A on (0,1), extended by 1: a measurable version of a Pickands function.

Equations

• ProbabilityTheory.Copula.PickandsSpearman.extend A = (Set.Ioo 0 1).piecewise A fun (x : ℝ) => 1

theorem ProbabilityTheory.Copula.PickandsSpearman.extend_eq {A : ℝ → ℝ} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : extend A t = A t

theorem ProbabilityTheory.Copula.PickandsSpearman.measurable_extend {A : ℝ → ℝ} (hA : IsPickandsFunction A) : Measurable (extend A)

theorem ProbabilityTheory.Copula.PickandsSpearman.extend_pos {A : ℝ → ℝ} (hA : IsPickandsFunction A) (t : ℝ) : 0 < extend A t

noncomputable def ProbabilityTheory.Copula.PickandsSpearman.kernel (A : ℝ → ℝ) (x y : ℝ) : ℝ

The Pickands CDF on (0,1)² as a function of two real variables.

Equations

• ProbabilityTheory.Copula.PickandsSpearman.kernel A x y = Real.exp (Real.log (x * y) * ProbabilityTheory.Copula.PickandsSpearman.extend A (Real.log y / Real.log (x * y)))

noncomputable def ProbabilityTheory.Copula.PickandsSpearman.kernelT (A : ℝ → ℝ) (t y : ℝ) : ℝ

The integrand after the substitution x = y^{1/t - 1}.

Equations

• ProbabilityTheory.Copula.PickandsSpearman.kernelT A t y = -Real.log y * (t⁻¹ ^ 2 * Real.exp (Real.log y * ((ProbabilityTheory.Copula.PickandsSpearman.extend A t + 1) * t⁻¹ - 1)))

theorem ProbabilityTheory.Copula.PickandsSpearman.measurable_kernelT {A : ℝ → ℝ} (hA : IsPickandsFunction A) : Measurable fun (p : ℝ × ℝ) => kernelT A p.2 p.1

theorem ProbabilityTheory.Copula.PickandsSpearman.kernelT_nonneg {A : ℝ → ℝ} {t y : ℝ} (hy : y ∈ Set.Ioo 0 1) : 0 ≤ kernelT A t y

noncomputable def ProbabilityTheory.Copula.PickandsSpearman.substMap (y t : ℝ) : ℝ

The substitution map t ↦ y ^ (1/t - 1) = exp(log y (1/t - 1)) of (0,1) onto itself.

Equations

• ProbabilityTheory.Copula.PickandsSpearman.substMap y t = Real.exp (Real.log y * (t⁻¹ - 1))

noncomputable def ProbabilityTheory.Copula.PickandsSpearman.substJac (y t : ℝ) : ℝ

The Jacobian |d/dt substMap y t| = (-log y) t⁻² substMap y t.

Equations

• ProbabilityTheory.Copula.PickandsSpearman.substJac y t = -Real.log y * (t⁻¹ ^ 2 * ProbabilityTheory.Copula.PickandsSpearman.substMap y t)

theorem ProbabilityTheory.Copula.PickandsSpearman.substMap_pos (y t : ℝ) : 0 < substMap y t

theorem ProbabilityTheory.Copula.PickandsSpearman.substJac_nonneg {y : ℝ} (hy : y ∈ Set.Ioo 0 1) (t : ℝ) : 0 ≤ substJac y t

theorem ProbabilityTheory.Copula.PickandsSpearman.lintegral_subst {y : ℝ} (hy : y ∈ Set.Ioo 0 1) (g : ℝ → ENNReal) : ∫⁻ (x : ℝ) in Set.Ioo 0 1, g x = ∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (substJac y t) * g (substMap y t)

The substitution x = y ^ (1/t - 1) for lower integrals over (0,1).

theorem ProbabilityTheory.Copula.PickandsSpearman.log_substMap_mul {y : ℝ} (hy : y ∈ Set.Ioo 0 1) (t : ℝ) : Real.log (substMap y t * y) = Real.log y * t⁻¹

theorem ProbabilityTheory.Copula.PickandsSpearman.ratio_substMap {y : ℝ} (hy : y ∈ Set.Ioo 0 1) (t : ℝ) : Real.log y / Real.log (substMap y t * y) = t

theorem ProbabilityTheory.Copula.PickandsSpearman.lintegral_gamma {b : ℝ} (hb0 : 0 < b) : ∫⁻ (y : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (-Real.log y * Real.exp (Real.log y * (b - 1))) = ENNReal.ofReal (1 / b ^ 2)

The Gamma integral ∫₀¹ (-log y) y^{b-1} dy = 1 / b² for b > 0.

theorem ProbabilityTheory.Copula.PickandsSpearman.lintegral_kernel {A : ℝ → ℝ} {y : ℝ} (hy : y ∈ Set.Ioo 0 1) : ∫⁻ (x : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (kernel A x y) = ∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (kernelT A t y)

The inner substitution x = exp(log y (1/t - 1)) for the Pickands CDF.

theorem ProbabilityTheory.Copula.PickandsSpearman.lintegral_kernelT {A : ℝ → ℝ} (hA : IsPickandsFunction A) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : ∫⁻ (y : ℝ) in Set.Ioo 0 1, ENNReal.ofReal (kernelT A t y) = ENNReal.ofReal (1 / (extend A t + 1) ^ 2)

The inner Gamma integral ∫₀¹ (-log y) y^{b-1} dy · t⁻² = (A(t) + 1)⁻².

theorem ProbabilityTheory.Copula.PickandsSpearman.lintegral_unitInterval_Ioo (G : ℝ → ENNReal) : ∫⁻ (u : ↑unitInterval), G ↑u = ∫⁻ (x : ℝ) in Set.Ioo 0 1, G x

theorem ProbabilityTheory.Copula.PickandsSpearman.cdf_eq_kernel {A : ℝ → ℝ} (hA : IsPickandsFunction A) {x y : ℝ} (hx : x ∈ Set.Ioo 0 1) (hy : y ∈ Set.Ioo 0 1) : (pickandsCopula A hA).cdf ![Set.projIcc 0 1 ⋯ x, Set.projIcc 0 1 ⋯ y] = kernel A x y

theorem ProbabilityTheory.Copula.PickandsSpearman.lintegral_cdf {A : ℝ → ℝ} (hA : IsPickandsFunction A) : ∫⁻ (x : Fin 2 → ↑unitInterval), ENNReal.ofReal ((pickandsCopula A hA).cdf x) ∂(independence 2).toMeasure = ENNReal.ofReal (∫ (t : ℝ) in Set.Ioo 0 1, 1 / (extend A t + 1) ^ 2)

The double integral ∬ C_A = ∫₀¹ (A(t) + 1)⁻² dt, as a lower Lebesgue integral.

theorem ProbabilityTheory.Copula.spearmanRho_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) : (pickandsCopula A hA).spearmanRho = (12 * ∫ (t : ℝ) in 0..1, 1 / (A t + 1) ^ 2) - 3

Spearman's rho of a Pickands copula: ρ(C_A) = 12 ∫₀¹ (A(t) + 1)⁻² dt - 3.

theorem ProbabilityTheory.Copula.IsExtremeValue.spearmanRho_eq {C : Copula 2} (hC : C.IsExtremeValue) : C.spearmanRho = (12 * ∫ (t : ℝ) in 0..1, 1 / (C.pickandsOf t + 1) ^ 2) - 3

Spearman's rho of a bivariate extreme-value copula: ρ(C) = 12 ∫₀¹ (A_C(t) + 1)⁻² dt - 3.