CStarMatrixPadding.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Isometric zero padding of C-star matrices

Padding along an injection is a nonunital star algebra monomorphism. Its isometry follows from the C-star norm theorem, and its represented action is the concrete zero extension on finite Hilbert sums.

def OAI.KadisonSimilarity.matrixZeroPadding line 22
Source documentation
A square matrix with zero entries outside the embedded index set.
```
def matrixZeroPadding (e : Fin r ↪ Fin m) (X : Matrix (Fin r) (Fin r) A) :
    Matrix (Fin m) (Fin m) A :=
…
```
theorem OAI.KadisonSimilarity.matrixZeroPadding_apply_image line 27
theorem OAI.KadisonSimilarity.matrixZeroPadding_not_mem_left line 32
theorem OAI.KadisonSimilarity.matrixZeroPadding_not_mem_right line 38
theorem OAI.KadisonSimilarity.matrixPadding_sum line 44
theorem OAI.KadisonSimilarity.matrixZeroPadding_mul line 58
theorem OAI.KadisonSimilarity.matrixZeroPadding_star line 82
def OAI.KadisonSimilarity.matrixZeroPaddingHom line 98
Source documentation
The algebraic zero-padding map, before assigning the C-star matrix norm.
```
def matrixZeroPaddingHom (e : Fin r ↪ Fin m) :
    Matrix (Fin r) (Fin r) A →⋆ₙₐ[ℂ] Matrix (Fin m) (Fin m) A where
…
```

def OAI.KadisonSimilarity.cstarMatrixPadding line 128

Source documentation

Zero padding with the actual C-star matrix norms.

def cstarMatrixPadding (e : Fin r ↪ Fin m) :
    CStarMatrix (Fin r) (Fin r) A →⋆ₙₐ[ℂ] CStarMatrix (Fin m) (Fin m) A :=
…

theorem OAI.KadisonSimilarity.cstarMatrixPadding_apply line 134
theorem OAI.KadisonSimilarity.cstarMatrixPadding_apply_image line 138
theorem OAI.KadisonSimilarity.cstarMatrixPadding_injective line 144
theorem OAI.KadisonSimilarity.norm_cstarMatrixPadding line 154
Source documentation
No norm or dimension factor is lost by matrix zero padding.
```
@[simp] theorem norm_cstarMatrixPadding (e : Fin r ↪ Fin m)
    (X : CStarMatrix (Fin r) (Fin r) A) : ‖cstarMatrixPadding e X‖ = ‖X‖ :=
…
```
Mentions: OAI.KadisonSimilarity.cstarMatrixPadding
theorem OAI.KadisonSimilarity.cstarMatrixPadding_isometry line 158
theorem OAI.KadisonSimilarity.representedPadding_entries line 169
theorem OAI.KadisonSimilarity.representedMatrixHom_cstarMatrixPadding line 184
Source documentation
The abstract C-star padding and concrete operator-matrix padding agree.
```
theorem representedMatrixHom_cstarMatrixPadding (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (e : Fin r ↪ Fin m) (X : CStarMatrix (Fin r) (Fin r) A) :
    representedMatrixHom σ m (cstarMatrixPadding e X) =
      matrixOperator (padOperatorMatrix e (fun i j => σ (X i j))) := by
…
```
Mentions: OAI.KadisonSimilarity.representedMatrixHom, OAI.KadisonSimilarity.cstarMatrixPadding, OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.padOperatorMatrix
theorem OAI.KadisonSimilarity.representedMatrixHom_cstarMatrixPadding_eq_extension line 192
Source documentation
The same identity expressed as extension of the represented operator.
```
theorem representedMatrixHom_cstarMatrixPadding_eq_extension
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (e : Fin r ↪ Fin m)
    (X : CStarMatrix (Fin r) (Fin r) A) :
    representedMatrixHom σ m (cstarMatrixPadding e X) =
      padArrayOperator e (representedMatrixHom σ r X) := by
…
```
Mentions: OAI.KadisonSimilarity.representedMatrixHom, OAI.KadisonSimilarity.cstarMatrixPadding, OAI.KadisonSimilarity.padArrayOperator