OAI/GroupTheory/PolycyclicRecognition/Algebra/UniformUnitNetBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform multiplicity of the unit-net cover

A finite cover of a compact ball at the identity bounds the number of separated centers at every translate. This proves the multiplicity estimate without needing a Haar-volume comparison.

  1. theorem OAI.PolycyclicRecognition.exists_uniform_unit_net_card line 22