OAI/Analysis/TracialSplitting/SimpleIdeals.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Pureness.closedTwoSidedIdeal line 17
  2. theorem OAI.Pureness.coe_closedTwoSidedIdeal line 42
  3. theorem OAI.Pureness.closure_span_singleton_eq_univ line 46
  4. def OAI.Pureness.finiteIdealSum line 68
  5. theorem OAI.Pureness.exists_finiteIdealSum line 71
  6. theorem OAI.Pureness.exists_invertible_finiteIdealSum line 110
  7. def OAI.Pureness.traceTransfer line 129
  8. theorem OAI.Pureness.trace_transfer_identity line 132
  9. theorem OAI.Pureness.traceTransfer_eq_sandwich line 153
  10. theorem OAI.Pureness.traceTransfer_eq_sum_conjugates line 157
  11. theorem OAI.Pureness.traceTransfer_nonneg line 162
  12. theorem OAI.Pureness.normalize_fullness_sum line 174
  13. theorem OAI.Pureness.sqrt_trace_transfer line 196
  14. theorem OAI.Pureness.invertible_positive_sum_of_invertible_sum line 215
  15. theorem OAI.Pureness.fullness line 259
  16. theorem OAI.Pureness.exists_positive_trace_transfer line 271
  17. theorem OAI.Pureness.TracialState.conjugate_le line 291
  18. theorem OAI.Pureness.TracialState.faithful line 311
  19. theorem OAI.Pureness.TracialState.map_eq_zero_iff line 324
  20. def OAI.Pureness.normalizePositive line 338
  21. lemma OAI.Pureness.normalizePositive_nonneg line 340
  22. lemma OAI.Pureness.normalizePositive_zero line 344
  23. lemma OAI.Pureness.normalizePositive_norm_le line 348
  24. lemma OAI.Pureness.normalizePositive_smul line 354
  25. def OAI.Pureness.normalizedRoot line 360
  26. def OAI.Pureness.normalizedRootRank line 363
  27. lemma OAI.Pureness.normalizedRoot_nonneg line 366
  28. lemma OAI.Pureness.normalizedRoot_le_one line 368
  29. lemma OAI.Pureness.normalizedRootRank_le_one line 374
  30. lemma OAI.Pureness.normalizedRootRank_smul line 384
  31. lemma OAI.Pureness.normalized_trace_le_rank line 388
  32. lemma OAI.Pureness.normalizedRoot_monotone line 393
  33. lemma OAI.Pureness.normalizedRootRank_tendsto line 419
  34. lemma OAI.Pureness.normalizedRootRank_pos line 427
  35. def OAI.Pureness.sandwichSubalgebra line 445
  36. def OAI.Pureness.hereditarySubalgebra line 461
  37. def OAI.Pureness.hereditaryCarrier line 464
  38. lemma OAI.Pureness.hereditarySubalgebra_coe line 466
  39. instance OAI.Pureness.hereditarySubalgebra_closed line 469
  40. lemma OAI.Pureness.hereditary_sqrt_mem line 472
  41. lemma OAI.Pureness.self_mem_hereditary line 478
  42. lemma OAI.Pureness.hereditary_sandwich_mem line 484
  43. lemma OAI.Pureness.sqrt_sandwich_mem_hereditary line 497
  44. lemma OAI.Pureness.normalizedRoot_mem_hereditary line 502