OAI/Analysis/Commutator/EndpointElimination2.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.matrixL1 line 21
2. def OAI.Kadison.matrixL2 line 24
3. lemma OAI.Kadison.single_nonneg line 27
4. lemma OAI.Kadison.sqrt_single line 32
5. theorem OAI.Kadison.matrixL1_single line 37
6. theorem OAI.Kadison.matrixL2_single line 44