BlockMatrices.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Two-by-two C⋆-matrix norm formulas

The diagonal embedding is a faithful star representation, so its norm is the supremum norm. Multiplying by the flip unitary gives the corresponding off-diagonal formula.

def OAI.KadisonKastler.diagonalStarAlgHom line 21
Source documentation
The diagonal star representation of a finite product of C⋆-algebras.
```
def diagonalStarAlgHom (n : Type*) [Fintype n] [DecidableEq n] :
    (n → A) →⋆ₐ[ℂ] CStarMatrix n n A :=
…
```
theorem OAI.KadisonKastler.diagonalStarAlgHom_apply line 35
theorem OAI.KadisonKastler.diagonalStarAlgHom_injective line 40
theorem OAI.KadisonKastler.norm_diagonalStarAlgHom line 48
Source documentation
The operator norm of a diagonal matrix is the finite-product norm.
```
theorem norm_diagonalStarAlgHom (n : Type*) [Fintype n] [DecidableEq n] (d : n → A) :
    ‖diagonalStarAlgHom n d‖ = ‖d‖ :=
…
```
Mentions: OAI.KadisonKastler.diagonalStarAlgHom
def OAI.KadisonKastler.blockDiagonal line 53
Source documentation
The diagonal matrix with entries a and b.
```
def blockDiagonal (a b : A) : CStarMatrix (Fin 2) (Fin 2) A :=
…
```
theorem OAI.KadisonKastler.norm_blockDiagonal line 56
def OAI.KadisonKastler.blockFlip line 65
Source documentation
The unitary that swaps the two coordinates.
```
def blockFlip : unitary (CStarMatrix (Fin 2) (Fin 2) A) :=
…
```
def OAI.KadisonKastler.blockOffDiagonal line 75
Source documentation
The off-diagonal matrix with entries a and b.
```
def blockOffDiagonal (a b : A) : CStarMatrix (Fin 2) (Fin 2) A :=
…
```
theorem OAI.KadisonKastler.blockOffDiagonal_eq_mul_flip line 79
theorem OAI.KadisonKastler.norm_blockOffDiagonal line 87
theorem OAI.KadisonKastler.block_commute_intertwines line 93
Source documentation
The lower-left entry of an operator commuting with a diagonal pair is an intertwiner for that pair.
```
theorem block_commute_intertwines (D : CStarMatrix (Fin 2) (Fin 2) A) (a b : A)
    (h : D * blockDiagonal a b = blockDiagonal a b * D) :
    D 1 0 * a = b * D 1 0 := by
…
```
Mentions: OAI.KadisonKastler.blockDiagonal
theorem OAI.KadisonKastler.norm_lowerLeft_sub_one_le line 102
Source documentation
Closeness to the flip controls the lower-left intertwiner.
```
theorem norm_lowerLeft_sub_one_le (D : CStarMatrix (Fin 2) (Fin 2) A) :
    ‖D 1 0 - 1‖ ≤ ‖D - (blockFlip (A := A) : CStarMatrix (Fin 2) (Fin 2) A)‖ := by
…
```
Mentions: OAI.KadisonKastler.blockFlip

theorem OAI.KadisonKastler.matrix_entry_norm_le line 110

Source documentation

Every individual entry is bounded by the operator norm, at any size.

theorem matrix_entry_norm_le {m n : Type*} [Fintype m] [Fintype n]
    (M : CStarMatrix m n A) (i : m) (j : n) : ‖M i j‖ ≤ ‖M‖ :=
…