← Mathematical handbook

Theorem 4.2 in the original theta coordinates

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_transport_value (theta : ℝ) (ht : 0 < theta) : have A := thetaCertificate theta ht; transportValue (thetaT theta) = 2 * ∫ (u : ↑unitInterval), A.dual ↑u ∧ 2 * ∫ (u : ↑unitInterval), A.dual ↑u = (thetaP theta - 3 / 2 * thetaT theta * thetaG theta) / 3

Equation (46), including the attained primal, dual and supporting values.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_supporting_inequality (theta : ℝ) (ht : 0 < theta) (C : ProbabilityTheory.Copula 2) : C.spearmanRho - 3 / 2 * thetaT theta * C.giniGamma ≤ thetaP theta - 3 / 2 * thetaT theta * thetaG theta

Equation (47), with the exact source multiplier and coordinates.