OAI/LinearAlgebra/MatrixMultiplication/Recovery/PhysicalOrders.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Finite orbit symmetries, masks and exact recovery operations.

  1. abbrev OAI.MatrixMultiplication.PhysicalOrders.PhysicalOrder line 17
  2. theorem OAI.MatrixMultiplication.PhysicalOrders.card_physical_orders line 19
  3. def OAI.MatrixMultiplication.PhysicalOrders.placementAmount line 22
  4. theorem OAI.MatrixMultiplication.PhysicalOrders.placementAmount_eq line 24
  5. theorem OAI.MatrixMultiplication.PhysicalOrders.sum_placementAmount line 27
  6. theorem OAI.MatrixMultiplication.PhysicalOrders.placement_has_unique_order line 34
  7. theorem OAI.MatrixMultiplication.PhysicalOrders.sum_selected_placement line 40
  8. def OAI.MatrixMultiplication.PhysicalOrders.aggregateCapacity line 58
  9. def OAI.MatrixMultiplication.PhysicalOrders.perPhysicalOrderCapacity line 61
  10. theorem OAI.MatrixMultiplication.PhysicalOrders.perPhysicalOrderCapacity_apply line 67
  11. theorem OAI.MatrixMultiplication.PhysicalOrders.perPhysicalOrderCapacity_eq line 80
  12. theorem OAI.MatrixMultiplication.PhysicalOrders.minCapacity_mul line 88
  13. theorem OAI.MatrixMultiplication.PhysicalOrders.sum_physical_order_minima line 93