Mission

Sharp diagonal Hlawka constants: foundation and proved cutoff 256Research Paper

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 establishes the best possible constant for complex diagonal matrices for every real $p\ge256$ . The result is proved in Lean. For each exponent, one constant works for every triple of diagonal matrices of the same size, across all finite sizes.

The constant comes from a simple family of three $3\times3$ diagonal matrices, called the cyclic family. Varying one parameter determines the largest comparison constant these examples require. The theorem proves that this value also works for every other triple of diagonal matrices, however large. The goal theorem gives the exact formula and statement.

This is the foundation of the sharp diagonal Hlawka campaign. It supplies the shared definitions and supporting results for lowering the exponent cutoff while keeping the same formula. A later mission has now established the result in Lean for every real $p\ge90$ ; the campaign invites further improvements.

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

Established results on Prove2Me

Goal · The least uniform complex coordinate Hlawka constant for p ≥ 256

PROVED

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

For a real exponent $p\ge256$ and $x\in\mathbb C^n$ , let

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

For a triple $x,y,z$ , put

\Delta_3=\|x\|_p+\|y\|_p+\|z\|_p-\|x+y+z\|_p,

\Delta_2=2(\|x\|_p+\|y\|_p+\|z\|_p) -\|x+y\|_p-\|x+z\|_p-\|y+z\|_p.

Define the cyclic constant by the fixed compact interval

K_p=\sup_{1/2\le t\le2} \frac{3(t^p+2)^{1/p}-3^{1/p}|2-t|} {6(t^p+2)^{1/p}-3(2|1-t|^p+2^p)^{1/p}}.

The theorem states that $K_p$ is the least real constant $C$ such that $\Delta_3\le C\Delta_2$ for every finite dimension $n$ and every triple in $\mathbb C^n$ . Thus it combines admissibility and dimension-independent optimality in one IsLeast statement. Dimension zero is included and has zero gaps. The lower-bound obstruction already occurs in dimension three; the theorem does not assert that the same constant is best in dimensions one or two. The coordinate norm agrees with the Schatten norm on diagonal matrices, but the statement does not quantify over general matrices.

Frontier · Open leaf nodes

Recent activity