OAI/Combinatorics/Progressions/Dynamics/AllocatedActualCoarseBudget.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedCommonSmoothingLog line 22
  2. def OAI.Erdos3.VectorPolynomial.allocatedCommonTailLog line 29
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonSmoothingLog_nonneg line 36
  4. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCommonRegularizationLog_bound line 49
  5. theorem OAI.Erdos3.VectorPolynomial.exists_regularizedCommonCoverThreshold_bound line 99
  6. theorem OAI.Erdos3.VectorPolynomial.exists_fixedRegularizedCommonCoverThreshold_bound line 133
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonTailLog_nonneg line 179
  8. def OAI.Erdos3.VectorPolynomial.allocatedCommonWidth line 190
  9. def OAI.Erdos3.VectorPolynomial.allocatedCommonGeometryLog line 193
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonWidth_bounds line 196
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonWidth_le line 207
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonGeometryLog_bounds line 214
  13. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCommonGeometryLog_bound line 240
  14. theorem OAI.Erdos3.VectorPolynomial.exists_geometricCommonCoverThreshold_bound line 275
  15. theorem OAI.Erdos3.VectorPolynomial.exists_fixedGeometricCommonCoverThreshold_bound line 305
  16. def OAI.Erdos3.VectorPolynomial.allocatedProductGeometryLog line 352
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedProductGeometryLog_bounds line 355
  18. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedProductGeometryLog_bound line 382
  19. theorem OAI.Erdos3.VectorPolynomial.exists_productGeometricCommonCoverThreshold_bound line 417
  20. theorem OAI.Erdos3.VectorPolynomial.exists_fixedProductGeometricCommonCoverThreshold_bound line 447
  21. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCommonCoarseBudget line 486
  22. def OAI.Erdos3.VectorPolynomial.allocatedActualCommonCoarseMesh line 504
  23. theorem OAI.Erdos3.VectorPolynomial.exists_actualCommonCoarseBudget line 513
  24. theorem OAI.Erdos3.VectorPolynomial.exists_fixedActualCommonCoarseBudget line 561