OAI/GroupTheory/PolycyclicRecognition/Analysis/InjectivePatchVolume.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Volume lower bounds from a controlled finite injective cover

This is the change-of-variables step for measurable polynomial parameters. The parameter set itself need not contain an open set. When it is compact, the image used below is a compact witness for inner volume.

  1. theorem OAI.PolycyclicRecognition.volume_image_lower_of_finite_injective_cover line 20