OAI/Analysis/Pureness/Traces/TracialRank.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.normalizePositive line 11
  2. lemma OAI.CuntzPureness.normalizePositive_nonneg line 13
  3. lemma OAI.CuntzPureness.normalizePositive_zero line 17
  4. lemma OAI.CuntzPureness.normalizePositive_norm_le line 21
  5. lemma OAI.CuntzPureness.normalizePositive_smul line 27
  6. def OAI.CuntzPureness.normalizedRoot line 33
  7. def OAI.CuntzPureness.normalizedRootRank line 36
  8. lemma OAI.CuntzPureness.normalizedRoot_nonneg line 39
  9. lemma OAI.CuntzPureness.normalizedRoot_le_one line 41
  10. lemma OAI.CuntzPureness.normalizedRootRank_le_one line 47
  11. lemma OAI.CuntzPureness.normalizedRootRank_smul line 57
  12. lemma OAI.CuntzPureness.normalized_trace_le_rank line 61
  13. lemma OAI.CuntzPureness.normalizedRoot_monotone line 66
  14. lemma OAI.CuntzPureness.normalizedRootRank_tendsto line 92
  15. lemma OAI.CuntzPureness.normalizedRootRank_pos line 100