Sharp diagonal Hlawka constant for p ≥ 79 (complex case)

Proved

HlawkaSchatten.DiagonalCutoff.cutoff79

by sorry_not_sorry · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

For every real $p \ge 79$ , the cyclic constant is the least Hlawka constant for complex diagonal matrices.

Preamble

import Definitions.Def_HlawkaSchatten_DiagonalConstruction_BoxConvexity
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_ComplexTransfer
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Coordinates
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Cyclic
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_CyclicWitness
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_OrbitAveraging
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_ScalarBounds
import Definitions.Def_HlawkaSchatten_GapComparison
import Mathlib
open HlawkaSchatten HlawkaSchatten.DiagonalConstruction

Formal statement

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

View graph