← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.norm_orderSign_le_one {α : Type u_1} [LinearOrder α] (x y : α) : ‖orderSign x y‖ ≤ 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.measurable_orderSign : Measurable fun (p : ↑unitInterval × ↑unitInterval) => orderSign p.1 p.2

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.integral_orderSign (C : Copula 2) (i : Fin 2) (t : ↑unitInterval) : ∫ (x : Fin 2 → ↑unitInterval), orderSign t (x i) ∂C.toMeasure = 1 - 2 * ↑t

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.integral_rank_product (C : Copula 2) : 3 * ∫ (x : Fin 2 → ↑unitInterval), (1 - 2 * ↑(x 0)) * (1 - 2 * ↑(x 1)) ∂C.toMeasure = C.spearmanRho

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.integral_orderSign_product (C : Copula 2) : ∫ (p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval)), orderSign (p.1 0) (p.2 0) * orderSign (p.1 1) (p.2 1) ∂C.toMeasure.prod C.toMeasure = C.kendallTau