OAI/Combinatorics/Progressions/Estimates/LocalBoostedAlmostPeriods.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.CyclicCrootSisask.setAverageTranslate_sub line 16
  2. theorem OAI.Erdos3.CyclicCrootSisask.setAverageTranslate_rightTranslate line 22
  3. theorem OAI.Erdos3.CyclicCrootSisask.setAverageTranslate_abs_pow_le line 32
  4. theorem OAI.Erdos3.CyclicCrootSisask.setAverageTranslate_abs_pow_le_total line 50
  5. theorem OAI.Erdos3.CyclicCrootSisask.convolution_period_moment_bound line 60
  6. def OAI.Erdos3.CyclicCrootSisask.realSetIndicator line 68
  7. theorem OAI.Erdos3.CyclicCrootSisask.sum_realSetIndicator_moment line 70
  8. theorem OAI.Erdos3.CyclicCrootSisask.triple_period_moment_bound line 77
  9. theorem OAI.Erdos3.CyclicCrootSisask.half_card_le_filter_of_sum_le line 103
  10. theorem OAI.Erdos3.CyclicCrootSisask.half_samples_good_input_moment line 128
  11. theorem OAI.Erdos3.CyclicCrootSisask.goodSamples_relative_moment_bound line 145
  12. def OAI.Erdos3.CyclicCrootSisask.convolutionMomentOrder line 175
  13. theorem OAI.Erdos3.CyclicCrootSisask.convolutionMomentOrder_pos line 178
  14. theorem OAI.Erdos3.CyclicCrootSisask.cardinal_ratio_le_exp_momentOrder line 184
  15. theorem OAI.Erdos3.CyclicCrootSisask.convolution_moment_to_pointwise line 195
  16. theorem OAI.Erdos3.CyclicCrootSisask.setAverageTranslate_approx_of_shifts line 225
  17. def OAI.Erdos3.CyclicCrootSisask.iteratedSetAverage line 246
  18. theorem OAI.Erdos3.CyclicCrootSisask.iteratedSetAverage_uniform_error line 251
  19. theorem OAI.Erdos3.CyclicCrootSisask.iteratedSetAverage_approx_of_shifts line 273
  20. theorem OAI.Erdos3.CyclicCrootSisask.exists_local_almostPeriods line 294
  21. theorem OAI.Erdos3.CyclicCrootSisask.exists_local_almostPeriods_of_smallDoubling line 329
  22. theorem OAI.Erdos3.CyclicCrootSisask.exists_local_triple_almostPeriods line 366
  23. theorem OAI.Erdos3.CyclicCrootSisask.exists_local_triple_almostPeriods_of_smallDoubling line 386
  24. theorem OAI.Erdos3.CyclicCrootSisask.exists_local_boosted_triple_almostPeriods line 421