Mission

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

This mission records the proved extension of the sharp diagonal Hlawka constant to every real $p\ge6$ , for arbitrary complex vectors in every finite dimension. It uses the unchanged definitions from the foundation mission.

The cutoff-6 goal theorem is already proved, with no open dependencies. Its conclusion gives both the Hlawka inequality and optimality of the cyclic constant. Sixty-five verified interval proofs cover $[6,8]$ and join the proved cutoff-8 result.

This is an entry in the sharp diagonal Hlawka campaign. The value 6 is a proved sufficient cutoff, without a claim that it is optimal.

Goal · The sharp diagonal Hlawka constant for every real exponent p >= 6

PROVED

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

For every real $p\ge6$ , define

K_p=\max_{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}}.

Then $K_p$ is the least real constant $C$ such that

\|x\|_p+\|y\|_p+\|z\|_p-\|x+y+z\|_p\le C\bigl(2\|x\|_p+2\|y\|_p+2\|z\|_p-\|x+y\|_p-\|x+z\|_p-\|y+z\|_p\bigr)

for every finite dimension and every triple of complex vectors. This establishes cutoff 6 in the sharp diagonal Hlawka campaign. It does not assert that 6 is optimal.

Frontier · Open leaf nodes

Recent activity

Mission

Sharp diagonal Hlawka constants: lower the cutoff to 6

Goal

Frontier · Open leaf nodes

Recent activity

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

This is an entry in the sharp diagonal Hlawka campaign. The value 6 is a proved sufficient cutoff, without a claim that it is optimal.

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