← Copula mathematical handbook

Convexity and fixed-coefficient attainment in the xi region

The full xi=1 boundary supplies the witnesses required by the general mixture proof. The curved extremal boundary is a separate obligation.

def ProbabilityTheory.Copula.RankRegion.XiRho.attainableRegion : Set (ℝ × ℝ)

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.attainableRegion = ProbabilityTheory.Copula.RankRegion.Common.xiCoefficientRegion ProbabilityTheory.Copula.spearmanRho

theorem ProbabilityTheory.Copula.RankRegion.XiRho.fixed_coefficient_upward (C : Copula 2) (x : ℝ) (hx : C.chatterjeeXi ≤ x) (hx1 : x ≤ 1) : ∃ (D : Copula 2), D.chatterjeeXi = x ∧ D.spearmanRho = C.spearmanRho

All xi values above an attained point occur at the same second coefficient.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.attainable_region_convex : Convex ℝ attainableRegion

The full attainable region is convex, without assuming boundary attainment or closure.