← Copula mathematical handbook

Benchmarks, range, and response-reflection symmetry of Blest's nu

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.blest_integral_formula_swapped (C : Copula 2) : blestNu C = (24 * ∫ (u : ↑unitInterval), (1 - ↑u) * ∫ (v : ↑unitInterval), C.cdf ![u, v]) - 2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.blest_comonotonic : blestNu (comonotonic 2) = 1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.blest_reflect_second (C : Copula 2) : blestNu (C.reflect {1}) = -blestNu C

Equation (13): only the second-coordinate reflection is asserted here.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.blest_countermonotonic : blestNu countermonotonic = -1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.blest_mem_Icc (C : Copula 2) : blestNu C ∈ Set.Icc (-1) 1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.xi_blest_reflection (C : Copula 2) : (C.reflect {1}).chatterjeeXi = C.chatterjeeXi ∧ blestNu (C.reflect {1}) = -blestNu C