Waist
Formalization of waist inequalities for different settings: (1) Gromov's waist theorem for the round sphere S^n (the original proof in Memarian arXiv:0911.3972 has gaps; here a spherical adaptation of Klartag's proof is used); (2) An explicit positive lower bound on the unnormalized (n-k)-dimensional Hausdorff measure (Mathlib's muH[n-k], defined via sum of (diam U_i)^{n-k} without the unit-ball normalization factor omega_{n-k} / 2^{n-k}, in the chordal metric on S^n) of a fiber on the round sphere S^n: muH[n-k](f^{-1}(y)) >= 1 / (12 * 4^n * 3^k), yielding the positive lower bound…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-16-000023
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-16-000023/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-16-000023/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'