OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/IncomingMasks.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.empiricalLaw_congr_decidable line 23
  2. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.typeWindow_mono_decidable line 29
  3. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.weight_append line 37
  4. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.strand_append line 41
  5. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.shapeTensor_append line 48
  6. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.shapeTensor_joinHalves line 57
  7. def OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.defaultStatistic line 65
  8. def OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.choiceAt line 70
  9. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.choiceAt_self line 73
  10. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.rawPairCount_eq_wordPopulation line 76
  11. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.fourStatistic_append line 84
  12. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.append_singletons line 88
  13. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.rawPass_stageB_typeWindow line 93
  14. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.incoming_stageA line 149
  15. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.incoming_stageB line 157
  16. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.incoming_stageC line 178
  17. def OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.stageCWeights line 214
  18. theorem OAI.MatrixMultiplication.AllFieldHistoryIncomingMasks.received_of_rawPass line 225