OAI/Combinatorics/Progressions/Estimates/BoundedInequalityGoodCutoff.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.sublevelCutoff_integral_loss_le line 15
  2. def OAI.Erdos3.goodDomainCutoff line 52
  3. theorem OAI.Erdos3.goodDomainCutoff_range line 56
  4. theorem OAI.Erdos3.goodDomainCutoff_smooth line 65
  5. theorem OAI.Erdos3.goodDomainCutoff_compact line 72
  6. theorem OAI.Erdos3.goodDomainCutoff_tsupport_subset line 77
  7. theorem OAI.Erdos3.goodDomainCutoff_eq_one line 89
  8. theorem OAI.Erdos3.goodDomainCutoff_fderiv_norm_le line 98
  9. theorem OAI.Erdos3.goodDomainCutoff_integral_loss_le line 132
  10. def OAI.Erdos3.sublevelCutoffProduct line 172
  11. theorem OAI.Erdos3.sublevelCutoffProduct_range line 176
  12. theorem OAI.Erdos3.sublevelCutoffProduct_smooth line 182
  13. theorem OAI.Erdos3.sublevelCutoffProduct_fderiv_norm_le line 189
  14. theorem OAI.Erdos3.sublevelCutoffProduct_integral_loss_le line 203
  15. theorem OAI.Erdos3.indicator_eventuallyEq_on_open line 226
  16. theorem OAI.Erdos3.indicator_measurable_of_continuousOn line 232
  17. theorem OAI.Erdos3.integral_indicator_weight_mul line 239
  18. theorem OAI.Erdos3.integral_indicator_weight_image line 247
  19. theorem OAI.Erdos3.weighted_selectedInverse_indicator_eq line 256
  20. theorem OAI.Erdos3.exists_good_domain_cutoff line 279
  21. theorem OAI.Erdos3.supported_density_cutoff_weight line 313
  22. theorem OAI.Erdos3.open_domain_image_comparison line 342
  23. theorem OAI.Erdos3.open_domain_image_comparison_sqrt line 406
  24. theorem OAI.Erdos3.exists_bounded_inequality_good_cutoff line 448