← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.a_smul {ι : Type u_1} [Fintype ι] (S : SignData ι) (u : ι → ℝ) (r : ℝ) : S.a (r • u) = r ^ 2 * S.a u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.b_smul {ι : Type u_1} [Fintype ι] (S : SignData ι) (u : ι → ℝ) (r : ℝ) : S.b (r • u) = r ^ 3 * S.b u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.bilinear_spike {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (i : ι) (v : ι → ℝ) : S.bilinear (spike i) v = (∑ j : ι, S.inversion i j * v j) / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.trilinear_spike {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (i : ι) (u v : ι → ℝ) : S.trilinear (spike i) u v = (∑ j : ι, ∑ k : ι, S.triple i j k * u j * v k) / 6

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.endpoint_expansion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (i : ι) (v : ι → ℝ) (hvi : v i = 0) (he : ∀ (j : ι), j ≠ i → S.edge i j = 1) (x : ℝ) : S.a (v + x • spike i) = x * ∑ j : ι, v j + S.a v ∧ S.b (v + x • spike i) = x * S.a v + S.b v

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.endpoint_coefficients {n : ℕ} (π : Equiv.Perm (Fin (n + 1))) (u : Fin (n + 1) → ℝ) (i : Fin (n + 1)) (he : ∀ (j : Fin (n + 1)), j ≠ i → (permutationSigns π).edge i j = 1) : (permutationSigns π).a u = u i * ∑ j : Fin n, u (i.succAbove j) + (permutationSigns (deletePermutation π i)).a (u ∘ i.succAbove) ∧ (permutationSigns π).b u = u i * (permutationSigns (deletePermutation π i)).a (u ∘ i.succAbove) + (permutationSigns (deletePermutation π i)).b (u ∘ i.succAbove)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.complete_cons {m : ℕ} (v : Fin m → ℝ) (x : ℝ) : completeSigns.a (Fin.cons x v) = x * ∑ j : Fin m, v j + completeSigns.a v ∧ completeSigns.b (Fin.cons x v) = x * completeSigns.a v + completeSigns.b v