OAI/Analysis/Pureness/Stabilization/Rank.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzTrace.Positive.power line 13
  2. def OAI.CuntzTrace.Positive.rootExponent line 16
  3. lemma OAI.CuntzTrace.Positive.rootExponent_pos line 18
  4. lemma OAI.CuntzTrace.Positive.rootExponent_le_one line 22
  5. lemma OAI.CuntzTrace.Positive.rootExponent_antitone line 26
  6. lemma OAI.CuntzTrace.Positive.power_monotone line 31
  7. lemma OAI.CuntzTrace.Positive.power_continuous line 35
  8. lemma OAI.CuntzTrace.Positive.power_norm_le_one line 39
  9. lemma OAI.CuntzTrace.Positive.roots_monotone line 45
  10. lemma OAI.CuntzTrace.Positive.power_one line 61
  11. lemma OAI.CuntzTrace.Positive.cut_norm_le_one line 64
  12. def OAI.CuntzTrace.ExtendedTrace.rank line 72
  13. lemma OAI.CuntzTrace.ExtendedTrace.rank_eq_iSup line 75
  14. theorem OAI.CuntzTrace.ExtendedTrace.tendsto_roots_rank line 79
  15. theorem OAI.CuntzTrace.ExtendedTrace.rank_monotone line 85
  16. theorem OAI.CuntzTrace.ExtendedTrace.apply_le_rank line 90
  17. theorem OAI.CuntzTrace.ExtendedTrace.rank_le_of_tendsto line 96
  18. theorem OAI.CuntzTrace.ExtendedTrace.rank_eq_iSup_cuts line 109
  19. lemma OAI.CuntzTrace.Positive.power_smul line 125
  20. def OAI.CuntzTrace.Positive.normalize line 138
  21. lemma OAI.CuntzTrace.Positive.normalize_norm_le_one line 140
  22. lemma OAI.CuntzTrace.Positive.normalize_continuous line 146
  23. lemma OAI.CuntzTrace.ExtendedTrace.root_scalars_tendsto_one line 157
  24. theorem OAI.CuntzTrace.ExtendedTrace.rank_smul line 165
  25. lemma OAI.CuntzTrace.ExtendedTrace.rank_normalize line 186
  26. theorem OAI.CuntzTrace.ExtendedTrace.tendsto_roots_rank_all line 190
  27. theorem OAI.CuntzTrace.ExtendedTrace.rank_le_of_tendsto_all line 208
  28. theorem OAI.CuntzTrace.ExtendedTrace.rank_eq_iSup_cuts_all line 218