RectangularCorner.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Isometric square corners of rectangular C⋆-matrices

The upper-right corner embeds a rectangular matrix into a square matrix without changing its operator norm. We prove this directly on the finite Hilbert C⋆-modules that define the matrix norms.

def OAI.KadisonKastler.moduleExtendLeft line 23
Source documentation
Extension by zero into the left summand of a finite Hilbert C⋆-module.
```
def moduleExtendLeft (x : C⋆ᵐᵒᵈ(A, m → A)) : C⋆ᵐᵒᵈ(A, (m ⊕ n) → A) :=
…
```
def OAI.KadisonKastler.moduleExtendRight line 27
Source documentation
Extension by zero into the right summand.
```
def moduleExtendRight (x : C⋆ᵐᵒᵈ(A, n → A)) : C⋆ᵐᵒᵈ(A, (m ⊕ n) → A) :=
…
```
def OAI.KadisonKastler.moduleRestrictLeft line 31
Source documentation
Restriction to the left summand.
```
def moduleRestrictLeft (x : C⋆ᵐᵒᵈ(A, (m ⊕ n) → A)) : C⋆ᵐᵒᵈ(A, m → A) :=
…
```
theorem OAI.KadisonKastler.norm_moduleExtendLeft line 35
theorem OAI.KadisonKastler.norm_moduleExtendRight line 41
theorem OAI.KadisonKastler.norm_moduleRestrictLeft_le line 46
def OAI.KadisonKastler.rectangularCorner line 57
Source documentation
A rectangular matrix as an upper-right corner of a square matrix.
```
def rectangularCorner (X : CStarMatrix m n A) :
    CStarMatrix (m ⊕ n) (m ⊕ n) A :=
…
```
theorem OAI.KadisonKastler.rectangularCorner_toCLM line 65
theorem OAI.KadisonKastler.norm_rectangularCorner line 75
Source documentation
The square-corner embedding preserves the rectangular operator norm.
```
theorem norm_rectangularCorner (X : CStarMatrix m n A) :
    ‖rectangularCorner X‖ = ‖X‖ := by
…
```
Mentions: OAI.KadisonKastler.rectangularCorner
theorem OAI.KadisonKastler.rectangularCorner_map line 96