← Copula mathematical handbook

Further tail coefficients of families of Nelsen's Table 4.1

Applications of Nelsen, An Introduction to Copulas, second edition, Corollary 5.4.3:

• for a strict generator, λ_L = lim_{x → ∞} ψ(2x)/ψ(x) (BivariateGenerator.hasLowerTailDependence_of_tendsto). Families 10, 13 and 17 are strict with ψ(2x)/ψ(x) → 0, so λ_L = 0 (hasLowerTailDependence_nelsen10, hasLowerTailDependence_nelsen13, hasLowerTailDependence_nelsen17). For family 13, ψ(2x)/ψ(x) = exp((1 + x)^{1/θ} − (1 + 2x)^{1/θ}); for family 10 it is ((e^x + 1)/(e^{2x} + 1))^{1/θ} ≤ (2e^{−x})^{1/θ}; for family 17, ψ(s) = G(e^{−s}) with G(0) = 0, G'(0) ≠ 0, so ψ(2x)/ψ(x) ~ e^{−x}.
• λ_U = 2 − lim_{x → 0⁺} (1 − ψ(2x))/(1 − ψ(x)) (BivariateGenerator.hasUpperTailDependence_of_tendsto). For family 21, 1 − ψ(x) = (1 − (1 − x)^θ)^{1/θ} near 0, so the limit is 2^{1/θ} and λ_U = 2 − 2^{1/θ} (hasUpperTailDependence_nelsen21).

The helper tendsto_ratio_of_hasDerivAt states the elementary fact that if H(0) = 0 and H'(0) = d ≠ 0 then H(2x)/H(x) → 2 as x → 0⁺.

theorem ProbabilityTheory.Copula.tendsto_ratio_of_hasDerivAt {H : ℝ → ℝ} {d : ℝ} (hH0 : H 0 = 0) (hd : HasDerivAt H d 0) (hd0 : d ≠ 0) : Filter.Tendsto (fun (x : ℝ) => H (2 * x) / H x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 2)

If H(0) = 0 and H'(0) = d ≠ 0, then H(2x)/H(x) → 2 as x → 0⁺.

Lower tails of strict families

theorem ProbabilityTheory.Copula.hasLowerTailDependence_nelsen13 (θ : ℝ) (hθ : 0 < θ) : (nelsen13 θ hθ).HasLowerTailDependence 0

Nelsen's family 13 has no lower tail dependence.

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

Nelsen's family 10 has no lower tail dependence.

theorem ProbabilityTheory.Copula.hasLowerTailDependence_nelsen17 (θ : ℝ) (hθ : θ ≠ 0) : (nelsen17 θ hθ).HasLowerTailDependence 0

Nelsen's family 17 has no lower tail dependence.

Upper tail of family 21

theorem ProbabilityTheory.Copula.hasUpperTailDependence_nelsen21 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen21 θ hθ).HasUpperTailDependence (2 - 2 ^ θ⁻¹)

Nelsen's family 21 has upper tail-dependence coefficient λ_U = 2 − 2^{1/θ}.