OAI/Combinatorics/Progressions/Estimates/CyclicCutNeighborhood.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_smoothing_scale line 12
  2. def OAI.Erdos3.finiteIndicator line 44
  3. def OAI.Erdos3.averagingKernel line 46
  4. def OAI.Erdos3.smoothedIndicator line 49
  5. theorem OAI.Erdos3.finiteIndicator_norm_le_one line 53
  6. theorem OAI.Erdos3.finiteIndicator_sub_norm_le_one line 58
  7. theorem OAI.Erdos3.smoothedIndicator_norm_le_one line 64
  8. theorem OAI.Erdos3.finiteIndicator_sub_smoothed_norm_le_one line 71
  9. theorem OAI.Erdos3.smoothedIndicator_eq_convolution line 82
  10. theorem OAI.Erdos3.mean_indicator_norm_sq line 96
  11. theorem OAI.Erdos3.mean_averagingKernel_norm_sq line 103
  12. theorem OAI.Erdos3.smoothedIndicator_fourier_mass line 111
  13. theorem OAI.Erdos3.gowersNorm_mul_smoothedIndicator line 131
  14. theorem OAI.Erdos3.mean_finiteIndicator_difference line 152
  15. theorem OAI.Erdos3.mean_indicator_smoothing_error line 162
  16. theorem OAI.Erdos3.finiteFourierCoeff_singleton line 193
  17. theorem OAI.Erdos3.finiteFourierCoeff_singleton_mass line 199
  18. theorem OAI.Erdos3.gowersNorm_mul_fourier_pullback line 206
  19. theorem OAI.Erdos3.gowersNorm_mul_fiber line 225
  20. theorem OAI.Erdos3.finiteCorrelation_mul_indicator line 243
  21. theorem OAI.Erdos3.norm_finiteCorrelation_mul_indicator line 258
  22. theorem OAI.Erdos3.retained_restricted_correlation line 264
  23. def OAI.Erdos3.cyclicInterval line 297
  24. theorem OAI.Erdos3.mem_cyclicInterval_shift line 300
  25. theorem OAI.Erdos3.cyclicInterval_sdiff_next line 314
  26. theorem OAI.Erdos3.cyclicInterval_next_sdiff line 329
  27. theorem OAI.Erdos3.card_cyclicInterval_symmDiff_next line 347
  28. theorem OAI.Erdos3.cyclicInterval_unit_shift_error line 358
  29. theorem OAI.Erdos3.cyclicInterval_card line 381
  30. theorem OAI.Erdos3.cyclicInterval_nonempty line 393
  31. theorem OAI.Erdos3.cyclicInterval_nat_shift_error line 398
  32. theorem OAI.Erdos3.exists_cyclic_interval_smoothing line 438
  33. theorem OAI.Erdos3.gowersNorm_cyclicInterval_cutoff line 467
  34. theorem OAI.Erdos3.mem_cyclicInterval_representatives line 495
  35. theorem OAI.Erdos3.gowersNorm_lower_bound_of_cyclicInterval line 522
  36. theorem OAI.Erdos3.gowersNorm_transfer_cyclicInterval line 536
  37. theorem OAI.Erdos3.expect_pi_coordinate line 559
  38. theorem OAI.Erdos3.product_indicator_difference line 569
  39. def OAI.Erdos3.cyclicProductBox line 595
  40. theorem OAI.Erdos3.cyclicProductBox_nat_shift_error line 598
  41. theorem OAI.Erdos3.exists_cyclic_product_smoothing line 618
  42. def OAI.Erdos3.quarterLower line 678
  43. def OAI.Erdos3.quarterUpper line 680
  44. def OAI.Erdos3.cyclicQuarter line 682
  45. theorem OAI.Erdos3.quarter_bounds line 685
  46. theorem OAI.Erdos3.quarter_short line 689
  47. theorem OAI.Erdos3.quarter_diameter_lt_third line 693
  48. theorem OAI.Erdos3.mem_cyclicQuarter line 697
  49. theorem OAI.Erdos3.sum_cyclicQuarter_indicator line 701
  50. def OAI.Erdos3.cyclicTranslationOffset line 716
  51. theorem OAI.Erdos3.cyclic_representative_add line 719
  52. theorem OAI.Erdos3.gowersNorm_cyclicProductBox_cutoff line 744
  53. theorem OAI.Erdos3.gowersNorm_transfer_cyclicProductBox line 773
  54. theorem OAI.Erdos3.gowersNorm_cyclicProductBox_fiber_cutoff line 793
  55. theorem OAI.Erdos3.exists_correlating_cyclicQuarter line 821
  56. def OAI.Erdos3.cyclicCutNeighborhood line 848
  57. theorem OAI.Erdos3.mem_cyclicCutNeighborhood line 852
  58. theorem OAI.Erdos3.cyclicCutNeighborhood_card_le line 857