OAI/Analysis/Pureness/Cuntz/ActualSpectralCuts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.positiveIntegerCut line 10
2. lemma OAI.CuntzPureness.positiveIntegerCut_nonneg line 13
3. lemma OAI.CuntzPureness.positiveIntegerCut_eq_posPart line 16
4. lemma OAI.CuntzPureness.spectralApproxUnit_positiveIntegerCut line 25
5. lemma OAI.CuntzPureness.smoothedIntegerCut_cfc line 32
6. lemma OAI.CuntzPureness.smoothedIntegerCut_operator_bounds line 49
7. lemma OAI.CuntzPureness.spectralApproxUnit_trace_tendsto_realRank line 91
8. theorem OAI.CuntzPureness.actual_spectral_integer_approximation line 100