The real coordinate Hlawka bound for p ≥ 80

Proved

HlawkaSchatten.DiagonalCutoff.real_bound80

by savarin · Oct 6, 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\ge80,\ \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\ge85$ .

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_bound80 :
    ∀ p : ℝ, 80 ≤ 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 number $p$ with $p \ge 80$ (any real, not only integers, with no upper bound), every natural number $n$ (including $n = 0$ ), and all vectors $x, y, z \in \mathbb{R}^n$ , the following non-strict inequality holds. Here $\mathbb{R}^n$ means real-valued functions on $\{0, 1, \dots, n-1\}$ with coordinatewise addition. There are no further conditions on $x, y, z$ : they may be zero, equal or parallel.

\|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].

In words, the triangle-inequality deficit of the triple is at most $C_p$ times the sum of the three pairwise deficits. The bracket equals $2(\|x\|_p + \|y\|_p + \|z\|_p) - \|x+y\|_p - \|x+z\|_p - \|y+z\|_p$ . The constant $C_p$ depends only on $p$ , so one constant covers every dimension $n$ and every triple.

The size functional. For $v \in \mathbb{R}^n$ ,

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

This is an explicitly defined power sum. For $p \ge 80$ it is the usual $\ell^p$ norm on $\mathbb{R}^n$ .

The constant. For $t \in [\tfrac12, 2]$ let

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

R_p(t) = \frac{3A_p(t) - 3^{1/p}\,|2-t|}{6A_p(t) - 3B_p(t)}, \qquad C_p = \sup\big\{ R_p(t) : \tfrac12 \le t \le 2 \big\}.

The supremum is taken over the closed interval, with both endpoints included.

Edge cases.

The only hypothesis is $p \ge 80$ . It can be satisfied, so the statement is not vacuous.
For $n = 0$ , $\mathbb{R}^0$ has a single element. Its norm is $(\text{empty sum})^{1/p} = 0$ , so the inequality reads $0 \le 0$ .
Every power has a nonnegative base and a positive exponent ( $p$ or $1/p$ ). So all of them are ordinary real powers, with $0^p = 0^{1/p} = 0$ .
Two formal conventions never come into play: "division by zero gives $0$ " and "the supremum of an empty set, or of a set with no upper bound, is $0$ ". For $t \in [\tfrac12, 2]$ we have $(2A_p(t))^p = (2t)^p + 2^{p+1} \ge 1 + 2^{p+1} > 2 + 2^p \ge B_p(t)^p$ . So the denominator $3\big(2A_p(t) - B_p(t)\big)$ is strictly positive and $R_p$ is continuous on the interval. Therefore $C_p$ is the maximum of $R_p$ , attained on the interval.
At $t = 2$ we have $A_p(2) = B_p(2)$ and $|2-t| = 0$ , so $R_p(2) = 1$ . Hence $C_p \ge 1$ .

Human review

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

View graph