← Copula mathematical handbook

The general SI/SD inequality and the conditional representation of rho

These results apply to all bivariate copulas, including singular laws. The full equality classification in Theorem 2 is proved in StochasticEquality.lean.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.rho_conditionalCDF_formula (C : Copula 2) : C.spearmanRho = (12 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), (1 - ↑u) * C.conditionalCDF u v) - 3

theorem ProbabilityTheory.Copula.RankRegion.XiRho.rho_derivative_formula (C : Copula 2) : C.spearmanRho = (12 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), (1 - ↑u) * deriv (C.cdfSection v) ↑u) - 3

theorem ProbabilityTheory.Copula.RankRegion.XiRho.si_xi_le_rho (C : Copula 2) (hC : C.IsSI) : C.chatterjeeXi ≤ C.spearmanRho

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sd_xi_le_neg_rho (C : Copula 2) (hC : C.IsSD) : C.chatterjeeXi ≤ -C.spearmanRho

theorem ProbabilityTheory.Copula.RankRegion.XiRho.stochastic_xi_le_abs_rho (C : Copula 2) (hC : C.IsSI ∨ C.IsSD) : C.chatterjeeXi ≤ |C.spearmanRho|

theorem ProbabilityTheory.Copula.RankRegion.XiRho.not_stochastically_monotone_of_abs_rho_lt_xi (C : Copula 2) (h : |C.spearmanRho| < C.chatterjeeXi) : ¬C.IsSI ∧ ¬C.IsSD