OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/TerminalRateFormulas.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldTerminalRates.initialRate line 17
  2. def OAI.MatrixMultiplication.AllFieldTerminalRates.S0 line 20
  3. def OAI.MatrixMultiplication.AllFieldTerminalRates.S1 line 24
  4. def OAI.MatrixMultiplication.AllFieldTerminalRates.secondLeafRate line 27
  5. def OAI.MatrixMultiplication.AllFieldTerminalRates.S2 line 35
  6. def OAI.MatrixMultiplication.AllFieldTerminalRates.S line 39
  7. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.four_shape_max_lt_five line 41
  8. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.four_zero_max line 44
  9. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.four_positive_max line 48
  10. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.second_shapeMax_lt_five line 52
  11. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.secondLeafRate_zero line 56
  12. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.secondLeafRate_positive line 74
  13. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.secondLeafRate_builder_expression line 80
  14. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.list_filter_sum line 95
  15. theorem OAI.MatrixMultiplication.AllFieldTerminalRates.initial_zero_history_rate line 102