OAI/GroupTheory/PolycyclicRecognition/Algebra/RegularHilbertRepresentation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The real regular Hilbert representation

This is the actual square-summable function space on the group, with explicit coordinate formulas for translation and the Dirac vector.

  1. abbrev OAI.PolycyclicRecognition.RegularHilbert line 15
  2. def OAI.PolycyclicRecognition.regularHilbertEvaluation line 17
  3. theorem OAI.PolycyclicRecognition.regularHilbert_sum_apply line 22
  4. theorem OAI.PolycyclicRecognition.regularHilbert_add_apply line 26
  5. theorem OAI.PolycyclicRecognition.regularHilbert_smul_apply line 29
  6. def OAI.PolycyclicRecognition.hilbertReindexVector line 32
  7. theorem OAI.PolycyclicRecognition.hilbertReindexVector_inner line 36
  8. theorem OAI.PolycyclicRecognition.hilbertReindexVector_norm line 42
  9. def OAI.PolycyclicRecognition.hilbertReindex line 49
  10. theorem OAI.PolycyclicRecognition.hilbertReindex_apply line 59
  11. def OAI.PolycyclicRecognition.regularHilbertRepresentation line 64
  12. theorem OAI.PolycyclicRecognition.regularHilbertRepresentation_apply line 69
  13. def OAI.PolycyclicRecognition.regularDirac line 72
  14. theorem OAI.PolycyclicRecognition.regularDirac_apply line 74
  15. theorem OAI.PolycyclicRecognition.regularHilbert_inner_dirac line 78
  16. theorem OAI.PolycyclicRecognition.regularHilbert_apply_le_norm line 87