OAI/Analysis/KadisonKastler/HilbertCompression.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.finiteDiagonalMap line 26

   Source documentation

   Applying a continuous linear map in each coordinate of a finite Hilbert sum.

   def finiteDiagonalMap (V : H →L[ℂ] K) (n : ℕ) :
       Generator.FiniteHilbert (Fin n) H →L[ℂ] Generator.FiniteHilbert (Fin n) K :=
   …

   Mentions: OAI.Generator.FiniteHilbert

2. theorem OAI.KadisonKastler.finiteDiagonalMap_apply line 33
3. theorem OAI.KadisonKastler.finiteDiagonalMap_adjoint line 37
4. def OAI.KadisonKastler.hilbertCompression line 48

   Source documentation

   Compression by a bounded operator between two different Hilbert spaces.

   def hilbertCompression (V : H →L[ℂ] K) : (K →L[ℂ] K) →ₗ[ℂ] (H →L[ℂ] H) where
   …

5. def OAI.KadisonKastler.hilbertCompressionCP line 54

   Source documentation

   Compression is completely positive at every finite matrix size.

   def hilbertCompressionCP (V : H →L[ℂ] K) : (K →L[ℂ] K) →CP (H →L[ℂ] H) where
   …