Mission

Sharp diagonal Hlawka constants: lower the cutoff to 89Open Problem

Functional Analysis·Captain: savarin

The Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge90$ , also holds for every real $p\ge89$ . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the cutoff-90 mission already covers every $p\ge90$ , the new work is the range from 89 to 90.

The argument for $p\ge90$ was reached by tightening its estimates step by step, starting from 256. With its current choices those estimates stop working below 90, and nobody has yet found a way past that point. It is not known whether 90 is a real limit of the method or only of the choices made so far, so this mission is the smallest test of whether the cutoff can move at all. The accepted proof for $p\ge90$ and its research note are the natural starting point. The goal theorem below gives the exact statement.

This is an open entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 89 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

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
Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

Goal · Sharp complex coordinate Hlawka constant for p ≥ 89

PROVED

theorem HlawkaSchatten.DiagonalCutoff.cutoff89 :
    ∀ p : ℝ, 89 ≤ p →
      IsLeast {C : ℝ | ∀ n : ℕ,
        HasHlawkaConstant (lpNorm p : (Fin n → ℂ) → ℝ) C}
        (cyclicConstant p) := by sorry

For a real exponent $p>1$ and a vector $x\in\mathbb C^n$ , the coordinate norm is

N_p(x)=\left(\sum_{i=1}^n|x_i|^p\right)^{1/p}.

For any three vectors in the same space, their triple deficit is

\Delta_3=N_p(x)+N_p(y)+N_p(z)-N_p(x+y+z),

and their pair-deficit sum is

\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).

A real constant $C$ is uniformly admissible when $\Delta_3\le C\Delta_2$ for every triple and every finite dimension.

For $t\in[1/2,2]$ , define

A_p(t)=(t^p+2)^{1/p},\qquad B_p(t)=(2|1-t|^p+2^p)^{1/p},

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

This cyclic constant is exactly the foundation's cyclicConstant. It comes from the three vectors $(-t,1,1),(1,-t,1),(1,1,-t)$ . The fixed compact interval and the absolute value in $B_p$ are part of the definition and remain unchanged in this task. Cyclic definitions

For every real $p\ge89$ , the theorem asks for

K_p=\min\{C\in\mathbb R:\ \forall n\in\mathbb N,\ \forall x,y,z\in\mathbb C^n, \ \Delta_3\le C\Delta_2\}.

This includes admissibility and uniform optimality, with all unequal-norm and zero triples allowed. Dimension zero is included. No proof is known for $89\le p<90$ ; the accepted cutoff-90 theorem covers every $p\ge90$ .

Frontier · Open leaf nodes

Recent activity