OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/InitialFamily.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldInitialFamily.grid line 21
  2. theorem OAI.MatrixMultiplication.AllFieldInitialFamily.grid_pos line 23
  3. theorem OAI.MatrixMultiplication.AllFieldInitialFamily.populationLength_eq_mul_grid line 26
  4. theorem OAI.MatrixMultiplication.AllFieldInitialFamily.initialJointCounts_dilation_ratio line 30
  5. theorem OAI.MatrixMultiplication.AllFieldInitialFamily.initialJointCounts_dilation_rate line 38
  6. theorem OAI.MatrixMultiplication.AllFieldInitialFamily.native_dilation_capacity line 46
  7. def OAI.MatrixMultiplication.AllFieldInitialFamily.hashRate line 56
  8. theorem OAI.MatrixMultiplication.AllFieldInitialFamily.selection_exponent line 60
  9. abbrev OAI.MatrixMultiplication.AllFieldInitialFamily.Sample line 70
  10. def OAI.MatrixMultiplication.AllFieldInitialFamily.Good line 75
  11. def OAI.MatrixMultiplication.AllFieldInitialFamily.executionWithWidth line 84
  12. theorem OAI.MatrixMultiplication.AllFieldInitialFamily.executionWithWidth_copies line 101
  13. def OAI.MatrixMultiplication.AllFieldInitialFamily.execution line 109
  14. theorem OAI.MatrixMultiplication.AllFieldInitialFamily.execution_copies line 119
  15. theorem OAI.MatrixMultiplication.AllFieldInitialFamily.eventually_exists_execution_with_width line 125
  16. theorem OAI.MatrixMultiplication.AllFieldInitialFamily.eventually_exists_execution line 159