AI 中文总结
该研究分析了高维随机格薄壳中点的球面统计，发现了多个相变阈值，并证明单个格在概率趋于一的情况下满足多种统计估计，且通过Lean形式化验证了主要结论。
AI 中文摘要
我们研究了高维随机格薄壳中所有点的球面统计。格点之间的精确关系使得仅基于球面几何的预测何时成立变得不明确。我们针对若干统计量回答了这一问题，包括壳点数、其方向的平衡性，以及它们之间差值的出现、重复和分布。我们确定了随着壳半径增长出现的尖锐阈值，并表明这些统计量经历了多个不同的相变。一个壳可能已经与一种几何预测一致，同时仍与另一种预测强烈偏离。我们的结果对单个采样格成立，且随着维度增长概率趋于一。结果包括对整个壳成立的估计、接近转变阈值的界限，以及扩展到随机平移格的情形。一个Lean形式化验证了主要结果，假设代码中陈述的经典公式和概率模型。
英文摘要
We study the spherical statistics of all the points in a thin shell of a high-dimensional random lattice. The exact relations between lattice points make it unclear when predictions based only on spherical geometry should hold. We answer this question for several statistics, including the number of shell points, the balance of their directions, and the occurrence, repetition, and distribution of differences between them. We identify sharp thresholds as the shell radius grows and show that these statistics undergo several distinct phase transitions. A shell can already agree with one geometric prediction while still differing strongly from another. Our results hold for a single sampled lattice, with probability tending to one as the dimension grows. They include estimates that hold across a complete shell, bounds close to the transition thresholds, and extensions to randomly shifted lattices. A Lean formalization verifies the main results, assuming the classical formulas and probability model stated in the code.
Comments63 pages, with a complete Lean formalization attached
