The real coordinate Hlawka bound for p ≥ 89

Proved

HlawkaSchatten.DiagonalCutoff.real_bound89

by savarin · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

hlawka-schattensharp-constant

For a real exponent $p>1$ and a vector $x\in\mathbb R^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

The theorem asks for

\forall p\ge89,\ \forall n\in\mathbb N,\ \forall x,y,z\in\mathbb R^n, \qquad \Delta_3\le K_p\Delta_2.

There is no equal-norm, normalization or nonzero restriction. The finite dimension may be zero. This is the real admissibility statement, without a leastness assertion. The accepted real bound covers every $p\ge90$ .

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.real_bound89 :
    ∀ p : ℝ, 89 ≤ p → ∀ n : ℕ,
      HasHlawkaConstant (lpNorm p : (Fin n → ℝ) → ℝ)
        (cyclicConstant p) := by sorry

Source

https://prove2.me/campaigns/sharp-diagonal-hlawka-constant

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

For every real $p \ge 89$ , every natural number $n$ (including $n = 0$ ), and all $x, y, z \in \mathbb{R}^n$ (real $n$ -tuples, added coordinatewise, with no further restriction), the statement asserts

\|x\|_p + \|y\|_p + \|z\|_p - \|x+y+z\|_p \;\le\; C_p\Big[\big(\|x\|_p + \|y\|_p - \|x+y\|_p\big) + \big(\|x\|_p + \|z\|_p - \|x+z\|_p\big) + \big(\|y\|_p + \|z\|_p - \|y+z\|_p\big)\Big].

The norm is the usual $\ell_p$ norm on $\mathbb{R}^n$ with a real exponent:

\|v\|_p = \Big(\sum_{i=1}^{n} |v_i|^p\Big)^{1/p}.

The left side is the triangle-inequality deficit of the triple. The bracket is the sum of the three pairwise deficits. If $C_p$ were replaced by $1$ , the inequality would be equivalent to Hlawka's inequality $\|x+y\|_p + \|x+z\|_p + \|y+z\|_p \le \|x\|_p + \|y\|_p + \|z\|_p + \|x+y+z\|_p$ .

The constant $C_p$ depends on $p$ alone:

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

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

Fine print.

Order of quantifiers. $C_p$ is fixed before $n$ is chosen. The same constant must therefore work in every dimension $n$ and for every triple $x, y, z$ .
Which $p$ . $p$ ranges over all real numbers $\ge 89$ , including non-integers; $p = \infty$ is not included. Such $p$ exist, so the statement is not vacuous.
The case $n = 0$ . It is included and trivial: the empty sum makes every norm $0$ , and the inequality reads $0 \le 0$ .
No division by zero. Under the formal convention, $a/0 = 0$ , but that never applies here. For $t \in [1/2, 2]$ we have $|1-t| \le 1$ , so $(2A_p)^p - B_p^p = 2^p t^p + 2^p - 2|1-t|^p > 0$ . Hence the denominator $3(2A_p - B_p)$ is strictly positive.
The supremum is a real maximum. $R_p$ is continuous on the compact interval $[1/2, 2]$ , so its set of values is nonempty and bounded. The formal default of $0$ for a set with no supremum does not arise.
Size of $C_p$ . Two exact values:
- $R_p(2) = 1$ ;
- $R_p(1) = \dfrac{3^{1/p}}{3(3^{1/p}-1)}$ , which is about $27.17$ at $p = 89$ .
So $C_p \ge R_p(1) > 1$ , and $C_p \to \infty$ as $p \to \infty$ . My own numerical check, which is not part of the statement, gives $C_{89} \approx 41.49$ , reached near $t \approx 0.947$ .
What is not claimed. The statement only says that $C_p$ suffices. It does not say $C_p$ is the smallest constant that works, and it says nothing about $p < 89$ .

Human review

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

View graph