OAI/Analysis/TracialSplitting/OrthogonalElements.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Pureness.rootExponent_tendsto line 19
  2. lemma OAI.Pureness.root_mul_uniform line 25
  3. lemma OAI.Pureness.normalizedRoot_mul_normalize_tendsto line 55
  4. lemma OAI.Pureness.norm_smul_normalizePositive line 81
  5. lemma OAI.Pureness.normalizedRoot_mul_self_tendsto line 86
  6. lemma OAI.Pureness.normalizedRoot_mul_hereditary_tendsto line 91
  7. lemma OAI.Pureness.trace_mul_contraction_le line 135
  8. lemma OAI.Pureness.trace_le_rank_of_mem_hereditary line 149
  9. theorem OAI.Pureness.hereditary_rank_domination line 168
  10. theorem OAI.Pureness.exists_rank_dominated_trace_transfer line 176
  11. lemma OAI.Pureness.trace_cfc_eq_of_moments line 201
  12. lemma OAI.Pureness.trace_star_mul_self_pow line 238
  13. lemma OAI.Pureness.trace_nnrpow_eq_of_moments line 252
  14. theorem OAI.Pureness.rank_star_mul_self line 264
  15. def OAI.Pureness.CuntzSubequiv line 292
  16. theorem OAI.Pureness.cuntzSubequiv_iff_sequence line 295
  17. theorem OAI.Pureness.cuntzSubequiv_iff_norm line 306
  18. theorem OAI.Pureness.cuntzSubequiv_conjugate line 318
  19. theorem OAI.Pureness.zero_cuntzSubequiv line 321
  20. theorem OAI.Pureness.cuntzSubequiv_of_tendsto line 324
  21. theorem OAI.Pureness.CuntzSubequiv.conjugate_left line 329
  22. theorem OAI.Pureness.CuntzSubequiv.trans line 339
  23. theorem OAI.Pureness.cuntzSubequiv_zero_iff line 344
  24. theorem OAI.Pureness.cuntzSubequiv_refl line 349
  25. def OAI.Pureness.cuntzSetoid line 352