← Copula mathematical handbook

Kendall's tau of the Raftery family

For the Raftery copula C_θ (0 ≤ θ < 1, exponent p = 1/(1-θ), see Copula.Families.Raftery) Kendall's tau is

τ(C_θ) = 2θ / (3 - θ) (kendallTau_raftery; Nelsen 2006, exercises of Ch. 5),

equivalently τ = 2(p-1)/(2p+1).

Proof. By kendallTau_conditional_product and exchangeability, τ = 1 - 4 ∬ ∂₁C ∂₂C. The conditional distribution functions agree almost everywhere with the classical partial derivatives (conditionalCDF_eq_deriv), which are explicit on both sides of the diagonal (Raftery.condDeriv; the two branches meet continuously on the diagonal). Below the diagonal (t ≤ x) the product of the partial derivatives is ∂₂C · ∂₁C = c(x) t^p/(2p-1) + p c(x) (x^p - x^{1-p}) t^{2p-1}/(2p-1)² with c(x) = p x^{p-1} + (p-1) x^{-p}, whose integral over t ∈ [0,x] is elementary (integral_partialProduct); above the diagonal the same integral appears after Fubini. Hence ∬ ∂₁C ∂₂C = 2 ∫₀¹ L = 3/(4(2p+1)).

References: A. E. Raftery, A continuous multivariate exponential distribution, Comm. Statist. A 13 (1984); R. B. Nelsen, An Introduction to Copulas (2006), exercises of Ch. 5 (Raftery family).

noncomputable def ProbabilityTheory.Copula.RafteryKendall.vDeriv (p t x : ℝ) : ℝ

∂C/∂v at (t, x) below the diagonal (t ≤ x).

Equations

• ProbabilityTheory.Copula.RafteryKendall.vDeriv p t x = t ^ p * (p * x ^ (p - 1) + (p - 1) * x ^ (-p)) / (2 * p - 1)

noncomputable def ProbabilityTheory.Copula.RafteryKendall.uDeriv (p t x : ℝ) : ℝ

∂C/∂u at (t, x) below the diagonal (t ≤ x).

Equations

• ProbabilityTheory.Copula.RafteryKendall.uDeriv p t x = 1 + p * t ^ (p - 1) * (x ^ p - x ^ (1 - p)) / (2 * p - 1)

noncomputable def ProbabilityTheory.Copula.RafteryKendall.partialProduct (p t x : ℝ) : ℝ

The product of the two partial derivatives below the diagonal.

Equations

• ProbabilityTheory.Copula.RafteryKendall.partialProduct p t x = ProbabilityTheory.Copula.RafteryKendall.vDeriv p t x * ProbabilityTheory.Copula.RafteryKendall.uDeriv p t x

theorem ProbabilityTheory.Copula.RafteryKendall.condDeriv_eq {p : ℝ} (u v : ℝ) : Raftery.condDeriv p u v = if u ≤ v then vDeriv p u v else uDeriv p v u

theorem ProbabilityTheory.Copula.RafteryKendall.vDeriv_zero_left {p : ℝ} (hp : 1 ≤ p) (x : ℝ) : vDeriv p 0 x = 0

theorem ProbabilityTheory.Copula.RafteryKendall.integrand_eq {p : ℝ} (hp : 1 ≤ p) {u v : ℝ} (hu : 0 ≤ u) : Raftery.condDeriv p v u * Raftery.condDeriv p u v = (if u ≤ v then partialProduct p u v else 0) + if v < u then partialProduct p v u else 0

The integrand ∂₁C ∂₂C split along the diagonal.

theorem ProbabilityTheory.Copula.RafteryKendall.rpow_mul_rpow_sub_one {p : ℝ} (hp : 1 ≤ p) {t : ℝ} (ht : 0 ≤ t) : t ^ p * t ^ (p - 1) = t ^ (2 * p - 1)

theorem ProbabilityTheory.Copula.RafteryKendall.derivative_identity {p a b c D : ℝ} (hq : 2 * p - 1 ≠ 0) (hr : p + 1 ≠ 0) : a * c / (2 * p - 1) * (1 + p * b * D / (2 * p - 1)) = c * ((p + 1) * a) / ((2 * p - 1) * (p + 1)) + c * D * (2 * p * (a * b)) / (2 * (2 * p - 1) ^ 2)

noncomputable def ProbabilityTheory.Copula.RafteryKendall.primitive (p x t : ℝ) : ℝ

An antiderivative of t ↦ ∂₂C(t,x) ∂₁C(t,x).

Equations

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

theorem ProbabilityTheory.Copula.RafteryKendall.hasDerivAt_primitive {p : ℝ} (hp : 1 ≤ p) (x : ℝ) {t : ℝ} (ht : 0 ≤ t) : HasDerivAt (primitive p x) (partialProduct p t x) t

noncomputable def ProbabilityTheory.Copula.RafteryKendall.lowerIntegral (p x : ℝ) : ℝ

The closed form of ∫₀ˣ ∂₂C(t,x) ∂₁C(t,x) dt.

Equations

• ProbabilityTheory.Copula.RafteryKendall.lowerIntegral p x = (p * x ^ (2 * p) + (p - 1) * x) / ((2 * p - 1) * (p + 1)) + (p * x ^ (4 * p - 1) - x ^ (2 * p) - (p - 1) * x) / (2 * (2 * p - 1) ^ 2)

theorem ProbabilityTheory.Copula.RafteryKendall.primitive_eq {p : ℝ} (hp : 1 ≤ p) {x : ℝ} (hx : 0 ≤ x) : primitive p x x - primitive p x 0 = lowerIntegral p x

theorem ProbabilityTheory.Copula.RafteryKendall.continuous_partialProduct {p : ℝ} (hp : 1 ≤ p) (x : ℝ) : Continuous fun (t : ℝ) => partialProduct p t x

theorem ProbabilityTheory.Copula.RafteryKendall.integral_partialProduct {p : ℝ} (hp : 1 ≤ p) (x : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic x, partialProduct p ↑t ↑x = lowerIntegral p ↑x

∫₀ˣ ∂₂C(t,x) ∂₁C(t,x) dt = L(x).

theorem ProbabilityTheory.Copula.RafteryKendall.continuous_lowerIntegral {p : ℝ} (hp : 1 ≤ p) : Continuous (lowerIntegral p)

theorem ProbabilityTheory.Copula.RafteryKendall.integral_lowerIntegral {p : ℝ} (hp : 1 ≤ p) : ∫ (x : ↑unitInterval), lowerIntegral p ↑x = 3 / (8 * (2 * p + 1))

∫₀¹ L = 3/(8(2p+1)).

theorem ProbabilityTheory.Copula.RafteryKendall.abs_partialProduct_le {p : ℝ} (hp : 1 ≤ p) {t x : ℝ} (ht : 0 ≤ t) (htx : t ≤ x) (hx0 : 0 < x) (hx1 : x ≤ 1) : |partialProduct p t x| ≤ 1

Bounds 0 ≤ ∂₂C, ∂₁C ≤ 1 below the diagonal.

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

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

Equations

• ProbabilityTheory.Copula.RafteryKendall.lower p v u = if ↑u ≤ ↑v then ProbabilityTheory.Copula.RafteryKendall.partialProduct p ↑u ↑v else 0

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

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

Equations

• ProbabilityTheory.Copula.RafteryKendall.upper p v u = if ↑v < ↑u then ProbabilityTheory.Copula.RafteryKendall.partialProduct p ↑v ↑u else 0

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

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

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

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

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

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

theorem ProbabilityTheory.Copula.RafteryKendall.measurable_condDeriv (p : ℝ) : Measurable fun (q : ↑unitInterval × ↑unitInterval) => Raftery.condDeriv p ↑q.1 ↑q.2

theorem ProbabilityTheory.Copula.conditionalCDF_raftery {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) (v : ↑unitInterval) : ∀ᵐ (u : ↑unitInterval), (raftery θ h0 h1).conditionalCDF u v = Raftery.condDeriv (1 / (1 - θ)) ↑v ↑u

The conditional distribution function of the Raftery copula is the partial derivative ∂₁C_θ(u, v) = Raftery.condDeriv p v u (p = 1/(1-θ)) for almost every u.

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

Kendall's tau of the Raftery copula: τ(C_θ) = 2θ/(3 - θ) (Nelsen 2006).