OAI/Analysis/JiangSu/CStarAlgebras/CutoffRank.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Pureness.spectralApproxUnit line 14
  2. lemma OAI.Pureness.spectralApproxUnit_nonneg line 17
  3. lemma OAI.Pureness.spectralApproxUnit_norm_le line 23
  4. lemma OAI.Pureness.spectralApproxUnit_le_one line 31
  5. lemma OAI.Pureness.spectralApproxUnit_mem line 36
  6. lemma OAI.Pureness.scalar_cutoff_error_bound line 43
  7. lemma OAI.Pureness.spectralApproxUnit_mul_tendsto line 53
  8. lemma OAI.Pureness.contractive_mul_hereditary_tendsto line 77
  9. lemma OAI.Pureness.spectralApproxUnit_monotone line 103
  10. def OAI.Pureness.cutoffTraceSup line 112
  11. lemma OAI.Pureness.cutoffTraceSup_eq_rank line 115
  12. theorem OAI.Pureness.spectralApproxUnit_trace_tendsto_rank line 145
  13. def OAI.Pureness.integerCutCount line 161
  14. theorem OAI.Pureness.integerCutCount_bounds line 164
  15. theorem OAI.Pureness.integerCutCount_zero line 193
  16. theorem OAI.Pureness.integerCutCount_at_positive_integer line 200