← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.weighted_inversion_sign {n : ℕ} (π : Equiv.Perm (Fin n)) (u : Fin n → ℝ) (hs : ∑ i : Fin n, u i = 1) : (weighted2 u fun (i j : Fin n) => orderSign i j * orderSign (π i) (π j)) = 1 - ∑ i : Fin n, u i ^ 2 - 4 * (permutationSigns π).a u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.finite_rho_moment {n : ℕ} (π : Equiv.Perm (Fin n)) (u : Fin n → ℝ) (hs : ∑ i : Fin n, u i = 1) : 1 - 6 * (permutationSigns π).a u + 6 * (permutationSigns π).b u = ∑ i : Fin n, u i ^ 3 + 3 * ∑ i : Fin n, (u i * ∑ j : Fin n, orderSign i j * u j) * ∑ k : Fin n, orderSign (π i) (π k) * u k

Spearman's finite permutation statistic, including the diagonal correction.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.finite_tau_moment {n : ℕ} (π : Equiv.Perm (Fin n)) (u : Fin n → ℝ) (hs : ∑ i : Fin n, u i = 1) : 1 - 4 * (permutationSigns π).a u = ∑ i : Fin n, u i ^ 2 + weighted2 u fun (i j : Fin n) => orderSign i j * orderSign (π i) (π j)