SupportColumnConstruction.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

A one-column partial isometry for a small diagonal support

def OAI.KadisonKastler.matrixEntry line 19
Source documentation
A single entry in a rectangular C⋆-matrix.
```
def matrixEntry (i : m) (j : n) (a : A) : CStarMatrix m n A :=
…
```
theorem OAI.KadisonKastler.matrixEntry_zero line 24
theorem OAI.KadisonKastler.matrixEntry_conjTranspose line 30
theorem OAI.KadisonKastler.matrixEntry_mul line 35

theorem OAI.KadisonKastler.isStarProjection_fintype_sum line 44

Source documentation

A finite orthogonal family of projections has a projection as its sum.

theorem isStarProjection_fintype_sum {B τ : Type*} [Ring B] [StarRing B] [Fintype τ]
    (P : τ → B) (hP : ∀ t, IsStarProjection (P t))
    (horth : ∀ s t, s ≠ t → P s * P t = 0) : IsStarProjection (∑ t, P t) := by
…

def OAI.KadisonKastler.supportAtom line 64
Source documentation
The diagonal atom labelled by a row and a matrix-unit index.
```
def supportAtom (E : Generator.MatrixUnitSystem k A) (s : m × k) : CStarMatrix m m A :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem
theorem OAI.KadisonKastler.supportAtom_projection line 68
theorem OAI.KadisonKastler.supportAtom_orthogonal line 77
theorem OAI.KadisonKastler.supportAtom_total line 86
Source documentation
All diagonal row-label atoms form a partition of the identity.
```
theorem supportAtom_total (E : Generator.MatrixUnitSystem k A) :
    (∑ s : m × k, supportAtom E s) = 1 := by
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.supportAtom
def OAI.KadisonKastler.supportProjection line 99
Source documentation
The projection onto a set of diagonal row-label atoms.
```
def supportProjection (E : Generator.MatrixUnitSystem k A) (S : Finset (m × k)) :
    CStarMatrix m m A := ∑ s : S, supportAtom E s.val
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.supportAtom
theorem OAI.KadisonKastler.supportProjection_eq_sum line 103
theorem OAI.KadisonKastler.supportProjection_isStarProjection line 108
def OAI.KadisonKastler.supportColumn line 114
Source documentation
The column sends distinct support atoms to distinct diagonal matrix-unit labels.
```
def supportColumn (E : Generator.MatrixUnitSystem k A) (S : Finset (m × k))
    (f : S ↪ k) : CStarMatrix m (Fin 1) A :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem
theorem OAI.KadisonKastler.supportColumn_atom_mul line 119
theorem OAI.KadisonKastler.matrix_conjTranspose_sum line 134
theorem OAI.KadisonKastler.matrix_sum_mul line 141
theorem OAI.KadisonKastler.matrix_mul_sum line 148
theorem OAI.KadisonKastler.supportColumn_mul_conjTranspose line 155
Source documentation
The range projection of the constructed column is exactly the given support.
```
theorem supportColumn_mul_conjTranspose (E : Generator.MatrixUnitSystem k A)
    (S : Finset (m × k)) (f : S ↪ k) :
    supportColumn E S f * (supportColumn E S f).conjTranspose = supportProjection E S := by
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.supportColumn, OAI.KadisonKastler.supportProjection