RectangularRowNorm.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Rectangular row norm estimates on finite Hilbert C-star modules.

theorem OAI.KadisonKastler.rectangular_norm_sq_le line 18
Source documentation
The C-star norm lower bound holds for rectangular matrices.
```
theorem rectangular_norm_sq_le (X : CStarMatrix ι κ A) :
    ‖X‖ ^ 2 ≤ ‖X * X.conjTranspose‖ := by
…
```

theorem OAI.KadisonKastler.rectangular_row_and_column_contract line 45

Source documentation

A contractive row has a contractive adjoint column.

theorem rectangular_row_and_column_contract (X : CStarMatrix ι κ A)
    (h : ‖X * X.conjTranspose‖ ≤ 1) : ‖X‖ ≤ 1 ∧ ‖X.conjTranspose‖ ≤ 1 := by
…

theorem OAI.KadisonKastler.norm_conjTranspose_le_finite line 58
Source documentation
Transposition to the adjoint column does not increase the rectangular norm.
```
theorem norm_conjTranspose_le_finite (Y : CStarMatrix ι κ A) :
    ‖Y.conjTranspose‖ ≤ ‖Y‖ := by
…
```
theorem OAI.KadisonKastler.norm_conjTranspose_finite line 67
Source documentation
Conjugate transpose preserves every rectangular matrix norm.
```
theorem norm_conjTranspose_finite (X : CStarMatrix ι κ A) : ‖X.conjTranspose‖ = ‖X‖ := by
…
```