← Mathematical handbook

Additional results in the JCAM resubmission

Proposition 3.4 and Corollaries 3.5--3.6 are absent from arXiv v1. The source is recorded by filename and hash in SOURCE_COMPARISON.md.

theorem Papers.Rockel2026XiFootrule.relaxed_mirrored_bound (μ : ℝ) (hμ : μ ∈ Set.Ioc 0 2) : -Verification.relaxedFootrule μ < √(Verification.relaxedXi μ)

The mirrored relaxed curve lies strictly below the square-root curve.

theorem Papers.Rockel2026XiFootrule.negative_footrule_strict (C : ProbabilityTheory.Copula 2) (hC : C.spearmanFootrule < 0) : |C.spearmanFootrule| < √C.chatterjeeXi

The absolute bound is strict whenever footrule is negative.

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

Absolute version of the upper bound, for every copula.

theorem Papers.Rockel2026XiFootrule.abs_footrule_eq_sqrt_xi_iff (C : ProbabilityTheory.Copula 2) : |C.spearmanFootrule| = √C.chatterjeeXi ↔ ∃ (a : ↑unitInterval), C = upperBoundary a

The equality cases are exactly the nonnegative Frechet mixtures.

theorem Papers.Rockel2026XiFootrule.footrule_pair_attained_as_rho (C : ProbabilityTheory.Copula 2) : ∃ (D : ProbabilityTheory.Copula 2), D.chatterjeeXi = C.chatterjeeXi ∧ D.spearmanRho = C.spearmanFootrule

Each footrule pair is attained as a rho pair by an actual copula.

theorem Papers.Rockel2026XiFootrule.footrule_region_ssubset_rho_region : attainableRegion ⊂ AnsariRockel2026XiRho.attainableRegion

Strict containment of the entire attained regions; W supplies a missing pair.