OAI/GroupTheory/PolycyclicRecognition/Algebra/UnitaryLazyEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Energy descent for the lazy symmetric averaging operator

The quantitative descent estimate produces almost harmonic coboundaries from slowly decaying regular-representation energy.

  1. def OAI.PolycyclicRecognition.unitaryCoboundary line 16
  2. theorem OAI.PolycyclicRecognition.unitaryCoboundary_isCocycle line 18
  3. def OAI.PolycyclicRecognition.unitaryGeneratorLaplacian line 23
  4. theorem OAI.PolycyclicRecognition.unitaryGeneratorLaplacian_apply line 26
  5. theorem OAI.PolycyclicRecognition.unitaryCoboundary_sum line 31
  6. theorem OAI.PolycyclicRecognition.unitaryGeneratorLaplacian_selfAdjoint line 36
  7. theorem OAI.PolycyclicRecognition.unitaryCoboundaryEnergy_inner line 59
  8. theorem OAI.PolycyclicRecognition.unitaryCoboundaryEnergy_upper line 70
  9. def OAI.PolycyclicRecognition.unitaryLazyStep line 82
  10. theorem OAI.PolycyclicRecognition.unitaryCoboundaryEnergy_step_exact line 85
  11. theorem OAI.PolycyclicRecognition.unitaryLazyStep_energy_descent line 99