OAI/Combinatorics/Progressions/Fourier/FiniteFourierSmoothing.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteFourierCoeff line 16
  2. theorem OAI.Erdos3.addChar_sub_star line 19
  3. theorem OAI.Erdos3.star_finiteFourierCoeff line 24
  4. theorem OAI.Erdos3.finiteFourier_inversion line 32
  5. theorem OAI.Erdos3.finiteFourier_inner line 62
  6. theorem OAI.Erdos3.finiteFourier_parseval line 77
  7. def OAI.Erdos3.fourierL1 line 95
  8. theorem OAI.Erdos3.norm_sub_translate_le_fourier_sum line 98
  9. theorem OAI.Erdos3.norm_sub_translate_le_mul_fourierL1 line 127
  10. theorem OAI.Erdos3.norm_sub_translate_le_spectrum_cutoff line 151
  11. theorem OAI.Erdos3.norm_sub_translate_le_of_uniform_approx_and_spectrum_cutoff line 188
  12. lemma OAI.Erdos3.norm_character_neg_sub_one line 232
  13. def OAI.Erdos3.finiteImageMass line 256
  14. def OAI.Erdos3.finiteImageCharacteristic line 260
  15. theorem OAI.Erdos3.finiteImageCharacteristic_norm_le_one line 264
  16. theorem OAI.Erdos3.finiteImageFourier_inversion line 270
  17. theorem OAI.Erdos3.finiteImageFourier_truncation line 294
  18. def OAI.Erdos3.Chang.spectrumSum line 327
  19. def OAI.Erdos3.Chang.largeSpectrum line 330
  20. theorem OAI.Erdos3.Chang.mem_largeSpectrum line 334
  21. def OAI.Erdos3.additiveCharacterKernel line 350
  22. theorem OAI.Erdos3.additiveCharacterKernel_ne_top line 362
  23. theorem OAI.Erdos3.primePowerCharacter_kernel_index line 373
  24. theorem OAI.Erdos3.primePowerCharacter_kernel_probability line 388
  25. def OAI.Erdos3.finiteSetAverage line 424
  26. def OAI.Erdos3.setFourierMultiplier line 427
  27. theorem OAI.Erdos3.finiteFourierCoeff_translate line 430
  28. theorem OAI.Erdos3.finiteFourierCoeff_finiteSetAverage line 445
  29. theorem OAI.Erdos3.setFourierMultiplier_eq line 458
  30. theorem OAI.Erdos3.norm_setFourierMultiplier line 463
  31. theorem OAI.Erdos3.norm_setFourierMultiplier_le_one line 467
  32. theorem OAI.Erdos3.mem_largeSpectrum_iff_le_multiplier line 473
  33. def OAI.Erdos3.iteratedFiniteSetAverage line 479
  34. theorem OAI.Erdos3.finiteFourierCoeff_iteratedFiniteSetAverage line 483
  35. def OAI.Erdos3.RelativeChangSanders.IsWeightedDissociated line 508
  36. def OAI.Erdos3.RelativeChangSanders.weightedSpectrumSum line 515
  37. def OAI.Erdos3.RelativeChangSanders.relativeLargeSpectrum line 518
  38. theorem OAI.Erdos3.RelativeChangSanders.mem_relativeLargeSpectrum line 524
  39. theorem OAI.Erdos3.Chang.spectrumSum_map_subRight line 546
  40. theorem OAI.Erdos3.Chang.norm_spectrumSum_map_subRight line 555
  41. theorem OAI.Erdos3.Chang.mem_largeSpectrum_map_subRight_iff line 559
  42. theorem OAI.Erdos3.iteratedFiniteSetAverage_translate_le line 577
  43. theorem OAI.Erdos3.translate_le_of_iteratedFiniteSetAverage_approx line 618