← Mathematical handbook

Coordinate direction and symmetric dependence properties

@[simp]

theorem ProbabilityTheory.Copula.cdf_reindex_swap (C : Copula 2) (u v : ↑unitInterval) : (C.reindex ![1, 0]).cdf ![u, v] = C.cdf ![v, u]

theorem ProbabilityTheory.Copula.reindex_swap_swap (C : Copula 2) : (C.reindex ![1, 0]).reindex ![1, 0] = C

theorem ProbabilityTheory.Copula.IsPQD.reindex_swap {C : Copula 2} (h : C.IsPQD) : (C.reindex ![1, 0]).IsPQD

theorem ProbabilityTheory.Copula.isPQD_reindex_swap_iff (C : Copula 2) : (C.reindex ![1, 0]).IsPQD ↔ C.IsPQD

theorem ProbabilityTheory.Copula.IsTP2CDF.reindex_swap {C : Copula 2} (h : C.IsTP2CDF) : (C.reindex ![1, 0]).IsTP2CDF

theorem ProbabilityTheory.Copula.isTP2CDF_reindex_swap_iff (C : Copula 2) : (C.reindex ![1, 0]).IsTP2CDF ↔ C.IsTP2CDF

theorem ProbabilityTheory.Copula.IsTP2CDF.isLTD_swap {C : Copula 2} (h : C.IsTP2CDF) : (C.reindex ![1, 0]).IsLTD

CDF-TP2 also implies LTD in the opposite coordinate direction.