OAI/Analysis/TracialSplitting/Completion.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Pureness.ClosedStarIdeal.quotientStarHom line 19
  2. lemma OAI.Pureness.ClosedStarIdeal.quotientStarHom_continuous line 22
  3. def OAI.CurrentMain.familyTraceNorm line 41
  4. lemma OAI.CurrentMain.familyTwoNorm_sub_le line 43
  5. lemma OAI.CurrentMain.familyTwoNorm_smul_le line 47
  6. lemma OAI.CurrentMain.familyTwoNorm_smul line 54
  7. lemma OAI.CurrentMain.familyTwoNorm_lipschitz line 62
  8. lemma OAI.CurrentMain.familyTraceNorm_bdd line 76
  9. lemma OAI.CurrentMain.traceNorm_le_family line 80
  10. lemma OAI.CurrentMain.familyTraceNorm_nonneg line 83
  11. lemma OAI.CurrentMain.familyTraceNorm_le_twoNorm line 87
  12. lemma OAI.CurrentMain.familyTraceNorm_le_norm line 92
  13. lemma OAI.CurrentMain.isFamilyCauchy_neg line 106
  14. lemma OAI.Pureness.ClosedStarIdeal.descendedTrace_map line 122
  15. lemma OAI.CurrentMain.ultraTrace_square_nonneg line 141
  16. lemma OAI.CurrentMain.familyLimitTrace_tendsto line 152
  17. lemma OAI.CurrentMain.uniform_sup_ultralimit line 166
  18. lemma OAI.CurrentMain.familyQuotientMap_eq_zero line 203
  19. lemma OAI.CurrentMain.traceTwoNorm_limitTrace_tendsto line 211
  20. lemma OAI.CurrentMain.familyTwoNorm_limitTrace line 220
  21. lemma OAI.CurrentMain.familyTwoNorm_limitTrace_tendsto line 237
  22. lemma OAI.CurrentMain.familyTraceNorm_limitTrace line 246
  23. lemma OAI.CurrentMain.familyTraceNorm_limitTrace_tendsto line 262
  24. lemma OAI.CurrentMain.limitTrace_detects_zero line 271
  25. lemma OAI.CurrentMain.completionTrace_tendsto line 292
  26. lemma OAI.CurrentMain.completionTwoNorm_tendsto line 297
  27. lemma OAI.CurrentMain.boundedFamilyConstant_apply line 306
  28. lemma OAI.CurrentMain.completionTrace_constant line 309
  29. lemma OAI.CurrentMain.completionTwoNorm_constant line 313
  30. lemma OAI.CurrentMain.familyTwoNorm_completionMap line 318
  31. lemma OAI.CurrentMain.completion_distance_tendsto_zero line 322
  32. theorem OAI.CurrentMain.completion_uniform_dense line 337
  33. lemma OAI.CurrentMain.familyTwoNorm_abs_sub_le line 344
  34. lemma OAI.CurrentMain.completion_uniformTwoNorm_tendsto line 353
  35. lemma OAI.CurrentMain.completionQuotientMap_eq_zero line 362
  36. lemma OAI.CurrentMain.completionTrace_detects_zero line 370
  37. lemma OAI.Pureness.ClosedStarIdeal.quotientMap_realPart line 389
  38. lemma OAI.Pureness.ClosedStarIdeal.exists_bounded_selfAdjoint_lift line 397
  39. lemma OAI.CurrentMain.familyLimitTrace_constant_tendsto line 420
  40. lemma OAI.CurrentMain.familyTwoNorm_ultrapowerMap line 425
  41. instance OAI.CurrentMain.familyUltrapowerNontrivial line 435
  42. lemma OAI.CurrentMain.familyUltrapowerMap_injective line 443
  43. lemma OAI.CurrentMain.completion_ultrapower_faithful line 460