OAI/Analysis/Commutator/InfiniteAmplification.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.InfiniteAmplification.Space line 20
2. lemma OAI.Kadison.InfiniteAmplification.map_mem line 23
3. def OAI.Kadison.InfiniteAmplification.mapLinear line 28
4. lemma OAI.Kadison.InfiniteAmplification.norm_mapLinear_le line 34
5. def OAI.Kadison.InfiniteAmplification.map line 43
6. lemma OAI.Kadison.InfiniteAmplification.map_apply line 47
7. lemma OAI.Kadison.InfiniteAmplification.map_adjoint line 49
8. def OAI.Kadison.InfiniteAmplification.diagonal line 55
9. lemma OAI.Kadison.InfiniteAmplification.diagonal_apply line 64
10. def OAI.Kadison.InfiniteAmplification.mapIsometry line 66
11. lemma OAI.Kadison.InfiniteAmplification.mapIsometry_apply line 74