Hlawka constants for Schatten $p$-norms (Audenaert–Kittaneh Problem 7)

Settles the "if it exists" part for every $p$: a finite size-independent constant $C_p$ exists exactly when $1 < p < \infty$. The proof gives some constant, not the best one, for complex matrices of every size, square or rectangular. At $p = 1$ no constant exists, already for $2 \times 2$ matrices, turning Audenaert and Kittaneh's numerical $C_1 \ge 40$ into $C_1 = \infty$. At $p = \infty$ none exists on $3 \times 3$ matrices, as they already knew. For diagonal matrices and $p \ge 256$ the best constant is an explicit $K_p$, the maximum of a ratio over the family $(-t,1,1), (1,-t,1), (1,1,-t)$, $t \in [1/2, 2]$, with $939p/2000 < K_p \le p$. Since diagonal matrices are matrices, $939p/2000 < C_p < \infty$ for $p \ge 256$. Open: the best $C_p$ for general matrices (except $C_2 = 1$) and the best diagonal constant for $1 < p < 256$; the cutoff 256 is not claimed optimal. All of this is in Lean except the one-line step from diagonal to general matrices.

Settles the "if it exists" part for every $p$: a finite size-independent constant $C_p$ exists exactly when $1 < p < \infty$. The proof gives some constant, not the best one, for complex matrices of every size, square or rectangular. At $p = 1$ no constant exists, already for $2 \times 2$ matrices, turning Audenaert and Kittaneh's numerical $C_1 \ge 40$ into $C_1 = \infty$. At $p = \infty$ none exists on $3 \times 3$ matrices, as they already knew. For diagonal matrices and $p \ge 256$ the best constant is an explicit $K_p$, the maximum of a ratio over the family $(-t,1,1), (1,-t,1), (1,1,-t)$, $t \in [1/2, 2]$, with $939p/2000 < K_p \le p$. Since diagonal matrices are matrices, $939p/2000 < C_p < \infty$ for $p \ge 256$. Open: the best $C_p$ for general matrices (except $C_2 = 1$) and the best diagonal constant for $1 < p < 256$; the cutoff 256 is not claimed optimal. All of this is in Lean except the one-line step from diagonal to general matrices.