OAI/Analysis/Commutator/TracialL2Tools.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.TracialL2.norm line 19
2. lemma OAI.Kadison.TracialL2.norm_nonneg line 21
3. lemma OAI.Kadison.TracialL2.norm_sq line 23
4. lemma OAI.Kadison.TracialL2.norm_zero line 27
5. lemma OAI.Kadison.TracialL2.norm_add line 29
6. lemma OAI.Kadison.TracialL2.norm_sub line 32
7. lemma OAI.Kadison.TracialL2.norm_smul line 35
8. lemma OAI.Kadison.TracialL2.norm_real_smul line 38
9. lemma OAI.Kadison.TracialL2.norm_mul_left line 43
10. lemma OAI.Kadison.TracialL2.norm_star line 52
11. lemma OAI.Kadison.TracialL2.norm_mul_right line 57
12. lemma OAI.Kadison.TracialL2.norm_trace_mul line 64
13. lemma OAI.Kadison.TracialL2.norm_projection_sq line 69
14. lemma OAI.Kadison.TracialL2.norm_mono_square line 72
15. lemma OAI.Kadison.TracialL2.norm_le_opnorm line 77
16. lemma OAI.Kadison.TracialL2.trace_two_corner_letters line 85