← Copula mathematical handbook

Restoring the inversion constraint after the extremal adjacent swap

For adjacent minimum and maximum entries, the two linear cubic coefficients coincide. After swapping them, their mass can be redistributed to restore the quadratic constraint, while retaining the strict cubic improvement. This strengthens the swap step in Schreyer–Paulin–Trutschnig, Lemma 4.11.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.restore_pair_quadratic (x y A B : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : ∃ (X : ℝ) (Y : ℝ), 0 ≤ X ∧ 0 ≤ Y ∧ X + Y = x + y ∧ A * X + B * Y + X * Y = A * x + B * y