OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/RateLimit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. structure OAI.MatrixMultiplication.AllFieldRateLimit.HasRates line 18
  2. structure OAI.MatrixMultiplication.AllFieldRateLimit.HasRateBounds line 25
  3. theorem OAI.MatrixMultiplication.AllFieldRateLimit.HasRates.toBounds line 35
  4. theorem OAI.MatrixMultiplication.AllFieldRateLimit.inequality_of_rates line 45
  5. theorem OAI.MatrixMultiplication.AllFieldRateLimit.inequality_of_rateBounds line 54
  6. theorem OAI.MatrixMultiplication.AllFieldRateLimit.omega_le_of_rates line 71
  7. theorem OAI.MatrixMultiplication.AllFieldRateLimit.omega_le_of_rateBounds line 78
  8. structure OAI.MatrixMultiplication.AllFieldRateLimit.FixedLotFamily line 85
  9. theorem OAI.MatrixMultiplication.AllFieldRateLimit.inequality_of_fixedLotFamily line 94
  10. theorem OAI.MatrixMultiplication.AllFieldRateLimit.inequality_of_outer_families line 104
  11. theorem OAI.MatrixMultiplication.AllFieldRateLimit.omega_le_of_outer_families line 119
  12. theorem OAI.MatrixMultiplication.AllFieldRateLimit.staggered_rank_constraint line 133
  13. theorem OAI.MatrixMultiplication.AllFieldRateLimit.omega_le_of_staggered_families line 149
  14. theorem OAI.MatrixMultiplication.AllFieldRateLimit.omega_lt_of_staggered_families line 161