← Mathematical handbook

Proposition 4.2: the right-boundary copulas D_b

D_b is the copula of (U, T_b(U)) (see dExchange). This file proves: T_b is measure preserving (intervalExchange_measurePreserving), D_b is completely dependent with ξ(D_b) = 1, β(D_b) = b, D_b is exchangeable, radially symmetric, and PQD for b ≥ 0. All statements hold for every b ∈ [-1, 1], including the degenerate cut points s_b ∈ {0, 1/2}.

theorem Papers.OrendayLaresRockel2026XiBeta.dExchange_ae_graph (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(dExchange b hb).toMeasure, x 1 = intervalExchange b (x 0)

D_b lives on the graph of T_b.

theorem Papers.OrendayLaresRockel2026XiBeta.dExchange_completelyDependent (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∃ (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)

D_b is completely dependent: the second coordinate is a.s. a measurable, Lebesgue-measure-preserving function of the first.

theorem Papers.OrendayLaresRockel2026XiBeta.dExchange_xi (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (dExchange b hb).chatterjeeXi = 1

noncomputable def Papers.OrendayLaresRockel2026XiBeta.dCdf (s u v : ℝ) : ℝ

Explicit CDF of the four-strip shuffle.

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.OrendayLaresRockel2026XiBeta.dExchange_cdf (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (u v : ↑unitInterval) : (dExchange b hb).cdf ![u, v] = dCdf (exchangeCut b) ↑u ↑v

theorem Papers.OrendayLaresRockel2026XiBeta.stripCut_nonneg {s a u : ℝ} (hs : 0 ≤ s) : 0 ≤ ProbabilityTheory.Copula.RankRegion.XiBlest.Support.stripCut s a u

theorem Papers.OrendayLaresRockel2026XiBeta.dExchange_beta (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (dExchange b hb).blomqvistBeta = b

theorem Papers.OrendayLaresRockel2026XiBeta.dExchange_exchangeable (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (dExchange b hb).IsExchangeable

theorem Papers.OrendayLaresRockel2026XiBeta.dExchange_radiallySymmetric (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (dExchange b hb).IsRadiallySymmetric

theorem Papers.OrendayLaresRockel2026XiBeta.dCdf_ge_mul {s : ℝ} (hs1 : 1 / 4 ≤ s) (hs2 : s ≤ 1 / 2) {u v : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1 / 2) : u * v ≤ dCdf s u v

theorem Papers.OrendayLaresRockel2026XiBeta.dExchange_pqd (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (hpos : 0 ≤ b) : (dExchange b hb).IsPQD

theorem Papers.OrendayLaresRockel2026XiBeta.proposition_4_2 (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (dExchange b hb).IsExchangeable ∧ (dExchange b hb).IsRadiallySymmetric ∧ (dExchange b hb).chatterjeeXi = 1 ∧ (dExchange b hb).blomqvistBeta = b ∧ (0 ≤ b → (dExchange b hb).IsPQD)

Proposition 4.2 (right boundary): for every b ∈ [-1,1], D_b is exchangeable and radially symmetric, ξ(D_b) = 1 and β(D_b) = b, and D_b is PQD for b ≥ 0.

theorem Papers.OrendayLaresRockel2026XiBeta.dCdf_le_half {s : ℝ} (hs1 : 0 ≤ s) (hs2 : s ≤ 1 / 2) {u v : ℝ} (hu0 : 0 ≤ u) (hv0 : 0 ≤ v) (hv1 : v ≤ 1 / 2) : dCdf s u v = min (min s u) (min s v) + min (min (1 / 2 - s) (max 0 (u - 1 / 2))) (min (1 / 2 - s) (max 0 (v - s)))

theorem Papers.OrendayLaresRockel2026XiBeta.dExchange_cdf_low (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (u v : ↑unitInterval) (hv : ↑v ≤ (1 + b) / 4) : (dExchange b hb).cdf ![u, v] = min ↑u ↑v

The article's formula for v ≤ s_b: D_b(u,v) = min{u,v}.

theorem Papers.OrendayLaresRockel2026XiBeta.dExchange_cdf_mid (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (u v : ↑unitInterval) (hv1 : (1 + b) / 4 < ↑v) (hv2 : ↑v ≤ 1 / 2) : (dExchange b hb).cdf ![u, v] = min (↑u) ((1 + b) / 4) + max 0 (min (↑u) (↑v + 1 / 2 - (1 + b) / 4) - 1 / 2)

The article's formula for s_b < v ≤ 1/2: D_b(u,v) = min{u, s_b} + (min{u, v + 1/2 - s_b} - 1/2)_+.