OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/PopulationCounts.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldPopulationCounts.denominator line 15
  2. def OAI.MatrixMultiplication.AllFieldPopulationCounts.baseCount line 17
  3. def OAI.MatrixMultiplication.AllFieldPopulationCounts.count line 20
  4. def OAI.MatrixMultiplication.AllFieldPopulationCounts.blockLength line 22
  5. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.denominator_pos line 25
  6. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.denominator_factor line 28
  7. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.baseCount_cast line 32
  8. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.count_cast line 48
  9. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.count_cast_blockLength line 52
  10. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.blockLength_pos line 58
  11. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.count_zero_iff line 61
  12. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.count_pos_iff line 71
  13. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.sum_count_cast line 79
  14. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.transition_sum line 86
  15. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.unit_sum line 93
  16. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.count_eq_of_mass_eq line 100
  17. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.count_ratio line 105
  18. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.count_dilate line 113
  19. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.dilation_le_count line 116
  20. theorem OAI.MatrixMultiplication.AllFieldPopulationCounts.two_le_positive_count line 125