OAI/Analysis/Commutator/CentralPinching.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.CentralAverage.reflection line 22
  2. lemma OAI.Kadison.CentralAverage.reflection_star line 28
  3. lemma OAI.Kadison.CentralAverage.pinch_commutes line 32
  4. def OAI.Kadison.CentralAverage.CentralProjection line 43
  5. def OAI.Kadison.CentralAverage.projectionElement line 46
  6. lemma OAI.Kadison.CentralAverage.projectionElement_projection line 48
  7. def OAI.Kadison.CentralAverage.pinch line 55
  8. lemma OAI.Kadison.CentralAverage.pinch_mem line 59
  9. lemma OAI.Kadison.CentralAverage.pinch_formula line 63
  10. lemma OAI.Kadison.CentralAverage.pinch_commutes_projection line 68
  11. lemma OAI.Kadison.CentralAverage.pinch_preserves line 72
  12. theorem OAI.Kadison.CentralAverage.exists_finite_average line 80