FullColumns.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Extending a corner intertwiner through finitely many matrix units

These are the matrix-coordinate steps of lem:full-column: coordinatewise amplification preserves the error norm and intertwines a full operator matrix as soon as it intertwines each entry. The geometric construction of the corner and its matrix-unit coordinates is still required.

theorem OAI.KadisonSimilarity.norm_mapCopies line 24
Source documentation
Positive finite amplification of a rectangular operator preserves its norm.
```
theorem norm_mapCopies (T : K →L[ℂ] F) {n : ℕ} (hn : 0 < n) :
    ‖mapCopies T n‖ = ‖T‖ := by
…
```
Mentions: OAI.KadisonSimilarity.mapCopies
theorem OAI.KadisonSimilarity.mapCopies_sub line 39
theorem OAI.KadisonSimilarity.norm_mapCopies_sub line 45
Source documentation
In the matrix-unit coordinates the error bound has no dimension factor.
```
theorem norm_mapCopies_sub (S T : K →L[ℂ] F) {n : ℕ} (hn : 0 < n) :
    ‖mapCopies S n - mapCopies T n‖ = ‖S - T‖ := by
…
```
Mentions: OAI.KadisonSimilarity.mapCopies

theorem OAI.KadisonSimilarity.mapCopies_intertwines_matrix line 50

Source documentation

Entrywise intertwining suffices for intertwining the full matrix algebra.

theorem mapCopies_intertwines_matrix (T : K →L[ℂ] F) {n : ℕ}
    (X : Matrix (Fin n) (Fin n) (K →L[ℂ] K))
    (Y : Matrix (Fin n) (Fin n) (F →L[ℂ] F))
    (hXY : ∀ i j, T.comp (X i j) = (Y i j).comp T) :
    (mapCopies T n).comp (matrixOperator X) =
      (matrixOperator Y).comp (mapCopies T n) := by
…

Mentions: OAI.KadisonSimilarity.mapCopies, OAI.KadisonSimilarity.matrixOperator

theorem OAI.KadisonSimilarity.norm_comp_isometricCoordinates line 63

Source documentation

Changing isometric domain coordinates preserves the operator norm.

theorem norm_comp_isometricCoordinates (T : K →L[ℂ] F) (U : E ≃ₗᵢ[ℂ] K) :
    ‖T.comp U.toContinuousLinearEquiv.toContinuousLinearMap‖ = ‖T‖ := by
…

theorem OAI.KadisonSimilarity.norm_isometricCoordinates_comp line 76

Source documentation

Isometric codomain coordinates also preserve the operator norm.

theorem norm_isometricCoordinates_comp (T : K →L[ℂ] F) (V : F ≃ₗᵢ[ℂ] E) :
    ‖V.toContinuousLinearEquiv.toContinuousLinearMap.comp T‖ = ‖T‖ := by
…