← Copula mathematical handbook

Endpoint cases and a restricted instance of Theorem 2

The general SI/SD inequality is proved in StochasticBounds.lean. The full equality classification is proved in StochasticEquality.lean. The curved diagonal-band boundary remains pending. The FGM result below has the explicit restriction abs θ ≤ 1 and is not advertised as the general stochastic-monotonicity theorem.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.xi_derivative_formula (C : Copula 2) : C.chatterjeeXi = (6 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), deriv (C.cdfSection v) ↑u ^ 2) - 2

theorem ProbabilityTheory.Copula.RankRegion.XiRho.xi_zero_slice (C : Copula 2) : C.chatterjeeXi = 0 ↔ C = independence 2 ∧ C.spearmanRho = 0

The xi=0 slice in Theorem 1 consists of the independence copula alone.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.rho_extreme_implies_xi_one (C : Copula 2) (h : C.spearmanRho = 1 ∨ C.spearmanRho = -1) : C.chatterjeeXi = 1

theorem ProbabilityTheory.Copula.RankRegion.XiRho.fgm_stochastically_monotone (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).IsCI ∨ (fgm θ hθ).IsCD

Every admissible FGM copula is conditionally increasing or decreasing.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.fgm_xi_le_abs_rho (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).chatterjeeXi ≤ |(fgm θ hθ).spearmanRho|

Theorem 2 restricted to the entire signed FGM family.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.fgm_xi_eq_abs_rho_iff (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).chatterjeeXi = |(fgm θ hθ).spearmanRho| ↔ θ = 0

In the restricted FGM result, equality occurs only at independence.