{"id":"palomar/PALOMAR-2026-10-16-000023","url":"https://github.com/akopjan/Waist-inequalities-lean-formalizatoin/tree/e7823b4b1252ecf3cc9f9342529bad01cb3080fa","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000023-v1.json","repo":"https://github.com/akopjan/Waist-inequalities-lean-formalizatoin","tags":["math.MG","math.DG","msc:53C23","msc:52A20","msc:28A75","msc:60D05","geometric-measure","waist-inequality","lean-formalization","sphere"],"score":0,"title":"Waist","trust":"high","domain":"math.MG","source":"palomar","authors":["Arseniy Akopyan"],"reviews":0,"subject":"math.MG","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"Isoperimetry of waists and subtleties in spaces","identifier":"GAFA, Geom. Funct. Anal. 13 (2003), no. 1, 178–215","relationship":"formalizes"},{"title":"On Gromov's waist of the sphere theorem","identifier":"arXiv:0911.3972 [math.MG]","relationship":"formalizes"},{"title":"Convex geometry and waist inequalities","identifier":"arXiv:1608.04121 [math.MG]","relationship":"formalizes"},{"title":"A tight estimate for the waist of the ball","identifier":"arXiv:1608.06279 [math.MG]","relationship":"formalizes"},{"title":"Waist of balls in hyperbolic and spherical spaces","identifier":"arXiv:1702.07513 [math.MG]","relationship":"formalizes"}]}