OAI/RepresentationTheory/GraphModels/Regular.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Regular coordinates and finite amplification of graph models.

  1. def OAI.GraphNormality.firstCoordinateMap line 16
  2. theorem OAI.GraphNormality.firstCoordinateMap_injective line 19
  3. theorem OAI.GraphNormality.firstCoordinateMap_surjective line 34
  4. def OAI.GraphNormality.firstCoordinates line 49
  5. theorem OAI.GraphNormality.firstCoordinates_smul line 53
  6. def OAI.GraphNormality.transportLp line 72
  7. theorem OAI.GraphNormality.transportLp_apply line 113
  8. theorem OAI.GraphNormality.transportLp_single line 119
  9. def OAI.GraphNormality.prodRatio line 139
  10. def OAI.GraphNormality.regularPerm line 147
  11. def OAI.GraphNormality.regularAction line 153
  12. theorem OAI.GraphNormality.regularAction_single line 157
  13. def OAI.GraphNormality.firstRegularUnitary line 167
  14. theorem OAI.GraphNormality.firstRegularUnitary_single line 174
  15. theorem OAI.GraphNormality.firstRegularUnitary_intertwines line 180
  16. def OAI.GraphNormality.secondCoordinateMap line 209
  17. theorem OAI.GraphNormality.secondCoordinateMap_injective line 212
  18. theorem OAI.GraphNormality.secondCoordinateMap_surjective line 226
  19. def OAI.GraphNormality.secondCoordinates line 241
  20. theorem OAI.GraphNormality.secondCoordinates_smul line 245
  21. def OAI.GraphNormality.inverseCocycle line 251
  22. def OAI.GraphNormality.secondRegularUnitary line 261
  23. theorem OAI.GraphNormality.secondRegularUnitary_single line 268
  24. theorem OAI.GraphNormality.secondRegularUnitary_intertwines line 274
  25. theorem OAI.GraphNormality.coordinate_actions_commute line 294
  26. def OAI.GraphNormality.bundleBasisVector line 312
  27. theorem OAI.GraphNormality.bundleBasisVector_orthonormal line 316
  28. theorem OAI.GraphNormality.bundleBasisVector_total line 337
  29. def OAI.GraphNormality.regularHilbertBasis line 352
  30. theorem OAI.GraphNormality.regularHilbertBasis_apply line 355
  31. def OAI.GraphNormality.scalarization line 359
  32. theorem OAI.GraphNormality.scalarization_apply line 362
  33. theorem OAI.GraphNormality.regularAction_apply line 374
  34. theorem OAI.GraphNormality.scalarization_intertwines line 385
  35. def OAI.GraphNormality.finiteSumBasisVector line 406
  36. theorem OAI.GraphNormality.finiteSumBasisVector_inner line 409
  37. theorem OAI.GraphNormality.finiteSumBasisVector_orthonormal line 418
  38. theorem OAI.GraphNormality.finiteSumBasisVector_total line 428
  39. def OAI.GraphNormality.finiteSumHilbertBasis line 439
  40. theorem OAI.GraphNormality.finiteSumHilbertBasis_apply line 443
  41. def OAI.GraphNormality.finiteRegrouping line 447
  42. theorem OAI.GraphNormality.finiteRegrouping_apply line 451
  43. def OAI.GraphNormality.amplify line 466
  44. theorem OAI.GraphNormality.amplify_apply line 473
  45. def OAI.GraphNormality.amplification line 476
  46. theorem OAI.GraphNormality.amplification_wot_continuous line 491
  47. def OAI.GraphNormality.scalarRegular line 512
  48. theorem OAI.GraphNormality.scalarRegular_apply line 516
  49. theorem OAI.GraphNormality.finiteRegrouping_intertwines line 521
  50. theorem OAI.GraphNormality.unitaryConjugation_wot_continuous line 540
  51. def OAI.GraphNormality.regularToFinite line 567
  52. theorem OAI.GraphNormality.regularToFinite_intertwines line 571
  53. def OAI.GraphNormality.firstFiniteRegularUnitary line 592
  54. theorem OAI.GraphNormality.firstFiniteRegularUnitary_intertwines line 598
  55. def OAI.GraphNormality.secondFiniteRegularUnitary line 612
  56. theorem OAI.GraphNormality.secondFiniteRegularUnitary_intertwines line 618
  57. def OAI.GraphNormality.firstExtension line 632
  58. def OAI.GraphNormality.secondExtension line 638
  59. theorem OAI.GraphNormality.firstExtension_generator line 644
  60. theorem OAI.GraphNormality.secondExtension_generator line 653
  61. theorem OAI.GraphNormality.firstExtension_wot_continuous line 663
  62. theorem OAI.GraphNormality.secondExtension_wot_continuous line 669