{"id":"palomar/PALOMAR-2026-08-23-000001","url":"https://github.com/geoconuk/lean-misc-math/tree/4a1b0c422b6b4e0fd98b04b31a5c41b33fcea123","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-23-000001-v1.json","repo":"https://github.com/geoconuk/lean-misc-math","tags":["math.MG","cs.IT","msc:52C17","msc:41A46","msc:94B65","covering-numbers","high-dimensional-geometry","information-theory"],"score":0,"title":"geoconuk/lean-misc-math","trust":"high","domain":"math.MG","source":"palomar","authors":["George A. Constantinides"],"reviews":0,"subject":"math.MG","summary":"For a fixed angular radius theta in (0, pi/2), the least number M(n, theta) of spherical caps of angular radius theta, centred at points of the unit sphere of R^n, whose union is that whole sphere satisfies (1/n) log M(n, theta) -> -log sin theta as n -> infinity. This is the covering half of Wyner (1967): the elementary volume bound gives the lower bound on the covering number and a random-covering argument gives the upper bound. The statement is given in Mathlib's own vocabulary, as an asymptotic for Metric.coveringNumber of Metric.sphere 0 1 in EuclideanSpace R (Fin n) at chordal radius 2…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-23","reactions":{},"formalized":true,"formalizes":[{"title":"Random packings and coverings of the unit n-sphere","identifier":"doi:10.1002/j.1538-7305.1967.tb04246.x","relationship":"formalizes"}]}