OAI/Analysis/InterpolatedFactors/Rerouting.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.CornerRerouting.Supported line 14
  2. def OAI.FreeGroupFactorMain.CornerRerouting.lift line 15
  3. theorem OAI.FreeGroupFactorMain.CornerRerouting.right_zero line 18
  4. theorem OAI.FreeGroupFactorMain.CornerRerouting.star_left_zero line 22
  5. theorem OAI.FreeGroupFactorMain.CornerRerouting.supported_star line 26
  6. theorem OAI.FreeGroupFactorMain.CornerRerouting.supported_mul_star_zero line 32
  7. theorem OAI.FreeGroupFactorMain.CornerRerouting.mul_supported_zero line 40
  8. theorem OAI.FreeGroupFactorMain.CornerRerouting.lift_mul_supported line 46
  9. theorem OAI.FreeGroupFactorMain.CornerRerouting.supported_mul_lift line 51
  10. theorem OAI.FreeGroupFactorMain.CornerRerouting.lift_commute_supported line 57
  11. theorem OAI.FreeGroupFactorMain.CornerRerouting.square_zero line 64
  12. theorem OAI.FreeGroupFactorMain.CornerRerouting.range_mul line 70
  13. theorem OAI.FreeGroupFactorMain.CornerRerouting.lift_commute_edge line 73
  14. theorem OAI.FreeGroupFactorMain.CornerRerouting.star_lift line 86
  15. theorem OAI.FreeGroupFactorMain.CornerRerouting.lift_commute_edge_star line 89
  16. def OAI.FreeGroupFactorMain.CornerRerouting.diagonal line 98
  17. def OAI.FreeGroupFactorMain.CornerRerouting.offDiagonal line 99
  18. def OAI.FreeGroupFactorMain.CornerRerouting.remaining line 100
  19. theorem OAI.FreeGroupFactorMain.CornerRerouting.diagonal_supported line 103
  20. theorem OAI.FreeGroupFactorMain.CornerRerouting.offDiagonal_supported line 108
  21. theorem OAI.FreeGroupFactorMain.CornerRerouting.remaining_supported line 116
  22. theorem OAI.FreeGroupFactorMain.CornerRerouting.reconstruct line 124
  23. theorem OAI.FreeGroupFactorMain.CornerRerouting.lift_commute_generator line 144
  24. theorem OAI.FreeGroupFactorMain.CornerRerouting.corner_bicommutant line 167
  25. theorem OAI.FreeGroupFactorMain.CornerRerouting.single_edge_corner_abelian line 195
  26. def OAI.FreeGroupFactorMain.WeightedFock.edgeAlgebra line 277
  27. theorem OAI.FreeGroupFactorMain.WeightedFock.edge_left_modulus_selfAdjoint line 282
  28. theorem OAI.FreeGroupFactorMain.WeightedFock.edge_corner_commutative line 290
  29. def OAI.FreeGroupFactorMain.WeightedFock.rightInsertEmbedding line 305
  30. def OAI.FreeGroupFactorMain.WeightedFock.rightInsert line 312
  31. theorem OAI.FreeGroupFactorMain.WeightedFock.rightInsert_single line 315
  32. theorem OAI.FreeGroupFactorMain.WeightedFock.P_commute_rightInsert line 320
  33. theorem OAI.FreeGroupFactorMain.WeightedFock.creation_commute_rightInsert line 328
  34. def OAI.FreeGroupFactorMain.WeightedFock.vacuumTo line 335
  35. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuumTo_nil line 338
  36. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuumTo_cons line 349
  37. theorem OAI.FreeGroupFactorMain.WeightedFock.annihilation_rightInsert line 354
  38. theorem OAI.FreeGroupFactorMain.WeightedFock.S_commute_rightInsert line 379
  39. def OAI.FreeGroupFactorMain.WeightedFock.oldPaths line 389
  40. def OAI.FreeGroupFactorMain.WeightedFock.oldProjection line 390
  41. def OAI.FreeGroupFactorMain.WeightedFock.oldAlgebra line 391
  42. theorem OAI.FreeGroupFactorMain.WeightedFock.oldProjection_commute_creation line 395
  43. theorem OAI.FreeGroupFactorMain.WeightedFock.oldProjection_commute_S line 402
  44. theorem OAI.FreeGroupFactorMain.WeightedFock.oldProjection_mem_commutant line 412
  45. theorem OAI.FreeGroupFactorMain.WeightedFock.rightInsert_mem_oldCommutant line 423
  46. theorem OAI.FreeGroupFactorMain.WeightedFock.annihilation_oldProjection line 436
  47. theorem OAI.FreeGroupFactorMain.WeightedFock.old_root_fixed line 452
  48. theorem OAI.FreeGroupFactorMain.WeightedFock.annihilation_old_root line 462
  49. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuumTo_apply line 469
  50. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_creation_contraction line 473
  51. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuumTrace_root_expansion line 492
  52. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_C_contraction line 503
  53. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_block_covariance line 518
  54. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_C_annihilates_old_vacuum line 535
  55. def OAI.FreeGroupFactorMain.WeightedFock.terminalVertex line 548
  56. def OAI.FreeGroupFactorMain.WeightedFock.edgeCreation line 549
  57. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_eq_proj line 551
  58. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_star line 558
  59. theorem OAI.FreeGroupFactorMain.WeightedFock.terminalVertex_star line 561
  60. theorem OAI.FreeGroupFactorMain.WeightedFock.terminalVertex_single line 563
  61. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeCreation_single line 568
  62. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeAnnihilation_nil line 574
  63. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeAnnihilation_cons line 578
  64. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_commute_rightInsert line 585
  65. theorem OAI.FreeGroupFactorMain.WeightedFock.terminalVertex_commute_creation line 594
  66. theorem OAI.FreeGroupFactorMain.WeightedFock.terminalVertex_commute_edgeCreation line 600
  67. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeCreation_commute_rightInsert line 605
  68. def OAI.FreeGroupFactorMain.WeightedFock.diagonalInsert line 609
  69. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_commute_diagonalInsert line 612
  70. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeCreation_commute_diagonalInsert line 617
  71. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuumTo_terminal line 622
  72. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_vacuumTo line 635
  73. theorem OAI.FreeGroupFactorMain.WeightedFock.crossAnnihilation_commute_diagonalInsert line 642
  74. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_true line 685
  75. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_false line 687
  76. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_edges line 689
  77. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_commute_diagonalInsert line 695
  78. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonalStar_commute_diagonalInsert line 701
  79. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalInsert_mem_edgeCommutant line 708
  80. def OAI.FreeGroupFactorMain.WeightedFock.alternatingList line 724
  81. def OAI.FreeGroupFactorMain.WeightedFock.alternatingProjection line 727
  82. theorem OAI.FreeGroupFactorMain.WeightedFock.alternatingProjection_pos line 730
  83. theorem OAI.FreeGroupFactorMain.WeightedFock.alternatingProjection_neg line 739
  84. theorem OAI.FreeGroupFactorMain.WeightedFock.alternating_commute_edgeCreation line 748
  85. theorem OAI.FreeGroupFactorMain.WeightedFock.alternating_commute_edgeAnnihilation line 769
  86. theorem OAI.FreeGroupFactorMain.WeightedFock.alternating_mem_edgeCommutant line 774
  87. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonal_annihilation_alternating line 794
  88. theorem OAI.FreeGroupFactorMain.WeightedFock.alternating_edge_root line 813
  89. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonal_annihilation_edge_root line 822
  90. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeAnnihilation_diagonalInsert_formula line 833
  91. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalAnnihilation_diagonalInsert line 859
  92. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalInsert_nil line 872
  93. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonal_edge_contraction line 878