← Copula mathematical handbook

The exact region in the paper's explicit coefficient parametrization

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.formula_zero : xiFormula 0 = 0 ∧ nuFormula 0 = 0

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.exact_region (x y : ℝ) : (x, y) ∈ attainableRegion ↔ x = 1 ∧ |y| ≤ 1 ∨ ∃ (b : ℝ), 0 ≤ b ∧ x = xiFormula b ∧ |y| ≤ nuFormula b

Equation (6), with the infinity endpoint written as the vertical segment.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.lower_boundary_unique (C : Copula 2) (b : ℝ) (hb : 0 < b) (hx : C.chatterjeeXi = xiFormula b) : blestNu C = -nuFormula b ↔ C = (extremalCopula b ⋯).reflect {1}

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.upper_boundary_unique (C : Copula 2) (b : ℝ) (hb : 0 < b) (hx : C.chatterjeeXi = xiFormula b) : blestNu C = nuFormula b ↔ C = extremalCopula b ⋯

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.formula_infinity_limits : Filter.Tendsto xiFormula Filter.atTop (nhds 1) ∧ Filter.Tendsto nuFormula Filter.atTop (nhds 1)