← Copula mathematical handbook

def ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.flipPair {ι : Type u_1} [DecidableEq ι] (S : SignData ι) (p q : ι) (hpq : p ≠ q) : SignData ι

Equations

• S.flipPair p q hpq = { edge := fun (i j : ι) => if i = p ∧ j = q ∨ i = q ∧ j = p then 1 else S.edge i j, symmetric := ⋯, diagonal := ⋯, values := ⋯ }

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.flipPair_edge_away {ι : Type u_1} [DecidableEq ι] (S : SignData ι) (p q : ι) (hpq : p ≠ q) (i j : ι) (hi : i ≠ p ∧ i ≠ q) : (S.flipPair p q hpq).edge i j = S.edge i j

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.flipPair_edge_away_right {ι : Type u_1} [DecidableEq ι] (S : SignData ι) (p q : ι) (hpq : p ≠ q) (i j : ι) (hj : j ≠ p ∧ j ≠ q) : (S.flipPair p q hpq).edge i j = S.edge i j

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.flipPair_bilinear_base {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (p q : ι) (hpq : p ≠ q) (v : ι → ℝ) (hvp : v p = 0) (hvq : v q = 0) (u : ι → ℝ) : (S.flipPair p q hpq).bilinear u v = S.bilinear u v

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.flipPair_trilinear_base {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (p q : ι) (hpq : p ≠ q) (v : ι → ℝ) (hvp : v p = 0) (hvq : v q = 0) (u : ι → ℝ) : (S.flipPair p q hpq).trilinear u v v = S.trilinear u v v

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.extremal_pair_equal_linear {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (p q : ι) (v : ι → ℝ) (hvp : v p = 0) (hvq : v q = 0) (hop : ∀ (i : ι), i ≠ p → i ≠ q → S.edge p i = -S.edge q i) : S.trilinear (spike p) v v = S.trilinear (spike q) v v

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.extremal_pair_coefficients {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (p q : ι) (hpq : p ≠ q) (v : ι → ℝ) (hvp : v p = 0) (hvq : v q = 0) (hedge : S.edge p q = -1) (hop : ∀ (i : ι), i ≠ p → i ≠ q → S.edge p i = -S.edge q i) : S.pairCoefficient v p q = ∑ i : ι, v i ∧ (S.flipPair p q hpq).pairCoefficient v p q = 0

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.extremal_pair_improvement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (p q : ι) (hpq : p ≠ q) (v : ι → ℝ) (_hv : ∀ (i : ι), 0 ≤ v i) (hvp : v p = 0) (hvq : v q = 0) (hedge : S.edge p q = -1) (hop : ∀ (i : ι), i ≠ p → i ≠ q → S.edge p i = -S.edge q i) (x y : ℝ) (hx : 0 < x) (hy : 0 < y) (hrest : 0 < ∑ i : ι, v i) : ∃ (X : ℝ) (Y : ℝ), 0 ≤ X ∧ 0 ≤ Y ∧ X + Y = x + y ∧ (S.flipPair p q hpq).a (v + (X • spike p + Y • spike q)) = S.a (v + (x • spike p + y • spike q)) ∧ (S.flipPair p q hpq).b (v + (X • spike p + Y • spike q)) < S.b (v + (x • spike p + y • spike q))

Exact restoration of a, with a strictly improved b when a third mass is present.