OAI/Analysis/JiangSu/TensorProducts/SpatialFiniteMatrices.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UnitalTomsWinter.StabilizationHilbert line 19
  2. abbrev OAI.UnitalTomsWinter.StabilizationOperators line 51
  3. def OAI.UnitalTomsWinter.spatialEntry line 68
  4. lemma OAI.UnitalTomsWinter.spatialEntry_zero line 72
  5. lemma OAI.UnitalTomsWinter.spatialEntry_add line 74
  6. lemma OAI.UnitalTomsWinter.spatialEntry_smul line 78
  7. lemma OAI.UnitalTomsWinter.spatialEntry_star line 82
  8. lemma OAI.UnitalTomsWinter.spatialEntry_mul line 88
  9. lemma OAI.UnitalTomsWinter.spatialEntry_sum line 99
  10. def OAI.UnitalTomsWinter.spatialMatrixSum line 106
  11. lemma OAI.UnitalTomsWinter.spatialMatrixSum_star line 110
  12. lemma OAI.UnitalTomsWinter.spatialMatrixSum_mul line 118
  13. def OAI.UnitalTomsWinter.spatialFiniteValue line 129
  14. lemma OAI.UnitalTomsWinter.spatialFiniteValue_star line 133
  15. lemma OAI.UnitalTomsWinter.spatialFiniteValue_mul line 138
  16. def OAI.UnitalTomsWinter.spatialFinite line 142
  17. lemma OAI.UnitalTomsWinter.spatialFinite_coefficient line 151
  18. theorem OAI.UnitalTomsWinter.spatialFinite_injective line 158
  19. theorem OAI.UnitalTomsWinter.spatialFinite_isometry line 168
  20. lemma OAI.UnitalTomsWinter.spatialFinite_successor line 172
  21. theorem OAI.UnitalTomsWinter.spatialFinite_compatible line 179
  22. instance OAI.UnitalTomsWinter.stabilizationOperatorsCStar line 221
  23. instance OAI.UnitalTomsWinter.stabilizationOperatorsContinuousStar line 223
  24. instance OAI.UnitalTomsWinter.stabilizationOperatorsTopologicalRing line 225
  25. def OAI.UnitalTomsWinter.spatialRepresentation line 228
  26. theorem OAI.UnitalTomsWinter.spatialRepresentation_stage line 231
  27. lemma OAI.UnitalTomsWinter.spatialRepresentation_continuous line 235
  28. theorem OAI.UnitalTomsWinter.spatialRepresentation_norm line 243
  29. theorem OAI.UnitalTomsWinter.spatialRepresentation_isometry line 255
  30. def OAI.UnitalTomsWinter.spatialMatrixAlgebra line 259
  31. lemma OAI.UnitalTomsWinter.spatialRepresentation_mem line 262
  32. theorem OAI.UnitalTomsWinter.spatialRepresentation_range line 274