OAI/Analysis/BoundedHochschild/PositiveKernelSpace.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The Hilbert-space construction for a positive scalar kernel, specialized later to the coefficient kernel of a completely positive map.

  1. def OAI.BoundedHochschild.KadisonRingrose.kernelForm line 17

    Source documentation

    The finite coefficient pairing of a scalar kernel.

    def kernelForm (K : Matrix I I ℂ) (x y : I →₀ ℂ) : ℂ :=
…
  2. lemma OAI.BoundedHochschild.KadisonRingrose.kernelForm_conj_symm line 20
  3. lemma OAI.BoundedHochschild.KadisonRingrose.kernelForm_add_left line 32
  4. lemma OAI.BoundedHochschild.KadisonRingrose.kernelForm_smul_left line 42
  5. lemma OAI.BoundedHochschild.KadisonRingrose.kernelForm_nonneg line 54
  6. def OAI.BoundedHochschild.KadisonRingrose.PositiveKernelPreSpace line 59

    Source documentation

    A type copy keeps the kernel seminorm separate from any norm on the free coefficient space. Its completion automatically removes the null vectors.

    def PositiveKernelPreSpace (K : Matrix I I ℂ) (_hK : K.PosSemidef) : Type _ := I →₀ ℂ
  7. instance OAI.BoundedHochschild.KadisonRingrose.kernelPreAddCommGroup line 61
  8. instance OAI.BoundedHochschild.KadisonRingrose.kernelPreModule line 64
  9. abbrev OAI.BoundedHochschild.KadisonRingrose.positiveKernelCore line 67
  10. instance OAI.BoundedHochschild.KadisonRingrose.kernelPreSeminormedAddCommGroup line 75
  11. instance OAI.BoundedHochschild.KadisonRingrose.kernelPreInnerProductSpace line 79
  12. abbrev OAI.BoundedHochschild.KadisonRingrose.PositiveKernelHilbert line 84

    Source documentation

    The separated Hilbert completion of the finite kernel vectors.

    abbrev PositiveKernelHilbert (K : Matrix I I ℂ) (hK : K.PosSemidef) :=
…