OAI/Analysis/Pureness/Divisibility/CutoffRank.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.spectralApproxUnit line 9
2. lemma OAI.CuntzPureness.spectralApproxUnit_nonneg line 12
3. lemma OAI.CuntzPureness.spectralApproxUnit_norm_le line 18
4. lemma OAI.CuntzPureness.spectralApproxUnit_le_one line 26
5. lemma OAI.CuntzPureness.spectralApproxUnit_mem line 31
6. lemma OAI.CuntzPureness.scalar_cutoff_error_bound line 38
7. lemma OAI.CuntzPureness.spectralApproxUnit_mul_tendsto line 48
8. lemma OAI.CuntzPureness.contractive_mul_hereditary_tendsto line 72
9. lemma OAI.CuntzPureness.spectralApproxUnit_monotone line 98
10. def OAI.CuntzPureness.cutoffTraceSup line 107
11. lemma OAI.CuntzPureness.cutoffTraceSup_eq_rank line 110
12. theorem OAI.CuntzPureness.spectralApproxUnit_trace_tendsto_rank line 140