← Mathematical handbook

Equality in the stochastic xi-rho bound

The scalar moment defect forces conditional CDFs to be constant or binary. Monotonicity in the response threshold excludes mixing these two types at interior thresholds. This argument includes singular copulas.

theorem Verification.conditionalCDF_constant_or_binary_of_moment_eq (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (v : ↑unitInterval) (he : ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2 = (2 * ∫ (u : ↑unitInterval), C.cdf ![u, v]) - ↑v + ↑v ^ 2) : (∀ᵐ (u : ↑unitInterval), C.conditionalCDF u v = ↑v) ∨ ∀ᵐ (u : ↑unitInterval), C.conditionalCDF u v = 0 ∨ C.conditionalCDF u v = 1

theorem Verification.conditionalCDF_constant_or_binary_of_xi_eq_rho (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (he : C.chatterjeeXi = C.spearmanRho) : ∀ᵐ (v : ↑unitInterval), (∀ᵐ (u : ↑unitInterval), C.conditionalCDF u v = ↑v) ∨ ∀ᵐ (u : ↑unitInterval), C.conditionalCDF u v = 0 ∨ C.conditionalCDF u v = 1

theorem Verification.conditionalCDF_monotone_threshold (C : ProbabilityTheory.Copula 2) (u : ↑unitInterval) : Monotone (C.conditionalCDF u)

theorem Verification.ae_unit_interior : ∀ᵐ (v : ↑unitInterval), 0 < ↑v ∧ ↑v < 1

theorem Verification.not_binary_of_constant_interior (C : ProbabilityTheory.Copula 2) (v w : ↑unitInterval) (hv : 0 < ↑v ∧ ↑v < 1) (hw : 0 < ↑w ∧ ↑w < 1) (hc : ∀ᵐ (u : ↑unitInterval), C.conditionalCDF u v = ↑v) : ¬∀ᵐ (u : ↑unitInterval), C.conditionalCDF u w = 0 ∨ C.conditionalCDF u w = 1

A constant conditional CDF at one interior threshold excludes a binary conditional CDF at every other interior threshold.

theorem Verification.xi_eq_one_of_conditionalCDF_binary (C : ProbabilityTheory.Copula 2) (hb : ∀ᵐ (v : ↑unitInterval) (u : ↑unitInterval), C.conditionalCDF u v = 0 ∨ C.conditionalCDF u v = 1) : C.chatterjeeXi = 1

theorem Verification.isSI_xi_eq_rho_iff (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi = C.spearmanRho ↔ C = ProbabilityTheory.Copula.independence 2 ∨ C = ProbabilityTheory.Copula.comonotonic 2

The full equality classification for arbitrary SI copulas.

theorem Verification.isSD_xi_eq_neg_rho_iff (C : ProbabilityTheory.Copula 2) (hC : C.IsSD) : C.chatterjeeXi = -C.spearmanRho ↔ C = ProbabilityTheory.Copula.independence 2 ∨ C = ProbabilityTheory.Copula.countermonotonic

The full equality classification for arbitrary SD copulas.

theorem Verification.stochastic_xi_eq_abs_rho_iff (C : ProbabilityTheory.Copula 2) (hC : C.IsSI ∨ C.IsSD) : C.chatterjeeXi = |C.spearmanRho| ↔ C = ProbabilityTheory.Copula.countermonotonic ∨ C = ProbabilityTheory.Copula.independence 2 ∨ C = ProbabilityTheory.Copula.comonotonic 2

Equality in xi <= abs(rho) holds exactly at W, independence, and M.