OAI/Analysis/Commutator/Average.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.WeakOperatorIntegral.norm_le_of_integral line 27
2. lemma OAI.Kadison.WeakOperatorIntegral.commutator_coeff line 46
3. lemma OAI.Kadison.WeakOperatorIntegral.commutator_norm line 53
4. lemma OAI.Kadison.WeakOperatorIntegral.commutes line 59
5. lemma OAI.Kadison.WeakOperatorIntegral.sandwich_coeff line 67
6. lemma OAI.Kadison.WeakOperatorIntegral.preserves_sandwich line 74
7. lemma OAI.Kadison.WeakOperatorIntegral.difference_coeff line 98
8. lemma OAI.Kadison.WeakOperatorIntegral.difference_norm line 106
9. lemma OAI.Kadison.WeakOperatorIntegral.compressed_commutator_coeff line 112
10. lemma OAI.Kadison.WeakOperatorIntegral.preserves_compressed_commutator line 117