← Copula mathematical handbook

The Plackett family

Plackett's family of copulas (R. L. Plackett, A class of bivariate distributions, J. Amer. Statist. Assoc. 60 (1965); Nelsen 2006, §3.3.1, (3.3.3)): for θ > 0, θ ≠ 1,

C_θ(u,v) = ([1 + (θ-1)(u+v)] - √([1 + (θ-1)(u+v)]² - 4uvθ(θ-1))) / (2(θ-1)),

and C_1 = Π. Main results:

• a derivative criterion for two-increasingness (rectangle_nonneg_of_hasDerivAt): if every vertical section v ↦ F(u,v) has derivative g(u,v) on (0,1) and g(·,v) is nondecreasing, then all rectangle increments of F are nonnegative;
• the discriminant [1 + (θ-1)(u+v)]² - 4uvθ(θ-1) is positive on the closed unit square (plackettDisc_pos), the partial derivative ∂C_θ/∂v = (1 - (1 + (θ-1)(u+v) - 2θu)/√disc) / 2 is nondecreasing in u (its u-derivative is the Plackett density θ(1 + (θ-1)(u+v-2uv)) / disc^{3/2} > 0, hasDerivAt_plackettDeriv_left, plackettDensity_pos), hence C_θ is a copula for every θ > 0 (plackett);
• C_1 = Π (plackett_one), and the defining constant cross-product ratio property C(1 - u - v + C) = θ (u - C)(v - C) (plackett_cross_ratio), i.e. P(U ≤ u, V ≤ v) P(U > u, V > v) = θ P(U ≤ u, V > v) P(U > u, V ≤ v);
• exchangeability and radial symmetry (isExchangeable_plackett, isRadiallySymmetric_plackett);
• Blomqvist's β(C_θ) = (√θ - 1)/(√θ + 1) (blomqvistBeta_plackett).

The concordance ordering in θ and the limits M, W are in Copula.Families.Plackett.Order, Spearman's rho in Copula.Families.Plackett.Spearman.

A derivative criterion for two-increasingness

theorem ProbabilityTheory.Copula.rectangle_nonneg_of_hasDerivAt {F g : ℝ → ℝ → ℝ} (hcont : ∀ u ∈ Set.Icc 0 1, ContinuousOn (F u) (Set.Icc 0 1)) (hder : ∀ u ∈ Set.Icc 0 1, ∀ v ∈ Set.Ioo 0 1, HasDerivAt (F u) (g u v) v) (hmono : ∀ v ∈ Set.Ioo 0 1, MonotoneOn (fun (u : ℝ) => g u v) (Set.Icc 0 1)) {a b c e : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ 1) (hc : 0 ≤ c) (hce : c ≤ e) (he : e ≤ 1) : 0 ≤ F b e - F a e - F b c + F a c

If each vertical section v ↦ F(u,v) (for u ∈ [0,1]) is continuous on [0,1] with derivative g(u,v) on (0,1), and each u ↦ g(u,v) is nondecreasing on [0,1], then F has nonnegative rectangle increments on the unit square.

The Plackett formula

def ProbabilityTheory.Copula.plackettLinear (θ u v : ℝ) : ℝ

The linear term 1 + (θ - 1)(u + v) of the Plackett formula.

Equations

• ProbabilityTheory.Copula.plackettLinear θ u v = 1 + (θ - 1) * (u + v)

def ProbabilityTheory.Copula.plackettDisc (θ u v : ℝ) : ℝ

The discriminant [1 + (θ-1)(u+v)]² - 4uvθ(θ-1) of the Plackett formula.

Equations

• ProbabilityTheory.Copula.plackettDisc θ u v = ProbabilityTheory.Copula.plackettLinear θ u v ^ 2 - 4 * θ * (θ - 1) * u * v

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

The Plackett CDF formula (Nelsen (3.3.3)); Π for θ = 1.

Equations

• ProbabilityTheory.Copula.plackettCDF θ u v = if θ = 1 then u * v else (ProbabilityTheory.Copula.plackettLinear θ u v - √(ProbabilityTheory.Copula.plackettDisc θ u v)) / (2 * (θ - 1))

theorem ProbabilityTheory.Copula.plackettLinear_comm (θ u v : ℝ) : plackettLinear θ u v = plackettLinear θ v u

theorem ProbabilityTheory.Copula.plackettDisc_comm (θ u v : ℝ) : plackettDisc θ u v = plackettDisc θ v u

theorem ProbabilityTheory.Copula.plackettCDF_comm (θ u v : ℝ) : plackettCDF θ u v = plackettCDF θ v u

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

theorem ProbabilityTheory.Copula.plackettDisc_pos {θ u v : ℝ} (hθ : 0 < θ) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : 0 < plackettDisc θ u v

The Plackett discriminant is positive on the closed unit square.

theorem ProbabilityTheory.Copula.plackettDisc_zero_left (θ v : ℝ) : plackettDisc θ 0 v = (1 + (θ - 1) * v) ^ 2

theorem ProbabilityTheory.Copula.plackettDisc_one_left (θ v : ℝ) : plackettDisc θ 1 v = (θ - (θ - 1) * v) ^ 2

theorem ProbabilityTheory.Copula.plackettCDF_zero_left {θ : ℝ} (hθ : 0 < θ) {v : ℝ} (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : plackettCDF θ 0 v = 0

theorem ProbabilityTheory.Copula.plackettCDF_one_left {θ : ℝ} (hθ : 0 < θ) {v : ℝ} (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : plackettCDF θ 1 v = v

theorem ProbabilityTheory.Copula.plackettCDF_quadratic {θ u v : ℝ} (hθ : 0 < θ) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : (θ - 1) * plackettCDF θ u v ^ 2 - plackettLinear θ u v * plackettCDF θ u v + θ * u * v = 0

The quadratic equation (θ - 1) C² - [1 + (θ-1)(u+v)] C + θuv = 0 satisfied by the Plackett formula on the unit square.

Derivatives

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

The partial derivative ∂C_θ/∂v = (1 - (1 + (θ-1)(u+v) - 2θu)/√disc) / 2 of the Plackett formula (θ ≠ 1).

Equations

• ProbabilityTheory.Copula.plackettDeriv θ u v = (1 - (ProbabilityTheory.Copula.plackettLinear θ u v - 2 * θ * u) / √(ProbabilityTheory.Copula.plackettDisc θ u v)) / 2

theorem ProbabilityTheory.Copula.hasDerivAt_plackettLinear_right (θ u v : ℝ) : HasDerivAt (fun (y : ℝ) => plackettLinear θ u y) (θ - 1) v

theorem ProbabilityTheory.Copula.hasDerivAt_plackettDisc_right (θ u v : ℝ) : HasDerivAt (fun (y : ℝ) => plackettDisc θ u y) (2 * plackettLinear θ u v * (θ - 1) - 4 * θ * (θ - 1) * u) v

theorem ProbabilityTheory.Copula.hasDerivAt_plackettLinear_left (θ u v : ℝ) : HasDerivAt (fun (x : ℝ) => plackettLinear θ x v) (θ - 1) u

theorem ProbabilityTheory.Copula.hasDerivAt_plackettDisc_left (θ u v : ℝ) : HasDerivAt (fun (x : ℝ) => plackettDisc θ x v) (2 * plackettLinear θ u v * (θ - 1) - 4 * θ * (θ - 1) * v) u

theorem ProbabilityTheory.Copula.plackettCDF_eq_of_ne {θ : ℝ} (hθ : θ ≠ 1) (u v : ℝ) : plackettCDF θ u v = (plackettLinear θ u v - √(plackettDisc θ u v)) / (2 * (θ - 1))

theorem ProbabilityTheory.Copula.continuous_plackettCDF (θ : ℝ) : Continuous fun (p : ℝ × ℝ) => plackettCDF θ p.1 p.2

theorem ProbabilityTheory.Copula.hasDerivAt_plackettCDF_right {θ u v : ℝ} (hθ : θ ≠ 1) (hD : 0 < plackettDisc θ u v) : HasDerivAt (fun (y : ℝ) => plackettCDF θ u y) (plackettDeriv θ u v) v

theorem ProbabilityTheory.Copula.hasDerivAt_plackettRatio_left {θ u v : ℝ} (hD : 0 < plackettDisc θ u v) : HasDerivAt (fun (x : ℝ) => (plackettLinear θ x v - 2 * θ * x) / √(plackettDisc θ x v)) (-2 * θ * (1 + (θ - 1) * (u + v - 2 * u * v)) / (√(plackettDisc θ u v) * plackettDisc θ u v)) u

The u-derivative of (1 + (θ-1)(u+v) - 2θu)/√disc: it equals -2θ(1 + (θ-1)(u+v-2uv)) / disc^{3/2}, minus twice the Plackett density.

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

The Plackett density c_θ(u,v) = θ(1 + (θ-1)(u+v-2uv)) / disc^{3/2}.

Equations

• ProbabilityTheory.Copula.plackettDensity θ u v = θ * (1 + (θ - 1) * (u + v - 2 * u * v)) / (√(ProbabilityTheory.Copula.plackettDisc θ u v) * ProbabilityTheory.Copula.plackettDisc θ u v)

theorem ProbabilityTheory.Copula.hasDerivAt_plackettDeriv_left {θ u v : ℝ} (hD : 0 < plackettDisc θ u v) : HasDerivAt (fun (x : ℝ) => plackettDeriv θ x v) (plackettDensity θ u v) u

The density is the mixed partial derivative: ∂/∂u (∂C_θ/∂v) = c_θ.

theorem ProbabilityTheory.Copula.plackettDensity_pos {θ u v : ℝ} (hθ : 0 < θ) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : 0 < plackettDensity θ u v

The Plackett density is positive on the closed unit square.

theorem ProbabilityTheory.Copula.plackettDeriv_monotoneOn {θ v : ℝ} (hθ : 0 < θ) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : MonotoneOn (fun (u : ℝ) => plackettDeriv θ u v) (Set.Icc 0 1)

The Plackett partial derivative ∂C_θ/∂v is nondecreasing in u.

The Plackett copula

theorem ProbabilityTheory.Copula.isClassical_plackettCDF (θ : ℝ) (hθ : 0 < θ) : IsClassical fun (u : Fin 2 → ↑unitInterval) => plackettCDF θ ↑(u 0) ↑(u 1)

The Plackett formula satisfies the classical copula conditions for every θ > 0.

noncomputable def ProbabilityTheory.Copula.plackett (θ : ℝ) (hθ : 0 < θ) : Copula 2

The Plackett copula C_θ, θ > 0 (Nelsen 2006, (3.3.3)).

Equations

• ProbabilityTheory.Copula.plackett θ hθ = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => ProbabilityTheory.Copula.plackettCDF θ ↑(u 0) ↑(u 1)) ⋯

@[simp]

theorem ProbabilityTheory.Copula.cdf_plackett (θ : ℝ) (hθ : 0 < θ) (u : Fin 2 → ↑unitInterval) : (plackett θ hθ).cdf u = plackettCDF θ ↑(u 0) ↑(u 1)

theorem ProbabilityTheory.Copula.cdf_plackett_two (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : (plackett θ hθ).cdf ![u, v] = plackettCDF θ ↑u ↑v

@[simp]

theorem ProbabilityTheory.Copula.plackett_one : plackett 1 ⋯ = independence 2

C_1 = Π.

theorem ProbabilityTheory.Copula.plackett_cross_ratio (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : (plackett θ hθ).cdf ![u, v] * (1 - ↑u - ↑v + (plackett θ hθ).cdf ![u, v]) = θ * (↑u - (plackett θ hθ).cdf ![u, v]) * (↑v - (plackett θ hθ).cdf ![u, v])

The constant cross-product ratio property defining the Plackett family: C(1 - u - v + C) = θ (u - C)(v - C) with C = C_θ(u,v). In terms of (U,V) ~ C_θ: P(U ≤ u, V ≤ v) P(U > u, V > v) = θ P(U ≤ u, V > v) P(U > u, V ≤ v).

theorem ProbabilityTheory.Copula.isExchangeable_plackett (θ : ℝ) (hθ : 0 < θ) : (plackett θ hθ).IsExchangeable

theorem ProbabilityTheory.Copula.plackettCDF_reflect (θ u v : ℝ) : plackettCDF θ u v = u + v - 1 + plackettCDF θ (1 - u) (1 - v)

theorem ProbabilityTheory.Copula.isRadiallySymmetric_plackett (θ : ℝ) (hθ : 0 < θ) : (plackett θ hθ).IsRadiallySymmetric

theorem ProbabilityTheory.Copula.blomqvistBeta_plackett (θ : ℝ) (hθ : 0 < θ) : (plackett θ hθ).blomqvistBeta = (√θ - 1) / (√θ + 1)

Blomqvist's beta of the Plackett copula: β(C_θ) = (√θ - 1)/(√θ + 1).