OAI/LinearAlgebra/MatrixMultiplication/Recovery/InheritedMaskConcentration.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Finite orbit symmetries, masks and exact recovery operations.

  1. abbrev OAI.MatrixMultiplication.PermutationMatching.ClassPermutations line 22
  2. def OAI.MatrixMultiplication.PermutationMatching.populationSize line 24
  3. def OAI.MatrixMultiplication.PermutationMatching.totalMatchingCount line 27
  4. def OAI.MatrixMultiplication.PermutationMatching.totalMatchingMean line 31
  5. theorem OAI.MatrixMultiplication.PermutationMatching.average_totalMatchingCount line 34
  6. theorem OAI.MatrixMultiplication.PermutationMatching.totalMatchingMean_eq line 45
  7. theorem OAI.MatrixMultiplication.PermutationMatching.totalMatchingCount_variance_le line 55
  8. theorem OAI.MatrixMultiplication.PermutationMatching.totalMatchingCount_deviation_le line 70
  9. theorem OAI.MatrixMultiplication.PermutationMatching.normalizedMatchingCount_deviation_le line 82
  10. theorem OAI.MatrixMultiplication.PermutationMatching.inheritedMask_rejection_le line 112
  11. theorem OAI.MatrixMultiplication.PermutationMatching.finite_inheritedMask_rejection_le line 136
  12. theorem OAI.MatrixMultiplication.PermutationMatching.pushforward_sum_rejection_le line 149
  13. def OAI.MatrixMultiplication.PermutationMatching.totalTwoHalfCount line 191
  14. theorem OAI.MatrixMultiplication.PermutationMatching.average_totalTwoHalfCount_test line 195
  15. theorem OAI.MatrixMultiplication.PermutationMatching.average_totalTwoHalfCounts_test line 207
  16. theorem OAI.MatrixMultiplication.PermutationMatching.twoHalf_pushforward_sum_rejection_le line 224
  17. theorem OAI.MatrixMultiplication.PermutationMatching.twoHalf_inheritedMask_rejection_le line 239
  18. def OAI.MatrixMultiplication.PermutationMatching.selectedTwoHalfCount line 251
  19. theorem OAI.MatrixMultiplication.PermutationMatching.selectedTwoHalfMask_rejection_le line 256
  20. theorem OAI.MatrixMultiplication.PermutationMatching.finite_selectedTwoHalfMask_rejection_le line 279
  21. theorem OAI.MatrixMultiplication.PermutationMatching.inverse_linear_mask_constant line 296
  22. theorem OAI.MatrixMultiplication.PermutationMatching.finite_selectedTwoHalfMask_inverse_linear line 307
  23. theorem OAI.MatrixMultiplication.PermutationMatching.statisticPositions_card line 333
  24. theorem OAI.MatrixMultiplication.PermutationMatching.average_bad_shift_eq_orbit_fraction line 349