← Mathematical handbook

Chatterjee's xi of Fréchet and Mardia copulas

The Fréchet formula is (a-b)^2 + a*b; the Mardia formula is θ^4 * (1+3*θ^2) / 4. The proof includes all boundary and singular cases, using the conditional-CDF mixture formula rather than a copula density. See Ansari and Rockel, Dependence properties of bivariate copula families, Table 6.

@[simp]

theorem ProbabilityTheory.Copula.frechet_zero_zero : frechet 0 0 ⋯ ⋯ ⋯ = independence 2

theorem ProbabilityTheory.Copula.frechet_eq_mix (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) (hpos : 0 < a + b) : frechet a b ha hb hab = ((comonotonic 2).mix countermonotonic ⟨a / (a + b), ⋯⟩).mix (independence 2) ⟨a + b, ⋯⟩

Split off the independent part, then normalize the weights of M and W.

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

theorem ProbabilityTheory.Copula.chatterjeeXi_mardia (θ : ℝ) (hθ : |θ| ≤ 1) : (mardia θ hθ).chatterjeeXi = θ ^ 4 * (1 + 3 * θ ^ 2) / 4

theorem ProbabilityTheory.Copula.chatterjeeXi_frechet_eq_zero_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).chatterjeeXi = 0 ↔ a = 0 ∧ b = 0

theorem ProbabilityTheory.Copula.chatterjeeXi_mardia_eq_zero_iff (θ : ℝ) (hθ : |θ| ≤ 1) : (mardia θ hθ).chatterjeeXi = 0 ↔ θ = 0