OAI/Analysis/Commutator/IntertwinerMatrixTransfer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.IntertwinerCompression.transfer_raw_commutator line 21
2. lemma OAI.Kadison.IntertwinerCompression.transfer_raw_commutator_norm_le line 33
3. lemma OAI.Kadison.IntertwinerCompression.pullback_matrix_commutator_norm_le line 49
4. lemma OAI.Kadison.IntertwinerCompression.transfer_back line 64