Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Hlawka's inequality in ℓp\ell_pℓp​ for 2≤p≤log⁡3/log⁡(3/2)2\le p\le\log 3/\log(3/2)2≤p≤log3/log(3/2)

Open
HlawkaSchatten.LpThreshold.hlawka_holds_below

by moona3k · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

hlawka-schattenhornich-hlawkalp-spaces

For a real exponent p≥1p\ge1p≥1 and v∈Rnv\in\mathbb R^nv∈Rn write ∥v∥p=(∑i∣vi∣p)1/p\|v\|_p=\big(\sum_i|v_i|^p\big)^{1/p}∥v∥p​=(∑i​∣vi​∣p)1/p (lpNorm p). Hlawka's inequality (also called the Hornich–Hlawka inequality) for ∥⋅∥p\|\cdot\|_p∥⋅∥p​ asserts that for all x,y,z∈Rnx,y,z\in\mathbb R^nx,y,z∈Rn,

∥x+y∥p+∥y+z∥p+∥z+x∥p ≤ ∥x∥p+∥y∥p+∥z∥p+∥x+y+z∥p.\|x+y\|_p+\|y+z\|_p+\|z+x\|_p\ \le\ \|x\|_p+\|y\|_p+\|z\|_p+\|x+y+z\|_p .∥x+y∥p​+∥y+z∥p​+∥z+x∥p​ ≤ ∥x∥p​+∥y∥p​+∥z∥p​+∥x+y+z∥p​.

In the platform's notation this is HasHlawkaConstant (lpNorm p) 1: the triple gap ∥x∥+∥y∥+∥z∥−∥x+y+z∥\|x\|+\|y\|+\|z\|-\|x+y+z\|∥x∥+∥y∥+∥z∥−∥x+y+z∥ is at most the sum of the three pair gaps ∥x∥+∥y∥−∥x+y∥\|x\|+\|y\|-\|x+y\|∥x∥+∥y∥−∥x+y∥. The threshold exponent is

pW=log⁡3log⁡(3/2)≈2.7095,p_W=\frac{\log 3}{\log(3/2)}\approx 2.7095 ,pW​=log(3/2)log3​≈2.7095,

the exponent at which 31/p=3/23^{1/p}=3/231/p=3/2.

Statement (open). For every real ppp with 2≤p≤pW2\le p\le p_W2≤p≤pW​ and every finite dimension nnn, Hlawka's inequality holds in ℓp(n)\ell_p(n)ℓp​(n) over R\mathbb RR.

Together with the failure for p>pWp>p_Wp>pW​, this would make pWp_WpW​ the exact threshold for Hlawka's inequality in ℓp\ell_pℓp​. Marinescu and Niculescu ask in their Problem 1 to prove that ℓp(3)\ell_p(3)ℓp​(3) is not Hornich–Hlawka for any p∈(2,∞]p\in(2,\infty]p∈(2,∞]. This statement asserts the opposite on (2,pW](2,p_W](2,pW​].

Numerical evidence: multi-start maximisation of the ratio of triple gap to pair-gap sum over R3\mathbb R^3R3, with 400 to 1500 starts per exponent, finds a maximum of exactly 111 for 2<p≤2.72<p\le 2.72<p≤2.7 and a strict violation just above pWp_WpW​. By the platform theorem real_bound_of_fin_three, the case n=3n=3n=3 already implies every nnn.

Preamble
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Basic
import Definitions.Def_HlawkaSchatten_GapComparison
import Mathlib

open HlawkaSchatten HlawkaSchatten.DiagonalConstruction
Formal statement
theorem HlawkaSchatten.LpThreshold.hlawka_holds_below :
    ∀ p : ℝ, 2 ≤ p → p ≤ Real.log 3 / Real.log (3 / 2) → ∀ n : ℕ,
      HasHlawkaConstant (lpNorm p : (Fin n → ℝ) → ℝ) 1 := by sorry
Source
D.-Ș. Marinescu and C. P. Niculescu, A survey of the Hornich-Hlawka inequality, arXiv:2407.03278v1 (2024), Section 3, remark following Theorem 2 (the triple x=(-1,1,1), y=(1,-1,1), z=(1,1,-1)) and Problem 1

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me