Euclidean signed and reordered prefix bounds

Possible paper match, with no recorded review

Let $1\le p\le\infty$, with $1/\infty=0$, and let $d,N\ge1$ be integers.
Every sequence $v_1,\ldots,v_N\in\R^d$ with $\lVert v_i\rVert_p\le1$
admits signs $\varepsilon_i\in\{-1,1\}$ such that
\[
 \max_{0\le k\le N}
 \left\lVert\sum_{i=1}^k\varepsilon_i v_i\right\rVert_p
 \le C d^{\max\{1/p,\,1-1/p\}}.
\]
If additionally $\sum_{i=1}^N v_i=0$, there is a permutation
$\pi\in\mathfrak S_N$ such that
\[
 \max_{0\le k\le N}
 \left\lVert\sum_{i=1}^k v_{\pi(i)}\right\rVert_p
 \le C d^{\max\{1/p,\,1-1/p\}}.
\]
Here $C$ is the same absolute constant as in
Theorems~\ref{thm:signing} and~\ref{thm:steinitz}, independent of $p,d,N$.
For $1\le p\le2$, both bounds have sharp dimension order $d^{1/p}$:
for every $d$ there is a unit-ball sequence for which every signing has
a prefix of norm at least $d^{1/p}$, and a finite indexed zero-sum
unit-ball family for which every permutation has a prefix of norm at
least $\tfrac13d^{1/p}$.

Other possible paper matches, closest wording first

• Theorem 1.1 of The Euclidean Steinitz–Bergström theorem. Words of the Lean statement, its names split into words, that also appear in the theorem: order, prefixes, sqrt, signs and integers. Found in the paper’s title, which its main theorem states: euclidean. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: prescribed.
• Corollary 6.2 of The Euclidean Steinitz–Bergström theorem. Words of the Lean statement, its names split into words, that also appear in the theorem: euclidean, pi, prefixes, sqrt, bound, integers and one more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: chosen and permutations.
• Proposition 2.2 of The Euclidean Steinitz–Bergström theorem. Words of the Lean statement, its names split into words, that also appear in the theorem: real, sqrt, bounded and integers.
• Theorem 1.2 of The Euclidean Steinitz–Bergström theorem. Words of the Lean statement, its names split into words, that also appear in the theorem: pi, euclidean, sqrt, bound, integers and signing. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: family and permutation.
• Proposition 2.1 of The Euclidean Steinitz–Bergström theorem. Words of the Lean statement, its names split into words, that also appear in the theorem: signs and bounded.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.