OAI/Analysis/Commutator/StinespringDilation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.Stinespring.elementary line 21
2. lemma OAI.Kadison.Stinespring.form_elementary line 24
3. lemma OAI.Kadison.Stinespring.leftLinear_elementary line 29
4. lemma OAI.Kadison.Stinespring.elementary_one_bound line 34
5. def OAI.Kadison.Stinespring.embedding line 46
6. lemma OAI.Kadison.Stinespring.embedding_apply line 50
7. lemma OAI.Kadison.Stinespring.embedding_norm_le line 53
8. theorem OAI.Kadison.Stinespring.factorization line 58
9. lemma OAI.Kadison.Stinespring.embedding_adjoint_embedding line 67
10. lemma OAI.Kadison.Stinespring.embedding_norm_sq line 71