OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/MaskCore.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. abbrev OAI.MatrixMultiplication.AllFieldHistoryMasks.Classes line 22
  2. abbrev OAI.MatrixMultiplication.AllFieldHistoryMasks.Positions line 24
  3. abbrev OAI.MatrixMultiplication.AllFieldHistoryMasks.Letters line 27
  4. abbrev OAI.MatrixMultiplication.AllFieldHistoryMasks.Words line 29
  5. instance OAI.MatrixMultiplication.AllFieldHistoryMasks.permutationsFintype line 32
  6. abbrev OAI.MatrixMultiplication.AllFieldHistoryMasks.SymbolChoice line 46
  7. abbrev OAI.MatrixMultiplication.AllFieldHistoryMasks.MaskIndex line 48
  8. def OAI.MatrixMultiplication.AllFieldHistoryMasks.testedClasses line 50
  9. def OAI.MatrixMultiplication.AllFieldHistoryMasks.pairWidth line 53
  10. def OAI.MatrixMultiplication.AllFieldHistoryMasks.childWidth line 55
  11. theorem OAI.MatrixMultiplication.AllFieldHistoryMasks.pairWidth_pos line 57
  12. theorem OAI.MatrixMultiplication.AllFieldHistoryMasks.childWidth_pos line 62
  13. def OAI.MatrixMultiplication.AllFieldHistoryMasks.classStatistic line 65
  14. def OAI.MatrixMultiplication.AllFieldHistoryMasks.leftSymbol line 67
  15. def OAI.MatrixMultiplication.AllFieldHistoryMasks.rightSymbol line 69
  16. def OAI.MatrixMultiplication.AllFieldHistoryMasks.leftProbability line 71
  17. def OAI.MatrixMultiplication.AllFieldHistoryMasks.rightProbability line 74
  18. def OAI.MatrixMultiplication.AllFieldHistoryMasks.center line 77
  19. def OAI.MatrixMultiplication.AllFieldHistoryMasks.passes line 81
  20. def OAI.MatrixMultiplication.AllFieldHistoryMasks.childWindows line 87
  21. def OAI.MatrixMultiplication.AllFieldHistoryMasks.lossConstant line 95
  22. theorem OAI.MatrixMultiplication.AllFieldHistoryMasks.lossConstant_nonneg line 100