Papers With

← All papers
First page of The trapezoid comparison inequality in metric spaces with curvature bounded above

The trapezoid comparison inequality in metric spaces with curvature bounded above

Christof Schötz

math.MG Sep 2, 2026 · v1
formalization mathlib geometry analysis
Read PDF arXiv abstract
TL;DR
A key elementary inequality (Lemma 4.5) and its case lemmas are machine-checked in Lean 4 against Mathlib; the file is provided as an arXiv ancillary file.
Abstract
Among four points of a CAT(0) space, the planar symmetric trapezoids are configurations on which Ptolemy's and Reshetnyak's inequalities are both equalities. We show that the symmetric trapezoids remain extremal for the entire family of inequalities interpolating between the two, indexed by the nondecreasing convex functions with concave derivative, and that this function class is characterized by this property. The result is qualitatively stronger than the known quadruple inequalities for this class of functions, and recovers them with their optimal constants, which were previously known only for power functions. Moreover, we extend the analysis to CAT($κ$) spaces with $κ>0$. We derive variants of Reshetnyak's quadrilateral comparison and of Ptolemy's inequality under positive upper curvature bounds, each with the optimal constant. These two inequalities yield the trapezoid comparison inequality in CAT($κ$) spaces, where the product of the bases carries an additional constant factor compared to the $κ=0$ case. Again the constant is optimal.
Problem

Among four points of a CAT(0) space, planar symmetric trapezoids make both Ptolemy's and Reshetnyak's inequalities equalities. The question is whether trapezoids remain extremal for the whole family of quadruple inequalities indexed by nondecreasing convex functions with concave derivative. A second question is how these results extend to CAT(κ) spaces with κ>0.

Approach

The trapezoid comparison inequality is reduced to an algebraic statement about six nonnegative numbers. Using a Choquet-type integral representation of the function cone, this becomes a single elementary inequality between piecewise-quadratic functions (Lemma 4.5). That inequality's interlocking case analysis is verified in Lean 4 with Mathlib, with no sorry and only the standard axioms. For CAT(κ), the authors derive variants of Reshetnyak's and Ptolemy's inequalities with an optimal curvature constant.

Results

Symmetric trapezoids are extremal for the entire function class, and this property characterizes the class. The result recovers the known quadruple inequalities with optimal constants, which were previously known only for power functions. For CAT(κ), a trapezoid comparison holds in which the product of the bases carries an extra optimal factor R/sin(R).