← Copula mathematical handbook

The full region in terms of the constructed extremal family

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_blest_nonneg (b : ℝ) (hb : 0 ≤ b) : 0 ≤ blestNu (extremalCopula b hb)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_slice_iff (b : ℝ) (hb : 0 < b) (y : ℝ) : ((extremalCopula b ⋯).chatterjeeXi, y) ∈ attainableRegion ↔ |y| ≤ blestNu (extremalCopula b ⋯)

Exact closed vertical slice at every positive-slope member, with actual witnesses.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.intermediate_slice_characterization (x : ℝ) (hx : x ∈ Set.Ioo 0 1) : ∃ (b : ℝ) (hb : 0 < b), (extremalCopula b ⋯).chatterjeeXi = x ∧ (∀ (y : ℝ), (x, y) ∈ attainableRegion ↔ |y| ≤ blestNu (extremalCopula b ⋯)) ∧ ∀ (C : Copula 2), C.chatterjeeXi = x → (blestNu C = blestNu (extremalCopula b ⋯) ↔ C = extremalCopula b ⋯)

Every intermediate xi slice has a uniquely attaining upper boundary and its reflection.