← Mathematical handbook

The upper xi-footrule boundary

Theorem 2.1 of arXiv:2509.07232v1, in the conditional-CDF formulation. The squared distance to (1-a) Π + a M proves the bound and its unique equality case. No density, stochastic monotonicity, or optimization assumption is imposed on the copula. See COVERAGE.md for the source conventions.

theorem Papers.Rockel2026XiFootrule.xi_upperBoundary (a : ↑unitInterval) : (upperBoundary a).chatterjeeXi = ↑a ^ 2

theorem Papers.Rockel2026XiFootrule.footrule_upperBoundary (a : ↑unitInterval) : (upperBoundary a).spearmanFootrule = ↑a

theorem Papers.Rockel2026XiFootrule.distance_to_upperBoundary (C : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : 6 * C.conditionalCDFDistanceSq (upperBoundary a) = C.chatterjeeXi + ↑a ^ 2 - 2 * ↑a * C.spearmanFootrule

The exact nonnegative defect; vanishing characterizes the extremizer.

theorem Papers.Rockel2026XiFootrule.footrule_le_sqrt_xi (C : ProbabilityTheory.Copula 2) : C.spearmanFootrule ≤ √C.chatterjeeXi

Theorem 2.1: the universal upper bound, including singular copulas.

noncomputable def Papers.Rockel2026XiFootrule.boundaryParameter (x : ↑unitInterval) : ↑unitInterval

The parameter that realizes a prescribed xi.

Equations

• Papers.Rockel2026XiFootrule.boundaryParameter x = ⟨√↑x, ⋯⟩

theorem Papers.Rockel2026XiFootrule.upperBoundary_attains (x : ↑unitInterval) : (upperBoundary (boundaryParameter x)).chatterjeeXi = ↑x ∧ (upperBoundary (boundaryParameter x)).spearmanFootrule = √↑x

Theorem 2.1: the maximum is attained for every x ∈ [0,1].

theorem Papers.Rockel2026XiFootrule.upperBoundary_unique (x : ↑unitInterval) (C : ProbabilityTheory.Copula 2) (hx : C.chatterjeeXi = ↑x) : C.spearmanFootrule = √↑x ↔ C = upperBoundary (boundaryParameter x)

Theorem 2.1: the equality case identifies the unique copula, also at xi=0,1.

theorem Papers.Rockel2026XiFootrule.maximal_footrule (x : ↑unitInterval) : (upperBoundary (boundaryParameter x)).chatterjeeXi = ↑x ∧ (upperBoundary (boundaryParameter x)).spearmanFootrule = √↑x ∧ ∀ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = ↑x → C.spearmanFootrule ≤ √↑x ∧ (C.spearmanFootrule = √↑x ↔ C = upperBoundary (boundaryParameter x))

Theorem 2.1 as a maximum statement together with its unique maximizer.

theorem Papers.Rockel2026XiFootrule.footrule_sub_xi_le (C : ProbabilityTheory.Copula 2) : C.spearmanFootrule - C.chatterjeeXi ≤ 1 / 4

The sharp gap stated after Theorem 2.1 and in the Fréchet row of Table 1.

theorem Papers.Rockel2026XiFootrule.footrule_sub_xi_eq_iff (C : ProbabilityTheory.Copula 2) : C.spearmanFootrule - C.chatterjeeXi = 1 / 4 ↔ C = upperBoundary ProbabilityTheory.Copula.unitHalf

The exact equality case for the gap; numerical rows of Table 1 are not claimed.