OAI/GroupTheory/PolycyclicRecognition/Analysis/RescaledTupleVolume.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact normalization of correlated tuple volume

The domain is an arbitrary tuple set. Its coordinates need not be independent after the successful parameters have been retained.

  1. def OAI.PolycyclicRecognition.rescaledTupleBases line 20
  2. theorem OAI.PolycyclicRecognition.exponential_rescaled_tuple_subset_measure line 29
  3. theorem OAI.PolycyclicRecognition.rescaled_tuple_volume_lower_sequence line 56
  4. theorem OAI.PolycyclicRecognition.rescaled_tuple_image_volume_lower_sequence line 87