OAI/Analysis/FreeWords/UltraTrace.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKUltraTrace.seqOrder line 17
  2. theorem OAI.KKUltraTrace.seqSOR line 22
  3. def OAI.KKUltraTrace.ultraTraceValue line 26
  4. theorem OAI.KKUltraTrace.tendsto_ultraTraceValue line 29
  5. theorem OAI.KKUltraTrace.ultraTraceValue_add line 41
  6. theorem OAI.KKUltraTrace.ultraTraceValue_smul line 47
  7. theorem OAI.KKUltraTrace.ultraTraceValue_mono line 53
  8. def OAI.KKUltraTrace.ultraTrace line 65
  9. theorem OAI.KKUltraTrace.ultraTrace_one line 71
  10. theorem OAI.KKUltraTrace.ultraTrace_tracial line 77
  11. def OAI.KKUltraTrace.gnsVector line 88
  12. theorem OAI.KKUltraTrace.gnsVector_inner line 91
  13. theorem OAI.KKUltraTrace.gnsStarAlgHom_vector line 97
  14. theorem OAI.KKUltraTrace.tracial_gns_zero line 103
  15. theorem OAI.KKUltraTrace.ultraTrace_exists line 134