OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/Canonicalization.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. def OAI.MatrixMultiplication.JointCanonicalization.fiberEquiv line 22
  2. def OAI.MatrixMultiplication.JointCanonicalization.positionEquiv line 26
  3. theorem OAI.MatrixMultiplication.JointCanonicalization.positionEquiv_shape line 31
  4. theorem OAI.MatrixMultiplication.JointCanonicalization.positionEquiv_symm_shape line 34
  5. abbrev OAI.MatrixMultiplication.JointCanonicalization.ClassKey line 40
  6. abbrev OAI.MatrixMultiplication.JointCanonicalization.ClassPositions line 41
  7. abbrev OAI.MatrixMultiplication.JointCanonicalization.RawPairs line 45
  8. abbrev OAI.MatrixMultiplication.JointCanonicalization.CanonicalPairs line 46
  9. def OAI.MatrixMultiplication.JointCanonicalization.pairEquiv line 49
  10. theorem OAI.MatrixMultiplication.JointCanonicalization.pairEquiv_fiber_left line 74
  11. theorem OAI.MatrixMultiplication.JointCanonicalization.pairEquiv_fiber_right line 79
  12. theorem OAI.MatrixMultiplication.JointCanonicalization.typeWindow_reindex line 84
  13. def OAI.MatrixMultiplication.JointCanonicalization.activeLaw line 102
  14. def OAI.MatrixMultiplication.JointCanonicalization.activeWidth line 106
  15. theorem OAI.MatrixMultiplication.JointCanonicalization.activeLaw_of_pos line 109
  16. def OAI.MatrixMultiplication.JointCanonicalization.rawWindows line 115
  17. theorem OAI.MatrixMultiplication.JointCanonicalization.rawWindows_iff_childWindows line 122
  18. def OAI.MatrixMultiplication.JointCanonicalization.coarseMask line 162
  19. def OAI.MatrixMultiplication.JointCanonicalization.coarseWord line 165
  20. def OAI.MatrixMultiplication.JointCanonicalization.sourceTensor line 168
  21. def OAI.MatrixMultiplication.JointCanonicalization.coarseIdeal line 171
  22. def OAI.MatrixMultiplication.JointCanonicalization.block line 177
  23. def OAI.MatrixMultiplication.JointCanonicalization.canonicalBase line 182
  24. theorem OAI.MatrixMultiplication.JointCanonicalization.product_pack line 188
  25. theorem OAI.MatrixMultiplication.JointCanonicalization.coarseIdeal_eq_canonicalBase line 206
  26. def OAI.MatrixMultiplication.JointCanonicalization.coordinateMatrix line 215
  27. theorem OAI.MatrixMultiplication.JointCanonicalization.coordinateMatrix_restrict line 219
  28. theorem OAI.MatrixMultiplication.JointCanonicalization.coarseIdeal_restrict line 230
  29. theorem OAI.MatrixMultiplication.JointCanonicalization.canonicalBase_eq_pairClassProduct line 240
  30. def OAI.MatrixMultiplication.JointCanonicalization.ideal line 260
  31. def OAI.MatrixMultiplication.JointCanonicalization.canonicalIdeal line 267
  32. def OAI.MatrixMultiplication.JointCanonicalization.usefulByTriple line 277
  33. theorem OAI.MatrixMultiplication.JointCanonicalization.usefulByTriple_target line 284
  34. theorem OAI.MatrixMultiplication.JointCanonicalization.ideal_eq_jointIdeal line 296
  35. theorem OAI.MatrixMultiplication.JointCanonicalization.ideal_eq_canonicalIdeal line 319
  36. theorem OAI.MatrixMultiplication.JointCanonicalization.ideal_restrict line 328