OAI/Analysis/JiangSu/CStarAlgebras/CStarPolarNormalization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CStarPolar.cutoffInverseSqrt line 14
2. lemma OAI.CStarPolar.cutoff_continuous line 15
3. lemma OAI.CStarPolar.cutoff_zero line 22
4. lemma OAI.CStarPolar.cutoff_one line 23
5. lemma OAI.CStarPolar.cutoff_square line 24
6. lemma OAI.CStarPolar.cutoff_ne_zero line 31
7. lemma OAI.CStarPolar.spectrum_lower line 38
8. lemma OAI.CStarPolar.isUnit_of_two_defects line 49
9. def OAI.CStarPolar.normalize line 63
10. theorem OAI.CStarPolar.normalize_unitary line 66