SquareCompleteBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Rectangular complete bounds from square levels of size at least two

theorem OAI.KadisonKastler.norm_map_square_of_fin line 18

Source documentation

Reindexing transports a bound at a finite ordinal to any finite square matrix of the same size.

theorem norm_map_square_of_fin (F : A →ₗ[ℂ] B) {c : ℝ}
    (hsquare : ∀ n : ℕ, 2 ≤ n → ∀ X : CStarMatrix (Fin n) (Fin n) A,
      ‖CStarMatrix.mapₗ F X‖ ≤ c * ‖X‖)
    {ι : Type*} [Fintype ι] [DecidableEq ι] (hι : 2 ≤ Fintype.card ι)
    (X : CStarMatrix ι ι A) : ‖CStarMatrix.mapₗ F X‖ ≤ c * ‖X‖ := by
…

theorem OAI.KadisonKastler.completelyBoundedBy_of_large_square line 37
Source documentation
Positive rectangular sizes embed isometrically into a square of size at least two; zero rectangular sizes contribute only the zero matrix.
```
theorem completelyBoundedBy_of_large_square (F : A →ₗ[ℂ] B) {c : ℝ}
    (hsquare : ∀ n : ℕ, 2 ≤ n → ∀ X : CStarMatrix (Fin n) (Fin n) A,
      ‖CStarMatrix.mapₗ F X‖ ≤ c * ‖X‖) : CompletelyBoundedBy F c := by
…
```
Mentions: OAI.KadisonKastler.CompletelyBoundedBy