OAI/Analysis/JiangSu/TraceCone/Pullback.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TraceCone.ExtendedTrace.pullback_apply line 17
  2. def OAI.TraceCone.ExtendedTrace.kernelWeight line 20
  3. theorem OAI.TraceCone.ExtendedTrace.kernelWeight_eq_zero line 22
  4. theorem OAI.TraceCone.ExtendedTrace.kernelWeight_lt_top line 25
  5. theorem OAI.TraceCone.ExtendedTrace.injective_of_surjective_pullback line 28
  6. lemma OAI.TraceCone.Positive.map_power line 62
  7. theorem OAI.TraceCone.ExtendedTrace.rank_zero_trace line 76
  8. theorem OAI.TraceCone.ExtendedTrace.rank_add line 79
  9. theorem OAI.TraceCone.ExtendedTrace.rank_pullback line 84
  10. theorem OAI.TraceCone.ExtendedTrace.rank_le_liminf_of_canonicalConverges line 91
  11. lemma OAI.TraceCone.Positive.exists_starMul_factor line 123
  12. lemma OAI.TraceCone.Positive.matrix_diagonal_nonneg line 127
  13. def OAI.TraceCone.Positive.matrixDiagonal line 135
  14. lemma OAI.TraceCone.Positive.matrixDiagonal_continuous line 138
  15. lemma OAI.TraceCone.Positive.matrixDiagonal_zero line 145
  16. lemma OAI.TraceCone.Positive.matrixDiagonal_add line 149
  17. lemma OAI.TraceCone.Positive.matrixDiagonal_smul line 153
  18. lemma OAI.TraceCone.Positive.matrixDiagonal_starMul line 156
  19. lemma OAI.TraceCone.Positive.matrixDiagonal_mulStar line 161
  20. def OAI.TraceCone.ExtendedTrace.matrixTrace line 169
  21. theorem OAI.TraceCone.ExtendedTrace.matrixTrace_apply line 182
  22. def OAI.TraceCone.matrixCorner line 188
  23. lemma OAI.TraceCone.Positive.matrixDiagonal_corner line 209
  24. theorem OAI.TraceCone.ExtendedTrace.matrixTrace_corner line 221
  25. lemma OAI.TraceCone.ExtendedTrace.matrixTrace_pullback_corner line 227
  26. theorem OAI.TraceCone.ExtendedTrace.matrixRank_corner line 232