← 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 Papers.Rockel2026XiBlest.attainableRegion : Set (ℝ × ℝ)

Equations

• Papers.Rockel2026XiBlest.attainableRegion = Verification.xiCoefficientRegion Papers.Rockel2026XiBlest.blestNu

theorem Papers.Rockel2026XiBlest.fixed_coefficient_upward (C : ProbabilityTheory.Copula 2) (x : ℝ) (hx : C.chatterjeeXi ≤ x) (hx1 : x ≤ 1) : ∃ (D : ProbabilityTheory.Copula 2), D.chatterjeeXi = x ∧ blestNu D = blestNu C

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

theorem Papers.Rockel2026XiBlest.attainable_region_convex : Convex ℝ attainableRegion

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