OAI/Analysis/Commutator/SubfactorExpectation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FreeMoments.Letter.enlarge line 20
2. lemma OAI.Kadison.FreeMoments.word_enlarge line 23
3. lemma OAI.Kadison.FreeMoments.Reduced.enlarge line 29
4. lemma OAI.Kadison.FreeMoments.residual_word_pairing line 36
5. lemma OAI.Kadison.FreeMoments.residual_generated_pairing line 60
6. def OAI.Kadison.SymmetryAlgebra.algebra line 80
7. lemma OAI.Kadison.SymmetryAlgebra.mem_algebra line 98
8. lemma OAI.Kadison.SymmetryAlgebra.self_mem line 100
9. lemma OAI.Kadison.SymmetryAlgebra.le_factor line 102
10. def OAI.Kadison.SymmetryAlgebra.factors line 108
11. lemma OAI.Kadison.SymmetryAlgebra.factors_le line 114
12. theorem OAI.Kadison.SymmetryAlgebra.pairing_projection line 120