OAI/Analysis/Pureness/Quasitrace/QuasitraceUltralimitPositive.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.boundedProductEval line 12
  2. def OAI.CuntzPureness.boundedProductPositiveEval line 21
  3. lemma OAI.CuntzPureness.boundedProductPositiveEval_add line 24
  4. lemma OAI.CuntzPureness.boundedProductPositiveEval_smul line 29
  5. def OAI.CuntzPureness.quasitraceUltraPositive line 38
  6. lemma OAI.CuntzPureness.quasitraceUltraPositive_tendsto line 43
  7. lemma OAI.CuntzPureness.quasitraceUltraPositive_nonneg line 63
  8. lemma OAI.CuntzPureness.quasitraceUltraPositive_zero line 68
  9. lemma OAI.CuntzPureness.quasitraceUltraPositive_one line 75
  10. lemma OAI.CuntzPureness.quasitraceUltraPositive_add line 82
  11. lemma OAI.CuntzPureness.quasitraceUltraPositive_smul line 95
  12. lemma OAI.CuntzPureness.quasitraceUltraPositive_polar line 104
  13. lemma OAI.CuntzPureness.quasitraceUltraPositive_monotone line 112
  14. def OAI.CuntzPureness.ultralimitPositiveQuasitrace line 122
  15. lemma OAI.CuntzPureness.ultralimitPositiveQuasitrace_metricSize line 131
  16. lemma OAI.CuntzPureness.ultralimitPositiveQuasitrace_metricSize_add line 138
  17. lemma OAI.CuntzPureness.ultralimitPositiveQuasitrace_sqrt_add line 147