← Mathematical handbook

Proposition 2.2: complete equality classification in the SI class

The source representation uses open intervals and equality almost everywhere in both variables. The cut functions are nondecreasing and measurable; the middle level is measurable. Singular copulas are included. The proof uses an elementary nonnegative moment defect rather than Lebesgue-Stieltjes integration by parts.

noncomputable def Papers.Rockel2026XiFootrule.siEqualityProfile (A B a u : ↑unitInterval) : ℝ

Equation (11), including the source's open-interval convention.

Equations

• Papers.Rockel2026XiFootrule.siEqualityProfile A B a u = (if u < A then 1 else 0) + ↑a * if A < u ∧ u < B then 1 else 0

theorem Papers.Rockel2026XiFootrule.si_equality_iff_diagonal_moments (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi = C.spearmanFootrule ↔ ∀ᵐ (v : ↑unitInterval), ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2 = C.cdf ![v, v]

theorem Papers.Rockel2026XiFootrule.si_equality_canonical_parameters (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (he : C.chatterjeeXi = C.spearmanFootrule) : Monotone (Verification.conditionalOneCut C) ∧ Monotone (Verification.conditionalPositiveCut C) ∧ Measurable (Verification.conditionalOneCut C) ∧ Measurable (Verification.conditionalPositiveCut C) ∧ Measurable (Verification.conditionalMiddle C) ∧ (∀ (v : ↑unitInterval), Verification.conditionalOneCut C v ≤ v ∧ v ≤ Verification.conditionalPositiveCut C v) ∧ ∀ᵐ (v : ↑unitInterval) (u : ↑unitInterval), C.conditionalCDF u v = siEqualityProfile (Verification.conditionalOneCut C v) (Verification.conditionalPositiveCut C v) (Verification.conditionalMiddle C v) u

Explicit witnesses for the existential functions in Proposition 2.2.

theorem Papers.Rockel2026XiFootrule.si_equality_iff_conditional_threeLevel (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi = C.spearmanFootrule ↔ ∃ (A : ↑unitInterval → ↑unitInterval) (B : ↑unitInterval → ↑unitInterval) (a : ↑unitInterval → ↑unitInterval), Monotone A ∧ Monotone B ∧ Measurable A ∧ Measurable B ∧ Measurable a ∧ ∀ᵐ (v : ↑unitInterval) (u : ↑unitInterval), C.conditionalCDF u v = siEqualityProfile (A v) (B v) (a v) u

Proposition 2.2 in the conditional-CDF convention.

theorem Papers.Rockel2026XiFootrule.si_equality_iff_derivative_threeLevel (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi = C.spearmanFootrule ↔ ∃ (A : ↑unitInterval → ↑unitInterval) (B : ↑unitInterval → ↑unitInterval) (a : ↑unitInterval → ↑unitInterval), Monotone A ∧ Monotone B ∧ Measurable A ∧ Measurable B ∧ Measurable a ∧ ∀ᵐ (v : ↑unitInterval) (u : ↑unitInterval), deriv (C.cdfSection v) ↑u = siEqualityProfile (A v) (B v) (a v) u

Proposition 2.2 in the source's first partial derivative convention.