OAI/Combinatorics/Progressions/Dynamics/PreparedFinalToleranceBudgets.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.detectedEarlyPhysical_primitive_bounds line 10
  2. theorem OAI.Erdos3.VectorPolynomial.exists_detectedCanonicalEarlyRadiusPhysicalBudget line 35
  3. theorem OAI.Erdos3.exists_detectedCanonicalEarlyRadiusMasterBudget line 115
  4. theorem OAI.Erdos3.detectedCanonicalEarlyRadiusMaster_le line 124
  5. theorem OAI.Erdos3.exists_detectedCanonicalEarlyRadiusMaster_bound line 131
  6. theorem OAI.Erdos3.exists_fixedPathPerturbationLog_prepared_budget line 153
  7. theorem OAI.Erdos3.preparedFinalTolerance_scale line 179
  8. theorem OAI.Erdos3.preparedFinalEarlySpatialWidth line 205
  9. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFinalCommonScaleBudget line 228
  10. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFinalWitnessScaleBudget line 277
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedPreparedFinalTolerance_tail line 301
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedPreparedFinalTolerance_chosen_tail line 327