OAI/Analysis/JiangSu/DimensionDrop/SequentialProjectionless.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CStarProjectionRounding.norm_selfAdjointPart_le line 16
  2. lemma OAI.CStarProjectionRounding.map_selfAdjointPart line 23
  3. lemma OAI.CStarProjectionRounding.defect_near_projection line 30
  4. lemma OAI.CStarProjectionRounding.trivial_projection_of_approximation line 49
  5. theorem OAI.SequentialCStar.System.limit_projection_trivial line 89
  6. theorem OAI.OriginalJiangSu.projection_trivial line 100
  7. lemma OAI.OriginalJiangSu.stage_trace_oscillation line 113
  8. lemma OAI.OriginalJiangSu.trace_stage_unique line 127
  9. theorem OAI.OriginalJiangSu.trace_unique line 176
  10. def OAI.OriginalJiangSu.stageTrace line 199
  11. lemma OAI.OriginalJiangSu.stageTrace_norm line 203
  12. lemma OAI.OriginalJiangSu.stageTrace_one line 205
  13. lemma OAI.OriginalJiangSu.stageTrace_tracial line 206
  14. def OAI.OriginalJiangSu.trace line 211
  15. lemma OAI.OriginalJiangSu.trace_one line 213
  16. lemma OAI.OriginalJiangSu.trace_tracial line 215
  17. lemma OAI.OriginalJiangSu.trace_norm line 217
  18. theorem OAI.OriginalJiangSu.existsUnique_trace line 219