← Copula mathematical handbook

The signed triple combinatorics of Schreyer–Paulin–Trutschnig

The parity representation in Lemma 4.5 makes the weighted triple coefficients satisfy triangle inequalities whenever the indexing triple has even inversion parity. Diagonal signs are negative, so repeated indices contribute zero without separate restrictions in the sums.

structure ProbabilityTheory.Copula.RankRegion.RhoTau.SignData (ι : Type u_1) : Type u_1

• edge : ι → ι → ℝ
• symmetric (i j : ι) : self.edge i j = self.edge j i
• diagonal (i : ι) : self.edge i i = -1
• values (i j : ι) : self.edge i j = -1 ∨ self.edge i j = 1

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

Equations

• S.triple i j k = (1 + S.edge i j * S.edge i k * S.edge j k) / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.triple_values {ι : Type u_1} (S : SignData ι) (i j k : ι) : S.triple i j k = 0 ∨ S.triple i j k = 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.triple_nonneg {ι : Type u_1} (S : SignData ι) (i j k : ι) : 0 ≤ S.triple i j k

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.triple_swap_left {ι : Type u_1} (S : SignData ι) (i j k : ι) : S.triple i j k = S.triple j i k

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.triple_swap_right {ι : Type u_1} (S : SignData ι) (i j k : ι) : S.triple i j k = S.triple i k j

@[simp]

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.triple_repeat {ι : Type u_1} (S : SignData ι) (i j : ι) : S.triple i i j = 0

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.triple_triangle {ι : Type u_1} (S : SignData ι) (p q r i : ι) (h : S.triple p q r = 0) : S.triple p q i ≤ S.triple p r i + S.triple q r i

The pointwise parity identity underlying Lemma 4.5.

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

Equations

• S.pairCoefficient u i j = ∑ k : ι, S.triple i j k * u k

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.pairCoefficient_symmetric {ι : Type u_1} (S : SignData ι) [Fintype ι] (u : ι → ℝ) (i j : ι) : S.pairCoefficient u i j = S.pairCoefficient u j i

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.pairCoefficient_nonneg {ι : Type u_1} (S : SignData ι) [Fintype ι] (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) (i j : ι) : 0 ≤ S.pairCoefficient u i j

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.pairCoefficient_triangle {ι : Type u_1} (S : SignData ι) [Fintype ι] (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) (p q r : ι) (h : S.triple p q r = 0) : S.pairCoefficient u p q ≤ S.pairCoefficient u p r + S.pairCoefficient u q r

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.triple_quadratic_nonpos {a b c x y z : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hab : a ≤ b + c) (hbc : b ≤ a + c) (hca : c ≤ a + b) (hxyz : x + y + z = 0) : a * x * y + b * x * z + c * y * z ≤ 0

The three-coordinate quadratic form from Lemma 4.6(i).

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.four_quadratic_nonpos {a b d x y : ℝ} (ha : |d| ≤ 2 * a) (hb : |d| ≤ 2 * b) : -a * x ^ 2 + d * x * y - b * y ^ 2 ≤ 0

The four-coordinate quadratic form from Lemma 4.6(ii).