OAI/Analysis/Commutator/FaithfulVectorGNS.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FaithfulNormalFunctional.weighted line 22
2. lemma OAI.Kadison.FaithfulNormalFunctional.weighted_norm_sq line 25
3. lemma OAI.Kadison.FaithfulNormalFunctional.weighted_mem line 30
4. def OAI.Kadison.FaithfulNormalFunctional.vector line 38
5. lemma OAI.Kadison.FaithfulNormalFunctional.vector_inner line 40
6. def OAI.Kadison.FaithfulNormalFunctional.gnsEmbedding line 53
7. lemma OAI.Kadison.FaithfulNormalFunctional.gnsEmbedding_intertwines line 57