OAI/Analysis/JiangSu/DimensionDrop/TraceExistence.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.JiangSuConstruction.normalizedMatrixTrace_norm line 17
  2. lemma OAI.JiangSuConstruction.normalizedMatrixTrace_one line 25
  3. def OAI.JiangSuConstruction.stageTrace line 34
  4. lemma OAI.JiangSuConstruction.stageTrace_norm line 38
  5. lemma OAI.JiangSuConstruction.stageTrace_one line 40
  6. lemma OAI.JiangSuConstruction.stageTrace_tracial line 41
  7. def OAI.JiangSuConstruction.primeDropTrace line 46
  8. lemma OAI.JiangSuConstruction.primeDropTrace_one line 49
  9. lemma OAI.JiangSuConstruction.primeDropTrace_tracial line 51
  10. lemma OAI.JiangSuConstruction.primeDropTrace_norm line 53
  11. theorem OAI.JiangSuConstruction.primeDropLimit_existsUnique_trace line 55
  12. lemma OAI.SequentialCStar.quotientTrace_star_mul_self_nonneg line 76
  13. lemma OAI.SequentialCStar.limitTrace_nonneg line 84
  14. instance OAI.JiangSuConstruction.primeDropOrder line 93
  15. instance OAI.JiangSuConstruction.primeDropOrderedRing line 94
  16. lemma OAI.JiangSuConstruction.normalizedMatrixTrace_star_mul_self_nonneg line 96
  17. lemma OAI.JiangSuConstruction.stageTrace_star_mul_self_nonneg line 102
  18. lemma OAI.JiangSuConstruction.primeDropTrace_nonneg line 105
  19. def OAI.JiangSuConstruction.primeDropPositiveTrace line 108
  20. lemma OAI.JiangSuConstruction.primeDropPositiveTrace_one line 115
  21. lemma OAI.JiangSuConstruction.primeDropPositiveTrace_tracial line 116
  22. def OAI.JiangSuConstruction.matrixUnit line 129
  23. lemma OAI.JiangSuConstruction.matrixUnit_star line 132
  24. lemma OAI.JiangSuConstruction.matrixUnit_sandwich line 136
  25. lemma OAI.JiangSuConstruction.matrixUnit_sum_sandwich line 143
  26. lemma OAI.JiangSuConstruction.matrixTrace_star_mul_self_pos line 156
  27. lemma OAI.JiangSuConstruction.matrixUnit_sum_posDef line 165
  28. def OAI.JiangSuConstruction.leftChannel line 181
  29. def OAI.JiangSuConstruction.rightChannel line 191
  30. def OAI.JiangSuConstruction.interiorChannel line 201
  31. lemma OAI.JiangSuConstruction.leftChannel_eval_left line 205
  32. lemma OAI.JiangSuConstruction.rightChannel_eval_right line 210
  33. def OAI.JiangSuConstruction.conjugationSum line 215
  34. def OAI.JiangSuConstruction.fullElement line 219
  35. lemma OAI.JiangSuConstruction.conjugationSum_mem line 224
  36. lemma OAI.JiangSuConstruction.fullElement_mem line 229
  37. lemma OAI.JiangSuConstruction.conjugationSum_eval line 235
  38. lemma OAI.JiangSuConstruction.conjugationSum_posSemidef line 240
  39. lemma OAI.JiangSuConstruction.weighted_sandwich line 249
  40. lemma OAI.JiangSuConstruction.interiorSum_eval line 254
  41. lemma OAI.JiangSuConstruction.leftSum_endpoint line 263
  42. lemma OAI.JiangSuConstruction.rightSum_endpoint line 274
  43. lemma OAI.JiangSuConstruction.fullElement_posDef line 285
  44. lemma OAI.JiangSuConstruction.fullElement_isUnit line 323
  45. theorem OAI.JiangSuConstruction.dimensionDrop_full_of_fiberwise_nonzero line 331