← Mathematical handbook

Definitions for Rockel2026XiFootrule

The direction of xi is coordinate 1 given coordinate 0. Footrule has range [-1/2, 1]. The family in Theorem 2.1 of arXiv:2509.07232v1 is represented by its probability measure, with its CDF proved below.

noncomputable def Papers.Rockel2026XiFootrule.upperBoundary (a : ↑unitInterval) : ProbabilityTheory.Copula 2

The Fréchet family (1-a) Π + a M in Theorem 2.1.

Equations

• Papers.Rockel2026XiFootrule.upperBoundary a = (ProbabilityTheory.Copula.comonotonic 2).mix (ProbabilityTheory.Copula.independence 2) a

theorem Papers.Rockel2026XiFootrule.cdf_upperBoundary (a u v : ↑unitInterval) : (upperBoundary a).cdf ![u, v] = (1 - ↑a) * (↑u * ↑v) + ↑a * min ↑u ↑v

Correspondence with the source's explicit CDF, including both endpoints.

theorem Papers.Rockel2026XiFootrule.xi_derivative_formula (C : ProbabilityTheory.Copula 2) : C.chatterjeeXi = (6 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), deriv (C.cdfSection v) ↑u ^ 2) - 2

The source's derivative normalization of xi, without a copula-density assumption.