OAI/Analysis/CharacterCriterion/States.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KirchbergRordam.GenericRW.States.norm_rotation line 20
2. lemma OAI.KirchbergRordam.GenericRW.States.eval_selfAdjoint_im_zero line 28
3. lemma OAI.KirchbergRordam.GenericRW.States.eval_nonneg line 47
4. theorem OAI.KirchbergRordam.GenericRW.States.exists_state line 76
5. def OAI.KirchbergRordam.GenericRW.PureStates.normStates line 90
6. def OAI.KirchbergRordam.GenericRW.PureStates.evaluationReal line 92
7. instance OAI.KirchbergRordam.GenericRW.PureStates.locallyConvexReal line 97
8. lemma OAI.KirchbergRordam.GenericRW.PureStates.normStates_compact line 100
9. lemma OAI.KirchbergRordam.GenericRW.PureStates.normStates_nonempty line 109
10. def OAI.KirchbergRordam.GenericRW.PureStates.IsPure line 115
11. theorem OAI.KirchbergRordam.GenericRW.PureStates.exists_pure line 118
12. lemma OAI.KirchbergRordam.GenericRW.PureStates.IsPure.norm_le_one line 125
13. lemma OAI.KirchbergRordam.GenericRW.PureStates.IsPure.map_one line 127
14. lemma OAI.KirchbergRordam.GenericRW.PureStates.IsPure.extreme line 130