OAI/Combinatorics/Progressions/Fourier/TranslatedBohrDifference.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.massCoeff line 18
  2. theorem OAI.Erdos3.massCoeff_realUniformMass line 21
  3. theorem OAI.Erdos3.norm_massCoeff_realUniformMass_lt_half_of_not_mem_largeSpectrum line 37
  4. theorem OAI.Erdos3.massCoeff_massConvolution line 60
  5. theorem OAI.Erdos3.massCoeff_convolutionPower line 92
  6. theorem OAI.Erdos3.norm_massCoeff_le_sum line 107
  7. theorem OAI.Erdos3.convolutionPower_realUniformMass_support line 136
  8. def OAI.Erdos3.bohrSmoothingMeasure line 168
  9. theorem OAI.Erdos3.bohrSmoothingMeasure_nonneg line 173
  10. theorem OAI.Erdos3.sum_bohrSmoothingMeasure line 179
  11. theorem OAI.Erdos3.bohrSmoothingMeasure_apply_of_mem line 186
  12. theorem OAI.Erdos3.card_dilate_one_add_le_two_mul line 220
  13. theorem OAI.Erdos3.realUniformMass_le_two_mul_bohrSmoothingMeasure line 248
  14. theorem OAI.Erdos3.norm_massCoeff_bohrSmoothingMeasure_le line 276
  15. lemma OAI.Erdos3.normalizedSpectrum_eq line 310
  16. lemma OAI.Erdos3.normalizedSpectrum_translate line 329
  17. theorem OAI.Erdos3.norm_one_sub_le_of_mem_largeSpectrum line 356
  18. theorem OAI.Erdos3.norm_one_sub_le_of_mem_largeSpectrum_half line 412
  19. theorem OAI.Erdos3.LocalConvolution.exists_dense_sets_of_bohr_correlation_moment line 438
  20. theorem OAI.Erdos3.CyclicBohr.Set.card_add_le_two_mul_of_small_bohr line 502
  21. def OAI.Erdos3.CyclicBohr.Set.initialSamplingScale line 521
  22. theorem OAI.Erdos3.CyclicBohr.Set.initialSamplingScale_pos line 524
  23. theorem OAI.Erdos3.CyclicBohr.Set.initialSamplingScale_le_one line 528
  24. theorem OAI.Erdos3.CyclicBohr.Set.exists_initial_regular_sampling_bohr line 533
  25. theorem OAI.Erdos3.CyclicBohr.Set.sumset_le_exp_of_relative_density line 551
  26. theorem OAI.Erdos3.CyclicBohr.Set.card_sub_translated_small_le_two_mul line 578