OAI/Analysis/JiangSu/MatrixAlgebras/MatrixProjectionGenerators.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ConcreteMatrixUnits.unit_projection line 14
  2. def OAI.ConcreteMatrixUnits.pairProjection line 17
  3. lemma OAI.ConcreteMatrixUnits.pairProjection_star line 20
  4. lemma OAI.ConcreteMatrixUnits.pairProjection_sq line 25
  5. lemma OAI.ConcreteMatrixUnits.pairProjection_projection line 33
  6. lemma OAI.ConcreteMatrixUnits.unit_trace line 37
  7. lemma OAI.ConcreteMatrixUnits.pairProjection_trace line 43
  8. lemma OAI.ConcreteMatrixUnits.pairProjection_recovers line 49
  9. lemma OAI.CurrentMain.ProjectionRow.matrixHom_projection line 66
  10. lemma OAI.CurrentMain.ProjectionRow.matrixHom_le line 73
  11. lemma OAI.CurrentMain.ProjectionRow.amplified_trace_rankone line 77
  12. lemma OAI.CurrentMain.ProjectionRow.amplified_rankone_trace_real line 91
  13. lemma OAI.CurrentMain.ProjectionRow.amplified_rankone_sampling line 103
  14. lemma OAI.DirectPacking.exists_round_matrix_maps line 148