OAI/Analysis/Commutator/TracialSmallCorners.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.TracialSequence.mapSequence line 21
2. lemma OAI.Kadison.TracialSequence.mapSequence_apply line 31
3. lemma OAI.Kadison.TracialSequence.leftRestricted_eq_of_eventuallyEq line 41
4. def OAI.Kadison.TracialSequence.cutSequence line 52
5. lemma OAI.Kadison.TracialSequence.cutSequence_apply line 61
6. lemma OAI.Kadison.TracialSequence.projection_operator_lift line 66
7. lemma OAI.Kadison.TracialSequence.projection_rep_lift line 74
8. theorem OAI.Kadison.TracialSequence.small_projection_lift line 84
9. theorem OAI.Kadison.TracialSequence.small_corner_bound line 123