StinespringBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The bounded left action on the positive-kernel construction.

def OAI.BoundedHochschild.KadisonRingrose.operatorMatrixVectorFunctional line 17
Source documentation
The quadratic form of a finite operator matrix, as a positive functional.
```
def operatorMatrixVectorFunctional (ξ : I → H) :
    CStarMatrix I I (H →L[ℂ] H) →ₚ[ℂ] ℂ :=
…
```
def OAI.BoundedHochschild.KadisonRingrose.cpMatrixVectorFunctional line 31
Source documentation
Applying a completely positive map entrywise before a vector quadratic form yields a positive functional on the original matrix algebra.
```
def cpMatrixVectorFunctional (φ : CompletelyPositiveMap M (H →L[ℂ] H)) (ξ : I → H) :
    CStarMatrix I I M →ₚ[ℂ] ℂ :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.completelyPositive_kernel_left_bound line 37