← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.a_add_pair {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (u : ι → ℝ) (p q : ι) (x y : ℝ) : S.a (u + (x • spike p + y • spike q)) = S.a u + 2 * x * S.bilinear (spike p) u + 2 * y * S.bilinear (spike q) u + S.inversion p q * x * y

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.b_add_pair {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (u : ι → ℝ) (p q : ι) (x y : ℝ) : S.b (u + (x • spike p + y • spike q)) = S.b u + 3 * x * S.trilinear (spike p) u u + 3 * y * S.trilinear (spike q) u u + S.pairCoefficient u p q * x * y