OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/ConstructionRates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. abbrev OAI.MatrixMultiplication.AllFieldConstructionRates.Copies line 18
  2. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.card_copies line 22
  3. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.card_copies_range line 34
  4. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.card_copies_pos line 44
  5. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.copies_subexponential line 47
  6. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.copies_rate line 58
  7. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.source_rank_rate line 71
  8. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.source_rank_terminal_rate line 89
  9. theorem OAI.MatrixMultiplication.AllFieldConstructionRates.source_rank_terminal_rate_of_cardinality line 98