OAI/Analysis/Commutator/CycleInvariants2.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Kadison.SchurWeyl.(instance at line 16) line 16
2. def OAI.Kadison.SchurWeyl.cycleMap line 18
3. lemma OAI.Kadison.SchurWeyl.cycleMap_apply line 21
4. def OAI.Kadison.SchurWeyl.cycleCard line 25
5. lemma OAI.Kadison.SchurWeyl.sum_cycleCard line 28
6. lemma OAI.Kadison.SchurWeyl.cycleCard_pos line 35
7. lemma OAI.Kadison.SchurWeyl.two_le_cycleCard line 41
8. lemma OAI.Kadison.SchurWeyl.three_le_cycleCard line 47
9. lemma OAI.Kadison.SchurWeyl.cycleMap_eq_fixed line 59
10. lemma OAI.Kadison.SchurWeyl.minimal_cycle_sum line 63
11. lemma OAI.Kadison.SchurWeyl.minimal_cycle_bound line 78
12. theorem OAI.Kadison.SchurWeyl.endpoint_cycle_classification line 91