OAI/Analysis/JiangSu/TraceCone/Rank.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TraceCone.Positive.rootExponent_pos line 16
  2. lemma OAI.TraceCone.Positive.rootExponent_le_one line 20
  3. lemma OAI.TraceCone.Positive.rootExponent_antitone line 24
  4. lemma OAI.TraceCone.Positive.power_monotone line 30
  5. lemma OAI.TraceCone.Positive.power_continuous line 34
  6. lemma OAI.TraceCone.Positive.power_norm_le_one line 38
  7. lemma OAI.TraceCone.Positive.roots_monotone line 44
  8. lemma OAI.TraceCone.Positive.power_one line 62
  9. lemma OAI.TraceCone.Positive.cut_norm_le_one line 65
  10. lemma OAI.TraceCone.ExtendedTrace.rank_eq_iSup line 73
  11. theorem OAI.TraceCone.ExtendedTrace.tendsto_roots_rank line 77
  12. theorem OAI.TraceCone.ExtendedTrace.rank_monotone line 83
  13. theorem OAI.TraceCone.ExtendedTrace.apply_le_rank line 88
  14. theorem OAI.TraceCone.ExtendedTrace.rank_le_of_tendsto line 94
  15. theorem OAI.TraceCone.ExtendedTrace.rank_eq_iSup_cuts line 107
  16. lemma OAI.TraceCone.Positive.power_smul line 123
  17. def OAI.TraceCone.Positive.normalize line 136
  18. lemma OAI.TraceCone.Positive.normalize_norm_le_one line 138
  19. lemma OAI.TraceCone.Positive.normalize_continuous line 144
  20. lemma OAI.TraceCone.ExtendedTrace.root_scalars_tendsto_one line 155
  21. theorem OAI.TraceCone.ExtendedTrace.rank_smul line 164
  22. lemma OAI.TraceCone.ExtendedTrace.rank_normalize line 185
  23. theorem OAI.TraceCone.ExtendedTrace.tendsto_roots_rank_all line 189
  24. theorem OAI.TraceCone.ExtendedTrace.rank_le_of_tendsto_all line 208
  25. theorem OAI.TraceCone.ExtendedTrace.rank_eq_iSup_cuts_all line 218