OAI/Analysis/TracialSplitting/Model.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Pureness.IsNuclear line 17
  2. def OAI.CurrentMain.RealRankZero line 30
  3. def OAI.CurrentMain.traceTwoNorm line 34
  4. lemma OAI.CurrentMain.traceTwoNorm_eq_gns line 40
  5. lemma OAI.CurrentMain.traceTwoNorm_nonneg line 45
  6. lemma OAI.CurrentMain.traceTwoNorm_zero line 50
  7. lemma OAI.CurrentMain.traceTwoNorm_one line 55
  8. lemma OAI.CurrentMain.traceTwoNorm_add_le line 58
  9. lemma OAI.CurrentMain.traceTwoNorm_star line 65
  10. lemma OAI.CurrentMain.traceTwoNorm_mul_left line 69
  11. lemma OAI.CurrentMain.traceTwoNorm_mul_right line 80
  12. lemma OAI.CurrentMain.traceTwoNorm_le_norm line 88
  13. lemma OAI.CurrentMain.trace_norm_le_twoNorm line 92
  14. lemma OAI.CurrentMain.trace_norm_le_norm line 101
  15. lemma OAI.CurrentMain.traceTwoNorm_neg line 111
  16. abbrev OAI.Pureness.ClosedStarIdeal.Quotient line 127
  17. def OAI.Pureness.ClosedStarIdeal.quotientMap line 129
  18. lemma OAI.Pureness.ClosedStarIdeal.quotientMap_surjective line 131
  19. lemma OAI.Pureness.ClosedStarIdeal.rel_star line 134
  20. instance OAI.Pureness.ClosedStarIdeal.quotientStar line 139
  21. lemma OAI.Pureness.ClosedStarIdeal.quotientMap_star line 142
  22. instance OAI.Pureness.ClosedStarIdeal.quotientStarRing line 145
  23. instance OAI.Pureness.ClosedStarIdeal.quotientStarModule line 160
  24. abbrev OAI.Pureness.ClosedStarIdeal.idealSubmodule line 165
  25. lemma OAI.Pureness.ClosedStarIdeal.idealSubmodule_coe line 168
  26. instance OAI.Pureness.ClosedStarIdeal.idealSubmodule_closed line 176
  27. def OAI.Pureness.ClosedStarIdeal.quotientLinearEquiv line 180
  28. lemma OAI.Pureness.ClosedStarIdeal.quotientLinearEquiv_mk line 184
  29. instance OAI.Pureness.ClosedStarIdeal.quotientNormedAddCommGroup line 187
  30. instance OAI.Pureness.ClosedStarIdeal.quotientNormedSpace line 191
  31. def OAI.Pureness.ClosedStarIdeal.quotientNormEquiv line 194
  32. lemma OAI.Pureness.ClosedStarIdeal.quotientMap_norm_le line 199
  33. lemma OAI.Pureness.ClosedStarIdeal.quotient_norm_lt_rep line 205
  34. instance OAI.Pureness.ClosedStarIdeal.quotientCompleteSpace line 212
  35. lemma OAI.Pureness.ClosedStarIdeal.quotient_norm_mul_le line 215
  36. instance OAI.Pureness.ClosedStarIdeal.quotientNormedRing line 233
  37. instance OAI.Pureness.ClosedStarIdeal.quotientNormedAlgebra line 237
  38. lemma OAI.Pureness.ClosedStarIdeal.quotient_norm_star line 240
  39. instance OAI.Pureness.ClosedStarIdeal.quotientNormedStarGroup line 249
  40. def OAI.Pureness.ClosedStarIdeal.idealStarAlgebra line 266
  41. instance OAI.Pureness.ClosedStarIdeal.idealStarAlgebraCompleteSpace line 277
  42. instance OAI.Pureness.ClosedStarIdeal.idealStarAlgebraCStar line 280
  43. instance OAI.Pureness.ClosedStarIdeal.idealPartialOrder line 283
  44. instance OAI.Pureness.ClosedStarIdeal.idealStarOrderedRing line 286
  45. def OAI.Pureness.ClosedStarIdeal.idealInclusion line 293
  46. lemma OAI.Pureness.ClosedStarIdeal.idealInclusion_nonneg line 301
  47. lemma OAI.Pureness.ClosedStarIdeal.norm_one_sub line 310
  48. lemma OAI.Pureness.ClosedStarIdeal.exists_ideal_contraction line 317
  49. lemma OAI.Pureness.ClosedStarIdeal.quotient_norm_square_le line 333
  50. instance OAI.Pureness.ClosedStarIdeal.quotientCStarAlgebra line 374
  51. def OAI.CurrentMain.familyTwoNorm line 389
  52. lemma OAI.CurrentMain.familyTwoNorm_bdd line 393
  53. lemma OAI.CurrentMain.traceTwoNorm_le_family line 398
  54. lemma OAI.CurrentMain.familyTwoNorm_nonneg line 402
  55. lemma OAI.CurrentMain.familyTwoNorm_le_norm line 406
  56. lemma OAI.CurrentMain.familyTwoNorm_zero line 409
  57. lemma OAI.CurrentMain.familyTwoNorm_add_le line 413
  58. lemma OAI.CurrentMain.familyTwoNorm_neg line 422
  59. lemma OAI.CurrentMain.familyTwoNorm_sub_swap line 427
  60. lemma OAI.CurrentMain.familyTwoNorm_sub_triangle line 430
  61. lemma OAI.CurrentMain.familyTwoNorm_star line 437
  62. lemma OAI.CurrentMain.familyTwoNorm_mul_left line 440
  63. lemma OAI.CurrentMain.familyTwoNorm_mul_right line 447
  64. instance OAI.CurrentMain.boundedFamilyProductCStar line 460
  65. def OAI.CurrentMain.IsFamilyNull line 469
  66. lemma OAI.CurrentMain.isFamilyNull_iff line 472
  67. lemma OAI.CurrentMain.isFamilyNull_zero line 477
  68. lemma OAI.CurrentMain.isFamilyNull_add line 481
  69. lemma OAI.CurrentMain.isFamilyNull_neg line 490
  70. lemma OAI.CurrentMain.isFamilyNull_star line 496
  71. lemma OAI.CurrentMain.isFamilyNull_mul_left line 500
  72. lemma OAI.CurrentMain.isFamilyNull_mul_right line 508
  73. lemma OAI.CurrentMain.familyNull_isClosed line 516
  74. def OAI.CurrentMain.familyNullTwoSided line 536
  75. lemma OAI.CurrentMain.familyNull_mem line 546
  76. lemma OAI.CurrentMain.familyNull_star line 551
  77. def OAI.CurrentMain.familyNullIdeal line 556
  78. def OAI.CurrentMain.IsFamilyCauchy line 571
  79. lemma OAI.CurrentMain.isFamilyCauchy_const line 574
  80. lemma OAI.CurrentMain.isFamilyCauchy_add line 578
  81. lemma OAI.CurrentMain.isFamilyCauchy_star line 584
  82. lemma OAI.CurrentMain.isFamilyCauchy_mul line 588
  83. def OAI.CurrentMain.familyCauchyAlgebra line 599
  84. lemma OAI.CurrentMain.familyCauchyAlgebra_isClosed line 610
  85. instance OAI.CurrentMain.familyCauchy_complete line 629
  86. instance OAI.CurrentMain.familyCauchy_cstar line 632
  87. def OAI.CurrentMain.familyCauchyNullIdeal line 634
  88. abbrev OAI.CurrentMain.UniformTracialCompletion line 644
  89. instance OAI.Pureness.ClosedStarIdeal.quotientOrder line 654
  90. instance OAI.Pureness.ClosedStarIdeal.quotientStarOrdered line 657
  91. lemma OAI.Pureness.ClosedStarIdeal.trace_congr line 668
  92. def OAI.Pureness.ClosedStarIdeal.descendedValue line 675
  93. lemma OAI.Pureness.ClosedStarIdeal.descendedValue_map line 679
  94. def OAI.Pureness.ClosedStarIdeal.descendedLinear line 681
  95. lemma OAI.Pureness.ClosedStarIdeal.descendedLinear_square_nonneg line 692
  96. def OAI.Pureness.ClosedStarIdeal.descendedTrace line 699
  97. lemma OAI.CurrentMain.bounded_ultrafilter_tendsto line 731
  98. instance OAI.CurrentMain.boundedFamilyProductOrder line 747
  99. instance OAI.CurrentMain.boundedFamilyProductStarOrdered line 750
  100. def OAI.CurrentMain.ultraTraceValue line 753
  101. lemma OAI.CurrentMain.ultraTraceValue_tendsto line 758
  102. lemma OAI.CurrentMain.ultraTraceValue_add line 765
  103. lemma OAI.CurrentMain.ultraTraceValue_smul line 771
  104. def OAI.CurrentMain.ultraTraceLinear line 777
  105. def OAI.CurrentMain.boundedFamilyEval line 782
  106. def OAI.CurrentMain.ultraTrace line 791
  107. abbrev OAI.CurrentMain.FamilyUltrapower line 817
  108. lemma OAI.CurrentMain.ultraTrace_null line 819
  109. def OAI.CurrentMain.familyLimitTrace line 830
  110. def OAI.CurrentMain.pullbackTrace line 848
  111. lemma OAI.CurrentMain.isFamilyCauchy_iff line 865
  112. lemma OAI.CurrentMain.cauchy_trace_values line 874
  113. instance OAI.CurrentMain.familyCauchyOrder line 884
  114. instance OAI.CurrentMain.familyCauchyStarOrdered line 887
  115. def OAI.CurrentMain.cauchyTrace line 890
  116. lemma OAI.CurrentMain.cauchyTrace_tendsto line 894
  117. lemma OAI.CurrentMain.cauchyTrace_null line 903
  118. def OAI.CurrentMain.completionTrace line 914
  119. def OAI.CurrentMain.boundedFamilyConstant line 917
  120. def OAI.CurrentMain.cauchyConstant line 920
  121. def OAI.CurrentMain.completionMap line 923
  122. instance OAI.CurrentMain.completionNontrivial line 944
  123. def OAI.CurrentMain.familyUltrapowerMap line 962
  124. def OAI.Pureness.TopologicallySimple line 981
  125. def OAI.CurrentMain.StablyFinite line 992
  126. def OAI.CurrentMain.UniformPropertyGammaAt line 996