OAI/Analysis/InterpolatedFactors/Ambient.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.WeightedFock.vertexOld line 15
  2. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_mul_vertex line 18
  3. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_commute_empty line 23
  4. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_empty_vertex line 36
  5. def OAI.FreeGroupFactorMain.WeightedFock.ambientRect line 41
  6. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientRect_covariance line 43
  7. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientRect_annihilate line 65
  8. def OAI.FreeGroupFactorMain.WeightedFock.diagonalCreate line 74
  9. def OAI.FreeGroupFactorMain.WeightedFock.diagonalCovariance line 76
  10. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalCreate_covariance line 80
  11. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalCreate_annihilate line 87
  12. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientRect_diagonal_orthogonal line 91
  13. def OAI.FreeGroupFactorMain.WeightedFock.diagonalBase line 96
  14. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonal_base_annihilate line 100
  15. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonal_vertex_annihilate line 108
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonal_residual_covariance line 114
  17. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_projection line 137
  18. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientRect_left line 141
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientRect_right line 145
  20. def OAI.FreeGroupFactorMain.WeightedFock.diagonalLeg line 149
  21. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalLeg_selfAdjoint line 152
  22. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalLeg_left line 155
  23. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalLeg_right line 161
  24. theorem OAI.FreeGroupFactorMain.WeightedFock.vertexRoot_inner line 166
  25. theorem OAI.FreeGroupFactorMain.WeightedFock.vertexRoot_ne_zero line 173
  26. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalLeg_eigen_root_zero line 185
  27. def OAI.FreeGroupFactorMain.WeightedFock.diagonalSelf line 198
  28. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalSelf_eq line 200
  29. def OAI.FreeGroupFactorMain.WeightedFock.diagonalShift line 205
  30. def OAI.FreeGroupFactorMain.WeightedFock.diagonalGenerator line 207
  31. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalSelf_selfAdjoint line 209
  32. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalGenerator_selfAdjoint line 213
  33. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalGenerator_eigen_root_zero line 218
  34. theorem OAI.FreeGroupFactorMain.WeightedFock.P_mem_diagonalBase line 228
  35. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalSelf_mem line 231
  36. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalGenerator_mem line 235
  37. theorem OAI.FreeGroupFactorMain.WeightedFock.P_commute_diagonalSelf line 238
  38. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalBase_eq_generated line 247
  39. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalBase_vertex_commute line 274
  40. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonal_residual_trace line 289
  41. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonal_residual_orthogonal line 300
  42. theorem OAI.FreeGroupFactorMain.WeightedFock.rect_paired_eq line 311
  43. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_mem_old line 316
  44. theorem OAI.FreeGroupFactorMain.WeightedFock.oldAlgebra_mono line 321
  45. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalBase_le_singleton line 326
  46. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalBase_le_ambient line 334
  47. theorem OAI.FreeGroupFactorMain.WeightedFock.ambient_C_rect_empty line 340
  48. theorem OAI.FreeGroupFactorMain.WeightedFock.ambient_C_diagonal_empty line 349
  49. theorem OAI.FreeGroupFactorMain.WeightedFock.ambient_C_residual line 353
  50. def OAI.FreeGroupFactorMain.WeightedFock.residualIndex line 364
  51. def OAI.FreeGroupFactorMain.WeightedFock.residualSlot line 365
  52. theorem OAI.FreeGroupFactorMain.WeightedFock.residualSlot_some line 369
  53. theorem OAI.FreeGroupFactorMain.WeightedFock.residualSlot_flip line 375
  54. def OAI.FreeGroupFactorMain.WeightedFock.diagonalVertex line 382
  55. def OAI.FreeGroupFactorMain.WeightedFock.ambientLeft line 385
  56. def OAI.FreeGroupFactorMain.WeightedFock.ambientRight line 387
  57. def OAI.FreeGroupFactorMain.WeightedFock.ambientExtra line 389
  58. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalVertex_projection line 392
  59. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientLeft_projection line 397
  60. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientRight_projection line 403
  61. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientLeft_flip line 409
  62. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientRight_flip line 414
  63. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientExtra_supported line 421
  64. def OAI.FreeGroupFactorMain.WeightedFock.diagonalTrace line 431
  65. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalTrace_tracial line 436
  66. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientExtra_covariance line 440
  67. def OAI.FreeGroupFactorMain.WeightedFock.ambientRaw line 463
  68. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientRaw_covariance line 465
  69. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientRaw_extra line 475
  70. def OAI.FreeGroupFactorMain.WeightedFock.ambientAbsorption line 482