← Copula mathematical handbook

Tail dependence of Archimedean copulas via the generator

Nelsen, An Introduction to Copulas, second edition, Corollary 5.4.3: for an Archimedean copula with inverse generator ψ = φ^[-1],

• λ_L = lim_{x → ∞} ψ(2x) / ψ(x) for a strict generator (BivariateGenerator.hasLowerTailDependence_of_tendsto), and λ_L = 0 for a non-strict one (BivariateGenerator.hasLowerTailDependence_zero_of_not_isStrict);
• λ_U = 2 − lim_{x → 0+} (1 − ψ(2x)) / (1 − ψ(x)) (BivariateGenerator.hasUpperTailDependence_of_tendsto). This comes from the left derivative of the diagonal at one, δ'(1⁻) = lim_{x → 0+} (1 − ψ(2x)) / (1 − ψ(x)) (BivariateGenerator.hasDerivWithinAt_diagonal_one).

If ψ has a finite nonzero right derivative at 0 (equivalently φ'(1⁻) ≠ 0), the limit is 2, so δ'(1⁻) = 2 and λ_U = 0 (BivariateGenerator.hasUpperTailDependence_zero_of_hasDerivWithinAt; Nelsen, Section 5.4). No differentiability is assumed in the general statements. The limits along the generator are transported to the tail ratios of Copula.TailDependence by the facts φ(t) → ∞ as t → 0+ for strict generators (BivariateGenerator.IsStrict.tendsto_invFun_atTop) and φ(t) → 0+ as t → 1- (BivariateGenerator.tendsto_invFunReal_one).

theorem ProbabilityTheory.Copula.BivariateGenerator.toFun_lt_one (g : BivariateGenerator) {s : ℝ} (hs : 0 < s) : g.toFun s < 1

ψ(s) < 1 for s > 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsStrict.tendsto_invFun_atTop {g : BivariateGenerator} (hg : g.IsStrict) : Filter.Tendsto (fun (t : ↑unitInterval) => g.invFun t) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

For a strict generator φ(t) → ∞ as t → 0+.

theorem ProbabilityTheory.Copula.BivariateGenerator.tendsto_invFunReal_one (g : BivariateGenerator) : Filter.Tendsto g.invFunReal (nhdsWithin 1 (Set.Icc 0 1 \ {1})) (nhdsWithin 0 (Set.Ioi 0))

φ(x) → 0+ as x → 1 within [0, 1] \ {1}.

theorem ProbabilityTheory.Copula.BivariateGenerator.lowerTailRatio_copula (g : BivariateGenerator) {t : ↑unitInterval} (ht : t ≠ 0) : g.copula.lowerTailRatio t = g.toFun (2 * g.invFun t) / g.toFun (g.invFun t)

The lower tail ratio along the generator: δ(t) / t = ψ(2φ(t)) / ψ(φ(t)).

theorem ProbabilityTheory.Copula.BivariateGenerator.hasLowerTailDependence_of_tendsto {g : BivariateGenerator} (hg : g.IsStrict) {l : ℝ} (h : Filter.Tendsto (fun (x : ℝ) => g.toFun (2 * x) / g.toFun x) Filter.atTop (nhds l)) : g.copula.HasLowerTailDependence l

Nelsen, Corollary 5.4.3 (lower tail): for a strict generator, λ_L = lim_{x → ∞} ψ(2x) / ψ(x) whenever this limit exists.

theorem ProbabilityTheory.Copula.BivariateGenerator.hasLowerTailDependence_zero_of_not_isStrict {g : BivariateGenerator} (hg : ¬g.IsStrict) : g.copula.HasLowerTailDependence 0

A non-strict generator has no lower tail dependence (Nelsen, Section 5.4).

theorem ProbabilityTheory.Copula.BivariateGenerator.hasDerivWithinAt_diagonal_one (g : BivariateGenerator) {m : ℝ} (h : Filter.Tendsto (fun (x : ℝ) => (1 - g.toFun (2 * x)) / (1 - g.toFun x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds m)) : HasDerivWithinAt (fun (x : ℝ) => g.copula.diagonal (Set.projIcc 0 1 ⋯ x)) m (Set.Icc 0 1) 1

Nelsen, Corollary 5.4.3 (the diagonal at one): if (1 − ψ(2x)) / (1 − ψ(x)) → m as x → 0+, the diagonal has left derivative m at one.

theorem ProbabilityTheory.Copula.BivariateGenerator.hasUpperTailDependence_of_tendsto (g : BivariateGenerator) {m : ℝ} (h : Filter.Tendsto (fun (x : ℝ) => (1 - g.toFun (2 * x)) / (1 - g.toFun x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds m)) : g.copula.HasUpperTailDependence (2 - m)

Nelsen, Corollary 5.4.3 (upper tail): λ_U = 2 − lim_{x → 0+} (1 − ψ(2x)) / (1 − ψ(x)) whenever this limit exists.

theorem ProbabilityTheory.Copula.BivariateGenerator.tendsto_upperRatio_of_hasDerivWithinAt (g : BivariateGenerator) {d : ℝ} (hd : HasDerivWithinAt g.toFun d (Set.Ici 0) 0) (hd0 : d ≠ 0) : Filter.Tendsto (fun (x : ℝ) => (1 - g.toFun (2 * x)) / (1 - g.toFun x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 2)

If ψ has a finite nonzero right derivative at 0, then (1 − ψ(2x)) / (1 − ψ(x)) → 2 as x → 0+.

theorem ProbabilityTheory.Copula.BivariateGenerator.hasDerivWithinAt_diagonal_one_two (g : BivariateGenerator) {d : ℝ} (hd : HasDerivWithinAt g.toFun d (Set.Ici 0) 0) (hd0 : d ≠ 0) : HasDerivWithinAt (fun (x : ℝ) => g.copula.diagonal (Set.projIcc 0 1 ⋯ x)) 2 (Set.Icc 0 1) 1

δ'(1⁻) = 2 when ψ has a finite nonzero right derivative at 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.hasUpperTailDependence_zero_of_hasDerivWithinAt (g : BivariateGenerator) {d : ℝ} (hd : HasDerivWithinAt g.toFun d (Set.Ici 0) 0) (hd0 : d ≠ 0) : g.copula.HasUpperTailDependence 0

A finite nonzero right derivative of ψ at 0 (equivalently φ'(1⁻) ≠ 0) excludes upper tail dependence.