OAI/Analysis/CharacterCriterion/Projectionless.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KirchbergRordam.PrimeProjectionless.tr line 41
  2. lemma OAI.KirchbergRordam.PrimeProjectionless.tr_continuous line 43
  3. lemma OAI.KirchbergRordam.PrimeProjectionless.tr_nat line 51
  4. lemma OAI.KirchbergRordam.PrimeProjectionless.tr_zero line 64
  5. lemma OAI.KirchbergRordam.PrimeProjectionless.tr_left line 76
  6. lemma OAI.KirchbergRordam.PrimeProjectionless.tr_right line 80
  7. lemma OAI.KirchbergRordam.PrimeProjectionless.tr_constant line 84
  8. lemma OAI.KirchbergRordam.PrimeProjectionless.tr_one_sub line 97
  9. lemma OAI.KirchbergRordam.PrimeProjectionless.prime_idempotent line 100
  10. def OAI.KirchbergRordam.ProjectionRounding.cut line 154
  11. lemma OAI.KirchbergRordam.ProjectionRounding.cut_continuous line 155
  12. lemma OAI.KirchbergRordam.ProjectionRounding.cut_low line 156
  13. lemma OAI.KirchbergRordam.ProjectionRounding.cut_high line 160
  14. lemma OAI.KirchbergRordam.ProjectionRounding.scalar_round line 163
  15. lemma OAI.KirchbergRordam.ProjectionRounding.polynomial_cfc line 185
  16. lemma OAI.KirchbergRordam.ProjectionRounding.spectrum_small_defect line 189
  17. lemma OAI.KirchbergRordam.ProjectionRounding.cut_idempotent line 194
  18. lemma OAI.KirchbergRordam.ProjectionRounding.cut_close line 201
  19. def OAI.KirchbergRordam.ProjectionRounding.part line 212
  20. lemma OAI.KirchbergRordam.ProjectionRounding.part_selfAdjoint line 213
  21. lemma OAI.KirchbergRordam.ProjectionRounding.part_sub line 217
  22. lemma OAI.KirchbergRordam.ProjectionRounding.part_fixed line 219
  23. lemma OAI.KirchbergRordam.ProjectionRounding.part_map line 222
  24. lemma OAI.KirchbergRordam.ProjectionRounding.norm_part_le line 224
  25. lemma OAI.KirchbergRordam.ProjectionRounding.norm_part_sub_le line 229
  26. lemma OAI.KirchbergRordam.ProjectionRounding.idempotent_eq_zero_of_norm_lt_one line 233
  27. lemma OAI.KirchbergRordam.ProjectionRounding.small_defect_of_near line 239
  28. lemma OAI.KirchbergRordam.ProjectionRounding.projection_trivial_from_approximation line 257
  29. theorem OAI.KirchbergRordam.BalancedDropLimit.projectionless line 287