← Mathematical handbook

Remark 5.4, the introduction's claims for SI copulas and the caption of Figure 1

• (a) At β = 0 the SI region is the segment 0 ≤ ξ ≤ 1/4, whose upper endpoint is attained by R_0, the copula of (U, (U + ε)/2); R_0ᵀ is completely dependent (U = 2V_0 - ε, ε = ⌊2 V_0⌋), so ξ(R_0ᵀ) = 1, while R_0 is SI and R_0ᵀ is not.
• (b) ξ(R_b) ≤ τ(R_b) ≤ ρ(R_b) for b ∈ [0,1].
• Introduction: for SI copulas ξ > 1/4 forces β > 0, β ≥ 1 - 2√((1-ξ)/3), and β = 0 is compatible with every ξ ∈ [0, 1/4].
• Figure 1: the SI region lies between the cubic ξ = β³/2 and the curve ξ = 1 - (3/4)(1-β)², degenerates to [0, 1/4] at β = 0, and the dots Π, R_0, L_1, M are attained by SI copulas.

Remark 5.4 (a)

theorem Papers.OrendayLaresRockel2026XiBeta.siRegion_fibre_beta_zero (x : ℝ) : (x, 0) ∈ siRegion ↔ x ∈ Set.Icc 0 (1 / 4)

The fibre of the SI region over β = 0 is the segment 0 ≤ ξ ≤ 1/4.

theorem Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_classSI_fibre_beta_zero (x : ℝ) : (x, 0) ∈ xiBetaRegion classSI ↔ x ∈ Set.Icc 0 (1 / 4)

Remark 5.4 (a): at β = 0 the SI region is exactly the segment 0 ≤ ξ ≤ 1/4.

theorem Papers.OrendayLaresRockel2026XiBeta.R0_upper_endpoint : (Rb 0 zero_mem_Icc01).chatterjeeXi = 1 / 4 ∧ (Rb 0 zero_mem_Icc01).blomqvistBeta = 0 ∧ (Rb 0 zero_mem_Icc01).IsSI

Remark 5.4 (a): the upper endpoint (1/4, 0) is attained by R_0, which is SI.

theorem Papers.OrendayLaresRockel2026XiBeta.V0_ae_eq : ∀ᵐ (ω : ↑unitInterval × Bool) ∂↑probVb, ↑(Vb 0 ω.1 ω.2) = (↑ω.1 + if ω.2 = true then 1 else 0) / 2

Remark 5.4 (a): R_0 is the copula of (U, (U + ε)/2): almost surely V_0 = (U + ε)/2 for the coupling (U, ε) of Proposition 5.3.

theorem Papers.OrendayLaresRockel2026XiBeta.V0_floor_ae : ∀ᵐ (ω : ↑unitInterval × Bool) ∂↑probVb, (↑⌊2 * ↑(Vb 0 ω.1 ω.2)⌋ = if ω.2 = true then 1 else 0) ∧ ↑ω.1 = 2 * ↑(Vb 0 ω.1 ω.2) - ↑⌊2 * ↑(Vb 0 ω.1 ω.2)⌋

Remark 5.4 (a): U = 2V_0 - ε with ε = ⌊2V_0⌋ almost surely.

noncomputable def Papers.OrendayLaresRockel2026XiBeta.doubling (v : ↑unitInterval) : ↑unitInterval

The doubling map v ↦ 2v - ⌊2v⌋ (fractional part of 2v) on the unit interval.

Equations

• Papers.OrendayLaresRockel2026XiBeta.doubling v = ⟨Int.fract (2 * ↑v), ⋯⟩

theorem Papers.OrendayLaresRockel2026XiBeta.measurable_doubling : Measurable doubling

theorem Papers.OrendayLaresRockel2026XiBeta.R0_transpose_ae_graph : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(Rb 0 zero_mem_Icc01).transpose.toMeasure, x 1 = doubling (x 0)

Remark 5.4 (a): R_0ᵀ lives on the graph of the doubling map, i.e. it is completely dependent: U = 2V_0 - ⌊2V_0⌋ almost surely.

theorem Papers.OrendayLaresRockel2026XiBeta.xi_R0_transpose : (Rb 0 zero_mem_Icc01).transpose.chatterjeeXi = 1

Remark 5.4 (a): R_0ᵀ is completely dependent, so ξ(R_0ᵀ) = 1.

theorem Papers.OrendayLaresRockel2026XiBeta.R0_SI_transpose_not_SI : (Rb 0 zero_mem_Icc01).IsSI ∧ ¬(Rb 0 zero_mem_Icc01).transpose.IsSI ∧ (Rb 0 zero_mem_Icc01).chatterjeeXi = 1 / 4 ∧ (Rb 0 zero_mem_Icc01).transpose.chatterjeeXi = 1

Remark 5.4 (a): R_0 is SI while R_0ᵀ is not; ξ(R_0) = 1/4 < 1 = ξ(R_0ᵀ).

Remark 5.4 (b)

theorem Papers.OrendayLaresRockel2026XiBeta.xi_le_tau_le_rho_Rb (b : ℝ) (hb : b ∈ Set.Icc 0 1) : (Rb b hb).chatterjeeXi ≤ (Rb b hb).kendallTau ∧ (Rb b hb).kendallTau ≤ (Rb b hb).spearmanRho

Remark 5.4 (b): ξ(R_b) ≤ τ(R_b) ≤ ρ(R_b) for all b ∈ [0,1].

Claims of the introduction for SI copulas

theorem Papers.OrendayLaresRockel2026XiBeta.si_xi_gt_quarter_beta_pos (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (h : 1 / 4 < C.chatterjeeXi) : 0 < C.blomqvistBeta

Introduction: for SI copulas, ξ > 1/4 forces β > 0.

theorem Papers.OrendayLaresRockel2026XiBeta.si_beta_zero_compatible (x : ℝ) (hx : x ∈ Set.Icc 0 (1 / 4)) : ∃ (C : ProbabilityTheory.Copula 2), C.IsSI ∧ C.IsRadiallySymmetric ∧ C.chatterjeeXi = x ∧ C.blomqvistBeta = 0

Introduction: β = 0 is compatible with every ξ ∈ [0, 1/4] under stochastic increasingness (even with radial symmetry).

theorem Papers.OrendayLaresRockel2026XiBeta.si_beta_zero_xi_le (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (h : C.blomqvistBeta = 0) : C.chatterjeeXi ≤ 1 / 4

Introduction: for SI copulas with β = 0, necessarily ξ ≤ 1/4.

Figure 1: the SI region

theorem Papers.OrendayLaresRockel2026XiBeta.siRegion_iff (x y : ℝ) : (x, y) ∈ siRegion ↔ y ∈ Set.Icc 0 1 ∧ y ^ 3 / 2 ≤ x ∧ x ≤ 1 - 3 / 4 * (1 - y) ^ 2

The SI region is the set between the cubic ξ = β³/2 and the curve ξ = 1 - (3/4)(1-β)².

theorem Papers.OrendayLaresRockel2026XiBeta.figure1_si_boundary (b : ℝ) (hb : b ∈ Set.Icc 0 1) (hb' : b ∈ Set.Icc (-1) 1) : ((leftBoundary b hb').IsSI ∧ (leftBoundary b hb').chatterjeeXi = b ^ 3 / 2 ∧ (leftBoundary b hb').blomqvistBeta = b) ∧ (Rb b hb).IsSI ∧ (Rb b hb).chatterjeeXi = 1 - 3 / 4 * (1 - b) ^ 2 ∧ (Rb b hb).blomqvistBeta = b

Figure 1: the boundary curves of the SI region are attained by L_b (cubic) and R_b (dash-dotted curve), both SI and radially symmetric.

theorem Papers.OrendayLaresRockel2026XiBeta.figure1_si_dots : ((ProbabilityTheory.Copula.independence 2).IsSI ∧ (ProbabilityTheory.Copula.independence 2).chatterjeeXi = 0 ∧ (ProbabilityTheory.Copula.independence 2).blomqvistBeta = 0) ∧ ((Rb 0 zero_mem_Icc01).IsSI ∧ (Rb 0 zero_mem_Icc01).chatterjeeXi = 1 / 4 ∧ (Rb 0 zero_mem_Icc01).blomqvistBeta = 0) ∧ ((leftBoundary 1 ⋯).IsSI ∧ (leftBoundary 1 ⋯).chatterjeeXi = 1 / 2 ∧ (leftBoundary 1 ⋯).blomqvistBeta = 1) ∧ (ProbabilityTheory.Copula.comonotonic 2).IsSI ∧ (ProbabilityTheory.Copula.comonotonic 2).chatterjeeXi = 1 ∧ (ProbabilityTheory.Copula.comonotonic 2).blomqvistBeta = 1

Figure 1: the dots Π, R_0, L_1, M, all attained by SI copulas.

theorem Papers.OrendayLaresRockel2026XiBeta.figure1_sd_boundary (b : ℝ) (hb : b ∈ Set.Icc 0 1) : ((Rb b hb).reflect {1}).IsSD ∧ ((Rb b hb).reflect {1}).chatterjeeXi = 1 - 3 / 4 * (1 - b) ^ 2 ∧ ((Rb b hb).reflect {1}).blomqvistBeta = -b

Figure 1: the SD region (dark orange) has right boundary attained by the mirror images Ř_b of R_b, which are SD with ξ(Ř_b) = ξ(R_b), β(Ř_b) = -b.