BlockAmplification.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Complete bounds for the off-diagonal commutator construction

Reordering the two finite matrix indices turns an amplification of b ↦ [0,-b;b,0] into the same off-diagonal matrix over a matrix algebra. Its norm is therefore exactly the norm of the original amplification.

def OAI.KadisonKastler.offDiagonalLinearMap line 22
Source documentation
The signed off-diagonal linear embedding used for paired representations.
```
def offDiagonalLinearMap : B →ₗ[ℂ] CStarMatrix (Fin 2) (Fin 2) B where
…
```
theorem OAI.KadisonKastler.offDiagonalLinearMap_apply line 34

def OAI.KadisonKastler.matrixBlockSwap line 38

Source documentation

Swap the finite amplification index and the two-by-two block index.

def matrixBlockSwap (n : Type*) [Fintype n] [DecidableEq n] :
    CStarMatrix n n (CStarMatrix (Fin 2) (Fin 2) B) ≃⋆ₐ[ℂ]
      CStarMatrix (Fin 2) (Fin 2) (CStarMatrix n n B) :=
…

theorem OAI.KadisonKastler.norm_matrixBlockSwap line 45
theorem OAI.KadisonKastler.matrixBlockSwap_offDiagonal line 50
theorem OAI.KadisonKastler.norm_map_offDiagonal_square line 58
Source documentation
The signed off-diagonal map preserves every square matrix norm.
```
theorem norm_map_offDiagonal_square {n : Type*} [Fintype n] [DecidableEq n]
    (X : CStarMatrix n n B) :
    ‖CStarMatrix.mapₗ offDiagonalLinearMap X‖ = ‖X‖ := by
…
```
Mentions: OAI.KadisonKastler.offDiagonalLinearMap
theorem OAI.KadisonKastler.norm_map_offDiagonal line 65
Source documentation
The same exact norm identity holds for rectangular amplifications.
```
theorem norm_map_offDiagonal {m n : Type*} [Fintype m] [Fintype n]
    (X : CStarMatrix m n B) :
    ‖CStarMatrix.mapₗ offDiagonalLinearMap X‖ = ‖X‖ := by
…
```
Mentions: OAI.KadisonKastler.offDiagonalLinearMap
theorem OAI.KadisonKastler.completelyBoundedBy_offDiagonal_iff line 80
Source documentation
The off-diagonal construction preserves exactly the complete bound.
```
theorem completelyBoundedBy_offDiagonal_iff (F : A →ₗ[ℂ] B) (e : ℝ) :
    CompletelyBoundedBy (offDiagonalLinearMap.comp F) e ↔ CompletelyBoundedBy F e := by
…
```
Mentions: OAI.KadisonKastler.CompletelyBoundedBy