OAI/Analysis/JiangSu/Nonunital/Stabilization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NonunitalGamma.finiteMatrixMap_apply line 18
2. lemma OAI.NonunitalGamma.stabilizationMap_stage line 21
3. lemma OAI.NonunitalGamma.finiteMatrixMap_injective line 26
4. lemma OAI.NonunitalGamma.stabilizationMap_isometry line 32
5. lemma OAI.NonunitalGamma.stabilizationInr_isometry line 49
6. lemma OAI.NonunitalGamma.NormalizedTrace.stabilized_stage line 52
7. lemma OAI.NonunitalGamma.NormalizedTrace.stabilized_rank_stage line 71
8. lemma OAI.NonunitalGamma.scaledTrace_apply line 94
9. lemma OAI.NonunitalGamma.scaledTrace_rank line 97
10. lemma OAI.NonunitalGamma.boundedStabilized_stage line 103
11. lemma OAI.NonunitalGamma.boundedStabilized_rank_stage line 116
12. lemma OAI.NonunitalGamma.comparison_of_normalized_rank_lt line 126