OAI/Combinatorics/Progressions/Dynamics/AllocatedCanonicalBudget.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckPeriodCap_le_exp line 12
  2. theorem OAI.Erdos3.VectorPolynomial.slicedSourcePrefactor_le_exp line 31
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealNormalizer_row_counts line 79
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedProductIdealNormalizer_early_budget line 112
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedProductIdealNormalizer_source_budget line 147
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedSourcePrefactor_le_exp line 188
  7. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedSlicedSourceUniformAccuracy line 201
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedSourceEarlyPrefactor_le_exp line 270
  9. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedSlicedSourceEarlyUniformAccuracy line 283
  10. def OAI.Erdos3.VectorPolynomial.allocatedCutoffAmplitudeLog line 326
  11. def OAI.Erdos3.VectorPolynomial.allocatedCutoffLipschitzLog line 330
  12. def OAI.Erdos3.VectorPolynomial.allocatedCutoffFourierLog line 334
  13. def OAI.Erdos3.VectorPolynomial.allocatedCutoffSamplingLog line 338
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffLipschitzLog_bounds line 343
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffFourierLog_bounds line 356
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffSamplingLog_bounds line 367
  17. theorem OAI.Erdos3.VectorPolynomial.normalizedCutoff_product_bound line 380
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealProfileLog_mono line 402
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteErrorFourierOutput_mono line 410
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedSeparatedGeometryLog_nonneg line 433
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedSeparatedGeometryLog_le_original line 441
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedCutoffSamplingLog_mono line 451
  23. def OAI.Erdos3.VectorPolynomial.allocatedCanonicalCoverParameter line 471
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalCoverParameter_le_common line 491
  25. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCanonicalCoverThreshold_bound line 529
  26. theorem OAI.Erdos3.VectorPolynomial.exists_regularizedCanonicalCoverThreshold_bound line 559