OAI/Analysis/BoundedHochschild/StinespringLeftAction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Left multiplication on the auxiliary positive-kernel Hilbert space.

  1. abbrev OAI.BoundedHochschild.KadisonRingrose.StinespringPreSpace line 17
  2. def OAI.BoundedHochschild.KadisonRingrose.stinespringLeftLabel line 20
  3. def OAI.BoundedHochschild.KadisonRingrose.stinespringShift line 22
  4. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringShift_one line 26
  5. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringShift_mul line 35
  6. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringLeft_bound line 46
  7. def OAI.BoundedHochschild.KadisonRingrose.stinespringPreOperator line 60

    Source documentation

    The bounded left action before completing the kernel space.

    def stinespringPreOperator (φ : CompletelyPositiveMap M (H →L[ℂ] H)) (b : M) :
    StinespringPreSpace φ →L[ℂ] StinespringPreSpace φ :=
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.StinespringPreSpace

  8. def OAI.BoundedHochschild.KadisonRingrose.stinespringOperator line 66

    Source documentation

    The induced action on the separated Hilbert completion.

    def stinespringOperator (φ : CompletelyPositiveMap M (H →L[ℂ] H)) (b : M) :
    StinespringSpace φ →L[ℂ] StinespringSpace φ :=
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.StinespringSpace

  9. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringOperator_coe line 70