OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/AssignmentLoss.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. theorem OAI.MatrixMultiplication.JointAssignmentLoss.uniqueAssignment_of_unique line 17
  2. theorem OAI.MatrixMultiplication.JointAssignmentLoss.assignUseful_of_unique line 29
  3. def OAI.MatrixMultiplication.JointAssignmentLoss.ambientXCollision line 40
  4. def OAI.MatrixMultiplication.JointAssignmentLoss.targetCompatibleCollision line 44
  5. theorem OAI.MatrixMultiplication.JointAssignmentLoss.eligible_of_no_ambientXCollision line 49
  6. theorem OAI.MatrixMultiplication.JointAssignmentLoss.not_eligible_iff_ambientXCollision line 61
  7. theorem OAI.MatrixMultiplication.JointAssignmentLoss.assignUseful_of_no_targetCollision line 73
  8. theorem OAI.MatrixMultiplication.JointAssignmentLoss.assignment_failure_implies_collision line 87
  9. theorem OAI.MatrixMultiplication.JointAssignmentLoss.retained_assignment_of_no_collision line 104
  10. theorem OAI.MatrixMultiplication.JointAssignmentLoss.passing_assignment_failure_subset line 120