← Mathematical handbook

Theorem 1.1, Corollary 4.3 and quantitative introduction claims (version 2)

The witnesses are the article's own: the tent copulas L_b (leftBoundary) and the interval-exchange copulas D_b (dExchange). Regions are the sets xiBetaRegion A.

def Papers.OrendayLaresRockel2026XiBeta.exactRegion : Set (ℝ × ℝ)

The region {(x, y) ∈ [0,1] × [-1,1] : |y|³ ≤ 2x}.

Equations

• Papers.OrendayLaresRockel2026XiBeta.exactRegion = {p : ℝ × ℝ | p.1 ∈ Set.Icc 0 1 ∧ p.2 ∈ Set.Icc (-1) 1 ∧ |p.2| ^ 3 ≤ 2 * p.1}

theorem Papers.OrendayLaresRockel2026XiBeta.theorem_1_1_region : xiBetaRegion Set.univ = exactRegion

Theorem 1.1, region statement: R_{ξ,β} = {(x,y) ∈ [0,1]×[-1,1] : |y|³ ≤ 2x}.

theorem Papers.OrendayLaresRockel2026XiBeta.theorem_1_1_inequality (C : ProbabilityTheory.Copula 2) : |C.blomqvistBeta| ^ 3 ≤ 2 * C.chatterjeeXi ∧ (|C.blomqvistBeta| ^ 3 = 2 * C.chatterjeeXi ↔ C = leftBoundary C.blomqvistBeta ⋯)

Theorem 1.1, inequality (1.3) with the equality case: |β(C)|³ ≤ 2ξ(C) with equality iff C = L_{β(C)}.

theorem Papers.OrendayLaresRockel2026XiBeta.theorem_1_1_right_boundary (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (dExchange b hb).chatterjeeXi = 1 ∧ (dExchange b hb).blomqvistBeta = b ∧ ∃ (f : ↑unitInterval → ↑unitInterval), Measurable f ∧ MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume ∧ ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(dExchange b hb).toMeasure, x 1 = f (x 0)

Theorem 1.1: every point of the right boundary {1} × [-1,1] is attained by D_b, a deterministic (completely dependent) copula.

theorem Papers.OrendayLaresRockel2026XiBeta.exactRegion_neg (x y : ℝ) : (x, -y) ∈ exactRegion ↔ (x, y) ∈ exactRegion

R_{ξ,β} is symmetric under y ↦ -y.

theorem Papers.OrendayLaresRockel2026XiBeta.region_of_witnesses {A : Set (ProbabilityTheory.Copula 2)} (hA : IsConvexClass A) {b x : ℝ} (hb : b ∈ Set.Icc (-1) 1) (hL : leftBoundary b hb ∈ A) (hD : dExchange b hb ∈ A) (hx : x ∈ Set.Icc 0 1) (hbound : |b| ^ 3 ≤ 2 * x) : (x, b) ∈ xiBetaRegion A

L_b and D_b both belong to any class A containing all radially symmetric copulas of the kind used in Corollary 4.3; here the general interpolation step.

theorem Papers.OrendayLaresRockel2026XiBeta.corollary_4_3_rs : xiBetaRegion classRS = exactRegion

Corollary 4.3: R^{RS} = R.

def Papers.OrendayLaresRockel2026XiBeta.exactRegionUpper : Set (ℝ × ℝ)

The upper half R ∩ ([0,1] × [0,1]).

Equations

• Papers.OrendayLaresRockel2026XiBeta.exactRegionUpper = Papers.OrendayLaresRockel2026XiBeta.exactRegion ∩ Set.Icc 0 1 ×ˢ Set.Icc 0 1

def Papers.OrendayLaresRockel2026XiBeta.exactRegionLower : Set (ℝ × ℝ)

The lower half R ∩ ([0,1] × [-1,0]).

Equations

• Papers.OrendayLaresRockel2026XiBeta.exactRegionLower = Papers.OrendayLaresRockel2026XiBeta.exactRegion ∩ Set.Icc 0 1 ×ˢ Set.Icc (-1) 0

theorem Papers.OrendayLaresRockel2026XiBeta.corollary_4_3_pqd : xiBetaRegion classPQD = exactRegionUpper ∧ xiBetaRegion (classPQD ∩ classRS) = exactRegionUpper

Corollary 4.3: R^{PQD} = R^{PQD,RS} = R ∩ ([0,1] × [0,1]).

theorem Papers.OrendayLaresRockel2026XiBeta.corollary_4_3_nqd : xiBetaRegion classNQD = exactRegionLower ∧ xiBetaRegion (classNQD ∩ classRS) = exactRegionLower

Corollary 4.3: R^{NQD} = R^{NQD,RS} = R ∩ ([0,1] × [-1,0]), by the reflection (2.4).

theorem Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_sd_rs_eq : xiBetaRegion (classSD ∩ classRS) = (fun (p : ℝ × ℝ) => (p.1, -p.2)) '' xiBetaRegion (classSI ∩ classRS)

Reflection for the SD/RS intersection, used with Theorem 1.2: Č maps SI ∩ RS onto SD ∩ RS, hence R^{SD,RS} is the mirror image of R^{SI,RS}.

theorem Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_sd_eq_sd_rs (h : xiBetaRegion classSI = xiBetaRegion (classSI ∩ classRS)) : xiBetaRegion classSD = xiBetaRegion (classSD ∩ classRS)

If R^{SI} = R^{SI,RS} then R^{SD} = R^{SD,RS} (used for Theorem 1.2).

Quantitative claims of the introduction

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_pm_one_xi : (leftBoundary 1 ⋯).chatterjeeXi = 1 / 2 ∧ (leftBoundary (-1) ⋯).chatterjeeXi = 1 / 2

L_{±1} attain the lower endpoint ξ = 1/2 of the horizontal edges β = ±1.

theorem Papers.OrendayLaresRockel2026XiBeta.exists_mixture_leftBoundary_dExchange (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) {x : ℝ} (hx : x ∈ Set.Icc (|b| ^ 3 / 2) 1) : ∃ (a : ↑unitInterval), ((dExchange b hb).mix (leftBoundary b hb) a).chatterjeeXi = x ∧ ((dExchange b hb).mix (leftBoundary b hb) a).blomqvistBeta = b

Mixtures of D_b and L_b fill the vertical segment of the fibre over β = b: for each x ∈ [|b|³/2, 1] there is a mixture with ξ = x and β = b.

theorem Papers.OrendayLaresRockel2026XiBeta.horizontal_edges_attained (x : ℝ) (hx : x ∈ Set.Icc (1 / 2) 1) : (x, 1) ∈ xiBetaRegion Set.univ ∧ (x, -1) ∈ xiBetaRegion Set.univ

"Mixtures of L_{±1} and D_{±1} fill the horizontal edges at β = ±1."

theorem Papers.OrendayLaresRockel2026XiBeta.pqd_rho_eq_zero_iff (C : ProbabilityTheory.Copula 2) (h : C.IsPQD) : C.spearmanRho = 0 ↔ C = ProbabilityTheory.Copula.independence 2

Introduction: for positively quadrant dependent copulas, Spearman's ρ vanishes only under independence.

theorem Papers.OrendayLaresRockel2026XiBeta.one_sub_sq_le_iff {x y : ℝ} (hx : x ≤ 1) (hy : y ≤ 1) : 3 * (1 - y) ^ 2 ≤ 4 * (1 - x) ↔ 1 - 2 * √((1 - x) / 3) ≤ y

Introduction, inequality (1.5) rewritten: 3(1-y)² ≤ 4(1-x) iff y ≥ 1 - 2√((1-x)/3) (for y ≤ 1, x ≤ 1).

theorem Papers.OrendayLaresRockel2026XiBeta.xi_gt_quarter_beta_pos {x y : ℝ} (hy0 : 0 ≤ y) (h : 3 * (1 - y) ^ 2 ≤ 4 * (1 - x)) (hx : 1 / 4 < x) : 0 < y

Introduction: in the SI region, ξ > 1/4 forces β > 0 (from 3(1-β)² ≤ 4(1-ξ) and β ≥ 0).

theorem Papers.OrendayLaresRockel2026XiBeta.abs_beta_le_rpow (C : ProbabilityTheory.Copula 2) : |C.blomqvistBeta| ≤ (2 * C.chatterjeeXi) ^ (↑3)⁻¹

Introduction: a small value of ξ pins β near zero, |β(C)| ≤ (2 ξ(C))^{1/3}.

theorem Papers.OrendayLaresRockel2026XiBeta.figure1_dots : ((ProbabilityTheory.Copula.independence 2).chatterjeeXi = 0 ∧ (ProbabilityTheory.Copula.independence 2).blomqvistBeta = 0) ∧ ((ProbabilityTheory.Copula.comonotonic 2).chatterjeeXi = 1 ∧ (ProbabilityTheory.Copula.comonotonic 2).blomqvistBeta = 1) ∧ (ProbabilityTheory.Copula.countermonotonic.chatterjeeXi = 1 ∧ ProbabilityTheory.Copula.countermonotonic.blomqvistBeta = -1) ∧ ((leftBoundary 1 ⋯).chatterjeeXi = 1 / 2 ∧ (leftBoundary 1 ⋯).blomqvistBeta = 1) ∧ (leftBoundary (-1) ⋯).chatterjeeXi = 1 / 2 ∧ (leftBoundary (-1) ⋯).blomqvistBeta = -1

The dots of Figure 1 (except R_0): Π = (0,0), M = (1,1), W = (1,-1), L_{±1} = (1/2, ±1).