OAI/GroupTheory/PolycyclicRecognition/Geometry/BoundaryMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Boundary masses determine trace height

This specializes the proved Haar averaging lemma to the exponential volume characters of the ray quotients. The conclusion is the uniformly bounded trace-height error, with the reference value subtracted.

  1. theorem OAI.PolycyclicRecognition.trace_bound_of_boundary_masses line 18