OAI/Combinatorics/Progressions/Dynamics/IntervalSplitBudget.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.mixedErrorPairBudget_mono line 9
  2. theorem OAI.Erdos3.mixedErrorBudget_mono line 14
  3. def OAI.Erdos3.intervalErrorBaseBudget line 19
  4. def OAI.Erdos3.intervalErrorBudget line 21
  5. theorem OAI.Erdos3.intervalErrorBaseBudget_bounds line 23
  6. theorem OAI.Erdos3.exists_interval_error_budget line 34
  7. def OAI.Erdos3.intervalSplitInput line 61
  8. def OAI.Erdos3.intervalSplitTermBudget line 63
  9. def OAI.Erdos3.intervalSplitLocalBudget line 65
  10. theorem OAI.Erdos3.intervalErrorBudget_nonneg line 68
  11. theorem OAI.Erdos3.intervalSplitInput_bounds line 72