← Mathematical handbook

Remark 2.2: the uniform cubic asymptotic at the comonotone endpoint

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.upper_boundary_cubic_remainder {g : ℝ} (hg : 99 / 100 < g) (hg1 : g < 1) : |upperRho g - (1 - 3 / 2 * (1 - g) ^ 2)| ≤ 98304 * (1 - g) ^ 3

A single explicit remainder constant works on every arc near gamma=1.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.upper_boundary_asymptotic : (fun (g : ℝ) => upperRho g - (1 - 3 / 2 * (1 - g) ^ 2)) =O[nhdsWithin 1 (Set.Iio 1)] fun (g : ℝ) => (1 - g) ^ 3

Equation (23), with the limit taken from below at gamma=1.