OAI/Combinatorics/Progressions/Estimates/PreparedUniformEarlyRadiusWithCutoff.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedBufferedRadiusInput line 12
  2. def OAI.Erdos3.VectorPolynomial.allocatedBufferedRadiusLog line 15
  3. def OAI.Erdos3.VectorPolynomial.allocatedCommonRadiusLog line 18
  4. def OAI.Erdos3.VectorPolynomial.allocatedCommonRadius line 22
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedRadiusInput_bounds line 25
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonRadiusLog_bounds line 39
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonRadius_bounds line 52
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonRadiusLog_mono line 60
  9. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCommonRadiusLog_bound line 69
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedRadius_inverse_from_primitive line 89
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonRadius_admissible line 123
  12. def OAI.Erdos3.VectorPolynomial.allocatedCommonProductRadiusLog line 152
  13. def OAI.Erdos3.VectorPolynomial.allocatedCommonProductRadius line 157
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonProductRadius_bounds line 160
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonProductRadiusLog_mono line 181
  16. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCommonProductRadiusLog_bound line 188
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonProductRadius_admissible line 207
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalSlice_source_geometry line 242
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedComparisonDimension_two_mul line 294
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalSourceGeometry line 313
  21. def OAI.Erdos3.VectorPolynomial.allocatedCommonProductRadiusLogWithCutoff line 342
  22. def OAI.Erdos3.VectorPolynomial.allocatedCommonProductRadiusWithCutoff line 346
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonProductRadiusWithCutoff_bounds line 349
  24. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCommonProductRadiusLogWithCutoff_bound line 361
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedProductChartLog_mono_layers line 379
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedRadius_inverse_from_primitive_with_cutoff line 392
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonProductRadiusWithCutoff_admissible line 436
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonProductRadiusLog_ge_geometry line 491
  29. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonProductRadius_le_exp_neg_geometry line 507
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonProductRadius_freezing_sum line 511
  31. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardTailCap_budget line 551
  32. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardTailCapExponent line 597
  33. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardTailCapExponent_two_le line 600
  34. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardTailCap_le_exp line 604
  35. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForward_shiftedPower_le_work line 617
  36. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardTailCap_le_exp_work line 630
  37. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalSlice_source_geometry_with_cutoff line 660
  38. theorem OAI.Erdos3.VectorPolynomial.exists_preparedUniformEarlyRadius_with_cutoff line 709