NestedMatrixAmplification.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Nested finite matrix amplifications and their actual C*-norms.

def OAI.BoundedHochschild.KadisonRingrose.nestedMatrixEquiv line 14

Source documentation

Flattening two finite matrix indices is a star-algebra equivalence.

def nestedMatrixEquiv (n k : ℕ) :
    CStarMatrix (Fin n) (Fin n) (CStarMatrix (Fin k) (Fin k) M) ≃⋆ₐ[ℂ]
      CStarMatrix (Fin n × Fin k) (Fin n × Fin k) M where
…

lemma OAI.BoundedHochschild.KadisonRingrose.nestedMatrix_norm line 33

lemma OAI.BoundedHochschild.KadisonRingrose.matrix_reindex_norm line 38

Source documentation

Reindexing a finite square amplification preserves its norm.

lemma matrix_reindex_norm {I J : Type*} [Fintype I] [Fintype J]
    (e : I ≃ J) (A : CStarMatrix I I M) :
    ‖CStarMatrix.reindexₐ ℂ M e A‖ = ‖A‖ :=
…

def OAI.BoundedHochschild.KadisonRingrose.matrixAmplification line 45
Source documentation
The entrywise amplification of a bounded map is a bounded linear map on each fixed finite matrix algebra.
```
def matrixAmplification (k : ℕ) (T : M →L[ℂ] M) :
    CStarMatrix (Fin k) (Fin k) M →L[ℂ] CStarMatrix (Fin k) (Fin k) M := by
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.matrixAmplification_apply line 53
lemma OAI.BoundedHochschild.KadisonRingrose.matrixAmplification_norm_le line 56
theorem OAI.BoundedHochschild.KadisonRingrose.matrixAmplification_completelyBounded line 62
Source documentation
A complete bound is unchanged by passing to any fixed finite amplification. The proof flattens the two genuine matrix norms.
```
theorem matrixAmplification_completelyBounded (k : ℕ) (T : M →L[ℂ] M) {C : ℝ}
    (hT : CompletelyBoundedEstimate T C) :
    CompletelyBoundedEstimate (matrixAmplification k T) C := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.CompletelyBoundedEstimate, OAI.BoundedHochschild.KadisonRingrose.matrixAmplification