OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanGoodTemplateComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Template comparison for the diagonal's actual positive good sets

The good sets have subexponential relative Haar mass and affine errors vanishing on every prescribed compact. They need not occupy a fixed positive fraction of the original sampling probability.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.good_affine_templates_support_le line 39