OAI/Combinatorics/Progressions/Estimates/LocalizedSiftingAlmostPeriods.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.goodDifferenceSet line 18
  2. theorem OAI.Erdos3.goodDifferenceSet_subset line 21
  3. theorem OAI.Erdos3.le_of_mem_goodDifferenceSet line 24
  4. theorem OAI.Erdos3.le_threshold_of_not_mem_goodDifferenceSet line 28
  5. theorem OAI.Erdos3.CyclicCrootSisask.sqrt_le_exp_of_le_exp_two_mul line 46
  6. theorem OAI.Erdos3.CyclicCrootSisask.old_frequency_scale_le_regularity line 51
  7. theorem OAI.Erdos3.CyclicCrootSisask.chosen_scales_error_le line 60
  8. theorem OAI.Erdos3.CyclicCrootSisask.exists_quartic_local_almostPeriods line 106
  9. theorem OAI.Erdos3.LocalConvolution.smoothed_correlation_ge_of_good_probability line 183
  10. def OAI.Erdos3.CyclicCrootSisask.almostPeriodicityWidthConstant line 211
  11. theorem OAI.Erdos3.CyclicCrootSisask.almostPeriodicityWidthConstant_pos line 214
  12. theorem OAI.Erdos3.CyclicCrootSisask.rankQuarticFactor_le_widthConstant line 220
  13. theorem OAI.Erdos3.CyclicCrootSisask.exists_difference_event_almostPeriods_with_width line 234
  14. def OAI.Erdos3.CyclicCrootSisask.quarticBogolyubovConstant line 342
  15. theorem OAI.Erdos3.CyclicCrootSisask.quarticBogolyubovConstant_pos line 345
  16. theorem OAI.Erdos3.CyclicCrootSisask.exists_quartic_bogolyubov line 348
  17. theorem OAI.Erdos3.LocalConvolution.exists_sifted_almostPeriods line 463
  18. def OAI.Erdos3.CyclicCrootSisask.quarticBogolyubovVolumeConstant line 524
  19. theorem OAI.Erdos3.CyclicCrootSisask.quarticBogolyubovVolumeConstant_pos line 527
  20. theorem OAI.Erdos3.CyclicCrootSisask.exists_quartic_bogolyubov_with_volume line 532
  21. def OAI.Erdos3.CyclicCrootSisask.quarticBogolyubovProgressionConstant line 555
  22. theorem OAI.Erdos3.CyclicCrootSisask.quarticBogolyubovProgressionConstant_pos line 558
  23. theorem OAI.Erdos3.CyclicCrootSisask.exists_quartic_bogolyubov_progression line 564
  24. theorem OAI.Erdos3.LocalConvolution.exists_smoothing_of_large_correlation_at_scale line 590
  25. theorem OAI.Erdos3.LocalConvolution.exists_smoothing_of_large_correlation line 670