PositiveKernelMatrices.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Positive finite Gram matrices and the coefficient inequality needed for the Hilbert-space construction of completely positive maps.

def OAI.BoundedHochschild.KadisonRingrose.algebraGram line 19
Source documentation
The Gram matrix of a finite family in the algebra.
```
def algebraGram (a : I → M) : CStarMatrix I I M := fun i j => star (a i) * a j
```
lemma OAI.BoundedHochschild.KadisonRingrose.algebraGram_nonneg line 21
lemma OAI.BoundedHochschild.KadisonRingrose.weighted_algebraGram_nonneg line 39
Source documentation
Inserting any positive algebra element still gives a positive matrix.
```
lemma weighted_algebraGram_nonneg (a : I → M) (q : M) (hq : 0 ≤ q) :
    0 ≤ CStarMatrix.ofMatrix (fun i j => star (a i) * q * a j) := by
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.algebraGram_left_le line 57
Source documentation
Left multiplication is bounded in every one of these positive kernels.
```
lemma algebraGram_left_le (a : I → M) (b : M) :
    algebraGram (fun i => b * a i) ≤ ‖b‖ ^ 2 • algebraGram a := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.algebraGram
lemma OAI.BoundedHochschild.KadisonRingrose.operatorMatrix_quadratic_nonneg line 74
Source documentation
Positivity of operator matrices implies positivity of their finite quadratic forms, with arbitrary Hilbert-space vectors.
```
lemma operatorMatrix_quadratic_nonneg
    (A : CStarMatrix I I (H →L[ℂ] H)) (hA : 0 ≤ A) (ξ : I → H) :
    0 ≤ ∑ i, ∑ j, inner ℂ (ξ i) (A i j (ξ j)) := by
…
```

lemma OAI.BoundedHochschild.KadisonRingrose.completelyPositive_kernel_nonneg line 86

Source documentation

A completely positive map produces positive finite coefficient kernels.

lemma completelyPositive_kernel_nonneg
    (φ : CompletelyPositiveMap M (H →L[ℂ] H)) (a : I → M) (ξ : I → H) :
    0 ≤ ∑ i, ∑ j, inner ℂ (ξ i) (φ (star (a i) * a j) (ξ j)) := by
…