OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/CanonicalCW.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. abbrev OAI.MatrixMultiplication.JointCanonicalCW.Left line 23
  2. abbrev OAI.MatrixMultiplication.JointCanonicalCW.Right line 24
  3. def OAI.MatrixMultiplication.JointCanonicalCW.shapeNat line 26
  4. def OAI.MatrixMultiplication.JointCanonicalCW.parentTensor line 28
  5. def OAI.MatrixMultiplication.JointCanonicalCW.coarse line 35
  6. def OAI.MatrixMultiplication.JointCanonicalCW.leftTensor line 38
  7. def OAI.MatrixMultiplication.JointCanonicalCW.rightTensor line 42
  8. theorem OAI.MatrixMultiplication.JointCanonicalCW.block_eq_product line 47
  9. theorem OAI.MatrixMultiplication.JointCanonicalCW.canonicalBase_eq_children line 66
  10. abbrev OAI.MatrixMultiplication.JointCanonicalCW.RawStrands line 94
  11. def OAI.MatrixMultiplication.JointCanonicalCW.rawParentSource line 97
  12. def OAI.MatrixMultiplication.JointCanonicalCW.joinWords line 101
  13. def OAI.MatrixMultiplication.JointCanonicalCW.joinMatrix line 105
  14. theorem OAI.MatrixMultiplication.JointCanonicalCW.parentTensor_restrict line 109