← Copula mathematical handbook

The Raftery family

Raftery's family (A. E. Raftery, A continuous multivariate exponential distribution, Comm. Statist. A 13 (1984); it appears in the exercises of Nelsen 2006, Ch. 2 and 5): for θ ∈ [0,1),

C_θ(u,v) = M(u,v) + (1-θ)/(1+θ) · (uv)^{1/(1-θ)} · (1 - max(u,v)^{-(1+θ)/(1-θ)}),

and C_θ → M as θ → 1. With p = 1/(1-θ) ≥ 1 and (1-θ)/(1+θ) = 1/(2p-1) this reads, for u ≤ v, C(u,v) = u + u^p (v^p - v^{1-p})/(2p-1) (and symmetrically).

Main results:

• C_θ is a copula for every θ ∈ [0,1) (raftery): its vertical sections are differentiable on (0,1), including across the diagonal where the two branches of the partial derivative ∂C/∂v meet continuously, and ∂C/∂v is nondecreasing in u (rectangle_nonneg_of_hasDerivAt); in particular C_θ has no singular component;
• Nelsen's closed form (raftery_cdf_eq), C_0 = Π (raftery_zero), exchangeability, and the uniform convergence |C_θ - M| ≤ (1-θ)/(1+θ) (tendsto_rafteryCDF_one);
• C_θ is PQD (Bernoulli's inequality);
• the diagonal δ(t) = (2θ t + (1-θ) t^{2/(1-θ)})/(1+θ), Blomqvist's beta, and the tail coefficients λ_L = 2θ/(1+θ), λ_U = 0.

noncomputable def ProbabilityTheory.Copula.Raftery.core (p u v : ℝ) : ℝ

The Raftery CDF in the exponent p = 1/(1-θ) ≥ 1.

Equations

• ProbabilityTheory.Copula.Raftery.core p u v = if u ≤ v then u + u ^ p * (v ^ p - v ^ (1 - p)) / (2 * p - 1) else v + v ^ p * (u ^ p - u ^ (1 - p)) / (2 * p - 1)

noncomputable def ProbabilityTheory.Copula.Raftery.condDeriv (p u v : ℝ) : ℝ

The partial derivative ∂C/∂v in the exponent p.

Equations

• ProbabilityTheory.Copula.Raftery.condDeriv p u v = if u ≤ v then u ^ p * (p * v ^ (p - 1) + (p - 1) * v ^ (-p)) / (2 * p - 1) else 1 + p * v ^ (p - 1) * (u ^ p - u ^ (1 - p)) / (2 * p - 1)

theorem ProbabilityTheory.Copula.Raftery.core_comm {p : ℝ} (u v : ℝ) : core p u v = core p v u

theorem ProbabilityTheory.Copula.Raftery.core_zero_left {p : ℝ} (hp : 1 ≤ p) {v : ℝ} (hv : 0 ≤ v) : core p 0 v = 0

theorem ProbabilityTheory.Copula.Raftery.core_one_left {p v : ℝ} (hv : v ≤ 1) : core p 1 v = v

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

The key identity at the diagonal: for x > 0, x^p (p x^{p-1} + (p-1) x^{-p})/(2p-1) = 1 + p x^{p-1} (x^p - x^{1-p})/(2p-1).

theorem ProbabilityTheory.Copula.Raftery.hasDerivAt_branch₁ {p : ℝ} (u : ℝ) {w : ℝ} (hw : 0 < w) : HasDerivAt (fun (y : ℝ) => u + u ^ p * (y ^ p - y ^ (1 - p)) / (2 * p - 1)) (u ^ p * (p * w ^ (p - 1) + (p - 1) * w ^ (-p)) / (2 * p - 1)) w

The first branch, valid for v ≥ u.

theorem ProbabilityTheory.Copula.Raftery.hasDerivAt_branch₂ {p : ℝ} (u : ℝ) {w : ℝ} (hw : 0 < w) : HasDerivAt (fun (y : ℝ) => y + y ^ p * (u ^ p - u ^ (1 - p)) / (2 * p - 1)) (1 + p * w ^ (p - 1) * (u ^ p - u ^ (1 - p)) / (2 * p - 1)) w

The second branch, valid for v ≤ u.

theorem ProbabilityTheory.Copula.Raftery.hasDerivAt_core {p : ℝ} (hp : 1 ≤ p) {u v : ℝ} (hu : 0 ≤ u) (hv : 0 < v) : HasDerivAt (fun (y : ℝ) => core p u y) (condDeriv p u v) v

theorem ProbabilityTheory.Copula.Raftery.continuousOn_core {p : ℝ} (hp : 1 ≤ p) {u : ℝ} (hu : 0 ≤ u) : ContinuousOn (fun (y : ℝ) => core p u y) (Set.Icc 0 1)

theorem ProbabilityTheory.Copula.Raftery.condDeriv_monotoneOn {p : ℝ} (hp : 1 ≤ p) {v : ℝ} (hv0 : 0 < v) (hv1 : v < 1) : MonotoneOn (fun (u : ℝ) => condDeriv p u v) (Set.Icc 0 1)

theorem ProbabilityTheory.Copula.Raftery.rectangle_nonneg {p : ℝ} (hp : 1 ≤ p) {a b c e : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ 1) (hc : 0 ≤ c) (hce : c ≤ e) (he : e ≤ 1) : 0 ≤ core p b e - core p a e - core p b c + core p a c

theorem ProbabilityTheory.Copula.Raftery.mul_le_core {p : ℝ} (hp : 1 ≤ p) {u v : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : u * v ≤ core p u v

Positive quadrant dependence of the core formula.

theorem ProbabilityTheory.Copula.Raftery.core_diag {p : ℝ} (hp : 1 ≤ p) {t : ℝ} (ht : 0 ≤ t) : core p t t = ((2 * p - 2) * t + t ^ (2 * p)) / (2 * p - 1)

The diagonal of the core formula.

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

The Raftery CDF formula C_θ for θ ∈ [0,1), in the exponent p = 1/(1-θ).

Equations

• ProbabilityTheory.Copula.rafteryCDF θ u v = ProbabilityTheory.Copula.Raftery.core (1 / (1 - θ)) u v

theorem ProbabilityTheory.Copula.one_le_raftery_exponent {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) : 1 ≤ 1 / (1 - θ)

theorem ProbabilityTheory.Copula.raftery_exponent_sub {θ : ℝ} (h1 : θ < 1) : 2 * (1 / (1 - θ)) - 1 = (1 + θ) / (1 - θ)

theorem ProbabilityTheory.Copula.raftery_scale {θ : ℝ} (h1 : θ < 1) : 1 / (2 * (1 / (1 - θ)) - 1) = (1 - θ) / (1 + θ)

theorem ProbabilityTheory.Copula.isClassical_rafteryCDF {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) : IsClassical fun (u : Fin 2 → ↑unitInterval) => rafteryCDF θ ↑(u 0) ↑(u 1)

noncomputable def ProbabilityTheory.Copula.raftery (θ : ℝ) (h0 : 0 ≤ θ) (h1 : θ < 1) : Copula 2

The Raftery copula C_θ, 0 ≤ θ < 1 (Raftery 1984; Nelsen 2006).

Equations

• ProbabilityTheory.Copula.raftery θ h0 h1 = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => ProbabilityTheory.Copula.rafteryCDF θ ↑(u 0) ↑(u 1)) ⋯

@[simp]

theorem ProbabilityTheory.Copula.cdf_raftery {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) (u : Fin 2 → ↑unitInterval) : (raftery θ h0 h1).cdf u = rafteryCDF θ ↑(u 0) ↑(u 1)

theorem ProbabilityTheory.Copula.cdf_raftery_two {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) (u v : ↑unitInterval) : (raftery θ h0 h1).cdf ![u, v] = rafteryCDF θ ↑u ↑v

theorem ProbabilityTheory.Copula.raftery_cdf_eq {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) (u v : ↑unitInterval) (hu : 0 < ↑u) (hv : 0 < ↑v) : (raftery θ h0 h1).cdf ![u, v] = min ↑u ↑v + (1 - θ) / (1 + θ) * (↑u * ↑v) ^ (1 / (1 - θ)) * (1 - max ↑u ↑v ^ (-((1 + θ) / (1 - θ))))

Nelsen's form of the Raftery CDF: for u, v > 0, C_θ(u,v) = min(u,v) + (1-θ)/(1+θ) (uv)^{1/(1-θ)} (1 - max(u,v)^{-(1+θ)/(1-θ)}).

@[simp]

theorem ProbabilityTheory.Copula.raftery_zero : raftery 0 ⋯ ⋯ = independence 2

C_0 = Π.

theorem ProbabilityTheory.Copula.isExchangeable_raftery {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) : (raftery θ h0 h1).IsExchangeable

theorem ProbabilityTheory.Copula.isPQD_raftery {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) : (raftery θ h0 h1).IsPQD

Raftery copulas are positively quadrant dependent.

theorem ProbabilityTheory.Copula.Raftery.min_sub_core_le {p : ℝ} (hp : 1 ≤ p) {u v : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : 0 ≤ min u v - core p u v ∧ min u v - core p u v ≤ 1 / (2 * p - 1)

The distance to the upper Fréchet–Hoeffding bound: 0 ≤ min(u,v) - C ≤ 1/(2p-1).

theorem ProbabilityTheory.Copula.min_sub_rafteryCDF_le {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) (u v : ↑unitInterval) : 0 ≤ min ↑u ↑v - rafteryCDF θ ↑u ↑v ∧ min ↑u ↑v - rafteryCDF θ ↑u ↑v ≤ (1 - θ) / (1 + θ)

Uniform distance to M: 0 ≤ min(u,v) - C_θ(u,v) ≤ (1-θ)/(1+θ).

theorem ProbabilityTheory.Copula.tendsto_rafteryCDF_one (u v : ↑unitInterval) : Filter.Tendsto (fun (θ : ℝ) => rafteryCDF θ ↑u ↑v) (nhdsWithin 1 (Set.Iio 1)) (nhds ((comonotonic 2).cdf ![u, v]))

C_θ → M as θ → 1⁻ (Nelsen 2006).

theorem ProbabilityTheory.Copula.raftery_diagonal {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) (t : ↑unitInterval) : (raftery θ h0 h1).diagonal t = (2 * θ * ↑t + (1 - θ) * ↑t ^ (2 / (1 - θ))) / (1 + θ)

The diagonal section δ(t) = (2θ t + (1-θ) t^{2/(1-θ)})/(1+θ).

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

Blomqvist's beta of the Raftery copula: β = (3θ - 1)/(1+θ) + 4(1-θ)/(1+θ) · (1/2)^{2/(1-θ)}.

theorem ProbabilityTheory.Copula.hasDerivAt_raftery_diagonal {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) (x : ℝ) : HasDerivAt (fun (t : ℝ) => (2 * θ * t + (1 - θ) * t ^ (2 / (1 - θ))) / (1 + θ)) ((2 * θ + (1 - θ) * (2 / (1 - θ) * x ^ (2 / (1 - θ) - 1))) / (1 + θ)) x

theorem ProbabilityTheory.Copula.hasLowerTailDependence_raftery {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) : (raftery θ h0 h1).HasLowerTailDependence (2 * θ / (1 + θ))

The lower tail dependence coefficient of the Raftery copula is 2θ/(1+θ).

theorem ProbabilityTheory.Copula.hasUpperTailDependence_raftery {θ : ℝ} (h0 : 0 ≤ θ) (h1 : θ < 1) : (raftery θ h0 h1).HasUpperTailDependence 0

The upper tail dependence coefficient of the Raftery copula is 0.