OAI/Combinatorics/Progressions/Fourier/UniformSpectrumAbsoluteCap.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.mem_rationalGridMajorBox line 12
  2. theorem OAI.Erdos3.grid_large_spectrum_card line 22
  3. theorem OAI.Erdos3.polynomial_weightedModerateBlock_major_arc line 49
  4. def OAI.Erdos3.gridJetFrequency line 116
  5. theorem OAI.Erdos3.gridJetFrequency_apply line 120
  6. def OAI.Erdos3.weightedCubeGridCoefficient line 125
  7. theorem OAI.Erdos3.weightedCubeGridCoefficient_mem_major line 132
  8. theorem OAI.Erdos3.weightedCubeGridCoefficient_large_card line 148
  9. def OAI.Erdos3.weightedAffineModerateGridCoefficient line 179
  10. theorem OAI.Erdos3.weightedAffineModerateGridCoefficient_mem_major line 188
  11. theorem OAI.Erdos3.weightedCubeGrid_sum_coefficient line 223
  12. theorem OAI.Erdos3.weightedCubeGridProduct_truncation_le line 238
  13. def OAI.Erdos3.weightedModerateGridCoefficient line 289
  14. theorem OAI.Erdos3.weightedModerateGridCoefficient_mem_major line 297
  15. theorem OAI.Erdos3.weightedModerateGridCoefficient_large_card line 317
  16. theorem OAI.Erdos3.weightedPositiveAffineModerateGridCoefficient_mem_polynomial line 351
  17. theorem OAI.Erdos3.weightedPositiveAffineModerateGridCoefficient_minor_polynomial line 441
  18. theorem OAI.Erdos3.weightedCubeGridCoefficient_norm_le_one line 473
  19. theorem OAI.Erdos3.weightedModerateGridCoefficient_norm_le_one line 480
  20. theorem OAI.Erdos3.sum_eq_retained_add_spectrumTail line 490
  21. theorem OAI.Erdos3.product_spectrum_absolute_cap line 499
  22. def OAI.Erdos3.uniformSpectrumAbsoluteCap line 521
  23. theorem OAI.Erdos3.uniformBlockSpectrum_absolute_cap line 524
  24. theorem OAI.Erdos3.finite_product_retained_mass_le line 543