OAI/Algebra/FormulaHitting/GeneratorCost.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NCHitting.generatorExpressionBudget line 10
  2. def OAI.NCHitting.entryCostBound line 13
  3. def OAI.NCHitting.entryOutputBound line 16
  4. theorem OAI.NCHitting.bounded_dimensionExpr line 18
  5. theorem OAI.NCHitting.dimensionExpr_cost_le line 57
  6. theorem OAI.NCHitting.bounded_entryExpressions line 68
  7. theorem OAI.NCHitting.entryProgram_bounds line 136
  8. def OAI.NCHitting.rowCostBound line 195
  9. def OAI.NCHitting.rowOutputBound line 199
  10. def OAI.NCHitting.variableCostBound line 201
  11. def OAI.NCHitting.variableOutputBound line 205
  12. theorem OAI.NCHitting.rowProgram_bounds line 207
  13. theorem OAI.NCHitting.variableProgram_bounds line 236
  14. def OAI.NCHitting.generatorCostBound line 266
  15. theorem OAI.NCHitting.generate_cost_le line 273