OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Bounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. theorem OAI.MatrixMultiplication.AllFieldHistory.work_source_amount_pos line 15
  2. theorem OAI.MatrixMultiplication.AllFieldHistory.work_source_population_pos line 23
  3. abbrev OAI.MatrixMultiplication.AllFieldHistory.PositiveBranch line 29
  4. theorem OAI.MatrixMultiplication.AllFieldHistory.branchPopulation_pos_iff line 32
  5. theorem OAI.MatrixMultiplication.AllFieldHistory.positive_branch_minimum line 38
  6. theorem OAI.MatrixMultiplication.AllFieldHistory.positive_joint_class_minimum line 43
  7. def OAI.MatrixMultiplication.AllFieldHistory.activeLengthRate line 51
  8. def OAI.MatrixMultiplication.AllFieldHistory.activePositions line 55
  9. instance OAI.MatrixMultiplication.AllFieldHistory.(instance at line 59) line 59
  10. theorem OAI.MatrixMultiplication.AllFieldHistory.active_totalLength_cast line 62
  11. def OAI.MatrixMultiplication.AllFieldHistory.activeLengthBudget line 77
  12. theorem OAI.MatrixMultiplication.AllFieldHistory.active_totalLength_le line 80
  13. theorem OAI.MatrixMultiplication.AllFieldHistory.active_cw5_support_bound line 94