The real coordinate Hlawka bound for p ≥ 90

For every real number $p$ satisfying $90\le p$ (including $p=90$), every natural number $n\ge0$, and every three real coordinate vectors $x,y,z\in\mathbb{R}^{I_n}$, where $I_n=\{i\in\mathbb{N}:i<n\}$, define $N_p(w)=\left(\sum_{i\in I_n}|w_i|^p\right)^{1/p}$ for each $w\in\mathbb{R}^{I_n}$. Define a set of real numbers and a real constant depending only on $p$ by

The declaration asserts

Here all vector additions are coordinatewise and the norm of an individual real coordinate is its ordinary absolute value. The powers are real powers: on a positive base $a$ they have the value $a^r=\exp(r\log a)$, and $0^r=0$ for the positive exponents occurring here. All bases in the displayed formulas are nonnegative, and $p\ge90$ ensures both $p>0$ and $1/p>0$. The interval defining $S_p$ includes both endpoints and is nonempty. In the definition of $C_p$, the real supremum is the least upper bound when its argument set is nonempty and bounded above, and is defined to be $0$ otherwise; in particular, the definition would give $C_p=0$ if $S_p$ were unbounded above. The scalar quotient uses total real division, so a zero denominator would give the value $0$; denominator nonvanishing and attainment of the supremum are not additional hypotheses of this declaration. The vectors are arbitrary, including zero vectors, repeated vectors, and triples for which the sum of the three bracketed quantities is zero; in that last case the asserted inequality has right-hand side zero. No positive lower bound on $n$ is imposed: when $n=0$, there is a unique empty coordinate vector, every defining sum for $N_p$ is empty and equals zero, every value of $N_p$ is zero, and the inequality reads $0\le0$. The condition $p\ge90$ is the only hypothesis beyond membership in the stated domains; $p$ need not be an integer, and the declaration imposes no conclusion for $p<90$.