OAI/Analysis/Commutator/OrbitStateHull.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.OrbitStateHull.vector line 29
2. lemma OAI.Kadison.OrbitStateHull.vector_apply line 47
3. lemma OAI.Kadison.OrbitStateHull.vector_norm line 50
4. lemma OAI.Kadison.OrbitStateHull.vector_nonneg line 53
5. def OAI.Kadison.OrbitStateHull.orbit line 56
6. def OAI.Kadison.OrbitStateHull.hull line 60
7. lemma OAI.Kadison.OrbitStateHull.vector_mem_hull line 62
8. lemma OAI.Kadison.OrbitStateHull.hull_nonempty line 66
9. lemma OAI.Kadison.OrbitStateHull.hull_compact line 68
10. lemma OAI.Kadison.OrbitStateHull.hull_norm line 73
11. lemma OAI.Kadison.OrbitStateHull.hull_one line 79
12. lemma OAI.Kadison.OrbitStateHull.hull_nonneg line 87
13. def OAI.Kadison.OrbitStateHull.positive line 93
14. theorem OAI.Kadison.OrbitStateHull.hull_projection_absolute_continuity line 110
15. theorem OAI.Kadison.OrbitStateHull.hull_projection_tendsto line 128