OAI/Analysis/BoundedHochschild/NormalGNSRepresentation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Restriction to normal vectors gives a faithful normal representation for the specified predual, without a faithful scalar state assumption.

  1. def OAI.BoundedHochschild.KadisonRingrose.NormalGNS line 21
  2. instance OAI.BoundedHochschild.KadisonRingrose.normalGNSNormedAddCommGroup line 24
  3. instance OAI.BoundedHochschild.KadisonRingrose.normalGNSInnerProductSpace line 28
  4. instance OAI.BoundedHochschild.KadisonRingrose.normalGNSCompleteSpace line 32
  5. instance OAI.BoundedHochschild.KadisonRingrose.normalGNSCoe line 36
  6. def OAI.BoundedHochschild.KadisonRingrose.normalGNSOperator line 39
  7. lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSOperator_coe line 44
  8. lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSOperator_zero line 48
  9. lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSOperator_one line 56
  10. lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSOperator_add line 64
  11. lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSOperator_mul line 73
  12. lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSOperator_commutes line 83
  13. lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSOperator_star line 92
  14. def OAI.BoundedHochschild.KadisonRingrose.normalGNSRepresentation line 102
  15. lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSRepresentation_coe line 112
  16. lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSRepresentation_coefficients line 116
  17. lemma OAI.BoundedHochschild.KadisonRingrose.universalGNS_positive_coefficient line 122

    Source documentation

    Every positive cyclic coefficient occurs in the universal representation.

    lemma universalGNS_positive_coefficient (ψ : M →ₚ[ℂ] ℂ) :
    ∀ a : M, coefficient universalGNSRepresentation
      (lp.single 2 ψ (positiveVector ψ)) (lp.single 2 ψ (positiveVector ψ)) a = ψ a := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.universalGNSRepresentation

  18. theorem OAI.BoundedHochschild.KadisonRingrose.normalGNSRepresentation_injective line 133

    Source documentation

    The normal subrepresentation remains faithful even when there is no faithful normal scalar state.

    theorem normalGNSRepresentation_injective (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    Function.Injective (normalGNSRepresentation e) := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.normalGNSRepresentation

  19. theorem OAI.BoundedHochschild.KadisonRingrose.normalGNSRepresentation_norm line 165