OAI/GroupTheory/PolycyclicRecognition/Analysis/SourceBundleHaarImage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Joint source-bundle Haar volume before conjugation

The polynomial image is taken in the product of all bundle coordinates. Thus a correlated restriction of the common parameter set is retained.

  1. def OAI.PolycyclicRecognition.sourceBundleProduct line 25
  2. theorem OAI.PolycyclicRecognition.source_bundle_haar_image_sequence line 35