OAI/Analysis/Commutator/RowOperator.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.OperatorAmplification.position line 20
2. lemma OAI.Kadison.OperatorAmplification.position_apply line 24
3. lemma OAI.Kadison.OperatorAmplification.norm_position_le line 28
4. lemma OAI.Kadison.OperatorAmplification.entry_position line 35
5. lemma OAI.Kadison.OperatorAmplification.norm_position line 41
6. lemma OAI.Kadison.OperatorAmplification.diagonal_commutator_position line 45
7. lemma OAI.Kadison.OperatorAmplification.norm_diagonal_commutator_position line 54