ColumnCompression.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Contractive extraction of one column of a C-star matrix.

def OAI.KadisonSimilarity.cstarColumn line 12

Source documentation

Extract a column without changing the number of rows.

def cstarColumn {n : ℕ} (X : CStarMatrix (Fin n) (Fin n) A) (j : Fin n) :
    CStarMatrix (Fin n) (Fin 1) A :=
…

theorem OAI.KadisonSimilarity.cstarColumn_apply line 16
theorem OAI.KadisonSimilarity.norm_cstarColumn_le line 22
Source documentation
A coordinate projection on the standard C-star module is contractive.
```
theorem norm_cstarColumn_le {n : ℕ} (X : CStarMatrix (Fin n) (Fin n) A) (j : Fin n) :
    ‖cstarColumn X j‖ ≤ ‖X‖ := by
…
```
Mentions: OAI.KadisonSimilarity.cstarColumn