OAI/Analysis/Commutator/IrreducibleTowerAveraging.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.IrreducibleTowerAveraging.stageUnitaries line 29
2. def OAI.Kadison.IrreducibleTowerAveraging.orbit line 37
3. lemma OAI.Kadison.IrreducibleTowerAveraging.orbit_self line 42
4. lemma OAI.Kadison.IrreducibleTowerAveraging.conjugation_orbit line 47
5. lemma OAI.Kadison.IrreducibleTowerAveraging.hull_bounded line 56
6. lemma OAI.Kadison.IrreducibleTowerAveraging.hull_trace line 70
7. theorem OAI.Kadison.IrreducibleTowerAveraging.scalar_mem_hull line 83
8. lemma OAI.Kadison.IrreducibleTowerAveraging.vector_expectation_conjugation line 124
9. def OAI.Kadison.IrreducibleTowerAveraging.eventualFiber line 148
10. lemma OAI.Kadison.IrreducibleTowerAveraging.eventualFiber_convex line 153
11. lemma OAI.Kadison.IrreducibleTowerAveraging.orbit_subset_eventualFiber line 168
12. theorem OAI.Kadison.IrreducibleTowerAveraging.expectation_tendsto line 177
13. theorem OAI.Kadison.IrreducibleTowerAveraging.expectation_tendsto_any line 220