← Copula mathematical handbook

Algebra of the Markov product: mixtures, idempotents and inverses

Further properties of the Darsow–Nguyen–Olsen Markov product A * B = A.markovProduct B (W. F. Darsow, B. Nguyen and E. T. Olsen, Copulas and Markov processes, Illinois J. Math. 36 (1992); W. F. Darsow and E. T. Olsen, Characterization of idempotent 2-copulas, Note Mat. 30 (2010); Durante and Sempi 2016, §5.2; Nelsen 2006, §6.3):

• the product is bilinear with respect to convex combinations (markovProduct_mix, mix_markovProduct);
• products within the Fréchet–Mardia-type families: (aM + (1-a)Π) * (bM + (1-b)Π) = abM + (1-ab)Π and (aM + (1-a)W) * (bM + (1-b)W) = (ab + (1-a)(1-b))M + (a(1-b)+(1-a)b)W;
• idempotent copulas (IsIdempotent, C * C = C): M and Π are idempotent, W is not, idempotents are closed under transposition, aM + (1-a)Π is idempotent iff a ∈ {0,1}, and C * Cᵀ is idempotent whenever C is left invertible;
• inverses: C has a left inverse (A * C = M for some A) iff Cᵀ * C = M iff ξ(C) = 1 (via the data-processing inequality); it has a right inverse iff ξ(Cᵀ) = 1; a copula with both a left and a right inverse has Cᵀ as its unique two-sided inverse.

Bilinearity

theorem ProbabilityTheory.Copula.integrable_conditionalCDF_mul_conditionalCDF (C D : Copula 2) (u v : ↑unitInterval) : MeasureTheory.Integrable (fun (s : ↑unitInterval) => C.conditionalCDF s u * D.conditionalCDF s v) MeasureTheory.volume

theorem ProbabilityTheory.Copula.markovProduct_mix (A B C : Copula 2) (a : ↑unitInterval) : A.markovProduct (B.mix C a) = (A.markovProduct B).mix (A.markovProduct C) a

Right distributivity: A * (aB + (1-a)C) = a (A * B) + (1-a) (A * C).

theorem ProbabilityTheory.Copula.mix_markovProduct (A B C : Copula 2) (a : ↑unitInterval) : (A.mix B a).markovProduct C = (A.markovProduct C).mix (B.markovProduct C) a

Left distributivity: (aA + (1-a)B) * C = a (A * C) + (1-a) (B * C).

theorem ProbabilityTheory.Copula.mix_mix_right (C D : Copula 2) (a b : ↑unitInterval) : (C.mix D b).mix D a = C.mix D (a * b)

Iterated mixtures of two copulas.

theorem ProbabilityTheory.Copula.markovProduct_mix_comonotonic_independence (a b : ↑unitInterval) : ((comonotonic 2).mix (independence 2) a).markovProduct ((comonotonic 2).mix (independence 2) b) = (comonotonic 2).mix (independence 2) (a * b)

(aM + (1-a)Π) * (bM + (1-b)Π) = abM + (1-ab)Π.

theorem ProbabilityTheory.Copula.cdf_markovProduct_mix_comonotonic_countermonotonic (a b : ↑unitInterval) (u : Fin 2 → ↑unitInterval) : (((comonotonic 2).mix countermonotonic a).markovProduct ((comonotonic 2).mix countermonotonic b)).cdf u = (↑a * ↑b + (1 - ↑a) * (1 - ↑b)) * (comonotonic 2).cdf u + (↑a * (1 - ↑b) + (1 - ↑a) * ↑b) * countermonotonic.cdf u

(aM + (1-a)W) * (bM + (1-b)W) = (ab + (1-a)(1-b)) M + (a(1-b) + (1-a)b) W.

Idempotent copulas

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

A copula is idempotent if C * C = C.

Equations

• C.IsIdempotent = (C.markovProduct C = C)

theorem ProbabilityTheory.Copula.isIdempotent_comonotonic : (comonotonic 2).IsIdempotent

theorem ProbabilityTheory.Copula.isIdempotent_independence : (independence 2).IsIdempotent

theorem ProbabilityTheory.Copula.comonotonic_ne_countermonotonic : comonotonic 2 ≠ countermonotonic

theorem ProbabilityTheory.Copula.not_isIdempotent_countermonotonic : ¬countermonotonic.IsIdempotent

W is not idempotent: W * W = M.

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

theorem ProbabilityTheory.Copula.isIdempotent_mix_comonotonic_independence_iff (a : ↑unitInterval) : ((comonotonic 2).mix (independence 2) a).IsIdempotent ↔ a = 0 ∨ a = 1

aM + (1-a)Π is idempotent only for a ∈ {0,1}.

theorem ProbabilityTheory.Copula.isIdempotent_markovProduct_transpose {C : Copula 2} (h : C.transpose.markovProduct C = comonotonic 2) : (C.markovProduct C.transpose).IsIdempotent

If C is left invertible (Cᵀ * C = M), then C * Cᵀ is idempotent.

theorem ProbabilityTheory.Copula.isIdempotent_markovProduct_transpose_of_chatterjeeXi_eq_one {C : Copula 2} (h : C.chatterjeeXi = 1) : (C.markovProduct C.transpose).IsIdempotent

Copulas with ξ(C) = 1 give idempotents C * Cᵀ.

Left and right inverses

theorem ProbabilityTheory.Copula.exists_left_inverse_iff (C : Copula 2) : (∃ (A : Copula 2), A.markovProduct C = comonotonic 2) ↔ C.chatterjeeXi = 1

C has a left inverse for the Markov product if and only if ξ(C) = 1; the transpose is then a left inverse.

theorem ProbabilityTheory.Copula.exists_right_inverse_iff (C : Copula 2) : (∃ (B : Copula 2), C.markovProduct B = comonotonic 2) ↔ C.transpose.chatterjeeXi = 1

C has a right inverse for the Markov product if and only if ξ(Cᵀ) = 1; the transpose is then a right inverse.

theorem ProbabilityTheory.Copula.markovProduct_transpose_eq_comonotonic_iff (C : Copula 2) : C.markovProduct C.transpose = comonotonic 2 ↔ C.transpose.chatterjeeXi = 1

theorem ProbabilityTheory.Copula.eq_transpose_of_left_right_inverse {A B C : Copula 2} (hA : A.markovProduct C = comonotonic 2) (hB : C.markovProduct B = comonotonic 2) : A = C.transpose ∧ B = C.transpose

A copula with a left inverse A and a right inverse B is invertible with A = B = Cᵀ.