OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/CanonicalInitial.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. abbrev OAI.MatrixMultiplication.JointCanonicalInitial.Word line 21
  2. abbrev OAI.MatrixMultiplication.JointCanonicalInitial.RawWords line 22
  3. abbrev OAI.MatrixMultiplication.JointCanonicalInitial.CanonicalWords line 23
  4. def OAI.MatrixMultiplication.JointCanonicalInitial.wholeEquiv line 25
  5. def OAI.MatrixMultiplication.JointCanonicalInitial.rawSource line 37
  6. def OAI.MatrixMultiplication.JointCanonicalInitial.coarseWord line 40
  7. def OAI.MatrixMultiplication.JointCanonicalInitial.ideal line 43
  8. def OAI.MatrixMultiplication.JointCanonicalInitial.canonical line 49
  9. theorem OAI.MatrixMultiplication.JointCanonicalInitial.canonical_pack line 54
  10. theorem OAI.MatrixMultiplication.JointCanonicalInitial.ideal_eq_canonical line 69
  11. def OAI.MatrixMultiplication.JointCanonicalInitial.coordinateMatrix line 79
  12. theorem OAI.MatrixMultiplication.JointCanonicalInitial.ideal_restrict line 82
  13. theorem OAI.MatrixMultiplication.JointCanonicalInitial.coarse_support line 93
  14. def OAI.MatrixMultiplication.JointCanonicalInitial.sideMask line 107
  15. def OAI.MatrixMultiplication.JointCanonicalInitial.maskedSource line 111
  16. theorem OAI.MatrixMultiplication.JointCanonicalInitial.sideMask_of_target line 116
  17. theorem OAI.MatrixMultiplication.JointCanonicalInitial.maskedSource_support line 124
  18. theorem OAI.MatrixMultiplication.JointCanonicalInitial.ideal_support_masks line 153
  19. theorem OAI.MatrixMultiplication.JointCanonicalInitial.delete_ideal_eq line 171