OAI/GroupTheory/PolycyclicRecognition/Algebra/RecurrentSourceBundles.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Backward recurrence produces the actual joint source-bundle volume

All bundle schemes and their number are fixed before the successful parameter set is selected. The image is taken before conjugating bundles.

  1. theorem OAI.PolycyclicRecognition.recurrent_source_bundle_haar_image_sequence line 26