Central Limit Theorem for Random Partial Sphere Coverings in High Dimensions

Steven Hoehner, Christoph Thäle

math.PR Apr 9, 2026 · v1 math.MG

Read PDF arXiv abstract

TL;DR

The proof of the main CLT theorem was formally verified in Lean 4 with the Aristotle framework; the Lean files are available on the authors' websites.

Abstract

We study a random partial covering model on the $(d-1)$-dimensional unit sphere, where $N$ spherical caps are placed independently and uniformly at random, each covering a surface fraction of $1/N$. This model provides a continuous geometric analogue of the classical balls-into-bins problem. We establish a Central Limit Theorem for the volume of the resulting random partial covering, showing that its fluctuations are asymptotically Gaussian. Moreover, we obtain a quantitative bound on the rate of convergence in the Kolmogorov distance. Our results hold both in fixed dimension and in a high-dimensional regime where the dimension grows at most logarithmically with $N$.

Problem

The model places N random spherical caps, each covering a 1/N surface fraction of the (d-1)-sphere. It is a continuous analogue of the balls-into-bins problem. The question is whether the covered volume has asymptotically Gaussian fluctuations, including when the dimension grows with N.

Approach

The authors apply a Berry–Esseen bound for symmetric functions of i.i.d. variables, controlled by first- and second-order replacement differences. They bound these differences using the cap measure and a locality lemma based on cap intersections. They combine this with a known lower bound on the variance. The proof of the main theorem was formally verified in Lean 4 using the Aristotle framework.

Results

A Central Limit Theorem holds for the covered volume, with a Kolmogorov-distance rate of C_d/√N in fixed dimension. A polynomial rate holds when the dimension grows at most logarithmically in N.

Papers With

Central Limit Theorem for Random Partial Sphere Coverings in High Dimensions