CompletelyPositive.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Contractivity of unital completely positive maps

The proofs use Mathlib's completely positive maps and the spectral order on C⋆-matrices. The Schwarz inequality is obtained from positivity of a two-by-two Gram matrix.

theorem OAI.KadisonKastler.cstarMatrix_diagonal_nonneg line 28

Source documentation

Every diagonal entry of a positive C⋆-matrix is positive.

theorem cstarMatrix_diagonal_nonneg {n : Type*} [Fintype n] [DecidableEq n]
    (M : CStarMatrix n n A) (hM : 0 ≤ M) (i : n) : 0 ≤ M i i := by
…

def OAI.KadisonKastler.schwarzGram line 40
Source documentation
The positive Gram matrix used for the Schwarz inequality.
```
def schwarzGram (a : A) : CStarMatrix (Fin 2) (Fin 2) A :=
…
```
theorem OAI.KadisonKastler.schwarzGram_nonneg line 43
theorem OAI.KadisonKastler.completelyPositive_map_star line 54
Source documentation
Complete positivity already forces preservation of the involution.
```
theorem completelyPositive_map_star (φ : A →CP B) (a : A) :
    φ (star a) = star (φ a) := by
…
```
theorem OAI.KadisonKastler.unital_completelyPositive_schwarz line 63
Source documentation
Kadison–Schwarz for a unital completely positive map.
```
theorem unital_completelyPositive_schwarz (φ : A →CP B) (hφ : φ 1 = 1) (a : A) :
    star (φ a) * φ a ≤ φ (star a * a) := by
…
```
theorem OAI.KadisonKastler.unital_completelyPositive_norm_le line 79
Source documentation
A unital completely positive map is contractive.
```
theorem unital_completelyPositive_norm_le (φ : A →CP B) (hφ : φ 1 = 1) (a : A) :
    ‖φ a‖ ≤ ‖a‖ := by
…
```
def OAI.KadisonKastler.unitalCompletelyPositiveToContinuousLinearMap line 93
Source documentation
A unital completely positive map, bundled for the closed-range argument.
```
def unitalCompletelyPositiveToContinuousLinearMap (φ : A →CP B) (hφ : φ 1 = 1) :
    A →L[ℂ] B :=
…
```
theorem OAI.KadisonKastler.unitalCompletelyPositiveToContinuousLinearMap_apply line 100

def OAI.KadisonKastler.cstarMatrixComp line 105

Source documentation

Flattening blocks of C⋆-matrices is a star-algebra equivalence.

def cstarMatrixComp (I J : Type*) [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] :
    CStarMatrix I I (CStarMatrix J J A) ≃⋆ₐ[ℂ] CStarMatrix (I × J) (I × J) A :=
…

def OAI.KadisonKastler.completelyPositiveAmplification line 114
Source documentation
A matrix amplification of a completely positive map is completely positive.
```
def completelyPositiveAmplification (φ : A →CP B) (n : Type*) [Fintype n] [DecidableEq n] :
    CStarMatrix n n A →CP CStarMatrix n n B where
…
```

theorem OAI.KadisonKastler.unital_completelyPositive_matrix_norm_le line 129

Source documentation

Every square amplification of a unital completely positive map is contractive.

theorem unital_completelyPositive_matrix_norm_le (φ : A →CP B) (hφ : φ 1 = 1)
    {n : Type*} [Fintype n] [DecidableEq n] (X : CStarMatrix n n A) :
    ‖CStarMatrix.mapₗ φ.toLinearMap X‖ ≤ ‖X‖ := by
…

theorem OAI.KadisonKastler.unital_completelyPositive_square_norm_le line 142
theorem OAI.KadisonKastler.unital_completelyPositive_completelyBoundedBy line 149
Source documentation
Unital complete positivity implies complete contractivity with the rectangular convention used in the multiplication-correction argument.
```
theorem unital_completelyPositive_completelyBoundedBy (φ : A →CP B) (hφ : φ 1 = 1) :
    CompletelyBoundedBy φ.toLinearMap 1 := by
…
```
Mentions: OAI.KadisonKastler.CompletelyBoundedBy