← Mathematical handbook

General order results, with explicit existence assumptions for tail limits

theorem Papers.AnsariRockel2024.survival_lowerOrthant_iff (C D : ProbabilityTheory.Copula 2) : C.LowerOrthantLE D ↔ C.survivalCopula.LowerOrthantLE D.survivalCopula

Proposition 3.2(i), including singular copulas.

theorem Papers.AnsariRockel2024.survival_cis_iff (C : ProbabilityTheory.Copula 2) : C.IsSI ↔ C.survivalCopula.IsSI

Proposition 3.2(ii), for directional conditional increase (CIS).

theorem Papers.AnsariRockel2024.survival_schur_iff (C D : ProbabilityTheory.Copula 2) : C.SchurLE D ↔ C.survivalCopula.SchurLE D.survivalCopula

Proposition 3.2(iii), using continuous convex tests of the conditional CDF.

theorem Papers.AnsariRockel2024.concordance_coefficients_mono (C D : ProbabilityTheory.Copula 2) (h : C.LowerOrthantLE D) : C.spearmanRho ≤ D.spearmanRho ∧ C.kendallTau ≤ D.kendallTau

Lemma 2.9 in copula form: both classical concordance coefficients are monotone.

theorem Papers.AnsariRockel2024.schur_xi_mono (C D : ProbabilityTheory.Copula 2) (h : C.SchurLE D) : C.chatterjeeXi ≤ D.chatterjeeXi

The copula specialization of Lemma 2.10, with the stated conditioning direction.

theorem Papers.AnsariRockel2024.lower_tail_mono (C D : ProbabilityTheory.Copula 2) (h : C.LowerOrthantLE D) (a b : ℝ) (ha : C.HasLowerTailDependence a) (hb : D.HasLowerTailDependence b) : a ≤ b

Lemma 2.12: lower tails, provided both limits exist.

theorem Papers.AnsariRockel2024.upper_tail_mono (C D : ProbabilityTheory.Copula 2) (h : C.LowerOrthantLE D) (a b : ℝ) (ha : C.HasUpperTailDependence a) (hb : D.HasUpperTailDependence b) : a ≤ b

Lemma 2.12: upper tails, provided both limits exist.

theorem Papers.AnsariRockel2024.schur_below_cis (C D : ProbabilityTheory.Copula 2) (h : C.SchurLE D) (hD : D.IsSI) : C.LowerOrthantLE D

Lemma 2.6(i): Schur comparison with a CIS copula implies lower orthant comparison.

theorem Papers.AnsariRockel2024.schur_below_cds (C D : ProbabilityTheory.Copula 2) (h : C.SchurLE D) (hD : D.IsSD) : D.LowerOrthantLE C

Lemma 2.8(i): Schur comparison with a CDS copula reverses the orthant direction.

theorem Papers.AnsariRockel2024.cis_schur_iff_orthant (C D : ProbabilityTheory.Copula 2) (hC : C.IsSI) (hD : D.IsSI) : C.SchurLE D ↔ C.LowerOrthantLE D

Lemma 2.6(ii): exact equivalence on the CIS class, without density assumptions.

theorem Papers.AnsariRockel2024.cds_schur_iff_reverse_orthant (C D : ProbabilityTheory.Copula 2) (hC : C.IsSD) (hD : D.IsSD) : C.SchurLE D ↔ D.LowerOrthantLE C

Lemma 2.8(ii): exact equivalence on the CDS class, with reversed orthant order.