OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Tensors.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistory.ResidentStatistic line 16
  2. instance OAI.MatrixMultiplication.AllFieldHistory.(instance at line 22) line 22
  3. instance OAI.MatrixMultiplication.AllFieldHistory.(instance at line 25) line 25
  4. def OAI.MatrixMultiplication.AllFieldHistory.residentStatistic line 27
  5. def OAI.MatrixMultiplication.AllFieldHistory.residentLawRat line 35
  6. def OAI.MatrixMultiplication.AllFieldHistory.residentLaw line 44
  7. theorem OAI.MatrixMultiplication.AllFieldHistory.residentLawRat_nonnegative line 48
  8. theorem OAI.MatrixMultiplication.AllFieldHistory.residentLawRat_normalized line 57
  9. def OAI.MatrixMultiplication.AllFieldHistory.residentWidth line 66
  10. abbrev OAI.MatrixMultiplication.AllFieldHistory.HistoryWord line 73
  11. def OAI.MatrixMultiplication.AllFieldHistory.residentMask line 76
  12. theorem OAI.MatrixMultiplication.AllFieldHistory.residentMask_zero_population line 86
  13. theorem OAI.MatrixMultiplication.AllFieldHistory.residentWidth_mono line 93
  14. theorem OAI.MatrixMultiplication.AllFieldHistory.residentMask_mono line 98
  15. def OAI.MatrixMultiplication.AllFieldHistory.historyTensor line 110
  16. def OAI.MatrixMultiplication.AllFieldHistory.stateTensor line 120
  17. theorem OAI.MatrixMultiplication.AllFieldHistory.historyTensor_support_shape line 128
  18. theorem OAI.MatrixMultiplication.AllFieldHistory.historyTensor_initial line 144
  19. theorem OAI.MatrixMultiplication.AllFieldHistory.historyTensor_afterC line 152