OAI/Combinatorics/Progressions/Dynamics/MarkedEvaluationHeightBudget.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.markedQuotient_source_height_bound line 9
  2. theorem OAI.Erdos3.markedQuotient_projection_height_bound line 44
  3. theorem OAI.Erdos3.markedQuotient_final_height_bound line 60
  4. theorem OAI.Erdos3.markedQuotientHeight_le_exp line 90
  5. def OAI.Erdos3.markedShiftInputBudget line 122
  6. def OAI.Erdos3.markedShiftHeightBudget line 125
  7. def OAI.Erdos3.markedShiftModelBudget line 128
  8. theorem OAI.Erdos3.markedShiftInputBudget_nonneg line 133
  9. theorem OAI.Erdos3.le_markedShiftInputBudget line 138
  10. theorem OAI.Erdos3.step_le_markedShiftInputBudget line 144
  11. theorem OAI.Erdos3.markedShift_dimension_budget line 149
  12. theorem OAI.Erdos3.markedShiftInputBudget_le_height line 158
  13. theorem OAI.Erdos3.markedShiftHeightBudget_nonneg line 162
  14. theorem OAI.Erdos3.markedShiftHeightBudget_le_model line 166
  15. theorem OAI.Erdos3.exists_markedShiftModel_budget line 171
  16. theorem OAI.Erdos3.markedEvaluation_extra_height_bound line 193
  17. theorem OAI.Erdos3.markedEvaluationHeight_le_exp line 230