← Mathematical handbook

Uniqueness in dimensions zero and one

instance ProbabilityTheory.Copula.instSubsingletonOfNatNat : Subsingleton (Copula 0)

@[simp]

theorem ProbabilityTheory.Copula.cdf_dim_one (C : Copula 1) (u : Fin 1 → ↑unitInterval) : C.cdf u = ↑(u 0)

instance ProbabilityTheory.Copula.instSubsingletonOfNatNat_1 : Subsingleton (Copula 1)

theorem ProbabilityTheory.Copula.eq_independence_dim_one (C : Copula 1) : C = independence 1

theorem ProbabilityTheory.Copula.independence_eq_comonotonic_dim_one : independence 1 = comonotonic 1