OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/ActiveCapacity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldActiveCapacity.canonicalSideMass line 17
  2. theorem OAI.MatrixMultiplication.AllFieldActiveCapacity.placedLaw_priority_sideMass line 20
  3. theorem OAI.MatrixMultiplication.AllFieldActiveCapacity.canonicalSideMass_stageA line 30
  4. theorem OAI.MatrixMultiplication.AllFieldActiveCapacity.canonicalSideMass_stageB line 44
  5. theorem OAI.MatrixMultiplication.AllFieldActiveCapacity.canonicalSideMass_stageC line 58
  6. theorem OAI.MatrixMultiplication.AllFieldActiveCapacity.workCapacity_first line 62
  7. theorem OAI.MatrixMultiplication.AllFieldActiveCapacity.workCapacity_stageC_physical line 78
  8. theorem OAI.MatrixMultiplication.AllFieldActiveCapacity.order_first_capacity line 86
  9. def OAI.MatrixMultiplication.AllFieldActiveCapacity.orderEntropyRate line 94
  10. def OAI.MatrixMultiplication.AllFieldActiveCapacity.orderNativeDegree line 99
  11. theorem OAI.MatrixMultiplication.AllFieldActiveCapacity.order_entropy_sub_native_degree line 105