OAI/RepresentationTheory/GraphModels/NormalActions.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Commuting normal actions and regular multiplicities.

  1. def OAI.GraphNormality.wotLift line 19
  2. theorem OAI.GraphNormality.closed_generated_commute line 29
  3. theorem OAI.GraphNormality.map_mem_closed_generated line 41
  4. theorem OAI.GraphNormality.isometries_commute_star_right line 49
  5. def OAI.GraphNormality.regularGenerator line 66
  6. def OAI.GraphNormality.twistedGroupAlgebra line 70
  7. theorem OAI.GraphNormality.regularGenerator_mem line 74
  8. def OAI.GraphNormality.coordinateOperator line 93
  9. theorem OAI.GraphNormality.coordinateOperator_centralizer line 97
  10. theorem OAI.GraphNormality.firstExtension_generating_image line 112
  11. theorem OAI.GraphNormality.secondExtension_generating_image line 120
  12. def OAI.GraphNormality.leftNormalAction line 128
  13. def OAI.GraphNormality.rightAdjointNormalAction line 133
  14. theorem OAI.GraphNormality.leftNormalAction_continuous line 138
  15. theorem OAI.GraphNormality.rightAdjointNormalAction_continuous line 141
  16. theorem OAI.GraphNormality.leftNormalAction_generator line 144
  17. theorem OAI.GraphNormality.rightAdjointNormalAction_generator line 149
  18. theorem OAI.GraphNormality.normalActions_commute line 155
  19. lemma OAI.GraphNormality.scalarLp_inner_star_star line 174
  20. lemma OAI.GraphNormality.scalarLp_inner_star_comm line 181
  21. def OAI.GraphNormality.operatorTranspose line 185
  22. lemma OAI.GraphNormality.operatorTranspose_inner line 192
  23. lemma OAI.GraphNormality.operatorTranspose_add line 199
  24. lemma OAI.GraphNormality.operatorTranspose_smul line 205
  25. lemma OAI.GraphNormality.operatorTranspose_mul line 212
  26. lemma OAI.GraphNormality.operatorTranspose_star line 218
  27. lemma OAI.GraphNormality.operatorTranspose_involutive line 226
  28. lemma OAI.GraphNormality.operatorTranspose_one line 235
  29. def OAI.GraphNormality.operatorOppositeEquiv line 241
  30. lemma OAI.GraphNormality.operatorTranspose_wot_continuous line 253
  31. def OAI.GraphNormality.wotTranspose line 269
  32. lemma OAI.GraphNormality.wotTranspose_continuous line 273
  33. lemma OAI.GraphNormality.wotTranspose_add line 276
  34. lemma OAI.GraphNormality.wotTranspose_mul line 280
  35. lemma OAI.GraphNormality.wotTranspose_smul line 284
  36. lemma OAI.GraphNormality.wotTranspose_star line 289
  37. lemma OAI.GraphNormality.wotTranspose_one line 293
  38. lemma OAI.GraphNormality.wotTranspose_involutive line 297
  39. lemma OAI.GraphNormality.wotTranspose_zero line 302
  40. lemma OAI.GraphNormality.wotTranspose_star_regularGenerator line 311
  41. lemma OAI.GraphNormality.wotTranspose_regularGenerator line 327
  42. def OAI.GraphNormality.transposePreimage line 331
  43. lemma OAI.GraphNormality.wotTranspose_mem_twistedGroupAlgebra line 360
  44. def OAI.GraphNormality.opTransposeOnTwisted line 376
  45. lemma OAI.GraphNormality.opTransposeOnTwisted_continuous line 389
  46. def OAI.GraphNormality.rightNormalAction line 410
  47. theorem OAI.GraphNormality.rightNormalAction_continuous line 415
  48. theorem OAI.GraphNormality.rightNormalAction_adjoint_generator line 419
  49. theorem OAI.GraphNormality.left_rightNormalActions_commute line 431
  50. theorem OAI.GraphNormality.induced_graph_normal_actions line 450
  51. def OAI.GraphNormality.standardRightRegular line 488
  52. lemma OAI.GraphNormality.standardRightRegular_apply line 492
  53. def OAI.GraphNormality.oppositeToStandard line 497
  54. lemma OAI.GraphNormality.oppositeToStandard_apply line 501
  55. lemma OAI.GraphNormality.rightStandard_phase line 506
  56. lemma OAI.GraphNormality.oppositeToStandard_intertwines line 518
  57. lemma OAI.GraphNormality.leftNormalAction_finite_regular line 557
  58. lemma OAI.GraphNormality.rightNormalAction_finite_regular line 566
  59. lemma OAI.GraphNormality.graph_regular_multiplicities line 587