← Copula mathematical handbook

Negative-parameter Clayton copulas in dimension d

The Clayton formula C_θ(u) = max(0, u₁^{-θ} + ⋯ + u_d^{-θ} - d + 1)^{-1/θ} is a d-copula for -1/(d-1) ≤ θ < 0 (Nelsen 2006, §4.6; McNeil–Nešlehová 2009, §4, where the bound θ ≥ -1/(d-1) is shown to be sharp): its inverse generator ψ(t) = max(0, 1 - t)^{-1/θ} is d-monotone exactly when -1/θ ≥ d - 1 (isMultiplyMonotone_truncated_rpow).

• claytonNegativeMultivariate d θ is the resulting d-copula, with the closed-form CDF cdf_claytonNegativeMultivariate; in dimension two it is the bivariate negative Clayton copula (claytonNegativeMultivariate_two).
• Conversely the bound is sharp (not_cdf_eq_claytonFormula): for θ < -1/(d-1) no d-copula has this CDF. The proof is elementary: a copula vanishing on {∑ uᵢ^β ≤ d - 1} is carried by {∑ Uᵢ^β ≥ d - 1}, hence d/(1+β) = E ∑ Uᵢ^β ≥ d - 1, i.e. (d - 1) β ≤ 1 (mul_le_one_of_cdf_eq_zero). With β = 1 this also re-proves that W_d is not a copula for d ≥ 3.

Truncated powers

theorem ProbabilityTheory.Copula.hasDerivAt_max_zero_rpow {α : ℝ} (hα : 1 < α) (y : ℝ) : HasDerivAt (fun (z : ℝ) => max 0 z ^ α) (α * max 0 y ^ (α - 1)) y

The truncated power z ↦ max(0, z)^α is differentiable for α > 1.

theorem ProbabilityTheory.Copula.isMultiplyMonotone_truncated_rpow (n : ℕ) {c α : ℝ} : 0 ≤ c → 0 ≤ α → ↑n - 1 ≤ α → IsMultiplyMonotone n fun (t : ℝ) => c * max 0 (1 - t) ^ α

c · max(0, 1 - t)^α is n-monotone whenever α ≥ n - 1 (c ≥ 0, α ≥ 0).

The negative Clayton family in dimension d

noncomputable def ProbabilityTheory.Copula.claytonNegativeGenerator (d : ℕ) (θ : ℝ) (hd : 2 ≤ d) (hθ : -1 / (↑d - 1) ≤ θ) (hn : θ < 0) : MultivariateGenerator d

The d-monotone generator max(0, 1 - t)^{-1/θ} of the Clayton family for -1/(d-1) ≤ θ < 0.

Equations

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

noncomputable def ProbabilityTheory.Copula.claytonNegativeMultivariate (d : ℕ) (θ : ℝ) (hd : 2 ≤ d) (hθ : -1 / (↑d - 1) ≤ θ) (hn : θ < 0) : Copula d

The d-dimensional Clayton copula with parameter -1/(d-1) ≤ θ < 0.

Equations

• ProbabilityTheory.Copula.claytonNegativeMultivariate d θ hd hθ hn = (ProbabilityTheory.Copula.claytonNegativeGenerator d θ hd hθ hn).copula

noncomputable def ProbabilityTheory.Copula.claytonFormula (d : ℕ) (θ : ℝ) (u : Fin d → ↑unitInterval) : ℝ

The Clayton CDF formula max(0, ∑ uᵢ^{-θ} - d + 1)^{-1/θ} (and 0 on the lower faces).

Equations

• ProbabilityTheory.Copula.claytonFormula d θ u = if ∃ (i : Fin d), u i = 0 then 0 else max 0 (∑ i : Fin d, ↑(u i) ^ (-θ) - ↑d + 1) ^ (-θ)⁻¹

theorem ProbabilityTheory.Copula.cdf_claytonNegativeMultivariate (d : ℕ) (θ : ℝ) (hd : 2 ≤ d) (hθ : -1 / (↑d - 1) ≤ θ) (hn : θ < 0) : (claytonNegativeMultivariate d θ hd hθ hn).cdf = claytonFormula d θ

Closed form of the negative Clayton CDF.

theorem ProbabilityTheory.Copula.claytonNegativeMultivariate_two (θ : ℝ) (hθ : -1 / (↑2 - 1) ≤ θ) (hθ' : -1 ≤ θ) (hn : θ < 0) : claytonNegativeMultivariate 2 θ ⋯ hθ hn = claytonNegative θ hθ' hn

In dimension two this is the bivariate negative Clayton copula.

theorem ProbabilityTheory.Copula.isArchimedean_claytonNegativeMultivariate (d : ℕ) (θ : ℝ) (hd : 2 ≤ d) (hθ : -1 / (↑d - 1) ≤ θ) (hn : θ < 0) : (claytonNegativeMultivariate d θ hd hθ hn).IsArchimedean

Sharpness of the parameter bound

theorem ProbabilityTheory.Copula.mul_le_one_of_cdf_eq_zero {d : ℕ} (C : Copula d) {β : ℝ} (hβ : 0 < β) (h0 : ∀ (u : Fin d → ↑unitInterval), ∑ i : Fin d, ↑(u i) ^ β ≤ ↑d - 1 → C.cdf u = 0) : (↑d - 1) * β ≤ 1

A copula vanishing on {∑ uᵢ^β ≤ d - 1} forces (d - 1) β ≤ 1. Such a copula is carried by {∑ Uᵢ^β ≥ d - 1} while E ∑ Uᵢ^β = d/(1 + β).

theorem ProbabilityTheory.Copula.not_cdf_eq_claytonFormula {d : ℕ} (hd : 2 ≤ d) {θ : ℝ} (hθ : θ < -1 / (↑d - 1)) (C : Copula d) : C.cdf ≠ claytonFormula d θ

Sharpness of the Clayton parameter bound: for θ < -1/(d-1) the Clayton formula is not the CDF of any d-copula (McNeil–Nešlehová 2009; Nelsen 2006, §4.6).

theorem ProbabilityTheory.Copula.exists_cdf_eq_claytonFormula_iff {d : ℕ} (hd : 2 ≤ d) {θ : ℝ} (hn : θ < 0) : (∃ (C : Copula d), C.cdf = claytonFormula d θ) ↔ -1 / (↑d - 1) ≤ θ

The Clayton formula with θ < 0 is a d-copula iff θ ≥ -1/(d-1).