← Mathematical handbook

Concordance ordering in the revised manuscript

noncomputable def Papers.Rockel2026XiBlest.signedExtremalCopula (b : ℝ) : ProbabilityTheory.Copula 2

The source's signed family, extended by independence at zero.

Equations

• Papers.Rockel2026XiBlest.signedExtremalCopula b = if hb : 0 ≤ b then Papers.Rockel2026XiBlest.extremalCopula b hb else (Papers.Rockel2026XiBlest.extremalCopula (-b) ⋯).reflect {1}

theorem Papers.Rockel2026XiBlest.signedExtremal_nonneg (b : ℝ) (hb : 0 ≤ b) : signedExtremalCopula b = extremalCopula b hb

theorem Papers.Rockel2026XiBlest.signedExtremal_neg (b : ℝ) (hb : b < 0) : signedExtremalCopula b = (extremalCopula (-b) ⋯).reflect {1}

theorem Papers.Rockel2026XiBlest.signed_extremal_reflection_coefficients (b : ℝ) (hb : 0 < b) : (signedExtremalCopula (-b)).chatterjeeXi = (signedExtremalCopula b).chatterjeeXi ∧ blestNu (signedExtremalCopula (-b)) = -blestNu (signedExtremalCopula b)

Revised Proposition basic_properties_cb(iii): response reflection fixes xi and negates Blest nu for the actual signed family.

theorem Papers.Rockel2026XiBlest.not_comonotonic_concordanceLE_countermonotonic : ¬(ProbabilityTheory.Copula.comonotonic 2).ConcordanceLE ProbabilityTheory.Copula.countermonotonic

The reversed concordance direction printed in arXiv v1 Lemma 4.3(iii) fails at the M/W endpoints.

theorem Papers.Rockel2026XiBlest.extremal_cdf_monotone (b d : ℝ) (hb : 0 ≤ b) (hd : 0 ≤ d) (hbd : b ≤ d) (u v : ↑unitInterval) : (extremalCopula b hb).cdf ![u, v] ≤ (extremalCopula d hd).cdf ![u, v]

The positive branch is ordered as copulas, not just by its rank coefficients.

theorem Papers.Rockel2026XiBlest.signed_extremal_concordance (b d : ℝ) (hbd : b ≤ d) (u v : ↑unitInterval) : (signedExtremalCopula b).cdf ![u, v] ≤ (signedExtremalCopula d).cdf ![u, v]

The full signed family is increasing in concordance order.

theorem Papers.Rockel2026XiBlest.signed_extremal_isSD (b : ℝ) (hb : b < 0) : (signedExtremalCopula b).IsSD

The reflected negative branch is stochastically decreasing.