OAI/Analysis/Commutator/AmplificationIsometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.HilbertPadding.amplifyIsometry line 28
2. lemma OAI.Kadison.HilbertPadding.amplifyIsometry_apply line 37
3. lemma OAI.Kadison.HilbertPadding.amplifyIsometry_adjoint line 40
4. lemma OAI.Kadison.HilbertPadding.diagonal_extend line 49
5. lemma OAI.Kadison.HilbertPadding.amplifyIsometry_matrix_intertwines line 54
6. lemma OAI.Kadison.HilbertPadding.amplifyIsometry_adjoint_matrix_intertwines line 68
7. theorem OAI.Kadison.HilbertPadding.amplified_extension_commutator_norm line 77