OAI/Analysis/FactorGeneration/TraceHilbert.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

A separate type with the constructed trace inner product. Its norm is the trace two-norm; the original concrete algebra retains its operator norm. Lean's inner product is linear in the second argument.

  1. def OAI.Generator.Tracial.TraceFreePreHilbert line 20

    Source documentation

    Algebraic type copy indexed by the original factor hypotheses.

    def TraceFreePreHilbert
(_hfactor : ∀ c : M.toStarSubalgebra,
  (∀ a : M.toStarSubalgebra, a*c=c*a) → ∃ z : ℂ, c=z • (1 : M.toStarSubalgebra))
(_hdiff : ∀ p : M.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
  ∃ q : M.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p*q=q ∧ q*p=q)
(_hfinite : ∀ a : M.toStarSubalgebra, star a*a=1 → a*star a=1)
(_hunit : (1 : M.toStarSubalgebra) ≠ 0)
    : Type _ := M.toStarSubalgebra
…
  2. instance OAI.Generator.Tracial.traceFreePreHilbertRing line 42
  3. instance OAI.Generator.Tracial.traceFreePreHilbertAlgebra line 43
  4. instance OAI.Generator.Tracial.traceFreePreHilbertStarRing line 45
  5. instance OAI.Generator.Tracial.traceFreePreHilbertStarModule line 47
  6. def OAI.Generator.Tracial.traceFreeCopy line 51

    Source documentation

    Algebraic identification only: it does not identify the two norms.

    def traceFreeCopy : M.toStarSubalgebra ≃⋆ₐ[ℂ] E :=
…
  7. def OAI.Generator.Tracial.traceFreeInnerCore line 56
  8. instance OAI.Generator.Tracial.traceFreePreHilbertNormedAddCommGroup line 74
  9. instance OAI.Generator.Tracial.traceFreePreHilbertInnerProductSpace line 76
  10. theorem OAI.Generator.Tracial.traceFreeCopy_inner line 79
  11. theorem OAI.Generator.Tracial.traceFreeCopy_norm_sq line 82
  12. abbrev OAI.Generator.Tracial.TraceFreeHilbert line 88

    Source documentation

    The actual Hilbert completion; no representation is supplied.

    abbrev TraceFreeHilbert := UniformSpace.Completion E
  13. def OAI.Generator.Tracial.traceFreeInclusion line 90
  14. theorem OAI.Generator.Tracial.traceFreeInclusion_inner line 93
  15. theorem OAI.Generator.Tracial.traceFreeInclusion_denseRange line 98
  16. theorem OAI.Generator.Tracial.traceFreeTrace_mul_square_le line 129
  17. theorem OAI.Generator.Tracial.traceFreeCopy_mul_norm_le line 143
  18. theorem OAI.Generator.Tracial.traceFreeInclusion_mul_norm_le line 149
  19. def OAI.Generator.Tracial.traceFreeLeftOnPreHilbert line 182
  20. theorem OAI.Generator.Tracial.traceFreeLeftOnPreHilbert_apply line 188
  21. def OAI.Generator.Tracial.traceFreeLeftAction line 191
  22. theorem OAI.Generator.Tracial.traceFreeLeftAction_inclusion line 197
  23. theorem OAI.Generator.Tracial.traceFreeLeftAction_coe line 204
  24. theorem OAI.Generator.Tracial.traceFreeLeftAction_norm_le line 208
  25. theorem OAI.Generator.Tracial.traceFreeLeftAction_one line 217
  26. theorem OAI.Generator.Tracial.traceFreeLeftAction_mul line 223
  27. theorem OAI.Generator.Tracial.traceFreeLeftAction_add line 230
  28. theorem OAI.Generator.Tracial.traceFreeLeftAction_smul line 237
  29. theorem OAI.Generator.Tracial.traceFreeLeftAction_zero line 248
  30. theorem OAI.Generator.Tracial.traceFreeLeftAction_star line 254
  31. def OAI.Generator.Tracial.traceFreeHilbertAction line 267
  32. theorem OAI.Generator.Tracial.traceFreeHilbertAction_inclusion line 280
  33. def OAI.Generator.Tracial.traceFreeHilbertVector line 285
  34. theorem OAI.Generator.Tracial.traceFreeHilbertAction_vector line 289
  35. theorem OAI.Generator.Tracial.traceFreeHilbertVector_norm line 294
  36. theorem OAI.Generator.Tracial.traceFreeHilbertAction_injective line 303
  37. theorem OAI.Generator.Tracial.traceFreeHilbertAction_norm line 309
  38. theorem OAI.Generator.Tracial.traceFreeHilbertAction_trace line 312
  39. theorem OAI.Generator.Tracial.traceFreeHilbertAction_cyclic line 317
  40. theorem OAI.Generator.Tracial.exists_traceFreeHilbert_representation line 324
  41. theorem OAI.Generator.Tracial.traceFreeCopy_star_norm line 364
  42. theorem OAI.Generator.Tracial.traceFreeCopy_mul_norm_le_right line 369
  43. def OAI.Generator.Tracial.traceFreeRightOnPreHilbert line 375
  44. def OAI.Generator.Tracial.traceFreeRightAction line 381
  45. theorem OAI.Generator.Tracial.traceFreeRightAction_inclusion line 387
  46. theorem OAI.Generator.Tracial.traceFreeRightAction_coe line 394
  47. theorem OAI.Generator.Tracial.traceFreeLeftRight_commute line 398
  48. theorem OAI.Generator.Tracial.traceFreeRightAction_vector line 406
  49. def OAI.Generator.Tracial.traceFreeHilbertClosure line 442

    Source documentation

    The bicommutant is a von Neumann algebra; no image-closedness is assumed.

    def traceFreeHilbertClosure : VonNeumannAlgebra K where
…
  50. theorem OAI.Generator.Tracial.traceFreeHilbertClosure_mem_iff line 456
  51. theorem OAI.Generator.Tracial.traceFreeHilbertAction_mem_closure line 463
  52. def OAI.Generator.Tracial.traceFreeHilbertIntoClosure line 468
  53. theorem OAI.Generator.Tracial.traceFreeHilbertClosure_strong_net line 473
  54. theorem OAI.Generator.Tracial.traceFreeHilbertClosure_right_commute line 482
  55. theorem OAI.Generator.Tracial.traceFreeHilbertClosure_separating line 489
  56. theorem OAI.Generator.Tracial.traceFreeHilbertClosure_trace_commute_copy line 501
  57. theorem OAI.Generator.Tracial.traceFreeHilbertClosure_trace_commute line 514
  58. def OAI.Generator.Tracial.traceFreeHilbertClosureTrace line 525

    Source documentation

    Output tracial representation on the actual bicommutant. Its fields are proved above; no TracialRepresentation is an input to this construction.

    def traceFreeHilbertClosureTrace : UltrapowerBridge.TracialRepresentation N where
…

    Mentions: OAI.UltrapowerBridge.TracialRepresentation

  59. theorem OAI.Generator.Tracial.traceFreeHilbertClosureTrace_copy line 531
  60. theorem OAI.Generator.Tracial.traceFreeHilbertClosureTrace_cyclic line 535
  61. def OAI.Generator.Tracial.traceFreeHilbertActionCLM line 569
  62. def OAI.Generator.Tracial.traceFreeHilbertCoefficient line 575
  63. theorem OAI.Generator.Tracial.traceFreeHilbertCoefficient_apply line 579
  64. theorem OAI.Generator.Tracial.traceFreeHilbertCoefficient_continuous line 582
  65. theorem OAI.Generator.Tracial.traceFreeHilbertCoefficient_copy_ball_continuous line 587
  66. theorem OAI.Generator.Tracial.traceFreeHilbertCoefficient_ball_continuous line 604
  67. def OAI.Generator.Tracial.traceFreeHilbertBallMap line 619
  68. theorem OAI.Generator.Tracial.traceFreeHilbertBallMap_continuous line 622
  69. theorem OAI.Generator.Tracial.traceFreeHilbertBallMap_injective line 627
  70. theorem OAI.Generator.Tracial.traceFreeHilbertBallMap_isClosedEmbedding line 635
  71. def OAI.Generator.Tracial.traceFreeHilbertWeakBall line 642
  72. theorem OAI.Generator.Tracial.traceFreeHilbertWeakBall_eq_range line 645
  73. theorem OAI.Generator.Tracial.traceFreeHilbertWeakBall_isCompact line 655
  74. theorem OAI.Generator.Tracial.traceFreeHilbertWeakBall_isClosed line 662