← Mathematical handbook

CDF TP2 under coordinatewise max-products

theorem ProbabilityTheory.Copula.IsTP2CDF.maxProduct {C D : Copula 2} (hC : C.IsTP2CDF) (hD : D.IsTP2CDF) (a : Fin 2 → ↑unitInterval) : (C.maxProduct D a).IsTP2CDF

A max-product of TP2 copulas has a TP2 CDF. This result concerns CDFs; it does not transfer MTP2 of Lebesgue densities.

theorem ProbabilityTheory.Copula.isTP2CDF_marshallOlkin (α β : ↑unitInterval) : (marshallOlkin α β).IsTP2CDF

Marshall–Olkin has a TP2 CDF for all weights, including singular cases. This differs from the separate MTP2-density classification.

theorem ProbabilityTheory.Copula.isTP2CDF_cuadrasAuge (α : ↑unitInterval) : (cuadrasAuge α).IsTP2CDF

The equal-weight Cuadras–Augé subfamily has a TP2 CDF.