FiniteMatrixBounds.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite index changes for the rectangular matrix estimates used in row averaging.

theorem OAI.KadisonKastler.norm_reindex_rectangular line 17

Source documentation

Independent changes of row and column indices preserve the matrix norm.

theorem norm_reindex_rectangular {ι κ ι' κ' : Type*}
    [Fintype ι] [Fintype κ] [Fintype ι'] [Fintype κ']
    (e : ι ≃ ι') (d : κ ≃ κ') (X : CStarMatrix ι κ A) :
    ‖CStarMatrix.reindexₗ ℂ A e d X‖ = ‖X‖ := by
…

theorem OAI.KadisonKastler.CompletelyBoundedBy.finite_square line 37

Source documentation

Complete bounds apply to arbitrary finite square index types.

theorem CompletelyBoundedBy.finite_square {F : A →ₗ[ℂ] B} {c : ℝ}
    (hF : CompletelyBoundedBy F c) {ι : Type*} [Fintype ι]
    (X : CStarMatrix ι ι A) : ‖CStarMatrix.mapₗ F X‖ ≤ c * ‖X‖ := by
…

Mentions: OAI.KadisonKastler.CompletelyBoundedBy

theorem OAI.KadisonKastler.CompletelyBoundedBy.finite line 52

Source documentation

Complete bounds apply to arbitrary finite rectangular index types.

theorem CompletelyBoundedBy.finite {F : A →ₗ[ℂ] B} {c : ℝ}
    (hF : CompletelyBoundedBy F c) {ι κ : Type*} [Fintype ι] [Fintype κ]
    (X : CStarMatrix ι κ A) : ‖CStarMatrix.mapₗ F X‖ ≤ c * ‖X‖ := by
…

Mentions: OAI.KadisonKastler.CompletelyBoundedBy

theorem OAI.KadisonKastler.rectangular_toCLM_mul_finite line 59
theorem OAI.KadisonKastler.rectangular_norm_mul_le_finite line 67