OAI/Analysis/KadisonKastler/ProjectionMatrices.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Matrices of orthogonal projections

The preservation-cut estimate uses an operator matrix whose nonzero entries are projections, orthogonal within each row and each column. Such a rectangular matrix is a contraction.

  1. theorem OAI.KadisonKastler.isStarProjection_sum_orthogonal line 19
  2. theorem OAI.KadisonKastler.inner_eq_zero_of_selfAdjoint_mul_eq_zero line 38
  3. theorem OAI.KadisonKastler.norm_projectionMatrix_le_one line 56

    Source documentation

    Orthogonality in both directions makes a matrix of projections a contraction, with no factor depending on the number of rows or columns.

    theorem norm_projectionMatrix_le_one {I J : Type*} [Fintype I] [Fintype J]
    (T : CStarMatrix I J (H →L[ℂ] H))
    (hT : ∀ i j, IsStarProjection (T i j))
    (hrow : ∀ i j k, j ≠ k → T i j * T i k = 0)
    (hcol : ∀ j i k, i ≠ k → T i j * T k j = 0) : ‖T‖ ≤ 1 := by
…