← Copula mathematical handbook

Independence, comonotonicity and failures at countermonotonicity

theorem ProbabilityTheory.Copula.hasTP2Kernel_independence : (independence 2).HasTP2Kernel

theorem ProbabilityTheory.Copula.hasTP2Kernel_comonotonic : (comonotonic 2).HasTP2Kernel

theorem ProbabilityTheory.Copula.isSI_independence : (independence 2).IsSI

theorem ProbabilityTheory.Copula.isSI_comonotonic : (comonotonic 2).IsSI

theorem ProbabilityTheory.Copula.isTP2CDF_comonotonic : (comonotonic 2).IsTP2CDF

theorem ProbabilityTheory.Copula.isPQD_independence : (independence 2).IsPQD

theorem ProbabilityTheory.Copula.isLTD_independence : (independence 2).IsLTD

theorem ProbabilityTheory.Copula.isRTI_independence : (independence 2).IsRTI

theorem ProbabilityTheory.Copula.isPQD_comonotonic : (comonotonic 2).IsPQD

theorem ProbabilityTheory.Copula.isLTD_comonotonic : (comonotonic 2).IsLTD

theorem ProbabilityTheory.Copula.isRTI_comonotonic : (comonotonic 2).IsRTI

theorem ProbabilityTheory.Copula.not_isPQD_countermonotonic : ¬countermonotonic.IsPQD

theorem ProbabilityTheory.Copula.not_isLTD_countermonotonic : ¬countermonotonic.IsLTD

theorem ProbabilityTheory.Copula.not_isRTI_countermonotonic : ¬countermonotonic.IsRTI

theorem ProbabilityTheory.Copula.not_isSI_countermonotonic : ¬countermonotonic.IsSI

theorem ProbabilityTheory.Copula.not_isTP2CDF_countermonotonic : ¬countermonotonic.IsTP2CDF

theorem ProbabilityTheory.Copula.not_hasTP2Kernel_countermonotonic : ¬countermonotonic.HasTP2Kernel