Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Marinescu–Niculescu Problem 1 (real exponents): no ℓp(3)\ell_p(3)ℓp​(3) with p>2p>2p>2 is Hornich–Hlawka

Open
HornichHlawka.MarinescuNiculescu.problem1_real

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 (as posed). Problem 1 of Marinescu–Niculescu asks to prove that none of the spaces ℓp(3)\ell_p(3)ℓp​(3) with p∈(2,∞]p\in(2,\infty]p∈(2,∞] is Hornich–Hlawka. This entry formalises the finite real exponents p∈(2,∞)p\in(2,\infty)p∈(2,∞): for every real p>2p>2p>2, Hlawka's inequality fails in ℓp(3)\ell_p(3)ℓp​(3). The case p=∞p=\inftyp=∞ is already settled by the triple above.

The survey establishes the range p>pWp>p_Wp>pW​. The range 2<p≤pW2<p\le p_W2<p≤pW​ is what the problem leaves open. A disproof needs a single exponent in (2,pW](2,p_W](2,pW​] at which ℓp(3)\ell_p(3)ℓp​(3) is Hornich–Hlawka, for example via hlawka_holds_five_halves.

Preamble
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Basic
import Definitions.Def_HlawkaSchatten_GapComparison
import Mathlib

open HlawkaSchatten HlawkaSchatten.DiagonalConstruction
Formal statement
theorem HornichHlawka.MarinescuNiculescu.problem1_real :
    ∀ p : ℝ, 2 < p → ¬ HasHlawkaConstant (lpNorm p : (Fin 3 → ℝ) → ℝ) 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