← Mathematical handbook

Theorem 2 and the equality cases in Lemma 8

The copula statements have no density or parametric-family restriction. For the scalar lemma, equality of functions is almost everywhere: integrals cannot distinguish choices on null sets, including interval endpoints. The proof uses pairwise moment defects, rather than the source's maximum-principle argument.

noncomputable def Papers.AnsariRockel2026XiRho.decreasingFunctional (g : ↑unitInterval → ℝ) : ℝ

The functional F_v from Lemma 8; its admissible functions have mean v.

Equations

• Papers.AnsariRockel2026XiRho.decreasingFunctional g = ∫ (u : ↑unitInterval), 2 * ((1 - ↑u) * g u) - g u ^ 2

theorem Papers.AnsariRockel2026XiRho.lemma8_bound {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (v : ↑unitInterval) (hm : ∫ (u : ↑unitInterval), g u = ↑v) : ↑v * (1 - ↑v) ≤ decreasingFunctional g

Lemma 8, inequality, including the mean endpoints.

theorem Papers.AnsariRockel2026XiRho.lemma8_equality {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (v : ↑unitInterval) (hm : ∫ (u : ↑unitInterval), g u = ↑v) : decreasingFunctional g = ↑v * (1 - ↑v) ↔ (∀ᵐ (u : ↑unitInterval), g u = ↑v) ∨ g =ᵐ[MeasureTheory.volume] (Set.Iic v).indicator fun (x : ↑unitInterval) => 1

Lemma 8, equality classification modulo null sets.

theorem Papers.AnsariRockel2026XiRho.si_xi_eq_rho_iff (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi = C.spearmanRho ↔ C = ProbabilityTheory.Copula.independence 2 ∨ C = ProbabilityTheory.Copula.comonotonic 2

theorem Papers.AnsariRockel2026XiRho.sd_xi_eq_neg_rho_iff (C : ProbabilityTheory.Copula 2) (hC : C.IsSD) : C.chatterjeeXi = -C.spearmanRho ↔ C = ProbabilityTheory.Copula.independence 2 ∨ C = ProbabilityTheory.Copula.countermonotonic

theorem Papers.AnsariRockel2026XiRho.stochastic_xi_eq_abs_rho_iff (C : ProbabilityTheory.Copula 2) (hC : C.IsSI ∨ C.IsSD) : C.chatterjeeXi = |C.spearmanRho| ↔ C = ProbabilityTheory.Copula.countermonotonic ∨ C = ProbabilityTheory.Copula.independence 2 ∨ C = ProbabilityTheory.Copula.comonotonic 2

Theorem 2: the full equality classification.

theorem Papers.AnsariRockel2026XiRho.stochastic_xi_lt_abs_rho (C : ProbabilityTheory.Copula 2) (hC : C.IsSI ∨ C.IsSD) (hw : C ≠ ProbabilityTheory.Copula.countermonotonic) (hp : C ≠ ProbabilityTheory.Copula.independence 2) (hm : C ≠ ProbabilityTheory.Copula.comonotonic 2) : C.chatterjeeXi < |C.spearmanRho|