← Copula mathematical handbook

Upper tail dependence of families of Nelsen's Table 4.1

Nelsen, An Introduction to Copulas, second edition, Corollary 5.4.3: if the inverse generator ψ has a finite nonzero right derivative at 0 (equivalently φ'(1⁻) ≠ 0), then δ'(1⁻) = 2 and λ_U = 0 (BivariateGenerator.hasUpperTailDependence_zero_of_hasDerivWithinAt). This file applies that criterion to the families of Table 4.1 whose generator has φ'(1) ∈ (−∞, 0):

family	ψ near 0	ψ'(0)
7 (0 < θ ≤ 1)	(e^{−s} + θ − 1)/θ	−1/θ
10	(2/(e^s + 1))^{1/θ}	−1/(2θ)
11	(2 − e^s)^{1/θ}	−1/θ
13	exp(1 − (1 + s)^{1/θ})	−1/θ
16	(1 − θ − s + √((1 − θ − s)² + 4θ))/2	−1/(1 + θ)
17	(1 + (2^{−θ} − 1)e^{−s})^{−1/θ} − 1	2(1 − 2^θ)/θ
22	(1 − sin s)^{1/θ}	−1/θ

so each of these families has λ_U = 0 (for family 7 also at θ = 0, where it is W). The helper BivariateGenerator.hasUpperTailDependence_zero_of_eventuallyEq reduces the criterion to an explicit formula valid on some [0, ε).

theorem ProbabilityTheory.Copula.BivariateGenerator.hasUpperTailDependence_zero_of_eventuallyEq (g : BivariateGenerator) {F : ℝ → ℝ} {d : ℝ} (hF : ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ici 0), g.toFun s = F s) (hd : HasDerivAt F d 0) (hd0 : d ≠ 0) : g.copula.HasUpperTailDependence 0

Corollary 5.4.3 with an explicit local formula: if ψ = F on a right neighbourhood of 0 and F'(0) = d ≠ 0, then λ_U = 0.

theorem ProbabilityTheory.Copula.hasUpperTailDependence_nelsen7 (θ : ↑unitInterval) : (nelsen7 θ).HasUpperTailDependence 0

Nelsen's family 7 has no upper tail dependence.

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

Nelsen's family 10 has no upper tail dependence.

theorem ProbabilityTheory.Copula.hasUpperTailDependence_nelsen11 (θ : ℝ) (hθ : 0 < θ) (h2 : θ ≤ 1 / 2) : (nelsen11 θ hθ h2).HasUpperTailDependence 0

Nelsen's family 11 has no upper tail dependence.

theorem ProbabilityTheory.Copula.hasUpperTailDependence_nelsen13 (θ : ℝ) (hθ : 0 < θ) : (nelsen13 θ hθ).HasUpperTailDependence 0

Nelsen's family 13 has no upper tail dependence.

theorem ProbabilityTheory.Copula.hasUpperTailDependence_nelsen16 (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen16 θ hθ).HasUpperTailDependence 0

Nelsen's family 16 has no upper tail dependence.

theorem ProbabilityTheory.Copula.hasUpperTailDependence_nelsen17 (θ : ℝ) (hθ : θ ≠ 0) : (nelsen17 θ hθ).HasUpperTailDependence 0

Nelsen's family 17 has no upper tail dependence.

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

Nelsen's family 22 has no upper tail dependence.