OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/RawMasks.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistoryRawMasks.rawPairCount line 18
  2. def OAI.MatrixMultiplication.AllFieldHistoryRawMasks.rawPass line 24
  3. theorem OAI.MatrixMultiplication.AllFieldHistoryRawMasks.sum_positiveClasses line 31
  4. theorem OAI.MatrixMultiplication.AllFieldHistoryRawMasks.selectedWordPairCount_pairEquiv line 65
  5. theorem OAI.MatrixMultiplication.AllFieldHistoryRawMasks.testedClasses_populationSize line 87
  6. theorem OAI.MatrixMultiplication.AllFieldHistoryRawMasks.raw_population_pos line 95
  7. theorem OAI.MatrixMultiplication.AllFieldHistoryRawMasks.passes_pairEquiv_iff_rawPass line 100
  8. theorem OAI.MatrixMultiplication.AllFieldHistoryRawMasks.passes_pairEquiv_target_independent line 111