OAI/NumberTheory/Ostmann/Arithmetic/HistoryHeightBudget.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.RationalHistory.Expr.fixedLiterals line 10
  2. def OAI.Ostmann.Characters.RationalHistory.Expr.fixedCount line 15
  3. def OAI.Ostmann.Characters.RationalHistory.Expr.addSubCount line 17
  4. def OAI.Ostmann.Characters.RationalHistory.Expr.heightCost line 22
  5. def OAI.Ostmann.Characters.RationalHistory.Expr.FixedBound line 24
  6. theorem OAI.Ostmann.Characters.RationalHistory.Expr.fixedBound_atom line 26
  7. theorem OAI.Ostmann.Characters.RationalHistory.Expr.fixedBound_fixed line 28
  8. theorem OAI.Ostmann.Characters.RationalHistory.Expr.fixedBound_add line 31
  9. theorem OAI.Ostmann.Characters.RationalHistory.Expr.fixedBound_sub line 34
  10. theorem OAI.Ostmann.Characters.RationalHistory.Expr.fixedBound_mul line 37
  11. theorem OAI.Ostmann.Characters.RationalHistory.Expr.fixedBound_divide line 40
  12. theorem OAI.Ostmann.Characters.RationalHistory.Expr.heightBudget_nonneg line 44
  13. theorem OAI.Ostmann.Characters.RationalHistory.Expr.heightBudget_le_separate line 51
  14. theorem OAI.Ostmann.Characters.RationalHistory.Expr.heightBudget_le_counts line 78
  15. theorem OAI.Ostmann.Characters.RationalHistory.Expr.heightBudget_le_cost line 93
  16. theorem OAI.Ostmann.Characters.RationalHistory.Expr.fraction_eval_abs_le_counts line 105