SupportColumn.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The column estimate on a small diagonal support

def OAI.KadisonKastler.matrixCommutator line 29
Source documentation
The entrywise spatial commutator, also for rectangular matrices.
```
def matrixCommutator (h : H →L[ℂ] H) (X : CStarMatrix m n (H →L[ℂ] H)) :
    CStarMatrix m n (H →L[ℂ] H) := CStarMatrix.mapₗ (innerDerivation h) X
…
```
Mentions: OAI.KadisonKastler.innerDerivation
theorem OAI.KadisonKastler.matrixCommutator_apply line 34
theorem OAI.KadisonKastler.matrixCommutator_eq_diagonal line 39
Source documentation
The entrywise commutator agrees with the usual amplified commutator.
```
theorem matrixCommutator_eq_diagonal [DecidableEq m] [DecidableEq n]
    (h : H →L[ℂ] H) (X : CStarMatrix m n (H →L[ℂ] H)) :
    matrixCommutator h X = diagonalAmplification h * X - X * diagonalAmplification h := by
…
```
Mentions: OAI.KadisonKastler.matrixCommutator, OAI.KadisonKastler.diagonalAmplification
theorem OAI.KadisonKastler.matrixCommutator_mul line 51
theorem OAI.KadisonKastler.matrixCommutator_eq_zero line 63
theorem OAI.KadisonKastler.supportColumn_entry_mem line 74
Source documentation
Each entry of the partial-isometry column lies in the given matrix algebra.
```
theorem supportColumn_entry_mem (E : Generator.MatrixUnitSystem k (H →L[ℂ] H))
    (S : Finset (m × k)) (f : S ↪ k) (i : m) (j : Fin 1) :
    supportColumn E S f i j ∈ E.algebra := by
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.supportColumn
theorem OAI.KadisonKastler.norm_supportColumn_le_one line 87
Source documentation
The support column is a contraction because its range projection is a projection.
```
theorem norm_supportColumn_le_one (E : Generator.MatrixUnitSystem k (H →L[ℂ] H))
    (S : Finset (m × k)) (f : S ↪ k) : ‖supportColumn E S f‖ ≤ 1 := by
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.supportColumn

theorem OAI.KadisonKastler.exists_supportColumn line 95

Source documentation

The cardinality assumption constructs the required column, including the empty case.

theorem exists_supportColumn (E : Generator.MatrixUnitSystem k (H →L[ℂ] H))
    (S : Finset (m × k)) (hS : S.card ≤ Fintype.card k) :
    ∃ V : CStarMatrix m (Fin 1) (H →L[ℂ] H),
      V * V.conjTranspose = supportProjection E S ∧ ‖V‖ ≤ 1 ∧
      ∀ i j, V i j ∈ E.algebra := by
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.supportProjection

theorem OAI.KadisonKastler.matrixCommutator_column_bound line 106
Source documentation
Applying the established column theorem to a column with entries in a concrete algebra.
```
theorem matrixCommutator_column_bound (M : VonNeumannAlgebra H)
    (hPublished : PublishedCyclicSimilarity.{u, u} (A := Algebra M))
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.small_support_commutator_bound line 125
Source documentation
A clipped coefficient has the uniform column bound on its small support.
```
theorem small_support_commutator_bound (M : VonNeumannAlgebra H)
    (hPublished : PublishedCyclicSimilarity.{u, u} (A := Algebra M))
…
```
Mentions: OAI.KadisonKastler.Algebra