← Mathematical handbook

The normalized splitting parameters in equations (18) and Lemma 3.7

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.sourceTheta (A : ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate) : ℝ

The source parameter is the reciprocal auxiliary multiplier.

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.sourceTheta A = 1 / A.s

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.sourceAlpha (A : ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate) : ℝ

The source normalizes the central length by the supporting multiplier.

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.sourceAlpha A = (1 + √(1 + 2 * Papers.AnsariRockelSteinmassl2026RhoGamma.sourceTheta A ^ 2 * A.c)) / 2

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.source_splitting_formulas (A : ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate) : A.t = 1 / (sourceTheta A + sourceAlpha A) ∧ ↑A.a = sourceAlpha A * A.t ∧ A.z = sourceTheta A * A.t

Equation (18), with the same theta and alpha normalizations as the paper.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.source_parameter_inequalities (A : ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate) : A.c < 0 ∧ sourceTheta A ^ 2 * A.w ^ 2 ≤ 1 + 2 * sourceTheta A ^ 2 * A.c ∧ (1 + sourceTheta A * A.w) / 2 ≤ sourceAlpha A ∧ sourceAlpha A < 1 ∧ A.t / 2 ≤ ↑A.a ∧ ↑A.a < A.t

All inequalities in Lemma 3.7, for every constructed branch certificate.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.source_alpha_matching (A : ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate) : sourceAlpha A ^ 2 - sourceAlpha A = sourceTheta A ^ 2 * A.c / 2

The potential matching equation directly in the source normalization.