← Copula mathematical handbook

Strict coefficient monotonicity and uniqueness of every interior parameter

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_coefficients_strictMono {b d : ℝ} (hb : 0 ≤ b) (hd : 0 ≤ d) (hbd : b < d) : (extremalCopula b hb).chatterjeeXi < (extremalCopula d hd).chatterjeeXi ∧ blestNu (extremalCopula b hb) < blestNu (extremalCopula d hd)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_finite_xi (b : ℝ) (hb : 0 ≤ b) : (extremalCopula b hb).chatterjeeXi < 1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_positive_xi (b : ℝ) (hb : 0 < b) : 0 < (extremalCopula b ⋯).chatterjeeXi

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_parameter_unique (x : ℝ) (hx : x ∈ Set.Ioo 0 1) : ∃! b : ↑(Set.Ioi 0), (extremalCopula ↑b ⋯).chatterjeeXi = x

The source parameter is unique for every xi strictly between zero and one.