← Mathematical handbook

The elementary boundary arc and the exact half-shift regime

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.halfShift_arc_coefficients {s : ℝ} (hs : 1 ≤ s) : have A := ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.halfShift s hs; have d := A.z / 2; A.copula.giniGamma = -1 + 8 * d - 10 * d ^ 2 ∧ A.copula.spearmanRho = -1 + 12 * d - 24 * d ^ 2 + 13 * d ^ 3

The source's polynomial elementary arc, with d equal to half the corner length.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.halfShift_arc_closed {s : ℝ} (hs : 1 ≤ s) : have A := ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.halfShift s hs; have g := A.copula.giniGamma; A.copula.spearmanRho = (144 + 420 * g + (9 + 65 * g) * √(6 - 10 * g)) / 500

Corollary 2.1's radical formula at every elementary-arc parameter.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_arc_coverage {g : ℝ} (hg : -1 < g) (hhi : g ≤ ProbabilityTheory.Copula.RankRegion.RhoGamma.contactGamma 1) : ∃ (s : ℝ) (hs : 1 ≤ s), (ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.halfShift s hs).gamma = g

Every gamma below the first contact, apart from W, has a half-shift parameter.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_upper_boundary {g : ℝ} (hg : g ∈ Set.Icc (-1) (ProbabilityTheory.Copula.RankRegion.RhoGamma.contactGamma 1)) : upperRho g = (144 + 420 * g + (9 + 65 * g) * √(6 - 10 * g)) / 500

Corollary 2.1: the closed formula on the whole elementary gamma interval.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.halfShift_not_optimal {s : ℝ} (hs : 0 < s) (hs1 : s < 1) : ∃ (C : ProbabilityTheory.Copula 2), ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 - s * |↑(x 0) - ↑(x 1)| ∂C.toMeasure < ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 - s * |↑(x 0) - ↑(x 1)| ∂ProbabilityTheory.Copula.RankRegion.RhoFootrule.halfTurn.toMeasure

An explicit competing copula improves the half-shift cost whenever 0<s<1.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.halfShift_optimal_iff {s : ℝ} (hs : 0 < s) : (∀ (C : ProbabilityTheory.Copula 2), ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 - s * |↑(x 0) - ↑(x 1)| ∂ProbabilityTheory.Copula.RankRegion.RhoFootrule.halfTurn.toMeasure ≤ ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 - s * |↑(x 0) - ↑(x 1)| ∂C.toMeasure) ↔ 1 ≤ s

Lemma 3.6 in both directions, with s=1/theta.