The cyclic Hlawka bound for all complex operators when p ≥ 256

Open

HlawkaSchatten.SchattenSharpness.cyclic_bound256

by savarin · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

hlawka-schattensharp-constant

Let $E$ and $F$ be finite-dimensional complex inner-product spaces. A complex-linear map $A:E\to F$ is represented, after choosing orthonormal bases, by a possibly rectangular complex matrix. Its singular values $s_i(A)$ are the nonnegative square roots of the eigenvalues of $A^*A$ , with zeros permitted. For real $p>1$ , its Schatten norm is

N_p(A)=\left(\sum_i s_i(A)^p\right)^{1/p}.

The finite sum and its outer root are the existing schattenPNorm definition. No normalization by dimension is used. Formal definition

For maps $A,B,C:E\to F$ , define the triple deficit and pair-deficit sum by

\Delta_3=N_p(A)+N_p(B)+N_p(C)-N_p(A+B+C),

\Delta_2=2\bigl(N_p(A)+N_p(B)+N_p(C)\bigr) -N_p(A+B)-N_p(A+C)-N_p(B+C).

An admissible Hlawka constant $K$ satisfies $\Delta_3\le K\Delta_2$ for all such maps.

The cyclic candidate is the real number

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}}.

It is the existing DiagonalConstruction.cyclicConstant, derived from the coordinate triple $(-t,1,1),(1,-t,1),(1,1,-t)$ . The supremum is attained and its defining denominator is positive for $p>1$ on the displayed interval. Cyclic definition and attainment

The conjecture asks for

\forall p\ge256,\ \forall E,F,\ \forall A,B,C:E\to_{\mathbb C}F, \qquad \Delta_3\le K_p\Delta_2,

where $E,F$ range over all finite-dimensional complex inner-product spaces. Their dimensions may differ or be zero. No positivity, commutativity, common diagonalization or equal-norm hypothesis is imposed. The real exponent is arbitrary in the stated tail, not restricted to integers.

Preamble

import Definitions.Def_HlawkaSchatten_SchattenNorm
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Cyclic
import Definitions.Def_HlawkaSchatten_GapComparison

open HlawkaSchatten HlawkaSchatten.DiagonalConstruction

Formal statement

theorem HlawkaSchatten.SchattenSharpness.cyclic_bound256
    (p : ℝ) (hp : 256 ≤ p)
    (E F : Type*)
    [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E]
    [NormedAddCommGroup F] [InnerProductSpace ℂ F] [FiniteDimensional ℂ F] :
    HasHlawkaConstant (schattenPNorm p : (E →ₗ[ℂ] F) → ℝ)
      (cyclicConstant p) := by sorry

Source

Conjecture motivated by Audenaert–Kittaneh, Problem 7, https://arxiv.org/abs/1201.5232; proved diagonal case: https://github.com/savarin/hlawka-schatten/blob/79aa498bfcf7b22bd91d771fb32ec278e2d4704b/HlawkaSchatten/DiagonalConstruction/ComplexTransfer.lean#L83

Read-back

What the Lean code literally says, in plain math · GPT-6

For every real number $p$ with $256 \le p$ , and for every pair of types $E,F$ equipped with normed commutative additive-group structures and compatible complex inner-product-space structures, each finite-dimensional over $\mathbb C$ , the following assertion holds. For a complex-linear map $T:E\to F$ , let $\sigma_i(T)$ , indexed by $i\in\mathbb N=\{0,1,\ldots\}$ , be the nonnegative square roots of the eigenvalues of $T^*T$ , in decreasing order with multiplicity and continued by zeros, where $T^*$ is the adjoint for the specified inner products. Put $S(T)=\{i\in\mathbb N:\sigma_i(T)\ne0\}$ , which is the finite set $\{0,\ldots,\dim_{\mathbb C}T(E)-1\}$ when the rank is positive and is empty when the rank is zero, and define $N_p(T)=\left(\sum_{i\in S(T)}\sigma_i(T)^p\right)^{1/p}$ . Define the real number $C_p=\operatorname{sSup}_{\mathbb R}\left\{\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}}\;\middle|\;t\in\mathbb R,\ \frac12\le t\le2\right\}$ . Here $\operatorname{sSup}_{\mathbb R}$ is the least upper bound when the set is nonempty and bounded above, and is $0$ if the set is empty or unbounded above; the particular set displayed is nonempty because its parameter interval is nonempty. The scalar quotient uses total real division, which assigns $a/0=0$ for every real $a$ , and the definition includes every parameter in the closed interval, including both endpoints and $t=1$ . All powers in these formulas are real powers; their bases are nonnegative and $p\ge256$ ensures $p>0$ and $1/p>0$ , so a zero base with either of these exponents contributes zero. Then, for every three complex-linear maps $X,Y,Z:E\to F$ , with addition of maps taken pointwise, $N_p(X)+N_p(Y)+N_p(Z)-N_p(X+Y+Z)\le C_p\bigl[(N_p(X)+N_p(Y)-N_p(X+Y))+(N_p(X)+N_p(Z)-N_p(X+Z))+(N_p(Y)+N_p(Z)-N_p(Y+Z))\bigr]$ . The exponent $p$ need not be an integer and may equal $256$ ; there is no upper bound on it. The spaces may have different dimensions and either may have dimension zero, and the maps may be zero, equal, or otherwise arbitrary. For a zero map the support is empty, the sum is $0$ , and $N_p(0)=0$ ; if either space has dimension zero, all the maps are zero and the asserted inequality is $0\le0$ . The inequality also includes triples for which the sum of the three parenthesized pair differences is zero, with no division by that sum. Its conclusion is the universal validity of this inequality for the specified scalar $C_p$ .

View graph