← Copula mathematical handbook

Tail independence of the Gaussian copula

The bivariate Gaussian copula with correlation r < 1 is tail independent: λ_L = λ_U = 0 (Sibuya 1960). For r = 1 it is M with λ_L = λ_U = 1.

Proof

For 0 ≤ r < 1 and x < 0, C_r(Φ(x), Φ(x)) = P(X ≤ x, Y ≤ x) ≤ P(X + Y ≤ 2x) = Φ(c x) with c = 2/√(2 + 2r) > 1. The Chernoff bound Φ(y) ≤ exp(−y²/2) and the density bound Φ(y) ≥ φ(y − 1) for y ≤ 0 give Φ(c x)/Φ(x) → 0 as x → −∞. Negative correlations are dominated by Π (Slepian), and the upper tail follows from radial symmetry.

References

• M. Sibuya, Bivariate extreme statistics I, Ann. Inst. Statist. Math. 11 (1960).
• R. B. Nelsen, An Introduction to Copulas, 2nd ed., Springer 2006, §5.4.
• H. Joe, Dependence Modeling with Copulas, CRC Press 2014, §4.3.

theorem ProbabilityTheory.Copula.standardNormalCDF_le_exp {y : ℝ} (hy : y ≤ 0) : ↑(ProbabilityTheory.cdf (gaussianReal 0 1)) y ≤ Real.exp (-y ^ 2 / 2)

Chernoff bound for the standard normal lower tail: Φ(y) ≤ exp(−y²/2) for y ≤ 0.

theorem ProbabilityTheory.Copula.gaussianPDFReal_sub_one_le_standardNormalCDF {y : ℝ} (hy : y ≤ 0) : gaussianPDFReal 0 1 (y - 1) ≤ ↑(ProbabilityTheory.cdf (gaussianReal 0 1)) y

Density lower bound for the standard normal lower tail: Φ(y) ≥ φ(y − 1) for y ≤ 0.

theorem ProbabilityTheory.Copula.cdf_bivariateGaussian_diag_le {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hr0 : 0 ≤ r) (x : ℝ) : (bivariateGaussian r hr).cdf (normalCDFPair (x, x)) ≤ ↑(ProbabilityTheory.cdf (gaussianReal 0 1)) (2 * x / √(2 + 2 * r))

For 0 ≤ r ≤ 1 and σ = √(2 + 2r), C_r(Φ(x), Φ(x)) ≤ Φ(2x/σ).

theorem ProbabilityTheory.Copula.exists_standardNormalCDF_mul_le {c : ℝ} (hc : 1 < c) {ε : ℝ} (hε : 0 < ε) : ∃ x₀ < 0, ∀ x ≤ x₀, ↑(ProbabilityTheory.cdf (gaussianReal 0 1)) (c * x) ≤ ε * ↑(ProbabilityTheory.cdf (gaussianReal 0 1)) x

The tail estimate: for c > 1, Φ(c x) ≤ ε Φ(x) for all sufficiently negative x.

theorem ProbabilityTheory.Copula.hasLowerTailDependence_zero_of_forall {C : Copula 2} (h : ∀ ε > 0, ∃ δ > 0, ∀ (t : ↑unitInterval), 0 < ↑t → ↑t < δ → C.diagonal t ≤ ε * ↑t) : C.HasLowerTailDependence 0

A criterion for vanishing lower tail dependence.

theorem ProbabilityTheory.Copula.hasLowerTailDependence_bivariateGaussian {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hr1 : r < 1) : (bivariateGaussian r hr).HasLowerTailDependence 0

Tail independence of the Gaussian copula (lower tail): λ_L(C_r) = 0 for r < 1.

theorem ProbabilityTheory.Copula.hasUpperTailDependence_bivariateGaussian {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hr1 : r < 1) : (bivariateGaussian r hr).HasUpperTailDependence 0

Tail independence of the Gaussian copula (upper tail): λ_U(C_r) = 0 for r < 1.

theorem ProbabilityTheory.Copula.hasLowerTailDependence_bivariateGaussian_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (bivariateGaussian r hr).HasLowerTailDependence 0 ↔ r < 1

Tail dependence of the Gaussian copula: λ_L(C_r) = 0 for r < 1 and λ_L(C_1) = 1.