← Copula mathematical handbook

Multivariate Archimedean copulas

McNeil–Nešlehová (2009), Theorem 2.2 ("if" part); Nelsen (2006), §4.6, and Kimberling (1974). Let ψ be a continuous, nonincreasing inverse generator on [0, ∞) with ψ(0) = 1, generalized inverse φ, and let ψ be d-monotone on (0, ∞). Then C(u) = ψ(φ(u₁) + ⋯ + φ(u_d)) (and C(u) = 0 when some uᵢ = 0) is a d-copula.

The rectangle increment of C over a box with positive lower corner a and upper corner b is the alternating corner sum of ψ at x = ∑ φ(bᵢ) with increments hᵢ = φ(aᵢ) - φ(bᵢ) ≥ 0 (rectangleIncrement_cdf_eq_cornerSum), which is nonnegative by d-monotonicity (IsMultiplyMonotone.cornerSum_nonneg_of_nonneg); boxes touching the lower faces are handled by an approximation from the inside (rectangleIncrement_cdf_nonneg). Completely monotone ψ (Kimberling) are d-monotone for every d.

Main declarations:

• MultivariateGenerator d: a bivariate generator whose inverse generator is continuous on [0, ∞) and d-monotone; MultivariateGenerator.copula is the d-copula and hasArchimedeanGenerator_copula records its Archimedean form;
• for d = 2 it agrees with the bivariate construction (copula_two), and all its margins have the same generator (hasArchimedeanGenerator_reindex);
• the positive-parameter Clayton family in every dimension is an instance, and the copula coincides with the gamma-frailty construction clayton d θ hθ (claytonMultivariate_copula).

structure ProbabilityTheory.Copula.MultivariateGenerator (d : ℕ) extends ProbabilityTheory.Copula.BivariateGenerator : Type

A generator of d-dimensional Archimedean copulas: a bivariate generator whose inverse generator ψ is continuous on [0, ∞) and d-monotone on (0, ∞).

• toFun : ℝ → ℝ
• invFun : ↑unitInterval → ℝ
• nonneg (t : ℝ) : 0 ≤ t → 0 ≤ self.toFun t
• antitone : AntitoneOn self.toFun (Set.Ici 0)
• convex : ConvexOn ℝ (Set.Ici 0) self.toFun
• inv_nonneg (u : ↑unitInterval) : u ≠ 0 → 0 ≤ self.invFun u
• inv_antitone (u v : ↑unitInterval) : u ≠ 0 → u ≤ v → self.invFun v ≤ self.invFun u
• inv_one : self.invFun 1 = 0
• right_inv (u : ↑unitInterval) : u ≠ 0 → self.toFun (self.invFun u) = ↑u
• continuousOn : ContinuousOn self.toFun (Set.Ici 0)

  Continuity of the inverse generator on [0, ∞).

• multiplyMonotone : IsMultiplyMonotone d self.toFun

  d-monotonicity of the inverse generator (McNeil–Nešlehová 2009, Definition 2.3).

noncomputable def ProbabilityTheory.Copula.MultivariateGenerator.cdf {d : ℕ} (g : MultivariateGenerator d) (u : Fin d → ↑unitInterval) : ℝ

The d-dimensional Archimedean formula, with grounded boundary values.

Equations

• g.cdf u = if ∃ (i : Fin d), u i = 0 then 0 else g.toFun (∑ i : Fin d, g.invFun (u i))

theorem ProbabilityTheory.Copula.MultivariateGenerator.cdf_of_exists_zero {d : ℕ} (g : MultivariateGenerator d) {u : Fin d → ↑unitInterval} (h : ∃ (i : Fin d), u i = 0) : g.cdf u = 0

theorem ProbabilityTheory.Copula.MultivariateGenerator.cdf_of_forall_ne_zero {d : ℕ} (g : MultivariateGenerator d) {u : Fin d → ↑unitInterval} (h : ∀ (i : Fin d), u i ≠ 0) : g.cdf u = g.toFun (∑ i : Fin d, g.invFun (u i))

theorem ProbabilityTheory.Copula.MultivariateGenerator.toFun_zero {d : ℕ} (g : MultivariateGenerator d) : g.toFun 0 = 1

theorem ProbabilityTheory.Copula.MultivariateGenerator.cdf_nonneg {d : ℕ} (g : MultivariateGenerator d) (u : Fin d → ↑unitInterval) : 0 ≤ g.cdf u

theorem ProbabilityTheory.Copula.MultivariateGenerator.cdf_le_coord {d : ℕ} (g : MultivariateGenerator d) (u : Fin d → ↑unitInterval) (i : Fin d) : g.cdf u ≤ ↑(u i)

theorem ProbabilityTheory.Copula.MultivariateGenerator.rectangleIncrement_cdf_eq_cornerSum {d : ℕ} (g : MultivariateGenerator d) {a b : Fin d → ↑unitInterval} (ha : ∀ (i : Fin d), a i ≠ 0) (hab : a ≤ b) : rectangleIncrement g.cdf a b = cornerSum g.toFun (∑ i : Fin d, g.invFun (b i)) (fun (i : Fin d) => g.invFun (a i) - g.invFun (b i)) Finset.univ

Rectangle increments are corner sums of the inverse generator for boxes whose lower corner has positive coordinates.

theorem ProbabilityTheory.Copula.MultivariateGenerator.rectangleIncrement_cdf_nonneg {d : ℕ} (g : MultivariateGenerator d) (a b : Fin d → ↑unitInterval) (hab : a ≤ b) : 0 ≤ rectangleIncrement g.cdf a b

The Archimedean formula is d-increasing.

theorem ProbabilityTheory.Copula.MultivariateGenerator.isClassical_cdf {d : ℕ} (g : MultivariateGenerator d) : IsClassical g.cdf

noncomputable def ProbabilityTheory.Copula.MultivariateGenerator.copula {d : ℕ} (g : MultivariateGenerator d) : Copula d

The d-dimensional Archimedean copula generated by a d-monotone inverse generator.

Equations

• g.copula = ProbabilityTheory.Copula.ofClassical g.cdf ⋯

@[simp]

theorem ProbabilityTheory.Copula.MultivariateGenerator.cdf_copula {d : ℕ} (g : MultivariateGenerator d) (u : Fin d → ↑unitInterval) : g.copula.cdf u = g.cdf u

theorem ProbabilityTheory.Copula.MultivariateGenerator.hasArchimedeanGenerator_copula {d : ℕ} (g : MultivariateGenerator d) : g.copula.HasArchimedeanGenerator g.toBivariateGenerator

theorem ProbabilityTheory.Copula.MultivariateGenerator.isArchimedean_copula {d : ℕ} (g : MultivariateGenerator d) : g.copula.IsArchimedean

theorem ProbabilityTheory.Copula.MultivariateGenerator.copula_two (g : MultivariateGenerator 2) : g.copula = g.copula

In dimension two the construction is the bivariate Archimedean copula.

theorem ProbabilityTheory.Copula.MultivariateGenerator.hasArchimedeanGenerator_reindex {d : ℕ} (g : MultivariateGenerator d) {e : ℕ} {ρ : Fin e → Fin d} (hρ : Function.Injective ρ) : (g.copula.reindex ρ).HasArchimedeanGenerator g.toBivariateGenerator

Margins of Archimedean copulas are Archimedean with the same generator.

Clayton copulas in every dimension

noncomputable def ProbabilityTheory.Copula.claytonMultivariateGenerator (d : ℕ) (θ : ℝ) (hθ : 0 < θ) : MultivariateGenerator d

Clayton's generator (1 + t)^{-1/θ} (θ > 0) is d-monotone for every d.

Equations

• ProbabilityTheory.Copula.claytonMultivariateGenerator d θ hθ = { toBivariateGenerator := ProbabilityTheory.Copula.claytonGenerator θ hθ, continuousOn := ⋯, multiplyMonotone := ⋯ }

theorem ProbabilityTheory.Copula.claytonMultivariate_copula (d : ℕ) (θ : ℝ) (hθ : 0 < θ) : (claytonMultivariateGenerator d θ hθ).copula = clayton d θ hθ

The analytic d-dimensional Clayton copula equals the gamma-frailty construction.