OAI/GroupTheory/PolycyclicRecognition/Analysis/HarmonicCoverEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Energy control for the kernel of the ball-averaging map

  1. theorem OAI.PolycyclicRecognition.sum_translatedWordBall line 12
  2. theorem OAI.PolycyclicRecognition.energy_translatedWordBall line 16
  3. theorem OAI.PolycyclicRecognition.translatedWordBall_zero_average_poincare line 21
  4. theorem OAI.PolycyclicRecognition.wordBall_sum_le_cover line 32
  5. theorem OAI.PolycyclicRecognition.wordBall_zero_averages_energy line 58
  6. def OAI.PolycyclicRecognition.harmonicCoverFactor line 86
  7. theorem OAI.PolycyclicRecognition.harmonicCoverFactor_nonneg line 91
  8. theorem OAI.PolycyclicRecognition.harmonic_wordBall_zero_averages line 96