Documentation

Copula.Rank.Region.RhoTau.SparseVariations

← Copula mathematical handbook
source
def ProbabilityTheory.Copula.RankRegion.RhoTau.spike {ι : Type u_1} [DecidableEq ι] (i : ι) :
ι → ℝ
Equations
Instances For
    source
    @[simp]
    theorem ProbabilityTheory.Copula.RankRegion.RhoTau.sum_spike {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) :
    ∑ j : ι, spike i j = 1
    source
    @[simp]
    theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.triple_repeat_right {ι : Type u_1} (S : SignData ι) (i j : ι) :
    S.triple i j j = 0
    source
    @[simp]
    theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.triple_repeat_outer {ι : Type u_1} (S : SignData ι) (i j : ι) :
    S.triple i j i = 0
    source
    theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.bilinear_spikes {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (i j : ι) :
    S.bilinear (spike i) (spike j) = S.inversion i j / 2
    source
    theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.trilinear_spikes {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (i j k : ι) :
    S.trilinear (spike i) (spike j) (spike k) = S.triple i j k / 6
    source
    theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.trilinear_two_spikes {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (i j : ι) (u : ι → ℝ) :
    S.trilinear (spike i) (spike j) u = S.pairCoefficient u i j / 6
    source
    @[simp]
    theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.pairCoefficient_diagonal {ι : Type u_1} [Fintype ι] (S : SignData ι) (i : ι) (u : ι → ℝ) :
    S.pairCoefficient u i i = 0
    source
    theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.a_three {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (p q r : ι) (x y z : ℝ) :
    S.a (x • spike p + y • spike q + z • spike r) = S.inversion p q * x * y + S.inversion p r * x * z + S.inversion q r * y * z
    source
    theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.b_three {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (p q r : ι) (x y z : ℝ) :
    S.b (x • spike p + y • spike q + z • spike r) = S.triple p q r * x * y * z
    source
    theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.second_three {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (p q r : ι) (x y z : ℝ) (u : ι → ℝ) :
    3 * S.trilinear (x • spike p + y • spike q + z • spike r) (x • spike p + y • spike q + z • spike r) u = S.pairCoefficient u p q * x * y + S.pairCoefficient u p r * x * z + S.pairCoefficient u q r * y * z
    source
    theorem ProbabilityTheory.Copula.RankRegion.RhoTau.SignData.increasing_triple_reduction {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (u : ι → ℝ) (hu : ∀ (i : ι), 0 < u i) (p q r : ι) (hpq : p ≠ q) (hpr : p ≠ r) (hqr : q ≠ r) (hpq' : S.inversion p q = 0) (hpr' : S.inversion p r = 0) (hqr' : S.inversion q r = 0) (ht : S.triple p q r = 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 increasing-triple direction preserves the quadratic and decreases the cubic at a simplex boundary, as in Lemmas 4.6(i) and 4.7.