OAI/Combinatorics/Progressions/Estimates/UniformRelativePatchSource.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.eventually_exp_loglog_rpow_le line 18
  2. theorem OAI.Erdos3.QuantitativeDensityBound.eventually_logarithmic line 40
  3. theorem OAI.Erdos3.QuantitativeDensityBound.logarithmic line 53
  4. theorem OAI.Erdos3.summable_dyadic_of_eventually_logarithmic line 81
  5. theorem OAI.Erdos3.QuantitativeDensityBound.summable_dyadic line 104
  6. theorem OAI.Erdos3.hasAP_of_eventually_logarithmic_bound line 110
  7. theorem OAI.Erdos3.QuantitativeDensityBound.hasAP line 117
  8. theorem OAI.Erdos3.reciprocalProgressionTheorem_of_quantitativeDensityTheorem line 121
  9. theorem OAI.Erdos3.eventually_quarter_resource_paid line 137
  10. theorem OAI.Erdos3.source_scaled_exponential_room line 147
  11. theorem OAI.Erdos3.source_exponential_room line 159
  12. theorem OAI.Erdos3.source_half_log_room line 166
  13. theorem OAI.Erdos3.eventually_source_exponential_room line 176
  14. theorem OAI.Erdos3.subquadratic_patch_descent line 198
  15. def OAI.Erdos3.SubquadraticPatchSource line 281
  16. theorem OAI.Erdos3.quantitative_density_of_patch_source line 296
  17. theorem OAI.Erdos3.relativePatchSliceScore_interval line 358
  18. theorem OAI.Erdos3.APFreeInterval.patch_of_relative_absolute line 372
  19. theorem OAI.Erdos3.subquadratic_patch_source_of_relative_family line 413
  20. theorem OAI.Erdos3.exists_subquadratic_patch_source_of_uniform_relative_lifting line 499
  21. theorem OAI.Erdos3.quantitative_density_bound_of_uniform_relative_lifting line 533
  22. theorem OAI.Erdos3.manuscript_targets_of_uniform_relative_lifting line 545