OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Counts.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistory.shapeCounts line 15
  2. theorem OAI.MatrixMultiplication.AllFieldHistory.shapeCounts_sum line 19
  3. theorem OAI.MatrixMultiplication.AllFieldHistory.shapeCounts_positive line 25
  4. theorem OAI.MatrixMultiplication.AllFieldHistory.shapeCounts_at line 38
  5. theorem OAI.MatrixMultiplication.AllFieldHistory.Work.parentShape_spec line 45
  6. theorem OAI.MatrixMultiplication.AllFieldHistory.Work.splitShape_spec line 54
  7. theorem OAI.MatrixMultiplication.AllFieldHistory.Work.splitShape_le line 61
  8. theorem OAI.MatrixMultiplication.AllFieldHistory.Work.splitShape_injective line 68
  9. def OAI.MatrixMultiplication.AllFieldHistory.branchShape line 75
  10. theorem OAI.MatrixMultiplication.AllFieldHistory.branchShape_injective line 78
  11. def OAI.MatrixMultiplication.AllFieldHistory.jointCounts line 83
  12. def OAI.MatrixMultiplication.AllFieldHistory.activeCounts line 87
  13. def OAI.MatrixMultiplication.AllFieldHistory.activeParentShape line 90
  14. def OAI.MatrixMultiplication.AllFieldHistory.activeHalfLength line 93
  15. theorem OAI.MatrixMultiplication.AllFieldHistory.jointCounts_sum line 95
  16. theorem OAI.MatrixMultiplication.AllFieldHistory.jointCounts_at line 100
  17. theorem OAI.MatrixMultiplication.AllFieldHistory.jointCounts_support_sum line 106
  18. theorem OAI.MatrixMultiplication.AllFieldHistory.jointCounts_support_le line 113
  19. def OAI.MatrixMultiplication.AllFieldHistory.shapePositionMap line 121
  20. theorem OAI.MatrixMultiplication.AllFieldHistory.shapePositionMap_injective line 128
  21. theorem OAI.MatrixMultiplication.AllFieldHistory.shapePositionMap_surjective line 138
  22. def OAI.MatrixMultiplication.AllFieldHistory.branchPositionEquiv line 147
  23. theorem OAI.MatrixMultiplication.AllFieldHistory.branchPositionEquiv_shape line 155
  24. def OAI.MatrixMultiplication.AllFieldHistory.rootShape line 161
  25. def OAI.MatrixMultiplication.AllFieldHistory.initialJointCounts line 164
  26. theorem OAI.MatrixMultiplication.AllFieldHistory.initialJointCounts_sum line 169
  27. theorem OAI.MatrixMultiplication.AllFieldHistory.initialJointCounts_support line 175