OAI/Analysis/Commutator/TracialL2Continuity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.TracialL2.trace_star line 22
2. lemma OAI.Kadison.TracialL2.norm_trace_star line 27
3. lemma OAI.Kadison.TracialL2.norm_trace_star_mul line 33
4. lemma OAI.Kadison.TracialL2.norm_mul_sub_mul line 37
5. lemma OAI.Kadison.TracialL2.norm_one line 44
6. lemma OAI.Kadison.TracialL2.norm_trace_le line 50
7. lemma OAI.Kadison.TracialL2.norm_pow_sub_pow line 54
8. lemma OAI.Kadison.TracialL2.tendsto_of_norm_sub_le line 74
9. lemma OAI.Kadison.TracialL2.tendsto_mul line 80
10. lemma OAI.Kadison.TracialL2.tendsto_trace line 92