OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/NativeLaws.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldNativeCapacity.indexedRationalLaw line 16
  2. def OAI.MatrixMultiplication.AllFieldNativeCapacity.stageASplitLaw line 26
  3. def OAI.MatrixMultiplication.AllFieldNativeCapacity.stageBSplitLaw line 31
  4. def OAI.MatrixMultiplication.AllFieldNativeCapacity.indexedMarginalLaw line 36
  5. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.indexedMarginalLaw_mass line 42
  6. def OAI.MatrixMultiplication.AllFieldNativeCapacity.stageAMarginalLaw line 51
  7. def OAI.MatrixMultiplication.AllFieldNativeCapacity.stageBMarginalLaw line 58
  8. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.stageACapacity_first_entropy line 65
  9. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.stageBCapacity_first_entropy line 76
  10. def OAI.MatrixMultiplication.AllFieldNativeCapacity.halfFiniteLaw line 87
  11. def OAI.MatrixMultiplication.AllFieldNativeCapacity.littleFiniteLaw line 92
  12. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.list_rat_cast line 97
  13. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.pairLaw_total line 103
  14. def OAI.MatrixMultiplication.AllFieldNativeCapacity.pairFiniteLaw line 121
  15. def OAI.MatrixMultiplication.AllFieldNativeCapacity.stageAPairLaw line 136
  16. def OAI.MatrixMultiplication.AllFieldNativeCapacity.stageBPairLaw line 147
  17. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.stageACapacity_sharing line 157
  18. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.stageBCapacity_sharing line 166