OAI/LinearAlgebra/MatrixMultiplication/ComplexArithmetic/Growth.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Complex arithmetic programs and asymptotic matrix multiplication costs.

  1. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.exists_power_cover line 18
  2. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.geometric_cost_recurrence_bound line 24
  3. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.power_cost_padding_bound line 57
  4. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_uniform_power_costs line 84
  5. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_power_costs line 100
  6. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_recursive_costs line 112
  7. def OAI.MatrixMultiplication.Foundation.Arithmetic.blockRecurrenceCost line 142
  8. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.blockRecurrenceCost_zero line 146
  9. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.blockRecurrenceCost_succ line 149
  10. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.power_programs_of_block_step line 153
  11. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_block_step_of_padding line 172
  12. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_block_step line 203
  13. theorem OAI.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_rankAtMost line 213