OAI/Analysis/Commutator/ProjectionPartition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.SpectralPartition.swap_middle line 18
2. def OAI.Kadison.SpectralPartition.splitPiece line 25
3. lemma OAI.Kadison.SpectralPartition.splitPiece_projection line 27
4. lemma OAI.Kadison.SpectralPartition.splitPiece_commute line 34
5. lemma OAI.Kadison.SpectralPartition.splitPiece_orthogonal line 40
6. lemma OAI.Kadison.SpectralPartition.splitPiece_sum line 45
7. theorem OAI.Kadison.SpectralPartition.exists_partition line 48