OAI/GroupTheory/PolycyclicRecognition/Analysis/CocycleHaarAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The defect of a Haar-weighted cocycle average

This is the analytic step of controlled Følner averaging. The weight and its translates are ordinary scalar functions; their difference, rather than an assumed cohomology conclusion, bounds the averaged affine displacement.

  1. theorem OAI.PolycyclicRecognition.IsUnitaryCocycle.haar_weighted_average line 25
  2. theorem OAI.PolycyclicRecognition.IsUnitaryCocycle.norm_haar_weighted_average_le line 47