← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.triple_zero_permutations {ι : Type u_1} (S : SignData ι) (p q r : ι) (h : S.triple p q r = 0) : S.triple p r q = 0 ∧ S.triple q p r = 0 ∧ S.triple q r p = 0 ∧ S.triple r p q = 0 ∧ S.triple r q p = 0

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.a_four_pattern {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (p q r s : ι) (x y : ℝ) (hpq : S.inversion p q = 0) (hrs : S.inversion r s = 0) (hpr : S.inversion p r = 1) (hps : S.inversion p s = 1) (hqr : S.inversion q r = 1) (hqs : S.inversion q s = 1) : S.a (x • spike p + -x • spike q + y • spike r + -y • spike s) = 0

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.b_four_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (p q r s : ι) (x y z w : ℝ) (hpqr : S.triple p q r = 0) (hpqs : S.triple p q s = 0) (hprs : S.triple p r s = 0) (hqrs : S.triple q r s = 0) : S.b (x • spike p + y • spike q + z • spike r + w • spike s) = 0

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

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.four_coefficient_bounds {ι : Type u_1} [Fintype ι] (S : SignData ι) (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) (p q r s : ι) (hpqr : S.triple p q r = 0) (hpqs : S.triple p q s = 0) (hprs : S.triple p r s = 0) (hqrs : S.triple q r s = 0) : |S.pairCoefficient u p r + S.pairCoefficient u q s - S.pairCoefficient u p s - S.pairCoefficient u q r| ≤ 2 * S.pairCoefficient u p q ∧ |S.pairCoefficient u p r + S.pairCoefficient u q s - S.pairCoefficient u p s - S.pairCoefficient u q r| ≤ 2 * S.pairCoefficient u r s

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.four_pattern_reduction {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (u : ι → ℝ) (hu : ∀ (i : ι), 0 < u i) (p q r s : ι) (hpq : p ≠ q) (hpr : p ≠ r) (hps : p ≠ s) (hqr : q ≠ r) (_hqs : q ≠ s) (hrs : r ≠ s) (hpq' : S.inversion p q = 0) (hrs' : S.inversion r s = 0) (hpr' : S.inversion p r = 1) (hps' : S.inversion p s = 1) (hqr' : S.inversion q r = 1) (hqs' : S.inversion q s = 1) (hpqr : S.triple p q r = 0) (hpqs : S.triple p q s = 0) (hprs : S.triple p r s = 0) (hqrs : S.triple q r s = 0) : ∃ (v : ι → ℝ), (∀ (i : ι), 0 ≤ v i) ∧ ∑ i : ι, v i = ∑ i : ι, u i ∧ (∃ (i : ι), v i = 0) ∧ S.a v = S.a u ∧ S.b v ≤ S.b u

The second forbidden pattern also admits a boundary reduction preserving a.