← Copula mathematical handbook

Copulas are determined by their distribution functions

Coordinate lower intervals generate the Borel sigma algebra of the unit interval. Their finite products form a generating pi-system on the cube. Consequently, two copulas with equal CDFs have equal underlying measures.

theorem ProbabilityTheory.Copula.ext_cdf {d : ℕ} {C D : Copula d} (h : ∀ (u : Fin d → ↑unitInterval), C.cdf u = D.cdf u) : C = D

Two copulas are equal if their distribution functions agree at every point.

theorem ProbabilityTheory.Copula.cdf_injective {d : ℕ} : Function.Injective cdf

The CDF representation is injective.

theorem ProbabilityTheory.Copula.cdf_eq_iff {d : ℕ} {C D : Copula d} : C.cdf = D.cdf ↔ C = D