← Copula mathematical handbook

Total positivity of the copula measure and the positive dependence hierarchy

A bivariate copula C is TP2 as a measure (IsTP2Measure) if for all measurable sets S₁ ≤ S₂ and T₁ ≤ T₂ of [0,1] (every point of the first set below every point of the second)

C(S₁ × T₂) · C(S₂ × T₁) ≤ C(S₁ × T₁) · C(S₂ × T₂).

For absolutely continuous copulas this is Lehmann's positive likelihood ratio dependence: we prove that an MTP2 (log-supermodular) Lebesgue density implies it (HasMTP2Density.isTP2Measure), by integrating the pointwise TP2 inequality as in the basic composition formula of Karlin. The measure form also covers singular copulas: M is TP2 as a measure but has no density.

From IsTP2Measure we obtain, by choosing the four sets as intervals, the top of the positive dependence hierarchy of Nelsen, An Introduction to Copulas, 2nd ed., §5.2.3, and Joe, Multivariate Models and Dependence Concepts (1997), §2.1:

TP2 density ⟹ IsTP2Measure ⟹ SI(V|U) and SI(U|V) (i.e. CI) ⟹ LTD, RTI ⟹ PQD
                          ⟹ LCSD (= TP2 CDF) ⟹ LTD in both directions
                          ⟹ RCSI (= TP2 survival function) ⟹ RTI in both directions

rectMass C S T denotes the copula mass of the product set S × T.

noncomputable def ProbabilityTheory.Copula.rectMass (C : Copula 2) (S T : Set ↑unitInterval) : ℝ

The copula mass of the product set S × T.

Equations

• C.rectMass S T = C.toMeasure.real {x : Fin 2 → ↑unitInterval | x 0 ∈ S ∧ x 1 ∈ T}

def ProbabilityTheory.Copula.IsTP2Measure (C : Copula 2) : Prop

Total positivity of order two of the copula measure on ordered product sets.

Equations

• One or more equations did not get rendered due to their size.

Rectangle masses

theorem ProbabilityTheory.Copula.measurableSet_rect {S T : Set ↑unitInterval} (hS : MeasurableSet S) (hT : MeasurableSet T) : MeasurableSet {x : Fin 2 → ↑unitInterval | x 0 ∈ S ∧ x 1 ∈ T}

theorem ProbabilityTheory.Copula.rectMass_union_left (C : Copula 2) {S S' T : Set ↑unitInterval} (hS' : MeasurableSet S') (hT : MeasurableSet T) (hd : Disjoint S S') : C.rectMass (S ∪ S') T = C.rectMass S T + C.rectMass S' T

theorem ProbabilityTheory.Copula.rectMass_union_right (C : Copula 2) {S T T' : Set ↑unitInterval} (hS : MeasurableSet S) (hT' : MeasurableSet T') (hd : Disjoint T T') : C.rectMass S (T ∪ T') = C.rectMass S T + C.rectMass S T'

theorem ProbabilityTheory.Copula.rectMass_univ_right (C : Copula 2) {S : Set ↑unitInterval} (hS : MeasurableSet S) : C.rectMass S Set.univ = MeasureTheory.volume.real S

theorem ProbabilityTheory.Copula.rectMass_univ_left (C : Copula 2) {T : Set ↑unitInterval} (hT : MeasurableSet T) : C.rectMass Set.univ T = MeasureTheory.volume.real T

theorem ProbabilityTheory.Copula.rectMass_Iic_Iic (C : Copula 2) (a b : ↑unitInterval) : C.rectMass (Set.Iic a) (Set.Iic b) = C.cdf ![a, b]

theorem ProbabilityTheory.Copula.rectMass_Ioc_left (C : Copula 2) {a b : ↑unitInterval} (hab : a ≤ b) {T : Set ↑unitInterval} (hT : MeasurableSet T) : C.rectMass (Set.Ioc a b) T = C.rectMass (Set.Iic b) T - C.rectMass (Set.Iic a) T

theorem ProbabilityTheory.Copula.rectMass_Ioc_right (C : Copula 2) {c d : ↑unitInterval} (hcd : c ≤ d) {S : Set ↑unitInterval} (hS : MeasurableSet S) : C.rectMass S (Set.Ioc c d) = C.rectMass S (Set.Iic d) - C.rectMass S (Set.Iic c)

theorem ProbabilityTheory.Copula.rectMass_Ioi_left (C : Copula 2) (a : ↑unitInterval) {T : Set ↑unitInterval} (hT : MeasurableSet T) : C.rectMass (Set.Ioi a) T = C.rectMass Set.univ T - C.rectMass (Set.Iic a) T

theorem ProbabilityTheory.Copula.rectMass_Ioi_right (C : Copula 2) (c : ↑unitInterval) {S : Set ↑unitInterval} (hS : MeasurableSet S) : C.rectMass S (Set.Ioi c) = C.rectMass S Set.univ - C.rectMass S (Set.Iic c)

theorem ProbabilityTheory.Copula.rectMass_Iic_Ioi (C : Copula 2) (a c : ↑unitInterval) : C.rectMass (Set.Iic a) (Set.Ioi c) = ↑a - C.cdf ![a, c]

theorem ProbabilityTheory.Copula.rectMass_Ioi_Ioi (C : Copula 2) (a c : ↑unitInterval) : C.rectMass (Set.Ioi a) (Set.Ioi c) = C.survival ![a, c]

Integrating the pointwise TP2 inequality

theorem ProbabilityTheory.Copula.HasMTP2Density.isTP2Measure {C : Copula 2} (h : C.HasMTP2Density) : C.IsTP2Measure

An MTP2 Lebesgue density makes the copula measure TP2 on ordered product sets (Lehmann's positive likelihood ratio dependence).

Consequences of TP2 of the copula measure

theorem ProbabilityTheory.Copula.rectMass_transpose (C : Copula 2) {S T : Set ↑unitInterval} (hS : MeasurableSet S) (hT : MeasurableSet T) : C.transpose.rectMass S T = C.rectMass T S

TP2 of the measure is symmetric in the coordinates.

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

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

TP2 of the measure implies TP2 of the CDF, i.e. LCSD (Nelsen, §5.2).

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

TP2 of the measure implies LCSD.

theorem ProbabilityTheory.Copula.IsTP2Measure.isSI {C : Copula 2} (h : C.IsTP2Measure) : C.IsSI

TP2 of the measure implies stochastic increasingness of V given U.

theorem ProbabilityTheory.Copula.IsTP2Measure.isCI {C : Copula 2} (h : C.IsTP2Measure) : C.IsCI

TP2 of the measure implies stochastic increasingness in both directions (CI).

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

TP2 of the measure implies TP2 of the joint survival function, i.e. RCSI.

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

TP2 of the measure implies RTI in both directions.

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

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

The density level of the hierarchy

theorem ProbabilityTheory.Copula.HasMTP2Density.isSI {C : Copula 2} (h : C.HasMTP2Density) : C.IsSI

An MTP2 density implies stochastic increasingness (Lehmann 1966; Nelsen, §5.2.3).

theorem ProbabilityTheory.Copula.HasMTP2Density.isCI {C : Copula 2} (h : C.HasMTP2Density) : C.IsCI

An MTP2 density implies conditional increasingness in both directions.

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

An MTP2 density implies a TP2 CDF (LCSD).

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

An MTP2 density implies LCSD.

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

An MTP2 density implies RCSI.

Benchmarks

theorem ProbabilityTheory.Copula.isTP2Measure_independence : (independence 2).IsTP2Measure

theorem ProbabilityTheory.Copula.isTP2Measure_comonotonic : (comonotonic 2).IsTP2Measure

M is TP2 as a measure although it has no MTP2 density (not_hasMTP2Density_comonotonic): the density level of the hierarchy is strictly stronger.

theorem ProbabilityTheory.Copula.not_isTP2Measure_countermonotonic : ¬countermonotonic.IsTP2Measure