OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/CoarseAssignment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. abbrev OAI.MatrixMultiplication.JointCoarseAssignment.Triple line 17
  2. def OAI.MatrixMultiplication.JointCoarseAssignment.survives line 19
  3. def OAI.MatrixMultiplication.JointCoarseAssignment.eligible line 22
  4. theorem OAI.MatrixMultiplication.JointCoarseAssignment.mem_eligible_iff line 27
  5. def OAI.MatrixMultiplication.JointCoarseAssignment.assignUseful line 34
  6. theorem OAI.MatrixMultiplication.JointCoarseAssignment.assignUseful_spec line 39
  7. def OAI.MatrixMultiplication.JointCoarseAssignment.assignments line 55
  8. theorem OAI.MatrixMultiplication.JointCoarseAssignment.assignments_coherent line 69