← Copula mathematical handbook

Three-coordinate minimization

The replacement step in Schreyer–Paulin–Trutschnig, Lemma 4.2, is expressed directly with a quadratic discriminant. It preserves the first two power sums and strictly decreases the third power sum whenever three positive coordinates have a unique largest member.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.improve_three_coordinates {x y z : ℝ} (hxy : y < x) (hyz : z ≤ y) (hz : 0 < z) : ∃ (a : ℝ) (b : ℝ) (c : ℝ), 0 < a ∧ 0 < b ∧ 0 < c ∧ a + b + c = x + y + z ∧ a ^ 2 + b ^ 2 + c ^ 2 = x ^ 2 + y ^ 2 + z ^ 2 ∧ a ^ 3 + b ^ 3 + c ^ 3 < x ^ 3 + y ^ 3 + z ^ 3