← Mathematical handbook

Uniqueness along every exact rho--footrule upper arc

theorem Verification.right_boundary_copula_unique (S : ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData) (C : ProbabilityTheory.Copula 2) (hp : C.spearmanFootrule = S.copula.spearmanFootrule) (hr : C.spearmanRho = S.copula.spearmanRho) : C = S.copula

theorem Verification.left_boundary_copula_unique (S : ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData) (C : ProbabilityTheory.Copula 2) (hp : C.spearmanFootrule = S.copula.spearmanFootrule) (hr : C.spearmanRho = S.copula.spearmanRho) : C = S.copula

theorem Verification.upper_parameter_copula_unique (a : ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter) (C : ProbabilityTheory.Copula 2) (hp : C.spearmanFootrule = a.footrule) (hr : C.spearmanRho = a.rho) : C = a.copula

Every arithmetic upper-boundary parameter determines a unique optimizing copula.