OAI/Analysis/TracialSplitting/ChallengeDefinitions.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

The final claim constructs the tracial quotients and states the original gamma assertion. Analysis.TracialSplitting.Challenge.main_iff_original verifies statement preservation.

  1. structure OAI.Pureness.CStarAlgebraNorm line 18

    Also declared: ComparatorChallenges/UniformGamma.lean:18 (same declaration text).

  2. structure OAI.Pureness.TracialState line 22

    Also declared: ComparatorChallenges/UniformGamma.lean:22 (same declaration text).

  3. structure OAI.Pureness.ClosedStarIdeal line 27

    Also declared: ComparatorChallenges/UniformGamma.lean:27 (same declaration text).

  4. abbrev OAI.ComparatorModel.Pureness.CStarAlgebraNorm line 44

    Also declared: ComparatorChallenges/UniformGamma.lean:42 (same declaration text).

  5. def OAI.ComparatorModel.Pureness.IsNuclear line 46

    Also declared: ComparatorChallenges/UniformGamma.lean:44 (same declaration text).

  6. abbrev OAI.ComparatorModel.Pureness.TracialState line 49

    Also declared: ComparatorChallenges/UniformGamma.lean:47 (same declaration text).

  7. def OAI.ComparatorModel.CurrentMain.RealRankZero line 59

    Also declared: ComparatorChallenges/UniformGamma.lean:57 (same declaration text).

  8. def OAI.ComparatorModel.CurrentMain.traceTwoNorm line 63

    Also declared: ComparatorChallenges/UniformGamma.lean:61 (same declaration text).

  9. abbrev OAI.ComparatorModel.Pureness.ClosedStarIdeal line 75

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:73 (different declaration text). Qualify references as OAI.ComparatorModel.Pureness.ClosedStarIdeal@path.

  10. abbrev OAI.ComparatorModel.Pureness.ClosedStarIdeal.Quotient line 81

    Also declared: ComparatorChallenges/UniformGamma.lean:81 (same declaration text).

  11. def OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientMap line 83

    Also declared: ComparatorChallenges/UniformGamma.lean:83 (same declaration text).

  12. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientStar line 85

    Also declared: ComparatorChallenges/UniformGamma.lean:85 (same declaration text).

  13. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientStarRing line 93

    Also declared: ComparatorChallenges/UniformGamma.lean:93 (same declaration text).

  14. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientStarModule line 98

    Also declared: ComparatorChallenges/UniformGamma.lean:98 (same declaration text).

  15. abbrev OAI.ComparatorModel.Pureness.ClosedStarIdeal.idealSubmodule line 101

    Also declared: ComparatorChallenges/UniformGamma.lean:101 (same declaration text).

  16. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.idealSubmodule_closed line 104

    Also declared: ComparatorChallenges/UniformGamma.lean:104 (same declaration text).

  17. def OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientLinearEquiv line 112

    Also declared: ComparatorChallenges/UniformGamma.lean:112 (same declaration text).

  18. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientNormedAddCommGroup line 116

    Also declared: ComparatorChallenges/UniformGamma.lean:116 (same declaration text).

  19. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientNormedSpace line 120

    Also declared: ComparatorChallenges/UniformGamma.lean:120 (same declaration text).

  20. def OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientNormEquiv line 123

    Also declared: ComparatorChallenges/UniformGamma.lean:123 (same declaration text).

  21. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientCompleteSpace line 128

    Also declared: ComparatorChallenges/UniformGamma.lean:128 (same declaration text).

  22. class OAI.ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction line 131

    Also declared: ComparatorChallenges/UniformGamma.lean:131 (same declaration text).

  23. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientNormedRing line 141

    Also declared: ComparatorChallenges/UniformGamma.lean:141 (same declaration text).

  24. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientNormedAlgebra line 145

    Also declared: ComparatorChallenges/UniformGamma.lean:145 (same declaration text).

  25. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientNormedStarGroup line 148

    Also declared: ComparatorChallenges/UniformGamma.lean:148 (same declaration text).

  26. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientCStarAlgebra line 167

    Also declared: ComparatorChallenges/UniformGamma.lean:163 (same declaration text).

  27. def OAI.ComparatorModel.CurrentMain.familyTwoNorm line 184

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:182 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.familyTwoNorm@path.

  28. instance OAI.ComparatorModel.CurrentMain.boundedFamilyProductCStar line 194

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:192 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.boundedFamilyProductCStar@path.

  29. def OAI.ComparatorModel.CurrentMain.IsFamilyNull line 203

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:201 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.IsFamilyNull@path.

  30. class OAI.ComparatorModel.CurrentMain.NullConstruction line 206

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:204 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.NullConstruction@path.

  31. def OAI.ComparatorModel.CurrentMain.familyNullTwoSided line 229

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:227 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.familyNullTwoSided@path.

  32. def OAI.ComparatorModel.CurrentMain.familyNullIdeal line 239

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:237 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.familyNullIdeal@path.

  33. def OAI.ComparatorModel.CurrentMain.IsFamilyCauchy line 261

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:259 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.IsFamilyCauchy@path.

  34. class OAI.ComparatorModel.CurrentMain.CauchyConstruction line 264

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:262 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.CauchyConstruction@path.

  35. def OAI.ComparatorModel.CurrentMain.familyCauchyAlgebra line 285

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:283 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.familyCauchyAlgebra@path.

  36. instance OAI.ComparatorModel.CurrentMain.familyCauchy_complete line 296

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:294 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.familyCauchy_complete@path.

  37. instance OAI.ComparatorModel.CurrentMain.familyCauchy_cstar line 299

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:297 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.familyCauchy_cstar@path.

  38. def OAI.ComparatorModel.CurrentMain.familyCauchyNullIdeal line 301

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:299 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.familyCauchyNullIdeal@path.

  39. abbrev OAI.ComparatorModel.CurrentMain.UniformTracialCompletion line 311

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:309 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.UniformTracialCompletion@path.

  40. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientOrder line 323

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:321 (different declaration text). Qualify references as OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientOrder@path.

  41. instance OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientStarOrdered line 326

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:324 (different declaration text). Qualify references as OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientStarOrdered@path.

  42. def OAI.ComparatorModel.Pureness.ClosedStarIdeal.descendedValue line 333

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:331 (different declaration text). Qualify references as OAI.ComparatorModel.Pureness.ClosedStarIdeal.descendedValue@path.

  43. def OAI.ComparatorModel.Pureness.ClosedStarIdeal.descendedLinear line 341

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:339 (different declaration text). Qualify references as OAI.ComparatorModel.Pureness.ClosedStarIdeal.descendedLinear@path.

  44. def OAI.ComparatorModel.Pureness.ClosedStarIdeal.descendedTrace line 346

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:344 (different declaration text). Qualify references as OAI.ComparatorModel.Pureness.ClosedStarIdeal.descendedTrace@path.

  45. instance OAI.ComparatorModel.CurrentMain.boundedFamilyProductOrder line 378

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:374 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.boundedFamilyProductOrder@path.

  46. instance OAI.ComparatorModel.CurrentMain.boundedFamilyProductStarOrdered line 381

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:377 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.boundedFamilyProductStarOrdered@path.

  47. def OAI.ComparatorModel.CurrentMain.ultraTraceValue line 384

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:380 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.ultraTraceValue@path.

  48. class OAI.ComparatorModel.CurrentMain.LimitConstruction line 387

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:383 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.LimitConstruction@path.

  49. def OAI.ComparatorModel.CurrentMain.ultraTraceLinear line 394

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:390 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.ultraTraceLinear@path.

  50. def OAI.ComparatorModel.CurrentMain.boundedFamilyEval line 405

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:401 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.boundedFamilyEval@path.

  51. def OAI.ComparatorModel.CurrentMain.ultraTrace line 414

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:410 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.ultraTrace@path.

  52. abbrev OAI.ComparatorModel.CurrentMain.FamilyUltrapower line 442

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:440 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.FamilyUltrapower@path.

  53. class OAI.ComparatorModel.CurrentMain.TraceConstruction line 444

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:442 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.TraceConstruction@path.

  54. def OAI.ComparatorModel.CurrentMain.familyLimitTrace line 452

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:450 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.familyLimitTrace@path.

  55. def OAI.ComparatorModel.CurrentMain.pullbackTrace line 478

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:470 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.pullbackTrace@path.

  56. instance OAI.ComparatorModel.CurrentMain.familyCauchyOrder line 495

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:489 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.familyCauchyOrder@path.

  57. instance OAI.ComparatorModel.CurrentMain.familyCauchyStarOrdered line 498

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:492 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.familyCauchyStarOrdered@path.

  58. def OAI.ComparatorModel.CurrentMain.cauchyTrace line 501

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:495 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.cauchyTrace@path.

  59. def OAI.ComparatorModel.CurrentMain.completionTrace line 505

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:499 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.completionTrace@path.

  60. def OAI.ComparatorModel.CurrentMain.boundedFamilyConstant line 515

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:509 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.boundedFamilyConstant@path.

  61. instance OAI.ComparatorModel.CurrentMain.completionNontrivial line 532

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:512 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.completionNontrivial@path.

  62. def OAI.ComparatorModel.CurrentMain.familyUltrapowerMap line 552

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:528 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.familyUltrapowerMap@path.

  63. def OAI.ComparatorModel.Pureness.TopologicallySimple line 573

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:549 (different declaration text). Qualify references as OAI.ComparatorModel.Pureness.TopologicallySimple@path.

  64. def OAI.ComparatorModel.CurrentMain.StablyFinite line 586

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:560 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.StablyFinite@path.

  65. def OAI.ComparatorModel.CurrentMain.UniformPropertyGammaAt line 590

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:564 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.UniformPropertyGammaAt@path.

  66. def OAI.ComparatorModel.CurrentMain.Statement line 604

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:580 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.Statement@path.

  67. def OAI.ComparatorModel.CurrentMain.MainClaim line 620

    Distinct definitions of this name: ComparatorChallenges/UniformGamma.lean:592 (different declaration text). Qualify references as OAI.ComparatorModel.CurrentMain.MainClaim@path.