OAI/Analysis/Commutator/CStarContractiveLifts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.CStarContractiveLifts.radial line 15
2. lemma OAI.Kadison.CStarContractiveLifts.radial_continuous line 17
3. lemma OAI.Kadison.CStarContractiveLifts.radial_eq_one line 22
4. lemma OAI.Kadison.CStarContractiveLifts.radial_square line 25
5. lemma OAI.Kadison.CStarContractiveLifts.radial_bound line 28
6. def OAI.Kadison.CStarContractiveLifts.clip line 36
7. lemma OAI.Kadison.CStarContractiveLifts.clip_norm_le line 38
8. lemma OAI.Kadison.CStarContractiveLifts.clip_fix line 57
9. lemma OAI.Kadison.CStarContractiveLifts.map_clip line 66
10. theorem OAI.Kadison.CStarContractiveLifts.contraction line 72
11. theorem OAI.Kadison.CStarContractiveLifts.norm_lift line 77
12. lemma OAI.Kadison.CStarContractiveLifts.operator_norm_lift line 98