Prove SubpolynomialLp (openai/math family 094: Subpolynomial dimension reduction in $L p$) in Lean 4 with…
Prove SubpolynomialLp (openai/math family 094: Subpolynomial dimension reduction in $L p$) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 094 of the release, Subpolynomial dimension reduction in $L p$ (Convex and metric…
The task
Context: this statement belongs to family 094 of the release, *Subpolynomial dimension reduction in $L_p$* (Convex and metric geometry). The family as a whole: For every fixed $1<p<\infty$ and distortion $D>1$, every $n$-point subset of real $L_p$ embeds into $\ell_p^d$ with distortion at most $D$ and dimension…
Part of raising-heart/openai-math.