← Copula mathematical handbook

The Schreyer–Paulin–Trutschnig prototype copulas

Schreyer, Paulin and Trutschnig (2017), On the exact region determined by Kendall's tau and Spearman's rho, Lemma 3.5. Reflected ordinal sums of W attain the junction points and every prototype arc. The parameter s ∈ I varies from n+2 equal blocks to n+1 equal blocks.

The universal sharp inequality is proved in RhoTau.Universal, and RhoTau.Exact proves the complete attainable-region characterization.

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.junctionCopula (n : ℕ) : Copula 2

Index n represents n+1 equal countermonotonic blocks, then reflection.

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.junctionCopula n = (ProbabilityTheory.Copula.RankRegion.equalBlocks n ProbabilityTheory.Copula.countermonotonic).reflect {1}

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.junctionCopula_coefficients (n : ℕ) : (junctionCopula n).kendallTau = -1 + 2 / (↑n + 1) ∧ (junctionCopula n).spearmanRho = -1 + 2 / (↑n + 1) ^ 2

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.junction_attainable (n : ℕ) : ∃ (C : Copula 2), C.kendallTau = -1 + 2 / (↑n + 1) ∧ C.spearmanRho = -1 + 2 / (↑n + 1) ^ 2

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.arcSplit (n : ℕ) (s : ↑unitInterval) : ↑unitInterval

Total width of the first n+1 equal blocks of a prototype.

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.arcSplit n s = ⟨(↑n + 1 + ↑s) / (↑n + 2), ⋯⟩

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.arcCopula (n : ℕ) (s : ↑unitInterval) : Copula 2

A prototype has n+1 equal blocks and one smaller block, followed by reflection.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.arcTau (n : ℕ) (s : ℝ) : ℝ

Polynomial parametrization of the tau coordinate of a prototype arc.

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.arcTau n s = -1 + 2 / (↑n + 2) + 2 * s ^ 2 / ((↑n + 1) * (↑n + 2))

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.arcRho (n : ℕ) (s : ℝ) : ℝ

Polynomial parametrization of the rho coordinate of a prototype arc.

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.arcRho n s = -1 + 2 / (↑n + 2) ^ 2 + 6 * s ^ 2 / ((↑n + 1) * (↑n + 2) ^ 2) - 2 * ↑n * s ^ 3 / ((↑n + 1) ^ 2 * (↑n + 2) ^ 2)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.arcCopula_coefficients (n : ℕ) (s : ↑unitInterval) : (arcCopula n s).kendallTau = arcTau n ↑s ∧ (arcCopula n s).spearmanRho = arcRho n ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.arc_attainable (n : ℕ) (s : ↑unitInterval) : ∃ (C : Copula 2), C.kendallTau = arcTau n ↑s ∧ C.spearmanRho = arcRho n ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.arc_zero (n : ℕ) : arcTau n 0 = -1 + 2 / (↑n + 2) ∧ arcRho n 0 = -1 + 2 / (↑n + 2) ^ 2

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.arc_one (n : ℕ) : arcTau n 1 = -1 + 2 / (↑n + 1) ∧ arcRho n 1 = -1 + 2 / (↑n + 1) ^ 2