OAI/GroupTheory/PolycyclicRecognition/Analysis/AlternatingHaarImage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Haar-volume rate of the actual alternating product

The compact coordinate image furnished by scalar Remez is transported through the actual exponential chart. The output determinant is the weight of the union template, not the sum of the input weights.

  1. theorem OAI.PolycyclicRecognition.alternating_haar_image_growing_sequence line 24