OAI/Analysis/Commutator/RepresentedTowerAverage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.RepresentedTower.unitaryRepresentation line 26
2. lemma OAI.Kadison.RepresentedTower.conjugate_distance line 32
3. def OAI.Kadison.RepresentedTower.stageUnitaryMap line 45
4. def OAI.Kadison.RepresentedTower.stageUnitaryRepresentation line 50
5. lemma OAI.Kadison.RepresentedTower.stageUnitary_continuous line 54
6. lemma OAI.Kadison.RepresentedTower.exists_stage_average line 60
7. theorem OAI.Kadison.RepresentedTower.exists_tower_average line 89