OAI/Analysis/RotationWeights/Regular.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ContinuousCircleWeight.lpPermute line 12
  2. theorem OAI.ContinuousCircleWeight.lpPermute_apply line 29
  3. theorem OAI.ContinuousCircleWeight.lpPermute_one line 32
  4. theorem OAI.ContinuousCircleWeight.lpPermute_mul line 36
  5. def OAI.ContinuousCircleWeight.lpPermuteHom line 41
  6. def OAI.ContinuousCircleWeight.lpPhase line 47
  7. theorem OAI.ContinuousCircleWeight.lpPhase_apply line 67
  8. def OAI.ContinuousCircleWeight.rotationScalar line 70
  9. abbrev OAI.ContinuousCircleWeight.RegularHilbert line 83
  10. abbrev OAI.ContinuousCircleWeight.RegularOperator line 84
  11. def OAI.ContinuousCircleWeight.regularShift line 86
  12. theorem OAI.ContinuousCircleWeight.regularShift_apply line 89
  13. def OAI.ContinuousCircleWeight.regularMagnetic line 95
  14. theorem OAI.ContinuousCircleWeight.regularMagnetic_apply line 98
  15. theorem OAI.ContinuousCircleWeight.regularShift_zero line 104
  16. theorem OAI.ContinuousCircleWeight.regularShift_add line 108
  17. theorem OAI.ContinuousCircleWeight.regularMagnetic_zero line 116
  18. theorem OAI.ContinuousCircleWeight.regularMagnetic_add line 120
  19. def OAI.ContinuousCircleWeight.regularShiftHom line 127
  20. def OAI.ContinuousCircleWeight.regularMagneticHom line 132
  21. theorem OAI.ContinuousCircleWeight.regularShift_zpow line 138
  22. theorem OAI.ContinuousCircleWeight.regularMagnetic_zpow line 144
  23. def OAI.ContinuousCircleWeight.regularU line 151
  24. def OAI.ContinuousCircleWeight.regularV line 154
  25. theorem OAI.ContinuousCircleWeight.regularU_zpow_apply line 157
  26. theorem OAI.ContinuousCircleWeight.regularV_zpow_apply line 162
  27. theorem OAI.ContinuousCircleWeight.regularU_apply line 169
  28. theorem OAI.ContinuousCircleWeight.regularV_apply line 173
  29. theorem OAI.ContinuousCircleWeight.regular_relation line 178
  30. def OAI.ContinuousCircleWeight.regularVacuum line 191
  31. theorem OAI.ContinuousCircleWeight.regular_monomial line 193
  32. theorem OAI.ContinuousCircleWeight.regular_moments line 208
  33. theorem OAI.ContinuousCircleWeight.regular_cyclic line 215