OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/ActiveSums.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldHistory.aRelot line 16
  2. def OAI.MatrixMultiplication.AllFieldHistory.bRelot line 19
  3. def OAI.MatrixMultiplication.AllFieldHistory.partRelot line 22
  4. def OAI.MatrixMultiplication.AllFieldHistory.workRelot line 25
  5. theorem OAI.MatrixMultiplication.AllFieldHistory.workRelot_lot line 30
  6. theorem OAI.MatrixMultiplication.AllFieldHistory.workRelot_stage line 33
  7. theorem OAI.MatrixMultiplication.AllFieldHistory.workRelot_self line 36
  8. theorem OAI.MatrixMultiplication.AllFieldHistory.workRelot_relot line 39
  9. theorem OAI.MatrixMultiplication.AllFieldHistory.workAmount_relot line 43
  10. def OAI.MatrixMultiplication.AllFieldHistory.workLotEquiv line 48
  11. theorem OAI.MatrixMultiplication.AllFieldHistory.workLotEquiv_symm_apply line 60
  12. def OAI.MatrixMultiplication.AllFieldHistory.workStagesEquiv line 63
  13. theorem OAI.MatrixMultiplication.AllFieldHistory.work_sum line 76
  14. theorem OAI.MatrixMultiplication.AllFieldHistory.sum_lot_tick line 87
  15. def OAI.MatrixMultiplication.AllFieldHistory.shapeValue line 102
  16. theorem OAI.MatrixMultiplication.AllFieldHistory.shapeValue_relot line 108
  17. def OAI.MatrixMultiplication.AllFieldHistory.stageASourceSum line 113
  18. def OAI.MatrixMultiplication.AllFieldHistory.stageBSourceSum line 116
  19. def OAI.MatrixMultiplication.AllFieldHistory.stageCSourceSum line 119
  20. theorem OAI.MatrixMultiplication.AllFieldHistory.stageA_one_lot_sum line 123
  21. theorem OAI.MatrixMultiplication.AllFieldHistory.stageB_one_lot_sum line 129
  22. theorem OAI.MatrixMultiplication.AllFieldHistory.stageC_one_lot_sum line 134
  23. theorem OAI.MatrixMultiplication.AllFieldHistory.subtype_sum_indicator line 143

    Also declared: OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Sums.lean:22 (same declaration text).

  24. theorem OAI.MatrixMultiplication.AllFieldHistory.active_shape_sum line 149
  25. def OAI.MatrixMultiplication.AllFieldHistory.shapeCapacity line 177
  26. def OAI.MatrixMultiplication.AllFieldHistory.stageASourceCapacity line 181
  27. def OAI.MatrixMultiplication.AllFieldHistory.stageBSourceCapacity line 184
  28. def OAI.MatrixMultiplication.AllFieldHistory.stageCSourceCapacity line 187
  29. theorem OAI.MatrixMultiplication.AllFieldHistory.activeAggregateCapacity_shapeCapacity line 191