OAI/Analysis/Commutator/StinespringAction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Kadison.Stinespring.gram_middle_nonneg line 19
2. def OAI.Kadison.Stinespring.middleForm line 27
3. lemma OAI.Kadison.Stinespring.middleForm_nonneg line 30
4. lemma OAI.Kadison.Stinespring.middleForm_sub line 44
5. lemma OAI.Kadison.Stinespring.middleForm_real_one line 49
6. def OAI.Kadison.Stinespring.leftLinear line 55
7. lemma OAI.Kadison.Stinespring.form_left line 58
8. lemma OAI.Kadison.Stinespring.form_right line 68
9. lemma OAI.Kadison.Stinespring.form_left_left line 81
10. lemma OAI.Kadison.Stinespring.leftLinear_bound line 94
11. def OAI.Kadison.Stinespring.leftAction line 108
12. lemma OAI.Kadison.Stinespring.leftAction_apply line 111