OAI/LinearAlgebra/MatrixMultiplication/Recovery/InheritedMaskAction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Finite orbit symmetries, masks and exact recovery operations.

  1. def OAI.MatrixMultiplication.PermutationMatching.wordPairLeftPositions line 22
  2. def OAI.MatrixMultiplication.PermutationMatching.wordPairRightPositions line 26
  3. def OAI.MatrixMultiplication.PermutationMatching.wordPairCount line 30
  4. theorem OAI.MatrixMultiplication.PermutationMatching.wordPairCount_smul line 37
  5. theorem OAI.MatrixMultiplication.PermutationMatching.average_wordPairCount_shift line 49
  6. def OAI.MatrixMultiplication.PermutationMatching.wordPairMaskBad line 61
  7. theorem OAI.MatrixMultiplication.PermutationMatching.wordPair_orbit_fraction_eq line 66
  8. theorem OAI.MatrixMultiplication.PermutationMatching.wordPair_orbit_rejection_le line 80
  9. theorem OAI.MatrixMultiplication.PermutationMatching.wordPair_orbit_rejection_of_windows_le line 94
  10. def OAI.MatrixMultiplication.PermutationMatching.selectedWordPairCount line 113
  11. theorem OAI.MatrixMultiplication.PermutationMatching.selectedWordPairCount_smul line 120
  12. theorem OAI.MatrixMultiplication.PermutationMatching.average_selectedWordPairCount_shift line 133
  13. def OAI.MatrixMultiplication.PermutationMatching.selectedWordPairMaskBad line 147
  14. theorem OAI.MatrixMultiplication.PermutationMatching.selectedWordPair_orbit_fraction_eq line 154
  15. theorem OAI.MatrixMultiplication.PermutationMatching.selectedWordPair_orbit_rejection_le line 169
  16. theorem OAI.MatrixMultiplication.PermutationMatching.selectedWordPair_orbit_rejection_of_windows_le line 186
  17. theorem OAI.MatrixMultiplication.PermutationMatching.selectedWordPair_orbit_rejection_of_completeWindows_le line 207
  18. theorem OAI.MatrixMultiplication.PermutationMatching.finite_selectedWordPair_sum_orbit_fraction_le line 243
  19. theorem OAI.MatrixMultiplication.PermutationMatching.finite_selectedWordPair_orbit_rejection_of_windows_le line 292
  20. theorem OAI.MatrixMultiplication.PermutationMatching.finite_selectedWordPair_orbit_inverse_linear_of_windows line 327