← Mathematical handbook

Exact xi plus footrule optimization over the full Frechet simplex

theorem ProbabilityTheory.Copula.frechet_xi_add_footrule_identity (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).chatterjeeXi + (frechet a b ha hb hab).spearmanFootrule = (b - 1 / 4) ^ 2 + a * (a + 1 - b) - 1 / 16

theorem ProbabilityTheory.Copula.frechet_xi_add_footrule_lower (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : -(1 / 16) ≤ (frechet a b ha hb hab).chatterjeeXi + (frechet a b ha hb hab).spearmanFootrule

The exact minimum is attained by three quarters independence plus one quarter W.

theorem ProbabilityTheory.Copula.frechet_xi_add_footrule_eq_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).chatterjeeXi + (frechet a b ha hb hab).spearmanFootrule = -(1 / 16) ↔ a = 0 ∧ b = 1 / 4