OAI/Analysis/BoundedHochschild/StinespringStar.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The adjoint and scalar identities of the positive-kernel representation.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringOperator_star line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringOperator_smul line 36
  3. def OAI.BoundedHochschild.KadisonRingrose.stinespringRepresentation line 51

    Source documentation

    The genuine unital star representation on the positive-kernel Hilbert space associated to a completely positive map.

    def stinespringRepresentation (φ : CompletelyPositiveMap M (H →L[ℂ] H)) :
    M →⋆ₐ[ℂ] (StinespringSpace φ →L[ℂ] StinespringSpace φ) where
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.StinespringSpace