OAI/LinearAlgebra/MatrixMultiplication/Tensor/Subdivision.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.Subdivision.concatenate line 22
  2. def OAI.MatrixMultiplication.Subdivision.concatenateEquiv line 25
  3. theorem OAI.MatrixMultiplication.Subdivision.wordPopulation_concatenate line 36
  4. theorem OAI.MatrixMultiplication.Subdivision.empiricalLaw_concatenate line 47
  5. def OAI.MatrixMultiplication.Subdivision.partWindows line 70
  6. theorem OAI.MatrixMultiplication.Subdivision.typeWindow_concatenate line 74
  7. theorem OAI.MatrixMultiplication.Subdivision.statisticWindow_concatenate line 102
  8. def OAI.MatrixMultiplication.Subdivision.positionsOfCounts line 115
  9. theorem OAI.MatrixMultiplication.Subdivision.typeWindow_reindex line 119
  10. theorem OAI.MatrixMultiplication.Subdivision.statisticWindow_concatenate_at line 126
  11. def OAI.MatrixMultiplication.Subdivision.repeated line 141
  12. def OAI.MatrixMultiplication.Subdivision.allParts line 144
  13. def OAI.MatrixMultiplication.Subdivision.subdivisionMatrix line 147
  14. theorem OAI.MatrixMultiplication.Subdivision.subdivisionMatrix_apply line 151
  15. theorem OAI.MatrixMultiplication.Subdivision.restrict_received line 165
  16. def OAI.MatrixMultiplication.Subdivision.subdivisionMatrixAt line 193
  17. theorem OAI.MatrixMultiplication.Subdivision.restrict_received_at line 199