Sharp complex coordinate Hlawka constant for p ≥ 90

Open

HlawkaSchatten.DiagonalCutoff.cutoff90

by savarin · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

hlawka-schattensharp-constant

For a real exponent $p>1$ and a vector $x\in\mathbb C^n$ , the coordinate norm is

N_p(x)=\left(\sum_{i=1}^n|x_i|^p\right)^{1/p}.

For any three vectors in the same space, their triple deficit is

\Delta_3=N_p(x)+N_p(y)+N_p(z)-N_p(x+y+z),

and their pair-deficit sum is

\Delta_2=2\bigl(N_p(x)+N_p(y)+N_p(z)\bigr) -N_p(x+y)-N_p(x+z)-N_p(y+z).

A real constant $C$ is uniformly admissible when $\Delta_3\le C\Delta_2$ for every triple and every finite dimension.

For $t\in[1/2,2]$ , define

A_p(t)=(t^p+2)^{1/p},\qquad B_p(t)=(2|1-t|^p+2^p)^{1/p},

R_p(t)=\frac{3A_p(t)-3^{1/p}|2-t|}{6A_p(t)-3B_p(t)}, \qquad K_p=\sup_{t\in[1/2,2]}R_p(t).

This cyclic constant is exactly the foundation's cyclicConstant. It comes from the three vectors $(-t,1,1),(1,-t,1),(1,1,-t)$ . The fixed compact interval and the absolute value in $B_p$ are part of the definition and remain unchanged in this task. Cyclic definitions

For every real $p\ge90$ , the theorem asks for

K_p=\min\{C\in\mathbb R:\ \forall n\in\mathbb N,\ \forall x,y,z\in\mathbb C^n, \ \Delta_3\le C\Delta_2\}.

This includes admissibility and uniform optimality, with all unequal-norm and zero triples allowed. Dimension zero is included. The supplied analytic proof has this scope; the Lean goal remains open.

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.DiagonalCutoff.cutoff90 :
    ∀ p : ℝ, 90 ≤ p →
      IsLeast {C : ℝ | ∀ n : ℕ,
        HasHlawkaConstant (lpNorm p : (Fin n → ℂ) → ℝ) C}
        (cyclicConstant p) := by sorry

Source

https://gist.github.com/savarin/4621846808053fe597d1a59f1b7acbbd/59d328b191c87c3b4963bb6b9aa491f98f695075#file-proof-md

Read-back

What the Lean code literally says, in plain math · GPT-6

For every real number $p$ satisfying $90\le p$ , define, for each natural number $n$ and each function $u:\{0,\ldots,n-1\}\to\mathbb C$ ,

N_{p,n}(u)=\left(\sum_{i=0}^{n-1}|u_i|^p\right)^{1/p},

where $|u_i|$ is the complex modulus, and define the real number

K_p=\sup\left\{ \frac{3(t^p+2)^{1/p}-3^{1/p}|2-t|} {6(t^p+2)^{1/p}-3\left(2|1-t|^p+2^p\right)^{1/p}} \;\middle|\; t\in\mathbb R,\ \frac12\le t\le2 \right\}.

All powers in these formulas are real powers; both endpoints $t=\frac12$ and $t=2$ are included. For the stipulated range $p\ge90$ , the denominator in this scalar formula is strictly positive throughout the interval, and its set of values is nonempty and bounded, so this is the ordinary real supremum. The declaration asserts that $K_p$ is the least real number $C$ such that, simultaneously for every natural number $n$ and every three functions $x,y,z:\{0,\ldots,n-1\}\to\mathbb C$ , one has

\begin{aligned} &N_{p,n}(x)+N_{p,n}(y)+N_{p,n}(z)-N_{p,n}(x+y+z)\\ &\quad\le C\Bigl[ \bigl(N_{p,n}(x)+N_{p,n}(y)-N_{p,n}(x+y)\bigr) +\bigl(N_{p,n}(x)+N_{p,n}(z)-N_{p,n}(x+z)\bigr) +\bigl(N_{p,n}(y)+N_{p,n}(z)-N_{p,n}(y+z)\bigr) \Bigr], \end{aligned}

with vector addition taken coordinate by coordinate in $\mathbb C$ . Explicitly, this inequality holds with $C=K_p$ for every such $n,x,y,z$ , and every real number $C$ for which it holds for every such $n,x,y,z$ satisfies $K_p\le C$ . The candidate $C$ has no separate sign restriction and must be the same constant for all dimensions and all triples, for the given $p$ . The boundary value $p=90$ is included. The dimension $n=0$ is also included: its coordinate set is empty, each vector is the unique empty function, the empty sum is $0$ , and the positive exponent $1/p$ gives $N_{p,0}=0$ , reducing the inequality to $0\le0$ for every real $C$ . In every dimension the vectors may be zero or have zero coordinates; there are no normalization or nonzero hypotheses.

Human review

Endorsed by marwahaha · Sep 30, 2026
Endorsed by savarin · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph