← Mathematical handbook

Exact coefficient formulas for slopes greater than one

noncomputable def Papers.Rockel2026XiBlest.xiFormula (b : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Papers.Rockel2026XiBlest.nuFormula (b : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.Rockel2026XiBlest.extremal_coefficients_hyperbolic (b : ℝ) (hb : 1 < b) : (extremalCopula b ⋯).chatterjeeXi = (183 * √((b - 1) / b) - 38 * b * √((b - 1) / b) - 88 * b ^ 2 * √((b - 1) / b) + 112 * b ^ 2 + 48 * b ^ 3 * √((b - 1) / b) - 48 * b ^ 3 - 105 * Real.arcosh √b / b) / 210 ∧ blestNu (extremalCopula b ⋯) = (87 * √((b - 1) / b) / b + 250 * √((b - 1) / b) - 376 * b * √((b - 1) / b) + 448 * b + 144 * b ^ 2 * √((b - 1) / b) - 144 * b ^ 2 - 105 * Real.arcosh √b / b ^ 2) / 420

theorem Papers.Rockel2026XiBlest.extremal_coefficients (b : ℝ) (hb : 0 ≤ b) : (extremalCopula b hb).chatterjeeXi = xiFormula b ∧ blestNu (extremalCopula b hb) = nuFormula b

Equations (4) and (5), including the b=0 endpoint extension.