← Copula mathematical handbook

Conditional total positivity does not require an MTP2 density

theorem ProbabilityTheory.Copula.volume_cube_diagonal : MeasureTheory.volume {x : Fin 2 → ↑unitInterval | x 0 = x 1} = 0

theorem ProbabilityTheory.Copula.not_hasMTP2Density_comonotonic : ¬(comonotonic 2).HasMTP2Density

Comonotonicity has a TP2 conditional kernel, but no Lebesgue MTP2 density.

theorem ProbabilityTheory.Copula.isNQD_independence : (independence 2).IsNQD

theorem ProbabilityTheory.Copula.isNQD_countermonotonic : countermonotonic.IsNQD

theorem ProbabilityTheory.Copula.isPQD_and_isNQD_iff (C : Copula 2) : C.IsPQD ∧ C.IsNQD ↔ C = independence 2