← Copula mathematical handbook

Invertible copulas and complete dependence

The characterization of the invertible elements of the Markov product (Darsow, Nguyen and Olsen, Copulas and Markov processes, Illinois J. Math. 36 (1992); Durante and Sempi 2016, §5.2): a bivariate copula has a left inverse if and only if it is completely dependent, i.e. V = f(U) almost surely for a measurable f, and then Cᵀ is a left inverse.

The new ingredient is the converse of IsCompletelyDependent.chatterjeeXi_eq_one (isCompletelyDependent_of_chatterjeeXi_eq_one): if ξ(C) = 1, then the conditional distribution functions take only the values 0 and 1 almost everywhere (∫∫ h(1-h) = 1/2 - ∫∫ h² = 0), hence almost every conditional law is a Dirac mass (eq_dirac_of_ae_cdf), located at the conditional mean f(u) = ∫₀¹ (1 - h(u,t)) dt, a measurable function of u. Consequently:

• C.IsCompletelyDependent ↔ ξ(C) = 1 ↔ Cᵀ * C = M ↔ ∃ A, A * C = M;
• Cᵀ.IsCompletelyDependent ↔ ∃ B, C * B = M;
• C is mutually completely dependent if and only if it is invertible, with inverse Cᵀ;
• M is the only idempotent copula with a left inverse (in particular the only completely dependent idempotent).

Probability measures with two-valued distribution functions

theorem ProbabilityTheory.Copula.eq_dirac_of_ae_cdf {ν : MeasureTheory.Measure ↑unitInterval} [MeasureTheory.IsProbabilityMeasure ν] (h : ∀ᵐ (t : ↑unitInterval), ν.real (Set.Iic t) * (1 - ν.real (Set.Iic t)) = 0) : ν = MeasureTheory.Measure.dirac (Set.projIcc 0 1 ⋯ (∫ (t : ↑unitInterval), 1 - ν.real (Set.Iic t)))

A probability measure on [0,1] whose distribution function takes only the values 0 and 1 (almost everywhere) is the Dirac mass at its mean ∫₀¹ (1 - F).

ξ = 1 forces complete dependence

theorem ProbabilityTheory.Copula.ae_ae_conditionalCDF_mul_one_sub_eq_zero {C : Copula 2} (h : C.chatterjeeXi = 1) : ∀ᵐ (u : ↑unitInterval) (t : ↑unitInterval), C.conditionalCDF u t * (1 - C.conditionalCDF u t) = 0

If ξ(C) = 1, then for almost every u the conditional distribution function t ↦ h(u,t) takes only the values 0 and 1 (almost everywhere).

theorem ProbabilityTheory.Copula.isCompletelyDependent_of_chatterjeeXi_eq_one {C : Copula 2} (h : C.chatterjeeXi = 1) : C.IsCompletelyDependent

Converse of IsCompletelyDependent.chatterjeeXi_eq_one: ξ(C) = 1 implies that V is almost surely a measurable function of U.

theorem ProbabilityTheory.Copula.isCompletelyDependent_iff_chatterjeeXi_eq_one (C : Copula 2) : C.IsCompletelyDependent ↔ C.chatterjeeXi = 1

A copula is completely dependent if and only if Chatterjee's xi equals one.

Invertibility

theorem ProbabilityTheory.Copula.isCompletelyDependent_iff_transpose_markovProduct_self (C : Copula 2) : C.IsCompletelyDependent ↔ C.transpose.markovProduct C = comonotonic 2

C is completely dependent if and only if Cᵀ * C = M.

theorem ProbabilityTheory.Copula.exists_left_inverse_iff_isCompletelyDependent (C : Copula 2) : (∃ (A : Copula 2), A.markovProduct C = comonotonic 2) ↔ C.IsCompletelyDependent

Darsow–Nguyen–Olsen: a copula has a left inverse for the Markov product if and only if it is completely dependent (V = f(U) almost surely).

theorem ProbabilityTheory.Copula.exists_right_inverse_iff_isCompletelyDependent (C : Copula 2) : (∃ (B : Copula 2), C.markovProduct B = comonotonic 2) ↔ C.transpose.IsCompletelyDependent

A copula has a right inverse if and only if its transpose is completely dependent (U = g(V) almost surely).

theorem ProbabilityTheory.Copula.isMutuallyCompletelyDependent_iff (C : Copula 2) : C.IsMutuallyCompletelyDependent ↔ C.transpose.markovProduct C = comonotonic 2 ∧ C.markovProduct C.transpose = comonotonic 2

A copula is invertible (Cᵀ * C = C * Cᵀ = M) if and only if it is mutually completely dependent.

theorem ProbabilityTheory.Copula.IsIdempotent.eq_comonotonic_of_left_inverse {A C : Copula 2} (hC : C.IsIdempotent) (hA : A.markovProduct C = comonotonic 2) : C = comonotonic 2

An idempotent copula with a left inverse is M.

theorem ProbabilityTheory.Copula.IsIdempotent.eq_comonotonic_of_isCompletelyDependent {C : Copula 2} (hC : C.IsIdempotent) (hd : C.IsCompletelyDependent) : C = comonotonic 2

The only completely dependent idempotent copula is M.