OAI/Analysis/BoundedHochschild/StinespringKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The positive scalar kernel of an operator-valued completely positive map. No normality or separability assumption is required.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.completelyPositive_star line 17
  2. def OAI.BoundedHochschild.KadisonRingrose.stinespringKernel line 26

    Source documentation

    The coefficient kernel on formal algebra-vector pairs.

    def stinespringKernel (φ : CompletelyPositiveMap M (H →L[ℂ] H)) :
    Matrix (M × H) (M × H) ℂ :=
…
  3. lemma OAI.BoundedHochschild.KadisonRingrose.stinespringKernel_hermitian line 30
  4. lemma OAI.BoundedHochschild.KadisonRingrose.kernelForm_coefficients line 40
  5. theorem OAI.BoundedHochschild.KadisonRingrose.stinespringKernel_positive line 58

    Source documentation

    Complete positivity makes all finite formal-vector norms nonnegative in this construction.

    theorem stinespringKernel_positive (φ : CompletelyPositiveMap M (H →L[ℂ] H)) :
    (stinespringKernel φ).PosSemidef := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.stinespringKernel

  6. abbrev OAI.BoundedHochschild.KadisonRingrose.StinespringSpace line 70

    Source documentation

    The auxiliary Hilbert space of a completely positive map.

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