← Mathematical handbook

Remark 2.6(c): the complete lower semilinear xi--footrule region

theorem Papers.Rockel2026XiFootrule.lowerSemilinear_xi_le_footrule (C : ProbabilityTheory.Copula 2) (hC : Verification.IsLowerSemilinear C) : C.chatterjeeXi ≤ C.spearmanFootrule

The sharp LSL lower bound holds without assuming stochastic increase.

theorem Papers.Rockel2026XiFootrule.exact_lowerSemilinear_xi_footrule_region (x y : ℝ) : (∃ (C : ProbabilityTheory.Copula 2), Verification.IsLowerSemilinear C ∧ C.chatterjeeXi = x ∧ C.spearmanFootrule = y) ↔ x ∈ Set.Icc 0 1 ∧ y ∈ Set.Icc 0 1 ∧ x ≤ y ∧ y ≤ √x

The full LSL region has the same two boundaries as the SI region.

theorem Papers.Rockel2026XiFootrule.lowerSemilinear_region_eq_si (x y : ℝ) : (∃ (C : ProbabilityTheory.Copula 2), Verification.IsLowerSemilinear C ∧ C.chatterjeeXi = x ∧ C.spearmanFootrule = y) ↔ ∃ (C : ProbabilityTheory.Copula 2), C.IsSI ∧ C.chatterjeeXi = x ∧ C.spearmanFootrule = y

Every pair is attainable in the LSL class exactly when it is attainable in the SI class.