OAI/Analysis/BoundedHochschild/StinespringEmbedding.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The bounded vector map and factorization of a completely positive map.

  1. def OAI.BoundedHochschild.KadisonRingrose.stinespringPreVector line 17
  2. def OAI.BoundedHochschild.KadisonRingrose.stinespringVector line 20
  3. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringVector_pairing line 23
  4. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringVector_add line 32
  5. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringVector_smul line 42
  6. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringVector_norm_sq line 55
  7. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringVector_bound line 63
  8. def OAI.BoundedHochschild.KadisonRingrose.stinespringEmbedding line 75

    Source documentation

    The bounded map sending a vector to its unit-labelled kernel vector.

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

    Mentions: OAI.BoundedHochschild.KadisonRingrose.StinespringSpace

  9. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringEmbedding_apply line 83
  10. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringVector_coefficient line 86
  11. theorem OAI.BoundedHochschild.KadisonRingrose.stinespring_factorization line 97

    Source documentation

    Stinespring factorization on the constructed auxiliary Hilbert space.

    theorem stinespring_factorization (φ : CompletelyPositiveMap M (H →L[ℂ] H)) (a : M) :
    φ a = (stinespringEmbedding φ).adjoint.comp
      ((stinespringRepresentation φ a).comp (stinespringEmbedding φ)) := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.stinespringEmbedding, OAI.BoundedHochschild.KadisonRingrose.stinespringRepresentation