CStarRowSquare.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The positive row square and its native C-star matrix norm.

theorem OAI.KadisonSimilarity.norm_rowSquare_le line 16

Source documentation

The sum of xx* of a row has norm bounded by its matrix norm squared.

theorem norm_rowSquare_le {n : ℕ} (X : Matrix (Fin 1) (Fin n) A) :
    ‖∑ j : Fin n, X 0 j * star (X 0 j)‖ ≤ ‖CStarMatrix.ofMatrix X‖ ^ 2 := by
…

theorem OAI.KadisonSimilarity.positiveFunctional_rowSquare_le line 49

Source documentation

A positive functional of mass at most one is bounded on the row square.

theorem positiveFunctional_rowSquare_le (f : A →ₚ[ℂ] ℂ) (hf : (f 1).re ≤ 1)
    {n : ℕ} (X : Matrix (Fin 1) (Fin n) A) :
    ∑ j : Fin n, (f (X 0 j * star (X 0 j))).re ≤ ‖CStarMatrix.ofMatrix X‖ ^ 2 := by
…