OAI/Analysis/Pureness/Comparison/SpectralIntegration.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzComparison.TracialState.integrable_spectralMeasure line 11
2. lemma OAI.CuntzComparison.TracialState.ae_mem_spectrum line 19
3. lemma OAI.CuntzComparison.TracialState.spectralMeasure_univ line 26
4. instance OAI.CuntzComparison.(instance at line 33) line 33
5. lemma OAI.CuntzComparison.TracialState.spectralSupportMass_le_one line 36
6. lemma OAI.CuntzComparison.integrable_strictCut line 41
7. lemma OAI.CuntzComparison.integral_strictCut line 46
8. lemma OAI.CuntzComparison.integrable_integerCutCount line 51
9. lemma OAI.CuntzComparison.integral_integerCutCount line 56
10. theorem OAI.CuntzComparison.TracialState.integer_spectral_trace_error line 62