OAI/Analysis/InterpolatedFactors/Cyclic.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.normal_mem_of_generator_invariant line 14
  2. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.normalHull_le_of_generator_invariant line 42
  3. theorem OAI.FreeGroupFactorMain.WeightedFock.P_range_apply line 58
  4. def OAI.FreeGroupFactorMain.WeightedFock.pRight line 63
  5. theorem OAI.FreeGroupFactorMain.WeightedFock.pRight_apply line 65
  6. theorem OAI.FreeGroupFactorMain.WeightedFock.pRight_projection line 73
  7. theorem OAI.FreeGroupFactorMain.WeightedFock.pRight_root line 88
  8. theorem OAI.FreeGroupFactorMain.WeightedFock.pRight_commute_ambient line 95
  9. theorem OAI.FreeGroupFactorMain.WeightedFock.weighted_normalHull_le_right line 111
  10. theorem OAI.FreeGroupFactorMain.WeightedFock.pRight_pSandwich_basis line 127
  11. theorem OAI.FreeGroupFactorMain.WeightedFock.right_le_weighted_normalHull line 144
  12. theorem OAI.FreeGroupFactorMain.WeightedFock.weighted_normalHull_eq_right line 166
  13. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseConj_square line 174
  14. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseConj_mem_commutant line 179
  15. theorem OAI.FreeGroupFactorMain.WeightedFock.pSandwich_rep_apply line 198
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.pSandwich_star line 207
  17. def OAI.FreeGroupFactorMain.WeightedFock.rightEdge line 214
  18. theorem OAI.FreeGroupFactorMain.WeightedFock.rightEdge_mem line 216
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.P_commute_rightEdge line 219
  20. def OAI.FreeGroupFactorMain.WeightedFock.pRightEdge line 222
  21. theorem OAI.FreeGroupFactorMain.WeightedFock.pRightEdge_apply line 224
  22. theorem OAI.FreeGroupFactorMain.WeightedFock.pRightEdge_star_apply line 227
  23. theorem OAI.FreeGroupFactorMain.WeightedFock.pRightEdge_commute_ambient line 236
  24. theorem OAI.FreeGroupFactorMain.WeightedFock.pRightEdge_left line 249
  25. theorem OAI.FreeGroupFactorMain.WeightedFock.pRightEdge_right line 259
  26. theorem OAI.FreeGroupFactorMain.WeightedFock.pRightEdge_initial line 271
  27. theorem OAI.FreeGroupFactorMain.WeightedFock.starProjection_congr line 283
  28. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedHull_projection line 288
  29. theorem OAI.FreeGroupFactorMain.WeightedFock.pRightEdge_mem_weightedCommutant line 294