OAI/Combinatorics/Progressions/Dynamics/NativeHorizontalLiftBudget.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.absorbedInitialParameter line 9
  2. theorem OAI.Erdos3.absorbedInitialParameter_bounds line 12
  3. theorem OAI.Erdos3.absorbedInitialParameter_nonneg line 41
  4. theorem OAI.Erdos3.exists_absorbedInitialParameter_budget line 44
  5. def OAI.Erdos3.imageDefiningHeight line 74
  6. theorem OAI.Erdos3.imageDefiningHeight_le_exp line 77
  7. theorem OAI.Erdos3.imageSection_bound_le_exp line 122
  8. theorem OAI.Erdos3.imageDefiningDenominator_le_exp line 131
  9. theorem OAI.Erdos3.imageDefiningRow_bound_le_exp line 144
  10. theorem OAI.Erdos3.exists_bchLogMetricConstant_exp_bound line 156
  11. def OAI.Erdos3.separationBudget line 179
  12. theorem OAI.Erdos3.separationBudget_nonneg line 181
  13. theorem OAI.Erdos3.separationBudget_small line 185
  14. theorem OAI.Erdos3.exists_separationBudget_bound line 201
  15. def OAI.Erdos3.extractedInitialParameter line 217
  16. theorem OAI.Erdos3.extractedInitialParameter_controls line 219
  17. theorem OAI.Erdos3.extractedInitialParameter_products line 226
  18. theorem OAI.Erdos3.exists_extractedInitialParameter_budget line 245
  19. theorem OAI.Erdos3.exists_native_horizontal_lift_budget line 279