OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/OrbitFibers.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. def OAI.MatrixMultiplication.JointOrbitFibers.fullFiber line 13
  2. theorem OAI.MatrixMultiplication.JointOrbitFibers.mem_fullFiber line 16
  3. theorem OAI.MatrixMultiplication.JointOrbitFibers.mem_fullFiber_mk line 20
  4. theorem OAI.MatrixMultiplication.JointOrbitFibers.fullFiber_nonempty line 30
  5. theorem OAI.MatrixMultiplication.JointOrbitFibers.fullFiber_card_pos line 35
  6. theorem OAI.MatrixMultiplication.JointOrbitFibers.fullFiber_mk line 43
  7. theorem OAI.MatrixMultiplication.JointOrbitFibers.fullFiber_eq_orbitSet line 50
  8. def OAI.MatrixMultiplication.JointOrbitFibers.transportedFiber line 57
  9. theorem OAI.MatrixMultiplication.JointOrbitFibers.mem_transportedFiber line 61
  10. theorem OAI.MatrixMultiplication.JointOrbitFibers.transportedFiber_card line 76
  11. theorem OAI.MatrixMultiplication.JointOrbitFibers.transportedFiber_card_pos line 81
  12. theorem OAI.MatrixMultiplication.JointOrbitFibers.transportedFiber_mk line 87
  13. theorem OAI.MatrixMultiplication.JointOrbitFibers.transportedFiber_filter_card line 115