← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.ext_edge {ι : Type u_1} (S T : SignData ι) (h : ∀ (i j : ι), S.edge i j = T.edge i j) : S = T

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.ext_edge_iff {ι : Type u_1} {S T : SignData ι} : S = T ↔ ∀ (i j : ι), S.edge i j = T.edge i j

def ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.relabel {ι : Type u_1} (S : SignData ι) (e : Equiv.Perm ι) : SignData ι

Equations

• S.relabel e = { edge := fun (i j : ι) => S.edge (e i) (e j), symmetric := ⋯, diagonal := ⋯, values := ⋯ }

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.a_relabel {ι : Type u_1} [Fintype ι] (S : SignData ι) (e : Equiv.Perm ι) (u : ι → ℝ) : (S.relabel e).a (u ∘ ⇑e) = S.a u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.b_relabel {ι : Type u_1} [Fintype ι] (S : SignData ι) (e : Equiv.Perm ι) (u : ι → ℝ) : (S.relabel e).b (u ∘ ⇑e) = S.b u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.inverse_signs {n : ℕ} (π : Equiv.Perm (Fin n)) : (permutationSigns (Equiv.symm π)).relabel π = permutationSigns π

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.inverse_coefficients {n : ℕ} (π : Equiv.Perm (Fin n)) (u : Fin n → ℝ) : (permutationSigns (Equiv.symm π)).a (u ∘ ⇑(Equiv.symm π)) = (permutationSigns π).a u ∧ (permutationSigns (Equiv.symm π)).b (u ∘ ⇑(Equiv.symm π)) = (permutationSigns π).b u