← Copula mathematical handbook

Independence, concordance and countermonotonicity benchmarks

theorem ProbabilityTheory.Copula.integral_unit_min_symm : ∫ (t : ↑unitInterval), min (↑t) (1 - ↑t) = 1 / 4

theorem ProbabilityTheory.Copula.integral_unit_max_two_mul_sub_one : ∫ (t : ↑unitInterval), max 0 (2 * ↑t - 1) = 1 / 4

@[simp]

theorem ProbabilityTheory.Copula.blomqvistBeta_independence : (independence 2).blomqvistBeta = 0

@[simp]

theorem ProbabilityTheory.Copula.blomqvistBeta_comonotonic : (comonotonic 2).blomqvistBeta = 1

@[simp]

theorem ProbabilityTheory.Copula.blomqvistBeta_countermonotonic : countermonotonic.blomqvistBeta = -1

@[simp]

theorem ProbabilityTheory.Copula.kendallTau_independence : (independence 2).kendallTau = 0

@[simp]

theorem ProbabilityTheory.Copula.kendallTau_comonotonic : (comonotonic 2).kendallTau = 1

@[simp]

theorem ProbabilityTheory.Copula.kendallTau_countermonotonic : countermonotonic.kendallTau = -1

@[simp]

theorem ProbabilityTheory.Copula.spearmanFootrule_independence : (independence 2).spearmanFootrule = 0

@[simp]

theorem ProbabilityTheory.Copula.spearmanFootrule_comonotonic : (comonotonic 2).spearmanFootrule = 1

@[simp]

theorem ProbabilityTheory.Copula.spearmanFootrule_countermonotonic : countermonotonic.spearmanFootrule = -1 / 2

@[simp]

theorem ProbabilityTheory.Copula.giniGamma_independence : (independence 2).giniGamma = 0

@[simp]

theorem ProbabilityTheory.Copula.giniGamma_comonotonic : (comonotonic 2).giniGamma = 1

@[simp]

theorem ProbabilityTheory.Copula.giniGamma_countermonotonic : countermonotonic.giniGamma = -1

theorem ProbabilityTheory.Copula.spearmanFootrule_mem_Icc (C : Copula 2) : C.spearmanFootrule ∈ Set.Icc (-1 / 2) 1

theorem ProbabilityTheory.Copula.giniGamma_mem_Icc (C : Copula 2) : C.giniGamma ∈ Set.Icc (-1) 1