OAI/Analysis/Commutator/FaithfulNormalFunctional.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FaithfulNormalFunctional.weight line 21
2. lemma OAI.Kadison.FaithfulNormalFunctional.weight_pos line 23
3. lemma OAI.Kadison.FaithfulNormalFunctional.weight_norm_bound line 28
4. def OAI.Kadison.FaithfulNormalFunctional.term line 35
5. lemma OAI.Kadison.FaithfulNormalFunctional.term_bound line 38
6. lemma OAI.Kadison.FaithfulNormalFunctional.term_summable line 47
7. lemma OAI.Kadison.FaithfulNormalFunctional.term_add line 51
8. lemma OAI.Kadison.FaithfulNormalFunctional.term_smul line 54
9. lemma OAI.Kadison.FaithfulNormalFunctional.term_nonneg line 58
10. def OAI.Kadison.FaithfulNormalFunctional.functional line 62
11. lemma OAI.Kadison.FaithfulNormalFunctional.functional_faithful line 79
12. lemma OAI.Kadison.FaithfulNormalFunctional.functional_boundedWOT line 94