OAI/Analysis/Pureness/Comparison/SupportApproximation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzComparison.supportCutoff line 11
2. lemma OAI.CuntzComparison.supportCutoff_continuous line 13
3. lemma OAI.CuntzComparison.supportCutoff_bounds line 17
4. lemma OAI.CuntzComparison.supportCutoff_zero line 22
5. lemma OAI.CuntzComparison.supportCutoff_le_indicator line 24
6. lemma OAI.CuntzComparison.supportCutoff_tendsto line 30
7. def OAI.CuntzComparison.supportApprox line 48
8. lemma OAI.CuntzComparison.supportApprox_nonneg line 50
9. lemma OAI.CuntzComparison.supportApprox_norm_le_one line 56
10. lemma OAI.CuntzComparison.supportApprox_mem line 62
11. theorem OAI.CuntzComparison.TracialState.supportApprox_trace_tendsto line 66
12. theorem OAI.CuntzComparison.TracialState.supportApprox_trace_le line 82