OAI/Analysis/JiangSu/Traceless/TracelessSpatialCorner.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentMain.Spatial.SpatialHilbert line 19
  2. def OAI.CurrentMain.Spatial.spatialTensorOp line 23
  3. lemma OAI.CurrentMain.Spatial.spatialTensorOp_coe line 27
  4. lemma OAI.CurrentMain.Spatial.spatialTensorOp_ext line 31
  5. lemma OAI.CurrentMain.Spatial.spatialTensorOp_zero_left line 42
  6. lemma OAI.CurrentMain.Spatial.spatialTensorOp_zero_right line 44
  7. lemma OAI.CurrentMain.Spatial.spatialTensorOp_add_left line 46
  8. lemma OAI.CurrentMain.Spatial.spatialTensorOp_add_right line 49
  9. lemma OAI.CurrentMain.Spatial.spatialTensorOp_smul_left line 52
  10. lemma OAI.CurrentMain.Spatial.spatialTensorOp_smul_right line 56
  11. lemma OAI.CurrentMain.Spatial.spatialTensorOp_mul line 59
  12. lemma OAI.CurrentMain.Spatial.completion_opNorm_le line 63
  13. lemma OAI.CurrentMain.Spatial.spatialTensorOp_norm_le line 71
  14. lemma OAI.CurrentMain.Spatial.spatialTensorOp_star line 76
  15. def OAI.CurrentMain.Compact.rankOneGenerators line 100
  16. def OAI.CurrentMain.Compact.finiteRankAlgebra line 102
  17. def OAI.CurrentMain.Compact.compactOperatorAlgebra line 105
  18. instance OAI.CurrentMain.Compact.compactOperatorAlgebra_closed line 108
  19. abbrev OAI.CurrentMain.Compact.CompactOperators line 111
  20. instance OAI.CurrentMain.Compact.(instance at line 113) line 113
  21. lemma OAI.CurrentMain.Compact.rankOne_isCompact line 118
  22. lemma OAI.CurrentMain.Compact.finiteRankAlgebra_compact line 123
  23. theorem OAI.CurrentMain.Compact.compactOperators_areCompact line 138
  24. theorem OAI.CurrentMain.Compact.rankOne_mem_compactOperators line 143
  25. abbrev OAI.CurrentMain.Compact.StandardHilbert line 147
  26. abbrev OAI.CurrentMain.Compact.StandardCompacts line 149
  27. def OAI.CurrentMain.Compact.standardVector line 160
  28. lemma OAI.CurrentMain.Compact.inner_standardVector line 161
  29. lemma OAI.CurrentMain.Compact.norm_standardVector line 163
  30. def OAI.CurrentMain.Compact.compactMatrixUnit line 166
  31. theorem OAI.CurrentMain.Compact.compactMatrixUnit_star line 169
  32. theorem OAI.CurrentMain.Compact.compactMatrixUnit_mul line 173
  33. theorem OAI.CurrentMain.Compact.compactMatrixUnit_norm line 181
  34. def OAI.CurrentMain.Compact.compactProjection line 185
  35. lemma OAI.CurrentMain.Compact.compactProjection_star line 187
  36. lemma OAI.CurrentMain.Compact.compactProjection_mul line 189
  37. theorem OAI.CurrentMain.Compact.compactProjection_compress line 193
  38. abbrev OAI.CurrentMain.Spatial.StabilizationHilbert line 212
  39. abbrev OAI.CurrentMain.Spatial.StabilizationOperators line 214
  40. def OAI.CurrentMain.Spatial.spatialEntry line 217
  41. lemma OAI.CurrentMain.Spatial.spatialEntry_zero line 220
  42. lemma OAI.CurrentMain.Spatial.spatialEntry_add line 221
  43. lemma OAI.CurrentMain.Spatial.spatialEntry_smul line 224
  44. lemma OAI.CurrentMain.Spatial.spatialEntry_star line 227
  45. lemma OAI.CurrentMain.Spatial.spatialEntry_mul line 232
  46. def OAI.CurrentMain.Spatial.spatialCorner line 255
  47. lemma OAI.CurrentMain.Spatial.spatialCorner_coefficient line 263
  48. lemma OAI.CurrentMain.Spatial.spatialCorner_injective line 269
  49. def OAI.CurrentMain.Spatial.spatialCompactAlgebra line 295
  50. def OAI.CurrentMain.Spatial.elementarySet line 299
  51. lemma OAI.CurrentMain.Spatial.elementary_mul line 303
  52. lemma OAI.CurrentMain.Spatial.elementary_star line 311
  53. def OAI.CurrentMain.Spatial.elementarySpan line 318
  54. lemma OAI.CurrentMain.Spatial.rankOne_compression line 344
  55. lemma OAI.CurrentMain.Spatial.spatialCorner_compress_elementary line 353
  56. lemma OAI.CurrentMain.Spatial.elementarySpan_compress line 362
  57. theorem OAI.CurrentMain.Spatial.spatialCorner_full line 379
  58. instance OAI.CurrentMain.Spatial.spatialCompactAlgebra_closed line 399
  59. def OAI.CurrentMain.Spatial.SpatialStabilization line 402
  60. instance OAI.CurrentMain.Spatial.(instance at line 404) line 404
  61. def OAI.CurrentMain.Spatial.spatialCornerInto line 407
  62. lemma OAI.CurrentMain.Spatial.spatialCornerInto_injective line 417
  63. theorem OAI.CurrentMain.Spatial.spatialCornerInto_full line 421