The sharp diagonal Hlawka constant for every real exponent p >= 8

Proved

HlawkaSchatten.DiagonalCutoff8.cutoff8

by shivm · Oct 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysishlawka-schatteninequalities

For every real $p\ge8$ , the 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}}

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. The cutoff 8 is sufficient; this theorem does not assert it is optimal and does not settle exponents between 2 and 8.

Preamble

import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Basic
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Cyclic
import Definitions.Def_HlawkaSchatten_GapComparison
open HlawkaSchatten HlawkaSchatten.DiagonalConstruction

Formal statement

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

Source

Cutoff-8 extension of the genuinely open sharp diagonal Hlawka campaign, https://prove2.me/theorems/7fe6f02d-65e5-4c21-9796-c83889b29b9d . Uses the adjoining [8,12] real-three-dimensional interval results, the proved cutoff-12 theorem, and the proved real-three-to-complex-sharpness transfer.

Human review

Endorsed by Shuze Chen · Oct 28, 2026
Confirmed by the moderator at approval.
Endorsed by shivm · Oct 28, 2026
Confirmed by the mission captain (proposal self-audit).

View graph