Positive quadrant dependence of ordinal sums #
theorem
ProbabilityTheory.Copula.IsPQD.ordinalSum
{C D : Copula 2}
(hC : C.IsPQD)
(hD : D.IsPQD)
(a : ↑unitInterval)
:
(C.ordinalSum D a).IsPQD
theorem
ProbabilityTheory.Copula.isPQD_ordinalSum_independence
(a : ↑unitInterval)
:
((independence 2).ordinalSum (independence 2) a).IsPQD