← Mathematical handbook

Definition 3.8 as an equality of probability measures

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.glued_copula_probability_law (A : ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate) : A.copula.toMeasure = (ENNReal.ofReal ↑A.a • ProbabilityTheory.Copula.RankRegion.fairMeasure MeasureTheory.volume (fun (u : ↑unitInterval) => ProbabilityTheory.Copula.RankRegion.RhoGamma.signedLift true false (ProbabilityTheory.Copula.OrdinalSum.lowerEmbed A.a u) (ProbabilityTheory.Copula.OrdinalSum.lowerEmbed A.a u)) fun (u : ↑unitInterval) => ProbabilityTheory.Copula.RankRegion.RhoGamma.signedLift false false (ProbabilityTheory.Copula.OrdinalSum.lowerEmbed A.a u) (ProbabilityTheory.Copula.OrdinalSum.lowerEmbed A.a u)) + ENNReal.ofReal A.z • ProbabilityTheory.Copula.RankRegion.fairMeasure A.D.toMeasure (fun (x : Fin 2 → ↑unitInterval) => ProbabilityTheory.Copula.RankRegion.RhoGamma.signedLift true true (ProbabilityTheory.Copula.OrdinalSum.upperEmbed A.a (x 0)) (ProbabilityTheory.Copula.OrdinalSum.upperEmbed A.a (x 1))) fun (x : Fin 2 → ↑unitInterval) => ProbabilityTheory.Copula.RankRegion.RhoGamma.signedLift false true (ProbabilityTheory.Copula.OrdinalSum.upperEmbed A.a (x 0)) (ProbabilityTheory.Copula.OrdinalSum.upperEmbed A.a (x 1))

The source construction: a diagonal lower-magnitude block with opposite signs, then the upper auxiliary block with equal signs, followed by an independent fair sign.