Exact Frechet-family minimum in Table 2 #
The weights a and b multiply M and W. The unique minimizer has a=0,b=1/4, so the independence weight in the source's prose convention is 3/4.
theorem
Papers.Rockel2026XiFootrule.frechet_coefficients
(a b : ℝ)
(ha : 0 ≤ a)
(hb : 0 ≤ b)
(hab : a + b ≤ 1)
:
(ProbabilityTheory.Copula.frechet a b ha hb hab).chatterjeeXi = (a - b) ^ 2 + a * b ∧ (ProbabilityTheory.Copula.frechet a b ha hb hab).spearmanFootrule = a - b / 2
theorem
Papers.Rockel2026XiFootrule.frechet_objective_lower
(a b : ℝ)
(ha : 0 ≤ a)
(hb : 0 ≤ b)
(hab : a + b ≤ 1)
:
-(1 / 16) ≤ (ProbabilityTheory.Copula.frechet a b ha hb hab).chatterjeeXi + (ProbabilityTheory.Copula.frechet a b ha hb hab).spearmanFootrule
theorem
Papers.Rockel2026XiFootrule.frechet_objective_eq_iff
(a b : ℝ)
(ha : 0 ≤ a)
(hb : 0 ≤ b)
(hab : a + b ≤ 1)
:
(ProbabilityTheory.Copula.frechet a b ha hb hab).chatterjeeXi + (ProbabilityTheory.Copula.frechet a b ha hb hab).spearmanFootrule = -(1 / 16) ↔ a = 0 ∧ b = 1 / 4
theorem
Papers.Rockel2026XiFootrule.frechet_minimizer_coefficients :
(ProbabilityTheory.Copula.frechet 0 (1 / 4) ⋯ ⋯ ⋯).chatterjeeXi = 1 / 16 ∧ (ProbabilityTheory.Copula.frechet 0 (1 / 4) ⋯ ⋯ ⋯).spearmanFootrule = -1 / 8