← Copula mathematical handbook

Order signs and the finite Spearman moment identity

def ProbabilityTheory.Copula.RankRegion.RhoTau.orderSign {α : Type u_1} [LinearOrder α] (i j : α) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.orderSign i j = if i < j then 1 else if j < i then -1 else 0

@[simp]

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.orderSign_self {α : Type u_1} [LinearOrder α] (i : α) : orderSign i i = 0

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.orderSign_skew {α : Type u_1} [LinearOrder α] (i j : α) : orderSign j i = -orderSign i j

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.orderSign_sq {α : Type u_1} [LinearOrder α] {i j : α} (h : i ≠ j) : orderSign i j ^ 2 = 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.orderSign_cycle {α : Type u_1} [LinearOrder α] (i j k : α) : orderSign i j - orderSign i k + orderSign j k = orderSign i j * orderSign i k * orderSign j k

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.orderSign_mem {α : Type u_1} [LinearOrder α] (i j : α) : orderSign i j ∈ Set.Icc (-1) 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.permutation_edge_sign {n : ℕ} (π : Equiv.Perm (Fin n)) {i j : Fin n} (hij : i ≠ j) : (permutationSigns π).edge i j = -orderSign i j * orderSign (π i) (π j)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.permutation_inversion_sign {n : ℕ} (π : Equiv.Perm (Fin n)) (i j : Fin n) : orderSign i j * orderSign (π i) (π j) = (if i = j then 0 else 1) - 2 * (permutationSigns π).inversion i j

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.permutation_triple_sign {n : ℕ} (π : Equiv.Perm (Fin n)) (i j k : Fin n) : (permutationSigns π).triple i j k = (completeSigns.triple i j k - (orderSign i j - orderSign i k + orderSign j k) * (orderSign (π i) (π j) - orderSign (π i) (π k) + orderSign (π j) (π k))) / 2