OAI/Analysis/Commutator/ReducingMatrix.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.ReducingRepresentation.matrixInclusion line 22
2. lemma OAI.Kadison.ReducingRepresentation.matrixInclusion_apply line 32
3. lemma OAI.Kadison.ReducingRepresentation.matrix_intertwines line 38
4. lemma OAI.Kadison.ReducingRepresentation.restricted_matrix_norm_le line 48
5. lemma OAI.Kadison.ReducingRepresentation.diagonal_intertwines line 61
6. lemma OAI.Kadison.ReducingRepresentation.matrix_commutator_intertwines line 67
7. lemma OAI.Kadison.ReducingRepresentation.compression_eq_restrict line 83