OAI/Analysis/JiangSu/TraceCone/MatrixRestriction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TraceCone.matrixRestrict line 16
  2. lemma OAI.TraceCone.matrixRestrict_self line 19
  3. lemma OAI.TraceCone.matrixMask_eraseLast line 23
  4. theorem OAI.TraceCone.matrixInclusion_restrict line 39
  5. theorem OAI.TraceCone.matrixRestrict_norm_le line 50
  6. lemma OAI.TraceCone.matrixMask_stage_range line 64
  7. theorem OAI.TraceCone.matrixCompression_range line 72
  8. def OAI.TraceCone.matrixCornerExtract line 87
  9. theorem OAI.TraceCone.matrixCornerExtract_spec line 90
  10. theorem OAI.TraceCone.matrixCornerExtract_norm_le line 94
  11. def OAI.TraceCone.matrixCornerExtractLinear line 98