Why determine the optimal constant?

The triangle inequality measures the loss when two vectors are added. A Hlawka inequality compares the analogous loss for three vectors with the combined losses for their three pairs. The best comparison constant records a geometric property of the norm. Audenaert and Kittaneh ask for this constant in the Schatten norm setting in Problem 7 of their 2012 collection. Audenaert–Kittaneh, §8.2

This result concerns the coordinate case (equivalently, complex diagonal matrices). It identifies the optimal constant, characterized by a one-variable maximization, for real exponents $p \ge 256$, including nonintegers. The cutoff 256 is a sufficient threshold supported by Lean proofs; it is not asserted to be the smallest possible.

Definitions and the goal

For $p > 1$, the coordinate norm of a complex vector $x = (x_i)$ is

$$N_p(x) = \left(\sum_i |x_i|^p\right)^{1/p}.$$

The triple deficit and pair-deficit sum are

$$\Delta_3 = N_p(x) + N_p(y) + N_p(z) - N_p(x+y+z),$$ $$\Delta_2 = 2\bigl(N_p(x) + N_p(y) + N_p(z)\bigr) - N_p(x+y) - N_p(x+z) - N_p(y+z).$$

The cyclic constant $K_p$ is defined by

$$K_p = \sup_{t \in [1/2,2]} \frac{3A_p(t) - 3^{1/p}|2-t|}{6A_p(t) - 3B_p(t)},$$

where $A_p(t) = (t^p+2)^{1/p}$ and $B_p(t) = (2|1-t|^p + 2^p)^{1/p}$. The fraction inside the supremum is the ratio $\Delta_3/\Delta_2$ for the cyclic triple $(-t,1,1), (1,-t,1), (1,1,-t)$. The denominator is positive on $[1/2, 2]$ for $p > 1$, and the supremum is attained. Cyclic definitions and attainment

The goal states that for all real $p \ge 256$, $K_p$ is the least constant $C$ such that $\Delta_3 \le C \Delta_2$ for every triple in every finite complex coordinate space. No normalization, nonzero, or equal-norm assumption is placed on the triple; one constant works across all finite dimensions. Lean expresses this as IsLeast of the set of uniformly admissible constants. Admissibility, lower bound

Foundation for cutoff improvements

This goal is already proved in Lean. This mission provides the proved baseline and shared definitions for later improvements to the exponent cutoff. Those improvements must use the same coordinate norm and cyclic constant. The general-matrix problem is a separate challenge.

The cyclic examples establish a lower bound, but proving that the constant works for arbitrary triples — including triples with unequal norms — is the difficult part.

References

• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
• Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library

Established results on Prove2Me

• The accepted sharp diagonal bound for every real p ≥ 256.
• The accepted diagonal Schatten norm identity.