← Mathematical handbook

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

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

theorem Papers.Rockel2026XiBlest.blest_comonotonic : blestNu (ProbabilityTheory.Copula.comonotonic 2) = 1

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

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

theorem Papers.Rockel2026XiBlest.blest_countermonotonic : blestNu ProbabilityTheory.Copula.countermonotonic = -1

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

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