← Copula mathematical handbook

Tail coefficients of Archimedean families via their generators

Applications of Nelsen, An Introduction to Copulas, second edition, Corollary 5.4.3 (Copula.Archimedean.TailDependence) to families of Table 4.1 without previously recorded tail coefficients (cf. Nelsen, Section 5.4):

Family	λ_L	λ_U
Frank (4.2.5), θ > 0	0	0
Gumbel–Barnett (4.2.9), 0 < θ ≤ 1	0	0
4.2.19, θ > 0	1	0
4.2.20, θ > 0	1	0

In each case ψ has a finite nonzero derivative at 0, so λ_U = 0. For the lower tail the limit ψ(2x)/ψ(x) as x → ∞ is computed: it is 0 for Frank and Gumbel–Barnett (their inverse generators decay exponentially) and 1 for families 19 and 20 (logarithmic decay).

theorem ProbabilityTheory.Copula.tendsto_log_add_div_log_two_mul_add {c : ℝ} (hc : 1 < c) : Filter.Tendsto (fun (x : ℝ) => Real.log (x + c) / Real.log (2 * x + c)) Filter.atTop (nhds 1)

log (x + c) / log (2x + c) → 1 as x → ∞, for c > 1.

Frank

theorem ProbabilityTheory.Copula.frankGenerator_isStrict (θ : ℝ) (hθ : 0 < θ) : (frankGenerator θ hθ).IsStrict

theorem ProbabilityTheory.Copula.hasUpperTailDependence_frank (θ : ℝ) (hθ : 0 < θ) : (frank θ hθ).HasUpperTailDependence 0

Frank copulas have no upper tail dependence.

theorem ProbabilityTheory.Copula.hasLowerTailDependence_frank (θ : ℝ) (hθ : 0 < θ) : (frank θ hθ).HasLowerTailDependence 0

Frank copulas with θ > 0 have no lower tail dependence.

Gumbel–Barnett (family 9)

theorem ProbabilityTheory.Copula.nelsen9Generator_isStrict (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : (nelsen9Generator θ hθ h1).IsStrict

theorem ProbabilityTheory.Copula.hasUpperTailDependence_nelsen9 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : (nelsen9 θ hθ h1).HasUpperTailDependence 0

Gumbel–Barnett copulas have no upper tail dependence.

theorem ProbabilityTheory.Copula.hasLowerTailDependence_nelsen9 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : (nelsen9 θ hθ h1).HasLowerTailDependence 0

Gumbel–Barnett copulas have no lower tail dependence.

Family 19

theorem ProbabilityTheory.Copula.nelsen19Generator_isStrict (θ : ℝ) (hθ : 0 < θ) : (nelsen19Generator θ hθ).IsStrict

theorem ProbabilityTheory.Copula.hasLowerTailDependence_nelsen19 (θ : ℝ) (hθ : 0 < θ) : (nelsen19 θ hθ).HasLowerTailDependence 1

Nelsen's family 19 has lower tail dependence one.

theorem ProbabilityTheory.Copula.hasUpperTailDependence_nelsen19 (θ : ℝ) (hθ : 0 < θ) : (nelsen19 θ hθ).HasUpperTailDependence 0

Nelsen's family 19 has no upper tail dependence.

Family 20

theorem ProbabilityTheory.Copula.nelsen20Generator_isStrict (θ : ℝ) (hθ : 0 < θ) : (nelsen20Generator θ hθ).IsStrict

theorem ProbabilityTheory.Copula.hasLowerTailDependence_nelsen20 (θ : ℝ) (hθ : 0 < θ) : (nelsen20 θ hθ).HasLowerTailDependence 1

Nelsen's family 20 has lower tail dependence one.

theorem ProbabilityTheory.Copula.hasUpperTailDependence_nelsen20 (θ : ℝ) (hθ : 0 < θ) : (nelsen20 θ hθ).HasUpperTailDependence 0

Nelsen's family 20 has no upper tail dependence.