OAI/LinearAlgebra/MatrixMultiplication/Recovery/InheritedMaskMargins.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Finite orbit symmetries, masks and exact recovery operations.

  1. def OAI.MatrixMultiplication.PermutationMatching.classWeight line 22
  2. def OAI.MatrixMultiplication.PermutationMatching.classDensity line 25
  3. def OAI.MatrixMultiplication.PermutationMatching.classProductMixture line 28
  4. theorem OAI.MatrixMultiplication.PermutationMatching.classWeight_nonneg line 33
  5. theorem OAI.MatrixMultiplication.PermutationMatching.sum_classWeight line 37
  6. theorem OAI.MatrixMultiplication.PermutationMatching.classDensity_nonneg line 44
  7. theorem OAI.MatrixMultiplication.PermutationMatching.classDensity_le_one line 48
  8. theorem OAI.MatrixMultiplication.PermutationMatching.totalMatchingMean_normalized_eq line 56
  9. theorem OAI.MatrixMultiplication.PermutationMatching.totalMatchingMean_prescribed_error line 71
  10. theorem OAI.MatrixMultiplication.PermutationMatching.totalMatchingMean_inherited_margin line 90
  11. theorem OAI.MatrixMultiplication.PermutationMatching.inheritedMask_rejection_of_windows_le line 108
  12. theorem OAI.MatrixMultiplication.PermutationMatching.twoHalf_inheritedMask_rejection_of_windows_le line 124
  13. theorem OAI.MatrixMultiplication.PermutationMatching.selectedTwoHalfMask_rejection_of_windows_le line 140
  14. theorem OAI.MatrixMultiplication.PermutationMatching.classDensity_statisticPositions line 173
  15. theorem OAI.MatrixMultiplication.PermutationMatching.totalMatchingMean_statistic_eq line 180
  16. theorem OAI.MatrixMultiplication.PermutationMatching.twoHalf_statistic_rejection_of_typeWindows_le line 192
  17. theorem OAI.MatrixMultiplication.PermutationMatching.selectedTwoHalf_statistic_rejection_of_completeWindows_le line 223