OAI/Analysis/FreeWords/ProjectionMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalStrongKK.HilbertSum line 16
  2. def OAI.UniversalStrongKK.operatorMatrix line 18
  3. theorem OAI.UniversalStrongKK.operatorMatrix_apply line 23
  4. theorem OAI.UniversalStrongKK.operatorMatrix_add line 28
  5. theorem OAI.UniversalStrongKK.operatorMatrix_smul line 33
  6. theorem OAI.UniversalStrongKK.operatorMatrix_mul line 38
  7. theorem OAI.UniversalStrongKK.operatorMatrix_star line 49
  8. theorem OAI.UniversalStrongKK.sum_pairwise_starProjection line 71
  9. theorem OAI.UniversalStrongKK.diagonalFamily_norm_le line 90
  10. theorem OAI.UniversalStrongKK.orthogonal_projection_matrix_contraction line 115