← Copula mathematical handbook

Polynomial variations of inversion and triple sums

Ordered sums carry the factors 1/2 and 1/6. This avoids choosing an enumeration of the index set when coordinates vanish during induction.

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.inversion {ι : Type u_1} (S : SignData ι) (i j : ι) : ℝ

Equations

• S.inversion i j = (1 + S.edge i j) / 2

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.bilinear {ι : Type u_1} [Fintype ι] (S : SignData ι) (u v : ι → ℝ) : ℝ

Equations

• S.bilinear u v = (∑ i : ι, ∑ j : ι, S.inversion i j * u i * v j) / 2

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.trilinear {ι : Type u_1} [Fintype ι] (S : SignData ι) (u v w : ι → ℝ) : ℝ

Equations

• S.trilinear u v w = (∑ i : ι, ∑ j : ι, ∑ k : ι, S.triple i j k * u i * v j * w k) / 6

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.a {ι : Type u_1} [Fintype ι] (S : SignData ι) (u : ι → ℝ) : ℝ

Equations

• S.a u = S.bilinear u u

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.b {ι : Type u_1} [Fintype ι] (S : SignData ι) (u : ι → ℝ) : ℝ

Equations

• S.b u = S.trilinear u u u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.inversion_symmetric {ι : Type u_1} (S : SignData ι) (i j : ι) : S.inversion i j = S.inversion j i

@[simp]

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.inversion_diagonal {ι : Type u_1} (S : SignData ι) (i : ι) : S.inversion i i = 0

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.bilinear_symm {ι : Type u_1} [Fintype ι] (S : SignData ι) (u v : ι → ℝ) : S.bilinear u v = S.bilinear v u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.trilinear_swap_left {ι : Type u_1} [Fintype ι] (S : SignData ι) (u v w : ι → ℝ) : S.trilinear u v w = S.trilinear v u w

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.trilinear_swap_right {ι : Type u_1} [Fintype ι] (S : SignData ι) (u v w : ι → ℝ) : S.trilinear u v w = S.trilinear u w v

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.bilinear_add_left {ι : Type u_1} [Fintype ι] (S : SignData ι) (u v w : ι → ℝ) : S.bilinear (u + v) w = S.bilinear u w + S.bilinear v w

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.bilinear_smul_left {ι : Type u_1} [Fintype ι] (S : SignData ι) (r : ℝ) (u v : ι → ℝ) : S.bilinear (r • u) v = r * S.bilinear u v

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.trilinear_add_left {ι : Type u_1} [Fintype ι] (S : SignData ι) (u v w z : ι → ℝ) : S.trilinear (u + v) w z = S.trilinear u w z + S.trilinear v w z

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.trilinear_smul_left {ι : Type u_1} [Fintype ι] (S : SignData ι) (r : ℝ) (u v w : ι → ℝ) : S.trilinear (r • u) v w = r * S.trilinear u v w

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.bilinear_add_right {ι : Type u_1} [Fintype ι] (S : SignData ι) (u v w : ι → ℝ) : S.bilinear u (v + w) = S.bilinear u v + S.bilinear u w

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.bilinear_smul_right {ι : Type u_1} [Fintype ι] (S : SignData ι) (r : ℝ) (u v : ι → ℝ) : S.bilinear u (r • v) = r * S.bilinear u v

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.trilinear_add_middle {ι : Type u_1} [Fintype ι] (S : SignData ι) (u v w z : ι → ℝ) : S.trilinear u (v + w) z = S.trilinear u v z + S.trilinear u w z

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.trilinear_add_right {ι : Type u_1} [Fintype ι] (S : SignData ι) (u v w z : ι → ℝ) : S.trilinear u v (w + z) = S.trilinear u v w + S.trilinear u v z

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.trilinear_smul_middle {ι : Type u_1} [Fintype ι] (S : SignData ι) (r : ℝ) (u v w : ι → ℝ) : S.trilinear u (r • v) w = r * S.trilinear u v w

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.trilinear_smul_right {ι : Type u_1} [Fintype ι] (S : SignData ι) (r : ℝ) (u v w : ι → ℝ) : S.trilinear u v (r • w) = r * S.trilinear u v w

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

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.b_variation {ι : Type u_1} [Fintype ι] (S : SignData ι) (u δ : ι → ℝ) (t : ℝ) : S.b (u + t • δ) = S.b u + 3 * t * S.trilinear δ u u + 3 * t ^ 2 * S.trilinear δ δ u + t ^ 3 * S.b δ