OAI/Analysis/Pureness/Stabilization/RankBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzTrace.Positive.power_cut_le line 11
2. theorem OAI.CuntzTrace.ExtendedTrace.rank_cut_le_trace line 50
3. theorem OAI.CuntzTrace.ExtendedTrace.rank_eq_zero_iff line 68
4. lemma OAI.CuntzTrace.Positive.cut_cut line 91
5. theorem OAI.CuntzTrace.ExtendedTrace.trace_le_norm_mul_rank line 114
6. theorem OAI.CuntzTrace.ExtendedTrace.controller_trace_bound line 137
7. theorem OAI.CuntzTrace.ExtendedTrace.trace_cut_loss line 153