OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/ZeroHistorySums.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldZeroHistorySums.zeroRate line 18
  2. theorem OAI.MatrixMultiplication.AllFieldZeroHistorySums.subtype_sum_indicator line 22
  3. theorem OAI.MatrixMultiplication.AllFieldZeroHistorySums.sum_subtype_complement line 28
  4. theorem OAI.MatrixMultiplication.AllFieldZeroHistorySums.list_filter_sum line 38
  5. theorem OAI.MatrixMultiplication.AllFieldZeroHistorySums.sum_placement_rate line 45
  6. theorem OAI.MatrixMultiplication.AllFieldZeroHistorySums.a_zero_canonical_rate line 60
  7. theorem OAI.MatrixMultiplication.AllFieldZeroHistorySums.a_zero_history_rate line 83
  8. theorem OAI.MatrixMultiplication.AllFieldZeroHistorySums.b_positive_secondLeafRate line 94
  9. theorem OAI.MatrixMultiplication.AllFieldZeroHistorySums.b_zero_canonical_rate line 107
  10. theorem OAI.MatrixMultiplication.AllFieldZeroHistorySums.b_zero_rate_eq_secondLeafRate line 116
  11. theorem OAI.MatrixMultiplication.AllFieldZeroHistorySums.b_zero_history_rate line 122
  12. theorem OAI.MatrixMultiplication.AllFieldZeroHistorySums.zero_history_sum line 137