← Mathematical handbook

The final inequality of Theorem 1.2 and its equality case

For every stochastically increasing copula C, ξ(C) ≤ 1 - (3/4)(1 - β(C))², with equality iff C = R_{β(C)}. We also record ξ(R_b) = 1 - (3/4)(1 - b)², a consequence of the equality case of Lemma 5.2.

theorem Papers.OrendayLaresRockel2026XiBeta.xi_Rb (b : ℝ) (hb : b ∈ Set.Icc 0 1) : (Rb b hb).chatterjeeXi = 1 - 3 / 4 * (1 - b) ^ 2

The value of ξ at the right-boundary copula R_b (Proposition 5.3 (iii), ξ part).

theorem Papers.OrendayLaresRockel2026XiBeta.si_beta_mem_Icc (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.blomqvistBeta ∈ Set.Icc 0 1

Stochastic increasingness forces β ∈ [0,1].

theorem Papers.OrendayLaresRockel2026XiBeta.si_bound_data (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : ∃ (s : MedianSection), (∀ (u : ↑unitInterval), s.A ↑u = C.cdf ![u, ProbabilityTheory.Copula.unitHalf]) ∧ s.slopeData.q = (1 - C.blomqvistBeta) / 2 ∧ C.chatterjeeXi ≤ s.completion.chatterjeeXi ∧ s.completion.chatterjeeXi = 1 - 3 / 2 * s.slopeData.J ∧ 2 * s.slopeData.q ^ 2 ≤ s.slopeData.J

The two-branch bound, together with the data needed for its equality case.

theorem Papers.OrendayLaresRockel2026XiBeta.xi_le_of_isSI (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi ≤ 1 - 3 / 4 * (1 - C.blomqvistBeta) ^ 2

The final inequality of Theorem 1.2: ξ(C) ≤ 1 - (3/4)(1 - β(C))² for SI copulas.

theorem Papers.OrendayLaresRockel2026XiBeta.xi_eq_iff_of_isSI (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi = 1 - 3 / 4 * (1 - C.blomqvistBeta) ^ 2 ↔ C = Rb C.blomqvistBeta ⋯

Equality case of Theorem 1.2: equality holds iff C = R_{β(C)}.