Documentation

Copula.Dependence.HierarchyCorner

← Copula mathematical handbook

Corner set monotonicity: LCSD and RCSI #

Harris (1970) introduced the corner set monotonicity notions (Nelsen, An Introduction to Copulas, 2nd ed., §5.2.3):

(X, Y) is left corner set decreasing (LCSD) if P(X ≤ x, Y ≤ y | X ≤ x', Y ≤ y') is nonincreasing in x' and y';
(X, Y) is right corner set increasing (RCSI) if P(X > x, Y > y | X > x', Y > y') is nondecreasing in x' and y'.

For copulas we state both conditions division-free, cross-multiplying the conditional probabilities (IsLCSD, IsRCSI); boundary cases with vanishing conditioning probabilities are then automatically included. We prove

LCSD is equivalent to total positivity of the copula CDF (isLCSD_iff_isTP2CDF);
RCSI is equivalent to total positivity of the joint survival function (u, v) ↦ 1 - u - v + C(u, v) (isRCSI_iff_isTP2_survival), and to LCSD of the survival copula (isRCSI_iff_survivalCopula_isLCSD); these two characterizations are covered by Nelsen's Theorem 5.2.15 and Corollary 5.2.17 (TP2 of C̄ is equivalent to TP2 of the survival copula Ĉ(u, v) = C̄(1 - u, 1 - v));
both notions are symmetric in the coordinates;
LCSD implies LTD in both directions, RCSI implies RTI in both directions (Nelsen §5.2.3), hence both imply PQD;
M and Π are LCSD and RCSI, while W is neither.

def ProbabilityTheory.Copula.IsLCSD (C : Copula 2) :

Left corner set decreasing, in cross-multiplied form: P(U ≤ u, V ≤ v | U ≤ a, V ≤ b) is nonincreasing in (a, b).

Equations

C.IsLCSD = ∀ (u v a b a' b' : ↑unitInterval), a ≤ a' → b ≤ b' → C.cdf ![min u a', min v b'] * C.cdf ![a, b] ≤ C.cdf ![min u a, min v b] * C.cdf ![a', b']

Instances For

def ProbabilityTheory.Copula.IsRCSI (C : Copula 2) :

Right corner set increasing, in cross-multiplied form: P(U > u, V > v | U > a, V > b) is nondecreasing in (a, b).

Equations

C.IsRCSI = ∀ (u v a b a' b' : ↑unitInterval), a ≤ a' → b ≤ b' → C.survival ![max u a, max v b] * C.survival ![a', b'] ≤ C.survival ![max u a', max v b'] * C.survival ![a, b]

Instances For

A two-step argument for TP2 functions #

LCSD #

theorem ProbabilityTheory.Copula.isLCSD_iff_isTP2CDF (C : Copula 2) :

C.IsLCSD ↔ C.IsTP2CDF

LCSD is equivalent to total positivity of the copula CDF (Nelsen, §5.2.3; cf. Theorem 5.2.15 and Corollary 5.2.17).

theorem ProbabilityTheory.Copula.IsLCSD.isTP2CDF {C : Copula 2} (h : C.IsLCSD) :

theorem ProbabilityTheory.Copula.IsTP2CDF.isLCSD {C : Copula 2} (h : C.IsTP2CDF) :

theorem ProbabilityTheory.Copula.IsLCSD.transpose {C : Copula 2} (h : C.IsLCSD) :

C.transpose.IsLCSD

LCSD is symmetric in the two coordinates.

theorem ProbabilityTheory.Copula.IsLCSD.isLTD {C : Copula 2} (h : C.IsLCSD) :

LCSD implies left tail decreasingness of V given U (Nelsen, §5.2.3).

theorem ProbabilityTheory.Copula.IsLCSD.isLTD_transpose {C : Copula 2} (h : C.IsLCSD) :

C.transpose.IsLTD

LCSD implies left tail decreasingness of U given V (Nelsen, §5.2.3).

theorem ProbabilityTheory.Copula.IsLCSD.isPQD {C : Copula 2} (h : C.IsLCSD) :

RCSI #

theorem ProbabilityTheory.Copula.survival_two_eq_survivalCopula (C : Copula 2) (x y : ↑unitInterval) :

C.survival ![x, y] = C.survivalCopula.cdf ![unitInterval.symm x, unitInterval.symm y]

The bivariate joint survival function as a CDF value of the survival copula.

theorem ProbabilityTheory.Copula.isRCSI_iff_survivalCopula_isLCSD (C : Copula 2) :

C.IsRCSI ↔ C.survivalCopula.IsLCSD

RCSI of a copula is LCSD of its survival copula.

theorem ProbabilityTheory.Copula.isRCSI_iff_isTP2_survival (C : Copula 2) :

C.IsRCSI ↔ IsTP2 fun (u v : ↑unitInterval) => C.survival ![u, v]

RCSI is equivalent to total positivity of the joint survival function (Nelsen, §5.2.3; cf. Theorem 5.2.15 and Corollary 5.2.17).

theorem ProbabilityTheory.Copula.survival_transpose_two (C : Copula 2) (x y : ↑unitInterval) :

C.transpose.survival ![x, y] = C.survival ![y, x]

The joint survival function of the transposed copula.

theorem ProbabilityTheory.Copula.IsRCSI.transpose {C : Copula 2} (h : C.IsRCSI) :

C.transpose.IsRCSI

RCSI is symmetric in the two coordinates.

theorem ProbabilityTheory.Copula.IsRCSI.isRTI {C : Copula 2} (h : C.IsRCSI) :

RCSI implies right tail increasingness of V given U (Nelsen, §5.2.3).

theorem ProbabilityTheory.Copula.IsRCSI.isRTI_transpose {C : Copula 2} (h : C.IsRCSI) :

C.transpose.IsRTI

RCSI implies right tail increasingness of U given V (Nelsen, §5.2.3).

theorem ProbabilityTheory.Copula.IsRCSI.isPQD {C : Copula 2} (h : C.IsRCSI) :

Benchmarks #

theorem ProbabilityTheory.Copula.isLCSD_independence :

(independence 2).IsLCSD

theorem ProbabilityTheory.Copula.isLCSD_comonotonic :

(comonotonic 2).IsLCSD

theorem ProbabilityTheory.Copula.isRCSI_independence :

(independence 2).IsRCSI

theorem ProbabilityTheory.Copula.isRCSI_comonotonic :

(comonotonic 2).IsRCSI

theorem ProbabilityTheory.Copula.not_isLCSD_countermonotonic :

¬countermonotonic.IsLCSD

theorem ProbabilityTheory.Copula.not_isRCSI_countermonotonic :

¬countermonotonic.IsRCSI