← Copula mathematical handbook

Removing a zero-weight strip from a permutation

def ProbabilityTheory.Copula.RankRegion.RhoTau.deletePermutation {n : ℕ} (π : Equiv.Perm (Fin (n + 1))) (i : Fin (n + 1)) : Equiv.Perm (Fin n)

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.deletePermutation π i = ((finSuccAboveEquiv i).trans (Equiv.subtypeEquiv π ⋯)).trans (finSuccAboveEquiv (π i)).symm

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.deletePermutation_commute {n : ℕ} (π : Equiv.Perm (Fin (n + 1))) (i : Fin (n + 1)) (j : Fin n) : π (i.succAbove j) = (π i).succAbove ((deletePermutation π i) j)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.delete_inversion {n : ℕ} (π : Equiv.Perm (Fin (n + 1))) (i : Fin (n + 1)) (j k : Fin n) : (permutationSigns π).inversion (i.succAbove j) (i.succAbove k) = (permutationSigns (deletePermutation π i)).inversion j k

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.delete_edge {n : ℕ} (π : Equiv.Perm (Fin (n + 1))) (i : Fin (n + 1)) (j k : Fin n) : (permutationSigns π).edge (i.succAbove j) (i.succAbove k) = (permutationSigns (deletePermutation π i)).edge j k

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.delete_triple {n : ℕ} (π : Equiv.Perm (Fin (n + 1))) (i : Fin (n + 1)) (j k l : Fin n) : (permutationSigns π).triple (i.succAbove j) (i.succAbove k) (i.succAbove l) = (permutationSigns (deletePermutation π i)).triple j k l

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.delete_zero_weight {n : ℕ} (π : Equiv.Perm (Fin (n + 1))) (u : Fin (n + 1) → ℝ) (i : Fin (n + 1)) (hi : u i = 0) : ∑ j : Fin n, u (i.succAbove j) = ∑ j : Fin (n + 1), u j ∧ (permutationSigns (deletePermutation π i)).a (u ∘ i.succAbove) = (permutationSigns π).a u ∧ (permutationSigns (deletePermutation π i)).b (u ∘ i.succAbove) = (permutationSigns π).b u