← Copula mathematical handbook

def ProbabilityTheory.Copula.RankRegion.RhoTau.completeSigns {ι : Type u_1} [DecidableEq ι] : SignData ι

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.completeSigns = { edge := fun (i j : ι) => if i = j then -1 else 1, symmetric := ⋯, diagonal := ⋯, values := ⋯ }

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.complete_inversion {ι : Type u_1} [DecidableEq ι] (i j : ι) : completeSigns.inversion i j = if i = j then 0 else 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.complete_triple {ι : Type u_1} [DecidableEq ι] (i j k : ι) : completeSigns.triple i j k = if i = j ∨ i = k ∨ j = k then 0 else 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.complete_a {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : ι → ℝ) : completeSigns.a u = ((∑ i : ι, u i) ^ 2 - ∑ i : ι, u i ^ 2) / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.complete_b {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : ι → ℝ) : completeSigns.b u = ((∑ i : ι, u i) ^ 3 - (3 * ∑ i : ι, u i) * ∑ i : ι, u i ^ 2 + 2 * ∑ i : ι, u i ^ 3) / 6

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.complete_minimum_prototype {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) (hs : ∑ i : ι, u i = 1) : ∃ (n : ℕ) (s : ↑unitInterval), (1 - arcTau n ↑s) / 4 = completeSigns.a u ∧ (arcRho n ↑s - 1 + 6 * completeSigns.a u) / 6 ≤ completeSigns.b u

The symmetric minimization lemma in the inversion and triple coordinates.