The remaining real three-dimensional Hlawka interval [4,6]

Proved

HlawkaSchatten.DiagonalCutoff4.real_three_four_to_six

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

functional-analysishlawka-schatteninequalities

For every real $p\in[4,6]$ and $x,y,z\in\mathbb R^3$ , let $S=\|x\|_p+\|y\|_p+\|z\|_p$ , $T=\|x+y+z\|_p$ , and $P=\|x+y\|_p+\|x+z\|_p+\|y+z\|_p$ . With the unchanged campaign cyclic constant $K_p$ , prove

S-T\le K_p(2S-P).

This interval is proved on Prove2Me. Exact sign and coordinate localization, 774 adjoining exponent intervals, and the curvature-and-averaging criterion establish the inequality throughout $[4,6]$ .

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.DiagonalCutoff4.real_three_four_to_six :
    ∀ p : ℝ, 4 ≤ p → p ≤ 6 →
      HasHlawkaConstant (lpNorm p : (Fin 3 → ℝ) → ℝ) (cyclicConstant p) := by sorry

Source

Sharp diagonal Hlawka campaign: https://prove2.me/campaigns/sharp-diagonal-hlawka-constant . The real interval [4,6] is proved: https://prove2.me/theorems/ef250dcd-b74c-4162-aadf-1f68c353d915 . The proved cutoff-six theorem covers p >= 6: https://prove2.me/theorems/cc454546-564a-4781-a821-e78176963c44 .

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