OAI/Combinatorics/Progressions/Dynamics/ComparisonEquivalenceBudget.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.normalizedSquareProjectionBudget line 11
  2. def OAI.Erdos3.normalizedSquareLeftBudget line 14
  3. def OAI.Erdos3.normalizedSquareObservableBudget line 17
  4. def OAI.Erdos3.normalizedSquareReconstructionBudget line 20
  5. def OAI.Erdos3.normalizedSquareComplexityBudget line 23
  6. theorem OAI.Erdos3.normalizedSquareProjectionBudget_nonneg line 26
  7. theorem OAI.Erdos3.normalizedSquareLeftBudget_nonneg line 29
  8. theorem OAI.Erdos3.normalizedSquareObservableBudget_nonneg line 34
  9. theorem OAI.Erdos3.normalizedSquareReconstructionBudget_nonneg line 41
  10. theorem OAI.Erdos3.exists_normalizedSquareComplexityBudget_bound line 48
  11. theorem OAI.Erdos3.squareObservableLipschitz_le_exp line 61
  12. theorem OAI.Erdos3.niltest_log_bound_of_exp line 82
  13. theorem OAI.Erdos3.exists_bounded_normalization_left_lipschitz line 106
  14. def OAI.Erdos3.comparisonProductLip line 151
  15. theorem OAI.Erdos3.comparisonProductLip_le_exp line 155
  16. def OAI.Erdos3.comparisonProductCost line 176
  17. def OAI.Erdos3.comparisonDescentBudget line 178
  18. theorem OAI.Erdos3.exists_comparisonDescent_cost line 182
  19. def OAI.Erdos3.comparisonEquivalenceBudget line 200
  20. theorem OAI.Erdos3.comparisonEquivalenceBudget_bounds line 203
  21. theorem OAI.Erdos3.exists_comparisonEquivalence_cost line 216