Mission

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

The campaign cyclic constant is proved sharp for every real $p\ge4$ , uniformly over finite-dimensional complex vectors. The Lean proof combines the complete real three-dimensional interval $[4,6]$ with the proved cutoff-six result and the campaign reductions.

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

PROVED

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

For every real $p\ge4$ , define the unchanged cyclic constant

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

Prove that $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 all complex vectors $x,y,z$ in that dimension. This theorem is proved on Prove2Me. The complete real three-dimensional interval $[4,6]$ , the campaign reductions, and the proved cutoff-six theorem establish the result for every $p\ge4$ . Four is not asserted to be the optimal cutoff.

Frontier · Open leaf nodes

Recent activity

Mission

Sharp diagonal Hlawka constants: lower the cutoff to 4

Goal

Frontier · Open leaf nodes

Recent activity

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

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