The sharp diagonal Hlawka constant for $p = 2$ is $1$

Proved

HlawkaSchatten.DiagonalCutoff.cutoff2

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

hlawka-schattensharp-constant

NOT the threshold cutoff2 — this is the p=2 endpoint (point result only). The name was a mistake; sorry for squatting the namespace. For p=2, the least uniform constant C such that the diagonal Hlawka inequality holds with constant C on l_2^n(C) for every n is C=1, via Hlawka's 1D inequality integrated against the Gaussian measure.

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.cutoff2 : IsLeast {C : ℝ | ∀ n : ℕ, HasHlawkaConstant (lpNorm 2 : (Fin n → ℂ) → ℝ) C} 1 := by sorry

Source

https://prove2.me/campaigns/sharp-diagonal-hlawka-constant (endpoint p=2; proof via Hlawka's 1D inequality + Gaussian integral)

View graph

The sharp diagonal Hlawka constant for p=2p = 2p=2 is 111

The sharp diagonal Hlawka constant for $p = 2$ is $1$